Scheduling Theory

Motivation

When several processors share a workload, the first question is how long the workload takes if it is spread out as well as possible. If a job may be interrupted and resumed later, possibly on another processor — preemption, the setting of operating systems, of communication links and of any resource that can be time-shared — the answer is a closed formula, and it is one of the oldest results in scheduling: McNaughton's wrap-around rule of 1959 (Scheduling with deadlines and loss functions, Management Science 6, doi:10.1287/mnsc.6.1.1) shows that on identical machines the optimal makespan is the larger of the longest job and the average load. Horvath, Lam and Sethi (A level algorithm for preemptive scheduling, Journal of the ACM 24, 1977, doi:10.1145/321992.321995) extended this to machines of different speeds, and Gonzalez and Sahni (Preemptive scheduling of uniform processor systems, Journal of the ACM 25, 1978, doi:10.1145/322047.322055) gave the fast algorithm with few preemptions. Brucker's Chapter 5 (doi:10.1007/978-3-540-69516-5) presents the level-algorithm version, and this mission formalizes the statements it proves about schedules.

Setting

There are $n$ jobs with processing requirements $p_1,\dots,p_n>0$ and $m$ uniform machines with speeds $s_1,\dots,s_m>0$: running job $i$ on machine $j$ for a period of length $\ell$ performs $s_j\ell$ units of its requirement, so the whole job would take $p_i/s_j$ time units there. Identical machines are the case $s_1=\dots=s_m=1$.

A preemptive schedule is a finite list of pieces, each a job, a machine, a start time and a stop time. It is feasible for the data $(s,p)$ when every piece lies in $[0,\infty)$, no two pieces on the same machine overlap, no two pieces of the same job overlap (a job is on at most one machine at any instant), and every job $i$ receives total work exactly $p_i$ over its pieces. Its makespan $C_{\max}$ is the largest stop time; the completion time $C_i$ of job $i$ is the largest stop time of one of its pieces. A schedule is nonpreemptive when every job consists of a single piece.

Following Section 5.1.2 the data are sorted, $p_1\ge\dots\ge p_n$ and $s_1\ge\dots\ge s_m$, with $n\ge m$, and one writes $P_j=\sum_{i\le j}p_i$, $S_j=\sum_{i\le j}s_i$. For a set $A$ of jobs, $h(A)=S_{|A|}$ if $|A|\le m$ and $h(A)=S_m$ otherwise: the largest combined speed that $|A|$ jobs can use at one instant.

Formalization targets

Goal — Theorem 5.8 (printed p. 127)

The optimal makespan of $Q\mid pmtn\mid C_{\max}$ is the bound (5.5):

$$w \;=\; \max\Bigl\{\max_{j=1}^{m-1}\frac{P_j}{S_j},\ \frac{P_n}{S_m}\Bigr\} ,$$

in the sense that some feasible preemptive schedule has makespan exactly $w$ and no feasible preemptive schedule has a smaller makespan.

The lower bound (5.5) (printed p. 125)

Every feasible preemptive schedule has makespan at least $w$.

$P\mid pmtn\mid C_{\max}$ (printed p. 108)

On identical machines, $LB=\max\{\max_i p_i,\ \tfrac1m\sum_i p_i\}$ is a lower bound on the makespan and is attained by some feasible preemptive schedule.

Condition (5.8) (printed p. 129)

The jobs can be scheduled preemptively within $[0,T]$ if and only if $\sum_{i\in A}p_i\le T\,h(A)$ for every set $A$ of jobs.

Theorem 5.7 (printed p. 121)

For $P\mid pmtn\mid\sum w_iC_i$ with nonnegative weights there is an optimal schedule without preemption.

Significance

Theorem 5.8 turns an optimization over an infinite family of schedules into a formula in the data, and the formula is tight in both directions: each of its terms is a resource bound that some schedule meets exactly. That is what makes preemptive makespan minimization one of the few parallel-machine problems that is solvable at all — its nonpreemptive counterpart $P2\parallel C_{\max}$ is NP-hard (p. 124) — and it is why the preemptive relaxation appears as a bound inside branch-and-bound methods for the nonpreemptive problems.

Condition (5.8) is the form in which the result is reused. It is a Hall-type condition, one inequality per set of jobs, and it is exactly what Section 5.1.2 needs to prove Theorem 5.9, which decides $Q\mid pmtn; r_i\mid L_{\max}$ by a maximum flow in an expanded network. Theorem 5.7 is the complementary statement for the other classical objective: for total weighted completion time preemption buys nothing, so the nonpreemptive solutions of Section 5.1.1 are optimal in the larger class too.

On status: every statement here is classical and proved, and the formalization adds a checked model of preemptive schedules. Mathlib has no scheduling material, and the platform's SchedulingAlgorithms series so far models only single-machine sequences (missions I, II, IV) and two-machine permutation flow shops (mission III), none of which allow a job to be split. The piece-list model of this mission is the first reusable object for preemptive and parallel-machine problems, and the later sections of Chapter 5 — $Q\mid pmtn; r_i\mid L_{\max}$, $P\mid pmtn\mid L_{\max}$ — are stated in it.

Difficulty

The obvious first idea for the goal is to run McNaughton's rule with the speeds ignored. It fails on uniform machines: filling machines one after another does not respect the constraint that a long job on a slow machine is not done when a short job on a fast one is. The correct idea is the level algorithm — always process the jobs of highest remaining requirement on the fastest free machines, sharing machines among tied jobs — and the difficulty is in the analysis rather than the idea. The proof of Theorem 5.8 has to show that the schedule it produces ends exactly at one of the terms of $w$: either no machine idles before the end, giving $P_n/S_m$, or the machines finish in speed order with the first $j$ jobs busy from time $0$, giving $P_j/S_j$. Making that case analysis rigorous requires tracking that the order of remaining requirements is preserved over time (the invariant (5.6)) and that ties are broken consistently.

A second, formal difficulty is that the level algorithm's output is defined by continuous-time events (the next completion, the next time two levels coincide), so producing an explicit finite list of pieces with the required properties is itself a construction. Any proof must build a concrete schedule; "the infimum of makespans equals $w$" is not the goal.

For the lower bound the trap is the opposite: it is tempting to argue only with total capacity $S_mT$, which gives $P_n/S_m$ but not $P_j/S_j$. The latter needs the rule that a job is on at most one machine at a time, so that $j$ jobs run at combined speed at most $S_j$; a model that let a job be split across machines simultaneously would make the theorem false, and the definition of feasibility rules it out explicitly.

Formalization scope

A schedule is a List of Pieces over jobs Fin n and machines Fin m, with real start and stop times. Feasibility is the three-part condition of the Setting, disjointness of two pieces meaning one stops no later than the other starts. Work is measured with the machine's speed, so the same definitions cover identical machines as the constant speed $1$. Pieces of length zero and unsorted lists are allowed; both are harmless.

The sorted orders are hypotheses Antitone p and Antitone s, the speeds and requirements are positive, $m\ge 1$ and, where the book assumes it, $n\ge m$. The book's normalization $s_1=1$ is not assumed: every statement here is invariant under scaling all speeds, and the book uses the normalization only for a running-time estimate. The bound $w$ is defined as the maximum of an explicit nonempty finite set, so no supremum of an empty or unbounded set occurs; $LB$ takes a proof that $n\ge 1$ so that $\max_i p_i$ is meaningful.

Two things are deliberately not stated. The level algorithm itself is not transcribed: Theorem 5.8 is stated as the existence of an optimal schedule of makespan $w$, which is what its proof establishes. And Theorem 5.9, the flow characterization for $Q\mid pmtn; r_i\mid L_{\max}$, is left for a later mission, since it needs release times and the expanded network on top of this model.

A trivializing reading is excluded by the existential form of the goal and of Theorem 5.7: each asserts that an optimal schedule exists, not merely that any optimal schedule has a property. A proof of the goal has to construct a schedule; a proof of Theorem 5.7 has to construct a nonpreemptive one that beats every preemptive competitor. Contributions welcome beyond the milestones: a general lemma that a feasible schedule can be normalized to sorted, positive-length pieces, and a proof that (5.8) for the sets $\{1,\dots,j\}$ is equivalent to $w\le T$.

Selected references

• Peter Brucker, Scheduling Algorithms, 5th ed., Springer, 2007, Chapter 5. doi:10.1007/978-3-540-69516-5
• Robert McNaughton, Scheduling with deadlines and loss functions, Management Science 6 (1959). doi:10.1287/mnsc.6.1.1
• E. C. Horvath, S. Lam and R. Sethi, A level algorithm for preemptive scheduling, Journal of the ACM 24 (1977). doi:10.1145/321992.321995
• Teofilo Gonzalez and Sartaj Sahni, Preemptive scheduling of uniform processor systems, Journal of the ACM 25 (1978). doi:10.1145/322047.322055

Motivation

Exact methods for the resource-constrained project scheduling problem — branch-and-bound over activity lists or over start-time assignments, and the lower-bound computations inside them — live or die by how much of the search space can be discarded before it is enumerated. The standard tool is constraint propagation: deducing, from the precedence, resource and time-window data, new precedence relations $i\to j$ that every feasible schedule must satisfy, and tighter time windows for the activities. Brucker and Knust's Section 3.6 (doi:10.1007/978-3-642-23929-8) presents the family of interval consistency tests — input, output, input-or-output and their negations — that constraint-programming schedulers apply at every node of the search, following Carlier and Pinson (An algorithm for solving the job-shop problem, Management Science 35, 1989, doi:10.1287/mnsc.35.2.164) and Baptiste, Le Pape and Nuijten (Constraint-Based Scheduling, Kluwer, 2001, doi:10.1007/978-1-4615-1479-4). Every test is an instance of one theorem, Theorem 3.7, and its cumulative-resource analogue, Theorem 3.8. Those two theorems, and the tests as their corollaries, are this mission.

Setting

The instance is the RCPSP of mission I: activities $0,\dots,n-1$ with integer processing times $p_i$, renewable resources $k$ with capacities $R_k$ and demands $r_{ik}$, and precedence arcs; a schedule is an integer start-time vector $S$, feasible when it meets the precedences and never exceeds a capacity. Section 3.6 adds three things.

Relations. A conjunction $i\to j$ holds in $S$ when $S_i+p_i\le S_j$. Two activities are parallel, $i\parallel j$, when they overlap for at least one time unit, and a disjunction $i-j$ is the negation of that: $i\to j$ or $j\to i$. The instance carries a set $C$ of conjunctions and a set $D$ of disjunctions that every feasible schedule must satisfy; initially $C_0$ is the precedence relation and $D_0$ the pairs whose combined demand exceeds some capacity, and propagation adds to them.

Disjunctive sets. A set $I$ of at least two activities is disjunctive when any two of its members are related by a disjunction or a conjunction, so no two are ever processed together: the activities of a unit-capacity resource, the jobs of a single machine, the operations of one job in a shop. Its total processing time is $P(I)=\sum_{i\in I}p_i$.

Time windows. Each activity has a head $r_i$ and a deadline $d_i$, and a feasible schedule has $r_i\le S_i$ and $S_i+p_i\le d_i$. An activity starts first in a set $J$ when no activity of $J$ starts earlier, and ends last when none completes later.

For a cumulative resource $k$ the work of activity $i$ is $w_i=r_{ik}p_i$ and $W(J)=\sum_{i\in J}w_i$.

Formalization targets

Goal — Theorem 3.7 (printed p. 169)

Let $I$ be a disjunctive set, $J\subseteq I$, and $J',J''$ proper subsets of $J$ with $J'\cup J''\ne\emptyset$. If

$$\max_{\substack{\nu\in J\setminus J',\ \mu\in J\setminus J''\\ \nu\ne\mu}}\bigl(d_\mu-r_\nu\bigr)<P(J),$$

then in every feasible schedule an activity from $J'$ starts first in $J$ or an activity from $J''$ ends last in $J$.

The first infeasibility test (printed p. 169)

If some nonempty $J\subseteq I$ has $\max_{\mu\in J}d_\mu-\min_{\nu\in J}r_\nu<P(J)$, no feasible schedule exists.

The input test (3.123) and the output test (3.124) (printed p. 171)

For $\Omega\subseteq I$ nonempty and $i\in I\setminus\Omega$: if $\max_{\mu\in\Omega\cup\{i\}}d_\mu-\min_{\nu\in\Omega}r_\nu<P(\Omega)+p_i$ then $i\to j$ for all $j\in\Omega$; symmetrically, if $\max_{\mu\in\Omega}d_\mu-\min_{\nu\in\Omega\cup\{i\}}r_\nu<P(\Omega)+p_i$ then $j\to i$ for all $j\in\Omega$.

The input-or-output test (printed p. 170)

For $i,j\in J\subseteq I$, $|J|\ge 2$: if $\max_{\mu\in J\setminus\{j\}}d_\mu-\min_{\nu\in J\setminus\{i\}}r_\nu<P(J)$ then $i$ starts first in $J$ or $j$ ends last in $J$, and $i\to j$ when $i\ne j$.

Theorem 3.8 (printed p. 186)

For a cumulative resource $k$, $J\subseteq I_k$ and proper subsets $J',J''$ of $J$: if $R_k\bigl(\max_{\mu\in J\setminus J''}d_\mu-\min_{\nu\in J\setminus J'}r_\nu\bigr)<W(J)$ then an activity from $J'$ starts first in $J$ or an activity from $J''$ ends last in $J$.

Significance

Theorem 3.7 is the single statement behind a whole toolbox. Every interval consistency test in the literature — the input and output tests that fix a new conjunction, the input-or-output test, the negation tests that only shrink a window — is the theorem with a particular choice of $J'$ and $J''$, and the book's Section 3.6.4 derives them one by one. A propagation engine that applies these tests to a fixpoint is what makes branch-and-bound for the job shop and the RCPSP practical; Carlier and Pinson's solution of the 10×10 job-shop instance is the historical demonstration. Theorem 3.8 extends the same reasoning from disjunctive to cumulative resources by replacing "no overlap" with "at most $R_k$ units per time unit", the energetic-reasoning viewpoint that the rest of Section 3.6.5 develops.

The results are elementary and proved; formalizing them fixes, once, what "feasible" means in the presence of the relation sets $C$ and $D$ and time windows, on top of the RCPSP model of mission I. That layer is reusable: the start-start distance matrix of Section 3.6.2 and the symmetric-triple rules of Section 3.6.3 are statements about the same schedules and the same relations. Nothing here is on the platform or in Mathlib.

Difficulty

The obvious argument for Theorem 3.7 is the correct one, and its difficulty is in the bookkeeping. If no activity of $J'$ starts first and none of $J''$ ends last, the first starter is some $\nu\in J\setminus J'$ and the last finisher some $\mu\in J\setminus J''$, and every activity of $J$ is processed inside $[S_\nu,\,S_\mu+p_\mu]\subseteq[r_\nu,d_\mu]$. Since the activities of a disjunctive set are pairwise non-overlapping, their total length $P(J)$ fits in that interval, contradicting (3.121). The formal work is the packing lemma: pairwise disjoint integer intervals inside an interval of length $L$ have total length at most $L$, which requires ordering the activities by start time and an induction that Mathlib does not supply.

The subtle point is the restriction $\nu\ne\mu$ in (3.121). The book allows it because "an activity which starts first cannot complete also last" when there are at least two activities with positive durations. The formal statement reads "starts first" and "ends last" with $\le$, which makes the theorem true without a positivity hypothesis: when the restriction empties the index set, $J\setminus J'=J\setminus J''=\{x\}$, the conclusion holds because $x$ cannot be both the unique first starter and the unique last finisher of a disjunctive set with two or more members. A solver should expect to handle that corner separately.

For the tests the extra step is turning "starts first" into a conjunction $i\to j$, which uses the disjunction between $i$ and $j$ together with positive processing times: with $p_j=0$ an activity could start at the same instant as $i$ without violating the disjunction, so the tests carry the positivity hypothesis that Theorem 3.7 itself does not need. Theorem 3.8 replaces the packing lemma by a work-counting lemma: over an interval of length $L$ a resource of capacity $R_k$ supplies at most $R_kL$ units, and every activity of $J$ consumes $r_{ik}p_i$ of them.

Formalization scope

Schedules are integer start-time vectors on Fin n, as in missions I and II, and a feasible schedule of this mission is one that is FeasibleSchedule for the RCPSP instance (mission I), respects the arcs of $C$ (RespectsArcs, mission II), satisfies the disjunctions of $D$ and lies within the time windows; these four hypotheses are the book's "feasible schedule" in Section 3.6 and are carried on every statement, although the arguments use only the last two, or, for Theorem 3.8, the resource constraint and the windows. The sets $C$ and $D$ are parameters, not derived from the instance, since propagation enlarges them.

Every inequality "$\max(\cdot)-\min(\cdot)<P$" is stated as the family of inequalities $d_\mu<r_\nu+P$ over the same index pairs. This is equivalent, avoids natural-number subtraction, and gives an empty index set the value the convention $\max\emptyset=-\infty$ would: the hypothesis is then vacuous. "Starts first" and "ends last" use $\le$. Proper-subset hypotheses $J'\subset J$, $J''\subset J$ are the book's; the first infeasibility test needs $J$ nonempty, and the input-or-output test needs $|J|\ge 2$.

A trivializing reading is ruled out on the disjunctive side by the nonemptiness hypotheses (an empty $J$ would make the infeasibility test's family vacuous and its conclusion false) and on the cumulative side by the observation that Theorem 3.8 with $J'=J''=\emptyset$ asserts infeasibility, which is the book's intended reading. Welcome contributions beyond the milestones: the input-negation and output-negation tests, the window-tightening rules of Section 3.6.4, and the SSD-matrix results of Section 3.6.2.

Selected references

• Peter Brucker and Sigrid Knust, Complex Scheduling, 2nd ed., Springer, 2012, Section 3.6. doi:10.1007/978-3-642-23929-8
• Jacques Carlier and Eric Pinson, An algorithm for solving the job-shop problem, Management Science 35 (1989). doi:10.1287/mnsc.35.2.164
• Philippe Baptiste, Claude Le Pape and Wim Nuijten, Constraint-Based Scheduling, Kluwer, 2001. doi:10.1007/978-1-4615-1479-4
• Ulrich Dorndorf, Erwin Pesch and Toàn Phan-Huy, Constraint propagation techniques for the disjunctive scheduling problem, Artificial Intelligence 122 (2000). doi:10.1016/S0004-3702(00)00040-0

Motivation

Minimizing the average completion time of jobs that arrive over time is one of the basic objectives of machine scheduling: it measures how long, on average, a job waits in the system. On a single machine with release dates and no preemption (written $1|r_j|\sum C_j$), the problem is strongly NP-hard, so research has focused on approximation algorithms whose guarantees are stated against every feasible schedule.

The standard route runs through the preemptive relaxation. When jobs may be interrupted and resumed, the shortest-remaining-processing-time rule (SRPT) produces an optimal schedule, and its value is a lower bound for every nonpreemptive schedule. The question is how to turn that preemptive schedule into a nonpreemptive one without losing too much.

Timeline:

• 1995, Phillips, Stein and Wein (WADS 1995, pp. 86–97): order the jobs by their SRPT completion times and schedule them nonpreemptively in that order. This gives a 2-approximation. Later 2-approximations are by Hoogeveen and Vestjens (IPCO 1996), Stougie (1995), and Goemans (SODA 1997). Hoogeveen and Vestjens also showed that deterministic on-line algorithms cannot beat 2.
• 2001, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1)): order by $\alpha$-points instead of completion times, choose $\alpha$ at random, and take the best $\alpha$ off-line. This gives the $e/(e-1)\approx1.58$ bound for Best-$\alpha$ that is the goal of this mission, and an optimal randomized on-line algorithm.
• 1999, Afrati et al. (FOCS 1999): a polynomial-time approximation scheme for $1|r_j|\sum w_jC_j$. This settled the approximability of the problem, but the resulting algorithms are far from simple.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$. Job $J_j$ has a processing time $p_j>0$, a release date $r_j\ge0$, and, where the objective is weighted, a weight $w_j>0$. There is one machine.

A nonpreemptive schedule assigns each job a start time $S_j\ge r_j$ such that the intervals $[S_j,S_j+p_j)$ are pairwise disjoint. Its completion times are $C_j=S_j+p_j$.

A preemptive schedule $P$ specifies, for each time $t$, which job runs at $t$, if any. Job $J_j$ runs only at times $t\ge\max(0,r_j)$, receives exactly $p_j$ units of processing in total, and finishes by some finite time. Its completion time $C^P_j$ is the first time by which all of $J_j$ has been processed. For $\alpha\in(0,1]$, its $\alpha$-point $C^P_j(\alpha)$ is the first time by which $\alpha p_j$ units have been processed.

For a job $J_i$, $T_i$ denotes the idle time of $P$ before $C^P_i$. $x_{ij}$ denotes the fraction of $J_j$ processed before $C^P_i$. The paper writes $S^P_i(\beta)$ for the set of jobs with $x_{ij}=\beta$, and also for their total processing time.

One-machine list scheduling in a given order runs the jobs nonpreemptively in that order. Each job starts at the later of its release date and the completion of the previous job in the list. An $\alpha$-schedule is list scheduling in nondecreasing order of the $\alpha$-points $C^P_j(\alpha)$. $C^\alpha_j$ denotes the completion times of an $\alpha$-schedule.

Random-$\alpha$ draws $\alpha$ from a distribution on $(0,1]$ and outputs the $\alpha$-schedule. Best-$\alpha$ outputs the $\alpha$-schedule of smallest total completion time $\min_\alpha\sum_j C^\alpha_j$.

Formalization targets

Goal: Corollary 2.7

Let $P$ be optimal among preemptive schedules for $\sum_j C_j$. Then there is $\alpha\in(0,1]$ such that every $\alpha$-schedule derived from $P$ satisfies

$$\sum_j C^\alpha_j\;\le\;\frac{e}{e-1}\sum_j C_j\qquad\text{for every feasible nonpreemptive schedule } (C_j)_j .$$

Since Best-$\alpha$ returns a schedule no worse than this $\alpha$-schedule, Best-$\alpha$ is an $e/(e-1)$-approximation.

Milestones

1. The calculus behind the constant. For $f(\alpha)=e^\alpha/(e-1)$ and every $\beta\in(0,1]$,

$$\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha=\frac1{e-1}.$$

2. Lemma 2.2: $C^P_i=T_i+\sum_{0<\beta\le1}\beta S^P_i(\beta)$.
3. Lemma 2.3: $C^\alpha_i\le T_i+(1+\alpha)\sum_{\beta\ge\alpha}S^P_i(\beta)+\sum_{\beta<\alpha}\beta S^P_i(\beta)$.
4. Lemma 2.5: if $\alpha$ has density $f$ on $(0,1]$, then $E[C^\alpha_i]\le(1+\delta)C^P_i$ with $\delta=\max_{0<\beta\le1}\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha$.
5. Theorem 2.6, for the weighted objective with $P$ optimal among preemptive schedules: the expected approximation ratio of Random-$\alpha$ is at most $2$ for uniform $\alpha$, at most $1.8$ for $\alpha=1$ w.p. $3/5$ and $\alpha=1/2$ w.p. $2/5$, and at most $e/(e-1)$ for the density $e^\alpha/(e-1)$.

Companion statements, not milestones:

• the upper bound of Theorem 2.1, $\sum_jC^\alpha_j\le(1+1/\alpha)\sum_jC^P_j$;
• the existence of an optimal preemptive schedule.

Significance

The $e/(e-1)$ bound shows that conversion from the preemptive relaxation can beat the factor 2 of the natural ordering. It does so by exploiting that no single instance is bad for many values of $\alpha$ at once. The $\alpha$-point technique was also used with LP relaxations, for example by Goemans (SODA 1997) and by Schulz and Skutella. The randomized version is an optimal randomized on-line algorithm for $1|r_j|\sum C_j$. Lemma 2.3 is a statement about any preemptive schedule, so it applies wherever a good preemptive or fractional schedule is available.

All results of the mission are proved in the paper, except that the proof of Theorem 2.6, part 2 is omitted there. No machine-checked proof of them is known. A complete development would give a verified model of preemptive one-machine schedules, $\alpha$-points and list scheduling, together with the averaging argument over $\alpha$. These are reusable for the later results of the same paper and for the $\alpha$-point literature.

Difficulty

The obvious argument bounds each job's $\alpha$-schedule completion time directly against its preemptive completion time. That argument loses a factor $1+1/\alpha$ (Theorem 2.1), which is at least 2 for every fixed $\alpha$. The improvement needs Lemma 2.3. There the charge to each job depends on how much of it was done by $C^P_i$ relative to $\alpha$, and the idle time $T_i$ is not inflated at all. Proving Lemma 2.3 requires reasoning about a preemptive schedule as a measure on time, and about how moving pieces of jobs changes completion times. A proof that treats the preemptive schedule as a finite list of pieces must first show that nothing is lost by this discretization.

The averaging step needs the expectation over $\alpha$ to be an honest integral. The map $\alpha\mapsto C^\alpha_i$ must be shown integrable, which requires a fixed rule for ties between equal $\alpha$-points.

Formalization scope

• Model. Jobs are Fin n, time is real, $p_j>0$ and $r_j\ge0$. The paper admits $p_j=0$ only in its tightness instances.
  • A preemptive schedule is a function $\sigma:\mathbb R\to$ Option (Fin n) (none = idle). Each job's run set is measurable, lies in $[\max(0,r_j),\infty)$, is bounded above, and has Lebesgue measure $p_j$.
  • Completion times and $\alpha$-points are infima of nonempty sets that are bounded below.
  • $T_i$ is the measure of the idle set in $[0,C^P_i)$.
  • The paper's sums over $\beta$ are sums over jobs, weighted by the fraction $x_{ij}$.
• List scheduling is strict: jobs never overtake the list order, and the machine is free from time $0$.
  • Lemma 2.3, Theorem 2.1, Theorem 2.6.2 and the goal hold for every tie-break among equal $\alpha$-points.
  • The expectations (Lemma 2.5, Theorem 2.6.1 and 2.6.3) use the tie-break by job index. They assert integrability as part of the conclusion.
• Optimality. "Approximation ratio $c$" is stated as an inequality against every feasible nonpreemptive schedule, never against an infimum.
  • The optimality of $P$ among preemptive schedules is the paper's standing assumption for its upper bounds (p. 151). It appears as a hypothesis of Theorem 2.6 and of the goal.
  • The lemmas hold for arbitrary $P$ and do not carry it.
  • An existence statement shows the hypothesis can be met.
• Lemma 2.5's $\delta$ is replaced by any upper bound of the integrals over $\beta\in(0,1]$. This is equivalent, and it avoids assuming that the maximum is attained.
• Not stated:
  • the running time $O(n^2)$ of Best-$\alpha$ and the optimality of SRPT;
  • the tightness parts of Theorem 2.1 and Corollary 2.4, and the lower bounds of Theorem 2.9, which use zero-length jobs;
  • the on-line Theorem 2.8, which needs a model of on-line algorithms.
• Trivializing formalization ruled out. Dropping the optimality of $P$ from the goal would turn it into a statement about arbitrary preemptive schedules, which is Lemma 2.5, not Corollary 2.7. Comparing against $\sum_jC^P_j$ instead of every nonpreemptive schedule would likewise remove the content of the corollary.

Contributions are welcome at every level. The calculus milestone and Lemma 2.2 are good first targets.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• C. Phillips, C. Stein, J. Wein, Scheduling jobs that arrive over time, Proc. 4th Workshop on Algorithms and Data Structures (WADS), 1995, pp. 86–97 (reference [25] of the paper; no link verified).
• J. A. Hoogeveen, A. P. A. Vestjens, Optimal on-line algorithms for single-machine scheduling, Proc. 5th IPCO, 1996, pp. 404–414 (reference [21]; no link verified).
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 1997, pp. 591–598 (reference [12]; no link verified).
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th FOCS, 1999 (reference [2]; no link verified).

Motivation

Minimizing the average completion time of jobs that arrive over time is a basic objective in machine scheduling. It measures how long a job spends in the system on average. With several identical machines, release dates and no preemption (written $P|r_j|\sum C_j$), the problem is strongly NP-hard already on one machine. Research has therefore looked for approximation algorithms: polynomial-time rules whose total completion time is provably within a constant factor of every feasible schedule.

A common approach solves a relaxation that is easy to optimize and converts its solution into a feasible schedule. Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) use a relaxation that needs neither linear programming nor dynamic programming: pretend that the $m$ machines are one machine that is $m$ times as fast, and allow preemption.

Timeline:

• 1996, Chakrabarti, Phillips, Schulz, Shmoys, Stein and Wein (ICALP 1996, LNCS 1099, pp. 646–657): a $(2.89+\epsilon)$-approximation for $P|r_j|\sum C_j$.
• 2001, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), §3 and §4.5). §3 gives a simple $(3-1/m)$-approximation by list scheduling from the one-machine relaxation. §4.5 combines it with the Delay List conversion to obtain $2\sqrt2\approx2.83$. This mission's goal is the §4.5 result.
• 1999, Afrati, Bampis, Chekuri, Karger, Kenyon, Khanna, Milis, Queyranne, Skutella, Stein and Sviridenko (FOCS 1999, pp. 32–43): polynomial-time approximation schemes for $P|r_j|\sum w_jC_j$. These settle the approximability, but the algorithms are far more involved than the ones formalized here.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$ and $m\ge1$ identical machines. Job $J_j$ has a processing time $p_j>0$ and a release date $r_j\ge0$.

A feasible schedule gives each job a start time $S_j\ge r_j$ and a machine. Job $J_j$ runs without interruption on its machine during $[S_j,S_j+p_j)$, and two jobs on the same machine never overlap. The completion times are $C_j=S_j+p_j$ and the objective is $\sum_j C_j$. $C^*_j$ denotes the completion times of an arbitrary feasible schedule, against which every bound is stated.

The one-machine relaxation $I1$ has the same jobs and a single machine. Job $J_j$ has processing time $p_j/m$ and release date $r_j$ in $I1$, and may be preempted. A preemptive schedule $P1$ of $I1$ gives each job a processing rate $\rho_j(t)\ge0$. The rates sum to at most $1$ at each time, and no job is processed before its release date. Each job receives $p_j/m$ units in total. Its completion time $C^{P1}_j$ is the first time by which all of it has been processed. $P1$ is optimal if $\sum_j C^{P1}_j$ is minimal among all such schedules.

A list is an ordering $\pi$ of the jobs, and the completion order of $P1$ lists the jobs by nondecreasing $C^{P1}_j$. Two ways of turning a list into an $m$-machine schedule are compared.

• Strict-order list scheduling gives the schedule $N$. The jobs start in the order of the list. Each job starts at the earliest time that is no earlier than its release date, no earlier than the previous job's start, and at which some machine is free.
• Delay List with parameter $\beta>0$ gives the schedule $D$. When a machine is idle, Delay List starts the first unscheduled job of the list if it has been released. If that job has not been released, the first released job of the list may jump ahead, but only once at least $\beta p_j$ units of idle time (machine × time) have accumulated that no earlier job has charged. The job then charges exactly that amount. A job started in list order charges all uncharged idle time since its release.

Formalization targets

Goal: Lemma 4.19

With $P1$ optimal, $\pi$ its completion order, $N$ the strict-order list schedule of $\pi$ and $D$ a Delay List schedule of $\pi$ with $\beta_0=\sqrt{3-2\sqrt2}$, every feasible schedule satisfies

$$\min\Bigl(\sum_j C^N_j,\ \sum_j C^D_j\Bigr)\le 2\sqrt2\,\sum_j C^*_j .$$

The printed lemma says $2.83$. Its proof gives $2\sqrt2\approx2.8284$, which is stated here.

Milestones

In the order the proof uses them:

1. (4.2): if $\sum_j p_j>\alpha\sum_j C^*_j$ then $\sum_j r_j\le(1-\alpha)\sum_j C^*_j$.
2. Lemma 3.1: $\sum_j C^{P1}_j\le\sum_j C^*_j$ for $P1$ optimal.
3. (3.3): $\sum_j C^N_j\le 2\sum_j C^{P1}_j+(1-1/m)\sum_j p_j$ for any $P1$.
4. Lemma 3.2: $\sum_j C^N_j\le(3-1/m)\sum_j C^*_j$.
5. Theorem 4.9, specialised to no precedence constraints. With $B_i$ the jobs at or before $J_i$ in the list,

$$C^D_i\le\frac{(1+\beta)p(B_i)}{m}+\Bigl(1+\frac1\beta\Bigr)(r_i+p_i)-\frac{p_i}{\beta}.$$

6. Lemma 4.18: $\sum_j C^D_j\le(2+\beta)\sum_j C^*_j+\frac1\beta\sum_j r_j$.
7. The balanced bound: under (4.2)'s hypothesis, $\sum_j C^D_j\le(2+\beta+(1-\alpha)/\beta)\sum_j C^*_j$.
8. The constants: at $\alpha=2\sqrt2-2$ and $\beta=\sqrt{3-2\sqrt2}$, $2+\alpha=2+\beta+(1-\alpha)/\beta=2\sqrt2$.

Two existence statements accompany them. One says an optimal $P1$ exists. The other says a Delay List schedule exists for every list and every $\beta>0$.

Significance

The result gives a $2\sqrt2$-approximation for $P|r_j|\sum C_j$ that is simple to state and runs in $O(n\log n)$ time. It improves the $2.89+\epsilon$ bound of Chakrabarti et al. Neither of its two algorithms achieves the ratio alone. It comes from an analysis in which each algorithm is good exactly when the other is bad. List scheduling is good when processing times are small relative to the optimum. Delay List is good when release dates are small. The inequality (4.2) connects the two cases.

The component results are reusable beyond this paper. The one-machine relaxation lower bound (Lemma 3.1) and the $(3-1/m)$ bound for list scheduling from it (Lemma 3.2) apply to any conversion from a fast single machine. The per-job bound of Theorem 4.9 is the core of the Delay List technique. Its general form, with precedence constraints, drives the paper's results for precedence-constrained scheduling.

All results are proved in the paper. None of them has a machine-checked proof that this mission knows of. A formalization would check the Delay List charging argument, which the paper states only in discrete time and adapts to continuous time in one sentence. It would also produce reusable Lean definitions of parallel-machine schedules with release dates and of list scheduling.

Difficulty

The arithmetic of the goal is routine once the milestones are in place. The substance lies in two places.

The first is Lemma 3.1 together with the "standard makespan argument" behind (3.2). The one-machine relaxation must be related to the $m$-machine schedule, and to the list schedule, with care about release dates. In particular, in the list schedule every machine is busy between the last release among the first $j$ jobs of the list and the start of the $j$-th job. Proving this needs the strict order.

The second, and harder, is Theorem 4.9. The obvious argument bounds the waiting time of job $J_i$ by the work of the jobs ahead of it, but Delay List lets later jobs jump ahead. The idle time before $J_i$ starts and the work of the jobs that jump ahead of it must both be controlled, and the paper's charging argument for this depends on where charged idle time lies on the time axis and on which jobs charged it. Making that bookkeeping precise for a continuous-time algorithm is the main formalization cost.

Formalization scope

Jobs are Fin n and machines Fin m with $m\ge1$. Times are real, processing times are positive and release dates nonnegative. There are no weights and no precedence constraints. "Optimal" is never an infimum. Every bound is stated against every feasible nonpreemptive schedule, and $P1$'s optimality is the hypothesis that its total completion time is at most that of every preemptive schedule of $I1$.

Committed conventions:

• Preemptive schedules of $I1$ are rate functions, so the machine of $I1$ may be shared. The paper's one-job-at-a-time schedules are a special case.
• Lists are bijections Fin n ≃ Fin n. A list of $P1$ may break ties in completion time in any way, and every such list is covered.
• $N$ is the strict-order variant of list scheduling, which footnote 3 of the paper contrasts with the greedy variant used in §4. It is a recursive definition over list positions.
• Delay List is the continuous-time algorithm, as adopted in the proof of Fact 4.6. It is a predicate on start times, machines, the scheduling order and charge windows. A job scheduled out of order takes its charge from the most recent uncharged idle time; the paper leaves this placement open. Theorem 4.9 and Lemma 4.18 assume $m\ge2$, the setting of §4.1. The goal assumes only $m\ge1$.
• The printed Lemma 4.18 lacks a $\sum_j$ on the $C^*$ term. The summed form of its proof's last display is stated.

The statement cannot be made easy by the hypotheses. Two existence items show that an optimal $P1$ and a Delay List schedule always exist, so no statement is vacuous. The bound is against every feasible schedule, not against the relaxation's value.

Not stated: the $O(n\log n)$ running time, the on-line version of §3's algorithm, and Delay List with precedence constraints (Theorem 4.9 in general, which is the subject of mission III of this series). Contributions welcome: proofs of the milestones, and reusable lemmas on list scheduling with release dates.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• S. Chakrabarti, C. A. Phillips, A. S. Schulz, D. B. Shmoys, C. Stein, J. Wein, Improved scheduling algorithms for minsum criteria, in Proceedings of ICALP 1996, LNCS 1099, Springer, pp. 646–657 (reference [3] of the paper).
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, in Proceedings of the 40th IEEE FOCS, 1999, pp. 32–43 (reference [2] of the paper).

Motivation

Minimizing the sum of weighted completion times $\sum_j w_jC_j$ is one of the standard objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. With release dates or precedence constraints the problem is NP-hard already on one machine, and on $m$ identical parallel machines it is harder still, so the literature of the 1990s concentrated on approximation algorithms. Many of these, including LP-based ones, are naturally designed for a single machine, where an order of the jobs determines the schedule.

Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) gave a generic way to move from one machine to many. Their §4 describes an algorithm, Delay List, that takes any one-machine schedule as a priority list and produces an $m$-machine schedule, and proves that a $\rho$-approximate one-machine schedule yields a $\bigl((1+\beta)\rho+1+1/\beta\bigr)$-approximate $m$-machine schedule for every $\beta>0$. The guarantee holds with release dates and arbitrary precedence constraints simultaneously, which at the time gave the best bounds known for several special cases, for example a factor 4 for series-parallel precedence without release dates.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$. Job $J_j$ has processing time $p_j>0$, release date $r_j\ge 0$ and weight $w_j>0$. Precedence constraints form a strict partial order $\prec$: $i\prec j$ means that $J_j$ may start only after $J_i$ completes.

A feasible nonpreemptive schedule on $m$ machines assigns each job a start time $S_j$ and a machine; each job runs uninterrupted for $p_j$ time units on its machine, two jobs on one machine do not overlap, $S_j\ge r_j$, and $S_i+p_i\le S_j$ whenever $i\prec j$. The completion time is $C_j=S_j+p_j$ and the value of the schedule is $\sum_j w_jC_j$. A one-machine schedule is the case $m=1$.

The critical-path length $\kappa_j$ (Definition 4.1) is $p_j+r_j$ for a job without predecessors and $p_j+\max\{\max_{i\prec j}\kappa_i,\,r_j\}$ otherwise; it is the earliest time $J_j$ could complete with unlimited machines.

A list is an ordering $\pi$ of the jobs. Delay List with parameter $\beta>0$ processes time continuously. A job is ready once it is released and all its predecessors have completed; $q^m_j$ is the time it becomes ready. The head is the first unscheduled job of the list. Idle machine-time is recorded as charged to jobs. Whenever a machine is idle:

1. if the head is ready, it is started, and charged all uncharged idle time in $(q^m_j,s^m_j)$;
2. otherwise the first ready job $J_k$ of the list is started as soon as at least $\beta p_k$ units of uncharged idle time have accumulated, and is charged $\beta p_k$ of it;
3. otherwise nothing happens.

For a job $J_i$, $B_i$ is the set of jobs up to and including $J_i$ in the list, $A_i$ the set after it, $O_i\subseteq A_i$ the set of jobs of $A_i$ started before $J_i$, and $p(A)=\sum_{k\in A}p_k$. Definition 4.4 builds from the schedule a backward path $P'_i$ ending at $J_i$, whose length is $\kappa'_i$.

Formalization targets

Goal: Theorem 4.13

Let $S^1$ be a feasible one-machine schedule of the instance with $\sum_j w_jC^1_j\le\rho\sum_j w_jC'_j$ for every feasible one-machine schedule $C'$. Let $m\ge 2$ and $\beta>0$. Every Delay List schedule $S^m$ built on the completion order of $S^1$ satisfies, for every feasible $m$-machine schedule $N$,

$$\sum_j w_jC^m_j\le\Bigl((1+\beta)\rho+1+\frac1\beta\Bigr)\sum_j w_jC^N_j .$$

Milestones, in the order the proof uses them

• Fact 4.5: $\kappa'_i\le\kappa_i$.
• Fact 4.6: the idle time charged to $J_i$ is at most $\beta p_i$.
• Lemma 4.7: no uncharged idle time remains in $(q^m_i,s^m_i)$, and that idle time is charged only to jobs in $B_i$.
• Lemma 4.8: the idle time charged to $A_i$ within $(0,s^m_i)$ is at most $m(\kappa'_i-p_i)$, so $p(O_i)\le m(\kappa'_i-p_i)/\beta\le m(\kappa_i-p_i)/\beta$.
• Theorem 4.9: $C^m_i\le(1+\beta)p(B_i)/m+(1+1/\beta)\kappa'_i-p_i/\beta$ for any list obeying precedence.
• Lemma 4.10: $C^m_{\mathrm{OPT}}\ge C^1_{\mathrm{OPT}}/m$.
• Lemma 4.11: $C^m_{\mathrm{OPT}}\ge\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$.
• Corollary 4.12: $C^m_i\le(1+\beta)C^1_i/m+(1+1/\beta)\kappa_i$ when the list is the completion order of $S^1$.

A further item states that a Delay List schedule exists for every instance and every list, so that the goal does not hold vacuously.

Significance

The result. Theorem 4.13 turns every one-machine approximation algorithm for weighted completion time with release dates and precedence into an $m$-machine algorithm at a bounded loss. With an optimal one-machine schedule and $\beta=1$ the factor is $4$ (Corollary 4.14, for series-parallel orders), and the bounds are job-by-job (Theorem 4.9, Corollary 4.12), which the paper uses in Remark 4.15 to extend the method to other metrics and to one-machine schedules that ignore release dates. The same algorithm is the engine of the paper's $2\sqrt2$-approximation for parallel machines with release dates (§4.5).

Formalizing it. The theorem has been proved since 1997 (SODA) and 2001 (journal). There is no machine-checked version of it or of any of its lemmas, and the platform currently has no model of scheduling with release dates and precedence constraints. A formalization produces a precise specification of Delay List, whose informal description is given in discrete time and repaired in a remark; a checked proof of the charging argument; and reusable lower bounds (Lemmas 4.10 and 4.11) for any later work on parallel-machine scheduling with precedence.

Difficulty

The obvious attempt, list scheduling (start the first available job of the list whenever a machine is free), fails with non-identical processing times: a long job taken out of order can occupy a machine and delay a more valuable job that becomes ready shortly afterwards. Delay List allows out-of-order jobs only against accumulated idle time, and the analysis rests on a charging invariant. Stating it needs care about time (the paper's discrete-time exposition can over-charge by a time unit), about which idle time a charge consumes, and about many jobs being scheduled at one instant. The bound must hold simultaneously for release dates and arbitrary precedence constraints, where idle machines can be forced both by jobs that are not yet released and by chains of predecessors, and it must hold for every tie-breaking choice of the algorithm.

Formalization scope

Jobs are Fin n, machines Fin m, and times are real numbers. Processing times are positive, release dates nonnegative and weights positive, as in §1. Precedence is a strict partial order, the transitive closure of the paper's DAG; $\kappa$, readiness and feasibility are unchanged by taking the closure. The optimum is never a real infimum: "within a factor $\rho$ of an optimal one-machine schedule" and "within a factor $c$ of an optimal $m$-machine schedule" are inequalities against every feasible schedule of the same instance, with the same release dates and precedence constraints.

Delay List is formalized in the continuous-time version described in the proof of Fact 4.6, as a predicate on runs that records start times, machines, the order in which jobs are scheduled at equal times, and charge windows. A case-2 charge takes the most recent uncharged idle time, and idle time is charged by whole time slices. Every guarantee is claimed for every run satisfying the predicate. The ties in Definition 4.4 are broken arbitrarily, so statements involving $\kappa'_i$ hold for every admissible path. Lemma 4.10 uses nonpreemptive one-machine schedules. Lemma 4.11's $C^\infty_{\mathrm{OPT}}$ is modelled by $n$ machines.

It would be trivializing to assume the conclusions of Fact 4.6 or Lemma 4.7 as properties of the run, or to measure $\rho$ against a relaxation without release dates or precedence; both are ruled out. The algorithm's rules are the only hypotheses on the run.

Not stated: the running time of Delay List; the discrete-time algorithm; Corollary 4.14 (it needs a formal class of series-parallel orders and the external one-machine algorithm of Adolphson for them); Remark 4.15 (release-date-free one-machine schedules), whose hypotheses the paper does not pin down; and the extension to delays between jobs. Contributions of general infrastructure, such as idle-time accounting for step functions and lemmas about list schedules under precedence, are welcome and reusable beyond this mission.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM Journal on Computing 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• R. L. Graham, Bounds for certain multiprocessing anomalies, Bell System Technical Journal 45:1563–1581, 1966. https://doi.org/10.1002/j.1538-7305.1966.tb01709.x
• D. Adolphson, Single machine job sequencing with precedence constraints, SIAM Journal on Computing 6(1):40–54, 1977. https://doi.org/10.1137/0206002

Motivation

Minimizing the sum of weighted completion times of jobs on identical parallel machines is one of the basic objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. When the jobs are subject to precedence constraints (a job may start only after certain other jobs have finished), the problem is strongly NP-hard already in very restricted cases, and the question becomes how close to optimal a polynomial-time algorithm can guarantee to be.

Chekuri, Motwani, Natarajan and Stein, Approximation Techniques for Average Completion Time Scheduling (SIAM J. Comput. 31(1), 2001, doi:10.1137/S0097539797327180), develop a general way to turn a good schedule for a single machine into a good schedule for $m$ machines. For arbitrary precedence constraints their conversion (Delay List, §4.1–4.3) loses a factor $(1+\beta)\rho+(1+1/\beta)$ over a $\rho$-approximate one-machine schedule, which is $4$ when the one-machine schedule is optimal. In §4.4 they show that for in-tree precedence without release dates, the plain list-scheduling rule of Graham, fed with an optimal one-machine schedule, already achieves ratio $2$. In-trees are the precedence structures of assembly processes: every job feeds into at most one later job.

Timeline of the relevant results:

• 1966–1969: Graham introduces list scheduling on parallel machines and analyzes it for makespan (Graham 1969).
• 1972: Horn gives a polynomial-time optimal one-machine algorithm for weighted completion time under treelike precedence (Horn 1972).
• 1977: Adolphson gives $O(n\log n)$ one-machine algorithms for tree and series-parallel precedence (Adolphson 1977, the paper's reference [1]).
• 2001: Chekuri, Motwani, Natarajan and Stein prove the ratio-$2$ bound for in-trees on $m$ machines (Theorem 4.17).

Setting

There are $n$ jobs $J_0,\dots,J_{n-1}$ and $m\ge 1$ identical machines. Job $J_j$ has a processing time $p_j>0$ and a weight $w_j>0$; every job is available at time $0$ (there are no release dates).

The precedence constraints form an in-tree (more generally, an in-forest): every job $j$ has at most one immediate successor $\operatorname{succ}(j)$, and following successors never returns to the start. Write $i\prec j$ if $j$ is reached from $i$ by following successors one or more times.

A feasible schedule $S^m$ on $m$ machines gives each job a start time $S_j\ge 0$ and a machine; a job runs without interruption for $p_j$ time units; two jobs on the same machine do not overlap; and $i\prec j$ implies that $j$ starts no earlier than $i$ completes. The completion time is $C^m_j=S_j+p_j$ and the value of the schedule is $\sum_j w_jC^m_j$.

The critical-path length $\kappa_j$ (Definition 4.1 with no release dates) is $\kappa_j=p_j$ if $j$ has no predecessors and $\kappa_j=p_j+\max_{i\prec j}\kappa_i$ otherwise.

A list is an ordering $\pi$ of the jobs that obeys the precedence constraints. It defines the one-machine schedule $S^1$ that runs the jobs in list order without idle time; its completion times are $C^1_j$, the total processing time of the jobs up to and including $j$ in the list. An optimal one-machine schedule is a list minimizing $C^1=\sum_j w_jC^1_j$.

List scheduling (Graham's rule, footnote 3 of the paper) on $m$ machines with list $\pi$: whenever a machine is free, start on it the first job of the list that is ready, i.e. whose predecessors have all completed.

Formalization targets

Goal: Theorem 4.17

Let $\pi$ be an optimal one-machine schedule and $G$ the list schedule on $m$ machines with list $\pi$. Then for every feasible $m$-machine schedule $N$,

$$\sum_j w_jC^G_j\ \le\ 2\sum_j w_jC^N_j .$$

Milestones

Lemma 4.16 (any precedence-respecting list $\pi$, with its idle-free one-machine schedule $S^1$): for every job $i$,

$$C^G_i\ \le\ \kappa_i+\frac{C^1_i}{m}.$$

Lemma 4.10: $C^m_{\mathrm{OPT}}\ge C^1_{\mathrm{OPT}}/m$, i.e. $\sum_j w_jC^1_j/m\le\sum_j w_jC^N_j$ for an optimal list and every feasible $N$.

Lemma 4.11: $C^m_{\mathrm{OPT}}\ge\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$, i.e. $\sum_i w_i\kappa_i\le\sum_i w_iC^N_i$ for every feasible $N$ on any number of machines, and the value $\sum_i w_i\kappa_i$ is attained by a feasible schedule on $n$ machines.

Significance

The result. Theorem 4.17 gives a simple, fast algorithm with a guaranteed factor $2$ for a strongly NP-hard problem, halving the factor $4$ that the general Delay List conversion gives for the same class. The per-job bound of Lemma 4.16 is stronger than the aggregate statement: every single job completes within its critical-path length plus a $1/m$ share of its one-machine completion time, so the same bound applies to other objectives built from completion times.

Formalizing it. The paper's proof is complete and short, but it argues about events at a time $t$ (jobs that finish exactly at $t$, jobs that become ready at $t$, machines freed at $t$) and runs an induction over jobs ordered by start time with an invariant about idle time. A machine-checked version fixes what "list scheduling" means precisely, pins down the counting argument that uses the in-tree structure, and yields reusable definitions of nonpreemptive parallel-machine schedules, critical paths and list schedules. To the knowledge of this mission, none of these results has a machine-checked proof.

Difficulty

List scheduling may start a job that is late in the list before an earlier one, because the earlier job is not yet ready; so the one-machine order is not preserved and the obvious comparison with $S^1$ fails. Idle machines are the other obstacle: a machine can stay idle while a job waits for its predecessors, and a per-job bound of the form $\kappa_i+C^1_i/m$ holds only if such idle time can be accounted for by $J_i$'s own chain of predecessors. For general precedence constraints, and for out-trees (every job has at most one immediate predecessor), the paper's accounting breaks down, and the paper states the per-job bound only for in-trees; the in-tree structure is essential to the argument. Events with several jobs finishing at the same instant, and ties in start times, have to be handled without loss.

Formalization scope

• Jobs are Fin n, machines Fin m, times real numbers. Processing times and weights are strictly positive. There are no release dates: start times are nonnegative. The paper admits $p_j=0$ only in lower-bound instances elsewhere; the bounds here assume $p_j>0$.
• In-trees are encoded by an immediate-successor map succ : Fin n → Option (Fin n) with no cycles; this covers in-forests, the reading of "in-trees" in Theorem 4.17. The precedence relation is its transitive closure.
• $\kappa$ is defined by well-founded recursion on the precedence order, exactly as Definition 4.1 with $r\equiv 0$.
• One-machine schedules are represented by their precedence-respecting order and are idle-free; with no release dates and positive processing times idle time only delays jobs, so optimality among orders is optimality among one-machine schedules. The optimal one-machine schedule is a hypothesis of the goal; the paper's $O(n\log n)$ algorithm for computing it (reference [1]) is not formalized, and the running-time claim of Theorem 4.17 is not stated. A separate item asserts that an optimal order exists.
• List scheduling is specified by two properties that determine Graham's rule up to machine labels: no machine is idle while a ready job waits, and among jobs ready at a start time the earlier one in the list starts first. A separate item asserts that such a schedule exists for every precedence-respecting list, so the goal is not vacuous.
• Optima are never formed as infima: the approximation ratio is stated against every feasible schedule. A statement of the form "there is an algorithm with ratio 2" would be trivial (an optimal schedule exists) and is ruled out: the goal is about the paper's algorithm.
• The equality $\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$ in Lemma 4.11 is stated as attainment on $n$ machines (as many machines as jobs), which together with the lower bound on every number of machines is the optimum with unboundedly many machines.

Welcome contributions: proofs of the two existence items (Graham's list schedule by event-driven construction; an optimal order over the finite set of linear extensions), of Lemmas 4.10 and 4.11, and of Lemma 4.16. The schedule and list-scheduling definitions are reusable for other parallel-machine results with precedence constraints.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• R. L. Graham, Bounds on multiprocessing timing anomalies, SIAM J. Appl. Math. 17(2):416–429, 1969. https://doi.org/10.1137/0117039
• W. A. Horn, Single-machine job sequencing with treelike precedence ordering and linear delay penalties, SIAM J. Appl. Math. 23(2):189–202, 1972. https://doi.org/10.1137/0123021
• D. L. Adolphson, Single machine job sequencing with precedence constraints, SIAM J. Comput. 6(1):40–54, 1977. https://doi.org/10.1137/0206002

Motivation

The Critical-Path Method (CPM) was introduced by J. E. Kelley, Jr. (Remington Rand) and M. R. Walker (du Pont) in Critical-Path Planning and Scheduling (Proc. Eastern Joint Computer Conference, 1959, pp. 160–173, doi:10.1145/1460299.1460318). Together with PERT, developed at the same time for the Polaris programme, it became the standard way to plan and schedule large projects in construction, maintenance and engineering, and it is taught in every introductory operations research course.

The paper reduces project scheduling to arithmetic on a directed acyclic graph: the earliest and latest times of the project's events are computed by two recursions, and the jobs whose timing has no slack, the critical jobs, are singled out by an equation. Its central structural claim is that critical jobs, when they exist, form a path from the start of the project to its end. The paper states this without proof ("a detailed development being reserved for a separate paper", p. 161). This mission formalizes that claim and the facts about the two recursions on which it rests.

Setting

A project network has $n+1$ events labelled $0,1,\dots,n$ with $n \ge 1$: event $0$ is the origin and event $n$ the terminus. A job is an arrow from an event $i$ to an event $j$, written job $(i,j)$; the jobs form a finite set $P$ of ordered pairs of events. Two standing assumptions of the paper (pp. 161–162) are part of the model:

1. every job has $i < j$ (events are labelled so that the head of an arrow has the larger label);
2. origin precedes and terminus follows every event: for every event $k$ there are chains of jobs from $0$ to $k$ and from $k$ to $n$.

Each job has a real duration $y_{ij}$. The earliest event times $t^{(0)}$ are given by display (1) of the paper,

$$t_0^{(0)} = 0,\qquad t_j^{(0)} = \max\,[\,y_{ij} + t_i^{(0)} \mid i<j,\ (i,j)\in P\,],\quad 1\le j\le n,$$

and, for a project completion time $\lambda \ge t_n^{(0)}$, the latest event times $t^{(1)}$ by display (2),

$$t_n^{(1)} = \lambda,\qquad t_i^{(1)} = \min\,[\,t_j^{(1)} - y_{ij} \mid i<j,\ (i,j)\in P\,],\quad 0\le i\le n-1.$$

The maximum time available for job $(i,j)$ is $t_j^{(1)} - t_i^{(0)}$. The job is critical if this equals its duration, $t_j^{(1)} - t_i^{(0)} = y_{ij}$, and a floater if it exceeds it. A critical path is a contiguous path of critical jobs from origin to terminus: events $0 = v_0, v_1, \dots, v_k = n$ with every $(v_{r-1}, v_r)$ a critical job of $P$.

In the Lean development these are ProjectNetwork n (with field P), earliest N y, latest N y λ, maxTimeAvailable, IsCritical, IsFloater and IsCriticalPath, in the namespace CriticalPath.Events.

Formalization targets

Goal: critical jobs force $\lambda = t_n^{(0)}$ and a critical path (p. 163)

For every project network, durations $y$ and completion time $\lambda \ge t_n^{(0)}$,

$$\bigl(\exists (i,j)\in P,\ t_j^{(1)} - t_i^{(0)} = y_{ij}\bigr) \;\Longrightarrow\; \lambda = t_n^{(0)} \ \wedge\ \exists\ \text{a critical path}.$$

This is the paper's "A project will contain critical jobs only when $\lambda = t_n^{(0)}$. If a project does contain critical jobs, then it also contains at least one contiguous path of critical jobs through the project diagram from origin to terminus." Only the "only when" direction is asserted, as on the page.

Milestones

1. Display (1), pp. 162–163. $t^{(0)}$ is the least vector $t$ with $t_0 = 0$ and $y_{ij} \le t_j - t_i$ for every job.
2. Display (2), p. 163. For $\lambda \ge t_n^{(0)}$, $t_n^{(1)} = \lambda$ and $t^{(1)}$ is the greatest vector $t$ with $t_n \le \lambda$ and $y_{ij} \le t_j - t_i$ for every job.
3. Critical or floater, p. 163. For $\lambda \ge t_n^{(0)}$, $t_i^{(0)} \le t_i^{(1)}$ for every event, and every job is critical or a floater: $t_j^{(1)} - t_i^{(0)} \ge y_{ij}$.
4. Delay of a critical job, p. 163. Lengthening a critical job by $\delta \ge 0$ raises $t_n^{(0)}$ by exactly $\delta$.

Significance

The result. The theorem is what makes the method's name meaningful: it says that the jobs without slack are not scattered but line up along an origin–terminus path, and that such jobs exist only when the project is scheduled at its earliest possible completion time. Project managers use this to decide which jobs to watch, which to expedite, and which may slip; the delay statement (milestone 4) is the quantitative form of that advice. The characterisations of (1) and (2) as least and greatest feasible schedules are the bridge between CPM and linear programming: they identify $t^{(0)}$ and $t^{(1)}$ with extreme solutions of the system of difference constraints $y_{ij} \le t_j - t_i$, which the paper's own §3 uses to build the project cost curve.

Formalizing it. The results are classical and folklore, but the paper proves none of them, and textbook treatments usually define the critical path as a longest path, which makes the goal a tautology. This mission states the claims with the paper's own definitions: criticality by the float equation, event times by the recursions. To the best of current knowledge no machine-checked version of these statements for activity-on-arrow networks exists; the platform has a related activity-on-node development (Brucker and Knust, Complex Scheduling) in which the critical path is defined as a longest path.

Difficulty

The recursions (1) and (2) are local: each event looks only at its immediate predecessors or successors. The goal is global: from one critical job it asserts a statement about the whole completion time and a whole origin–terminus path. The float equation $t_j^{(1)} - t_i^{(0)} = y_{ij}$ mixes a quantity computed forward from the origin with one computed backward from the terminus, and neither recursion alone says anything about the other. The naive reading "a critical job lies on a longest path" is not available as a definition: it is, in substance, what has to be established from the recursions. The formal overhead is the well-founded recursion on the labels, in both directions, and the bookkeeping of lists of events forming a path.

Formalization scope

Events are Fin (n + 1), origin 0, terminus Fin.last n, with 1 ≤ n. Jobs are a Finset of ordered pairs, so there is at most one job per ordered pair. The standing assumptions (labels increase along jobs; origin precedes and terminus follows every event, via Relation.ReflTransGen) are fields of the structure ProjectNetwork and are never dropped. Durations and times are real numbers; durations are a function Fin (n+1) → Fin (n+1) → ℝ read only on jobs of P, with no sign condition, as in the paper's deterministic case.

The event times are defined by the recursions (1) and (2) themselves, by well-founded recursion on the label with Finset.sup'/Finset.inf' over the predecessor/successor set; these sets are nonempty by the standing assumptions, so no fallback value exists. The latest times are defined for every real $\lambda$; the paper's assumption $\lambda \ge t_n^{(0)}$ is a hypothesis of every theorem that uses them.

Disclosed readings: "earliest time occurance" (milestone 1) and "latest time … relative to a fixed project completion time" (milestone 2) are read as least and greatest vectors satisfying the job constraints $y_{ij} \le t_j - t_i$ (the paper's constraint (8), p. 165); milestone 3 is the fact implicit in the dichotomy "critical or floater"; "comparable delay" (milestone 4) is read as an exact delay of $\delta$ in $t_n^{(0)}$ for $\delta \ge 0$.

A trivializing formalization is ruled out: defining a critical job or path through longest paths, or taking $t^{(0)}$ and $t^{(1)}$ as arbitrary functions satisfying (1) and (2), would make the goal a restatement of its definitions; here criticality is the float equation and the times are computed by the recursions. Dropping the reachability assumptions would make (2) ill-defined at events without successors.

Contributions welcome: proofs of the milestones, general lemmas on longest paths in finite labelled DAGs and on difference constraints $y_{ij} \le t_j - t_i$, which are reusable for the companion mission on the project cost curve.

Selected references

• J. E. Kelley, Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Papers presented at the December 1–3, 1959, Eastern Joint IRE-AIEE-ACM Computer Conference, pp. 160–173, 1959. doi:10.1145/1460299.1460318
• J. E. Kelley, Jr., Critical-Path Planning and Scheduling: Mathematical Basis, Operations Research 9(3), pp. 296–320, 1961. doi:10.1287/opre.9.3.296
• P. Brucker and S. Knust, Complex Scheduling, 2nd ed., Springer, 2012. doi:10.1007/978-3-642-23929-8