Scheduling Theory

Motivation

Open shops model production and service systems in which every job must visit every machine, but the order of the visits is free: a car that needs an inspection, a wash and a tyre change, a patient who needs several tests, a student who sits several exams. The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) fixed the three-field notation $\alpha|\beta|\gamma$ that the scheduling literature still uses, and classified the complexity of the problems it can express. Among the polynomially solvable cases, the preemptive open shop with makespan objective, $O|pmtn|C_{\max}$, is one of the few multi-machine problems whose optimal value has a closed form for any number of machines and jobs.

Timeline.

• 1976: Gonzalez and Sahni (J. ACM 23) prove that the optimal preemptive open-shop makespan is the largest machine load or job length, and give a polynomial algorithm. In the same paper they solve $O2\|C_{\max}$ in linear time and show $O3\|C_{\max}$ NP-hard.
• 1978: Lawler and Labetoulle (J. ACM 25) give a linear-programming treatment of preemptive scheduling on unrelated machines and reformulate the open-shop construction in terms of decrementing sets, found by an assignment problem through the Birkhoff–von Neumann theorem.
• 1979: the survey (§5.2.2, p. 313) presents this construction as the standard argument and records the $O(r+\min\{m^4,n^4,r^2\})$ bound of Gonzalez (1976), where $r$ is the number of nonzero processing times.

Setting

There are $m$ machines $M_1,\dots,M_m$ and $n$ jobs $J_1,\dots,J_n$. Job $J_j$ consists of operations $O_{1j},\dots,O_{mj}$; operation $O_{ij}$ must be processed on machine $M_i$ for $p_{ij}\ge 0$ time units. The processing-time matrix is $P=(p_{ij})$: its rows are machines and its columns are jobs. Every job is available at time $0$.

Preemption is allowed: an operation may be interrupted and resumed later. A schedule is a finite list of pieces $(i,j,s,e)$, each meaning that $M_i$ processes $J_j$ during $[s,e)$. A schedule is feasible if

1. every piece satisfies $0\le s\le e$;
2. each machine processes at most one job at a time, and each job is processed on at most one machine at a time: two pieces that share a machine or a job do not overlap;
3. for every pair $(i,j)$ the pieces of $O_{ij}$ have total length exactly $p_{ij}$.

The makespan $C_{\max}$ is the time at which the last piece ends, and $C^*_{\max}$ is its minimum over feasible schedules. The load of machine $M_i$ is the row sum $\sum_j p_{ij}$, the length of job $J_j$ is the column sum $\sum_i p_{ij}$, and

$$C=\max\Big\{\max_j \sum_i p_{ij},\ \max_i \sum_j p_{ij}\Big\}.$$

A row or column is tight if its sum equals $C$ and slack otherwise. A decrementing set is a set $S$ of strictly positive entries of $P$ with exactly one element in each tight row and each tight column and at most one in each slack row and each slack column.

Formalization targets

Goal: $C^*_{\max}=C$

For every $T\ge 0$,

$$\big(\exists \text{ feasible schedule with } C_{\max}\le T\big)\iff \Big(\sum_j p_{ij}\le T\ \forall i\ \text{ and }\ \sum_i p_{ij}\le T\ \forall j\Big).$$

This says that the optimal makespan is exactly the largest machine load or job length, and that it is attained.

Milestones (all from §5.2.2, p. 313)

1. Lower bound $C^*_{\max}\ge C$.
2. Existence of a decrementing set for every nonzero nonnegative $P$.
3. Positive step: for a decrementing set, the largest $\delta$ satisfying the constraints (1)–(3) of the survey exists and is positive.
4. Step property: after replacing each $p_{ij}\in S$ by $\max\{0,p_{ij}-\delta\}$, the largest line sum is exactly $C-\delta$.
5. Partial schedule: for each $p_{ij}\in S$, $M_i$ processes $J_j$ for $\min\{p_{ij},\delta\}$ time units, with no machine or job used twice.
6. Termination: every run of the procedure reaches $P'=(0)$ within a bounded number of stages.
7. Joining: the concatenated partial schedules form a feasible schedule with $C_{\max}\le C$.

Significance

The result. The theorem turns an optimization over continuous-time schedules into the computation of $m+n$ sums. It certifies optimality by a counting argument, it is the base case for preemptive open shops with release dates and due dates, and it is used elsewhere in the survey (§4.4.6) to reduce problems on unrelated machines with preemption to open-shop instances. Because a nonnegative matrix whose row and column sums are all equal is a multiple of a doubly stochastic matrix, the theorem is a scheduling form of the Birkhoff–von Neumann decomposition. It also underlies timetabling and edge-colouring results for bipartite multigraphs.

Formalizing it. The theorem has been proved since 1976 and is textbook material. No machine-checked proof is known to exist: Mathlib has the Birkhoff–von Neumann theorem for doubly stochastic matrices but no model of open-shop schedules. A formalization adds a reusable model of preemptive multi-machine schedules with both disjointness requirements, a checked proof of the decrementing-set construction, and a termination argument the survey asserts without proof.

Difficulty

The lower bound is a one-line counting argument. The difficulty is the construction of a schedule of length exactly $C$. Scheduling each machine's operations back to back gives length $\max_i\sum_j p_{ij}$, but may run one job on two machines at once. Scheduling job by job has the symmetric defect. A greedy list schedule that only respects both constraints can leave machines idle and overshoot $C$. The construction must keep every tight line busy at every moment while never letting a slack line fall behind. The existence of the decrementing set at each stage is the combinatorial core: it is a Hall-type matching condition, not a local choice. Termination is also not automatic, because a careless choice of step length can produce infinitely many shrinking steps.

Formalization scope

All objects live in the namespace SchedSurvey.OPmtn. Machines and jobs are Fin m and Fin n, both 0-based, and processing times and piece endpoints are real numbers; integer data are a special case. A schedule is a List of pieces. Feasibility requires nonnegative start times, disjointness for pieces sharing a machine or a job (touching intervals allowed), and exactly $p_{ij}$ units of processing for every pair $(i,j)$. Every theorem assumes $p_{ij}\ge 0$.

"$C$ is the maximum" is the predicate IsMaxLoad P C: all line sums are at most $C$ and one equals $C$. The goal is stated in threshold form and mentions no maximum at all. The display defining $C$ on p. 313 prints $\max_i\{\sum_i p_{ij}\}$ for the second term; the following sentence shows it means the row sums $\sum_j p_{ij}$, and the formalization uses those. The hypothesis $T\ge 0$ matters only for $P=0$, where the empty schedule finishes by every $T$.

A trivializing formalization is ruled out: the goal mentions neither decrementing sets nor $\delta$. Its "if" direction asserts that a schedule exists. Feasibility counts work per pair (machine, job), not per job, and forbids a job from running on two machines at once. Without either requirement the statement would be a different and easier theorem.

A complete development needs: list sums of interval lengths over disjoint intervals, the existence of decrementing sets (via Birkhoff–von Neumann, König's theorem or Hall's theorem on the bipartite graph of positive entries), the step and termination lemmas, and concatenation of schedules. The schedule model and the decrementing-set lemma are reusable for other preemptive shop problems. Contributions of alternative proofs of any milestone, for example a direct Hall-theorem proof of the existence of decrementing sets, are welcome.

Selected references

• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• T. Gonzalez, S. Sahni, Open shop scheduling to minimize finish time, Journal of the ACM 23 (1976) 665–679. https://doi.org/10.1145/321978.321985
• E. L. Lawler, J. Labetoulle, On preemptive scheduling of unrelated parallel processors by linear programming, Journal of the ACM 25 (1978) 612–619. https://doi.org/10.1145/322077.322090

Motivation

Shop scheduling asks how to process a set of jobs, each a sequence of tasks on prescribed machines, so that all work is completed as early as possible. The flow shop, in which every job visits the machines in the same order, is the most studied of these models in operations research. For two machines, Johnson's rule (1954) computes a schedule of minimum finish time in $O(n\log n)$ time, and for two machines allowing interruptions (preemption) does not help. Garey, Johnson and Sethi (Math. Oper. Res. 1976) and Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum report BW 43/75, 1975; Ann. Discrete Math. 1977) showed that the non-preemptive problem becomes NP-complete with three machines.

Gonzalez and Sahni (Operations Research, 1978) extended this picture to preemptive schedules. Their Theorem 1 shows that minimizing the finish time of a three-machine flow shop is NP-complete with or without preemption, even when every job has at most two tasks of nonzero length. When every job has only one task the problem is trivial, so this is the simplest NP-complete case of the flow-shop finish-time problem. The result explains why no exact polynomial algorithm is expected and motivates the approximation results in the second half of the same paper.

Timeline:

• 1954: Johnson, two-machine flow shop, optimal non-preemptive rule.
• 1975: Brucker, Lenstra, Rinnooy Kan: non-preemptive three-machine flow shop NP-complete, including the case of two nonzero tasks per job (the paper's Corollary 1, which it says "is also obtained in [1]").
• 1976: Garey, Johnson, Sethi: non-preemptive three-machine flow shop NP-complete even when the problem size is the sum of the task lengths.
• 1978: Gonzalez, Sahni: the preemptive three-machine flow shop is NP-complete, by a reduction from PARTITION that also covers the non-preemptive case with two nonzero tasks per job.

Setting

A flow shop has $m\ge1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ must be processed on $P_j$ for $t_{j,i}\ge 0$ time units, and it can start only after task $j-1$ of the same job is completed. Task times may be zero. The schedule starts at time $0$.

A preemptive schedule gives every task a finite set of pieces $(s,f)$ with $0\le s<f$: the task is processed on its processor during $[s,f)$. Pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$, and every piece of a task starts after every piece of the earlier tasks of the same job has ended. A non-preemptive schedule processes every task in at most one piece. For a schedule $S$, $f_i(S)$ is the time at which job $i$ is completed and the finish time is $\mathrm{FT}(S)=\max_i f_i(S)$.

PARTITION. A multiset $S=\{a_1,\dots,a_n\}$ of nonnegative integers has a partition if some set $u$ of indices satisfies $\sum_{i\in u}a_i=\tfrac12\sum_{i=1}^n a_i$.

The instance FS. With $T=\sum_i a_i$, the flow shop $\mathrm{FS}$ has $m=3$ processors and $n+2$ jobs:

$$t_{\cdot,i}=(a_i,0,a_i)\ (1\le i\le n),\qquad t_{\cdot,n+1}=(T/2,\,T,\,0),\qquad t_{\cdot,n+2}=(0,\,T,\,T/2),$$

and the threshold is $\tau=2T$. Every job has at most two nonzero tasks.

Formalization targets

Goal: Theorem 1 (p. 38)

For every $n$ and every $a_1,\dots,a_n\in\mathbb N$:

$$\mathrm{FS}\ \text{has at most two nonzero tasks per job},$$ $$\big(\exists\,S'\ \text{preemptive},\ \mathrm{FT}(S')\le 2T\big)\iff S\ \text{has a partition},$$ $$\big(\exists\,S'\ \text{non-preemptive},\ \mathrm{FT}(S')\le 2T\big)\iff S\ \text{has a partition}.$$

Milestones

• Lemma 1(a) (p. 39): a partition of $S$ yields a non-preemptive schedule of FS with $\mathrm{FT}=2T$ (Figure 1).
• Observations (i)–(ii) (p. 39): in any preemptive schedule with $\mathrm{FT}\le 2T$, task $t_{1,n+1}$ ends by $T$ and task $t_{3,n+2}$ starts no earlier than $T$.
• Lemma 1(b) (p. 39): if $S$ has no partition, every preemptive schedule of FS has $\mathrm{FT}>2T$.
• Lemma 1 (p. 38): the preemptive equivalence.
• Corollary 1 (p. 39): the non-preemptive equivalence.

Significance

The result. The equivalence shows that a polynomial-time algorithm deciding whether a three-machine flow shop (with two nonzero tasks per job) has a schedule of finish time at most $\tau$, preemptive or not, would decide PARTITION in polynomial time. With membership in NP (the paper's Lemma 2) it gives NP-completeness of both versions. It also marks the boundary with the polynomial cases: $m=2$ (Johnson's rule), and jobs with a single task.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no machine-checked proof of this reduction exists, and the platform has no formal model of preemptive shop schedules. The mission produces one: a piece-based preemptive schedule with zero task times, which subsumes the non-preemptive case, together with the first formal NP-hardness reduction for preemptive flow shops on the platform.

Difficulty

Direction (a) asks for one explicit schedule. Direction (b) must rule out every preemptive schedule of FS, and preemption is exactly what makes this delicate: a task may be split into any finite number of pieces placed anywhere on its processor, so the naive intuition that a failed partition leaves "unusable gaps" is no longer evident, since pieces of different jobs can be interleaved to fill gaps. A correct argument must therefore be an accounting of processor time over the pieces, valid for any number and position of pieces, and it must treat zero-length tasks, which occupy no processor time but still delay the next task of their job. Finally, the non-preemptive equivalence is not a formal consequence of the preemptive one alone: it uses that (a) produces a non-preemptive schedule and that (b) holds for all preemptive schedules, which include the non-preemptive ones.

Formalization scope

• Processors are Fin 3 ($P_1,P_2,P_3$ = 0, 1, 2), jobs of FS are Fin n ⊕ Fin 2 (Sum.inr 0 is job $n+1$, Sum.inr 1 is job $n+2$). Task times are real numbers; the PARTITION data are a : Fin n → ℕ, and "has a partition" is $2\sum_{i\in u}a_i=\sum_i a_i$ in $\mathbb N$.
• A schedule is a Finset of pieces $(s,f)$ per task with the four conditions of the Setting. Non-preemptive means at most one piece per task. Zero tasks have no pieces and occupy no processor time. $f_i(S)$ and $\mathrm{FT}(S)$ are maxima with baseline $0$.
• Explicit constants: $T=\sum_i a_i$, the times $T/2$ and $T$ of jobs $n+1,n+2$, and the threshold $\tau=2T$, as on p. 39. Lemma 1(a) states finish time exactly $2T$, as the paper does.
• Not formalized: "NP-complete", the reducibility relation "$\alpha$", membership in NP (Lemma 2, p. 40) and the polynomial computability of FS from $S$. The paper states Theorem 1, Lemma 1 and Corollary 1 as complexity claims. Their proofs establish the equivalences above for the constructed instance, and those equivalences are what is formalized.
• No trivializing reading is admitted: the statements concern the specific instance FS built from $a$, not an arbitrary flow shop, and the schedule model rules out overlapping pieces and out-of-order tasks while still allowing zero tasks. A sorry-free check confirms that Figure 1 is a valid non-preemptive schedule of FS for $S=\{1,1\}$.
• Reusable beyond this mission: the flow-shop model with preemptive pieces, and PARTITION. Proofs of the milestones and a proof of the goal from them are welcome.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
• P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum report BW 43/75, 1975; Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

A flow shop is the simplest multi-stage production model: every job passes through the same machines in the same order, and the question is how to sequence the work so that everything is finished as early as possible. Gonzalez and Sahni's 1978 paper in Operations Research settled the computational complexity of the preemptive version of this problem, in which a task may be interrupted and resumed later on the same machine. For two machines the optimal finish time is computed by Johnson's rule, and preemption does not help. The paper shows that with three machines the preemptive problem is already NP-complete, and its second result, Theorem 2, strengthens this to NP-completeness in the strong sense: the problem stays hard even when the task times are written in unary.

Strong NP-completeness matters because it rules out a pseudo-polynomial algorithm, one whose running time is polynomial in the sum of the task lengths. The preemptive three-machine flow shop ($F3\mid pmtn\mid C_{\max}$ in later notation) is a standard entry in complexity classifications of scheduling problems, and Theorem 2 is the reference for its status. The paper notes that Garey and Johnson obtained a proof independently.

Timeline. Johnson (1954) solved the two-machine flow shop. Garey, Johnson and Sethi (1976) proved the non-preemptive three-machine flow shop NP-complete in the strong sense. Gonzalez and Sahni (1978) treated the preemptive case: Theorem 1 (ordinary NP-completeness via Partition) and Theorem 2 (strong NP-completeness via 3-Partition), the subject of this mission.

Setting

A flow shop has $m\ge 1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ runs on $P_j$ and takes time $t_{j,i}\ge 0$; zero times are allowed. For each job, task $j\ge 2$ can begin only after task $j-1$ has been completed, and schedules start at time $0$.

A preemptive schedule is given, as in the paper's footnote on p. 40, by finitely many pieces $(s,f)$ per task: the task is processed on its processor during $[s,f)$. Pieces have $0\le s<f$, pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$, and a piece of task $j'$ starts only after every piece of every earlier task $j<j'$ of the same job has ended. A task has no preemption when it is processed in at most one piece; a non-preemptive schedule has no preemption anywhere. The completion time of job $i$ is $f_i(S)$, the end of its last piece, and the finish time is $FT(S)=\max_i f_i(S)$.

3-Partition. An instance $C=(a_1,\dots,a_s,B)$, $s=3t$, consists of a positive integer $B$ and nonnegative integers $a_i$ with $\sum_i a_i=tB$ and $B/4<a_i<B/2$. It has a 3-partition if $\{1,\dots,s\}$ splits into $t$ disjoint sets $L_1,\dots,L_t$, each of three elements with $\sum_{j\in L_k}a_j=B$.

The instance FS. From $C$ the proof of Lemma 4 builds a three-processor flow shop with $s+t+2$ jobs:

• jobs $1,\dots,s$: times $(a_i,\,0,\,a_i)$ on $(P_1,P_2,P_3)$;
• job $s+1$: $(0,\,2B,\,B)$;
• jobs $s+i+1$, $1\le i\le t-2$: $(B,\,2B,\,B)$;
• job $s+t$: $(B,\,2B,\,0)$;
• job $s+t+1$: $(0,\,0,\,B)$;
• job $s+t+2$: $(B,\,0,\,0)$.

Each processor carries total work exactly $2tB$, and the threshold is $\tau=2tB$.

Formalization targets

Goal: Theorem 2, as Lemma 4's equivalence

For every 3-Partition instance $C$ with $t\ge 2$,

$$\exists\,S \text{ preemptive schedule of } FS:\ FT(S)\le 2tB \quad\Longleftrightarrow\quad C \text{ has a 3-partition},$$

and every task time of $FS$ satisfies $t_{j,i}\le 2B$. The second clause records that the instance's numbers are bounded by those of $C$, the reduction's contribution to "the problem size being measured as the sum of the length of the tasks".

Milestones

1. Lemma 3 (p. 40). For a flow shop with $m\ge 1$ processors, every preemptive schedule $S$ can be replaced by a schedule $S'$ with no preemptions on $P_1$ and on $P_m$ and $FT(S')=FT(S)$.
2. Lemma 4(a) (p. 41). If $C$ has a 3-partition, $FS$ has a non-preemptive schedule with $FT\le 2tB$.
3. First step of Lemma 4(b) (pp. 41–42). In every preemptive schedule of $FS$ with $FT\le 2tB$, the jobs among $1,\dots,s$ whose $P_1$ task is completed by time $2B$ have $\sum t_{1,i}=B$.
4. Lemma 4(b) (pp. 41–42). If $C$ has no 3-partition, every preemptive schedule of $FS$ has $FT>2tB$.

Significance

The result. Theorem 2 places the preemptive three-machine flow shop among the strongly NP-hard scheduling problems, so no algorithm polynomial in the number of jobs and the total processing time exists unless P = NP. It also shows that allowing preemption, which makes several single-stage problems (such as $P\mid pmtn\mid C_{\max}$) easy, does not help for three-stage flow shops. Lemma 3, that preemptions on the first and last machines can be removed without changing the finish time, holds for any number of machines and is a reusable structural fact about flow-shop schedules.

Formalizing it. The result is proved on paper, and its proof of the "only if" direction is an informal busy-processor argument repeated window by window. As far as is known, no part of it has a machine-checked proof. A formal development has to make the interval accounting rigorous: why each processor is busy throughout $[0,2tB]$, why exactly $B$ units of element jobs end on $P_1$ by $2B$, and how the argument restarts on $[2B,2tB]$. Lemma 3 needs an exchange argument on piece representations. Both are new for the platform.

Difficulty

The direction "3-partition $\Rightarrow$ schedule" is a direct construction. The hard direction is the converse. Preemption lets any task be split across many intervals, so the usual non-preemptive arguments, which reason about the order in which whole tasks run, do not apply directly. The paper's argument that the window $[0,2B]$ must contain exactly three element jobs of total $B$ on $P_1$ depends on every processor being continuously busy, and turning "otherwise there is idle time" into a precise statement requires a careful account of which jobs are available to each processor at each moment. The induction on windows is then not a literal restriction of the schedule to a smaller instance, because pieces may cross the boundary at $2B$.

Formalization scope

• Times are real numbers; the 3-Partition data are natural numbers cast to $\mathbb R$. Processors are Fin m with $P_1=$ 0; in $FS$, $P_1,P_2,P_3$ are 0, 1, 2.
• The 3-Partition instance is the published ResourceScheduling.Chain.ThreePartition (0-based indices, t parts, b $=B$, Valid, HasSolution), whose definition is the paper's p. 37 problem.
• Preemptive schedules are finite sets of pieces per task; precedence is required between every pair of tasks $j<j'$ of a job, so a zero task occupies no time and does not break the job's order. Finish time is a maximum over jobs with baseline $0$, never an unattained supremum.
• "No preemptions on $P_j$" means at most one piece per task on $P_j$.
• Not formalized: "NP-complete", the reduction symbol $\propto$, "the problem size being measured as the sum of the length of the tasks", and Lemma 2 (membership in NP). The goal states the equivalence Lemma 4 proves for the constructed instance, plus the bound $t_{j,i}\le 2B$ on its task times.
• Added hypothesis: $t\ge 2$. For $t<2$ the paper's job indices $s+1$ and $s+t$ coincide with conflicting times, so the construction is undefined there.
• The first step of Lemma 4(b) is read as: the sum of $t_{1,i}$ over element jobs whose $P_1$ task has completed by time $2B$ equals $B$.
• A trivializing formalization is ruled out: the schedules quantified over are all preemptive schedules of the specific instance $FS(C)$, the threshold $2tB$ is explicit, and the validity conditions $B/4<a_i<B/2$ are kept, so the schedule side cannot match the weaker "partition into $t$ groups of sum $B$".

Contributions welcome: the interval-accounting lemmas (busy processors, work available before a time), Lemma 3's exchange argument, and the schedule of Figure 2.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1):36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, "Strong" NP-Completeness Results: Motivation, Examples, and Implications, Journal of the ACM 25(3):499–508, 1978. https://doi.org/10.1145/322077.322090

Motivation

In a job shop, each job has an ordered list of tasks, and each task must use a specified machine. A production planner may be able to interrupt a task and resume it later, yet still be unable to find a short schedule efficiently. Gonzalez and Sahni studied how the ability to preempt changes the difficulty of minimizing the time at which all jobs are complete. Their 1978 paper establishes complexity results for flow shops and job shops and then examines approximation schedules when exact optimization is difficult (Gonzalez and Sahni, 1978).

This mission concerns the paper's two-machine construction from 3-PARTITION. It is the reduction used for their claim that finding an optimal preemptive or non-preemptive finish-time schedule remains NP-complete when input size is measured by the sum of task lengths. The formal target isolates the decision equivalence proved for the constructed instance. It gives solvers a precise schedule statement to establish without conflating the scheduling theorem with the separate complexity-class argument.

Setting

A 3-PARTITION input $C$ comprises an integer $t\ge0$, a positive integer target $B$, and $s=3t$ positive integer sizes $a_1,\ldots,a_s$. A valid input satisfies

$$\sum_{i=1}^{s}a_i=tB,\qquad B/4<a_i<B/2\quad(1\le i\le s).$$

It has a 3-partition when the $s$ indices can be assigned to $t$ disjoint groups, each containing exactly three indices and having total size $B$. The strict bounds rule out groups of other cardinalities at that sum and are part of the source problem, not a convenience added for formalization. When $t=0$, the input has no sizes or groups and the empty grouping is a solution.

The paper builds a job shop $JS(C)$ with machines $P_1,P_2$ and $s+1$ jobs. For $1\le i\le s$, job $i$ has a task of length $a_i$ on $P_1$, followed by a task of length $a_i$ on $P_2$. The last job, $s+1$, has $2t$ tasks, each of length $B$. Its tasks alternate between the machines, starting on $P_2$. This last order matters: reversing it would produce a different construction. The source gives the decision threshold $\tau=2tB$ (Lemma 7, p. 44).

A non-preemptive schedule gives each task one continuous processing interval. A preemptive schedule may divide an operation into finitely many positive-length intervals. In either case, jobs obey their task order, distinct pieces on the same machine do not overlap, and processing starts at or after time zero. Write $FT(S)$ for the time at which all tasks of schedule $S$ have finished. The paper allows the same job to revisit a machine, as the final job does here.

Formalization targets

Lemma 7: the constructed instance

For every valid $C$, the main goal states both the paper's preemptive equivalence and the non-preemptive form established by its two directions:

$$\begin{aligned} \exists S\text{ preemptive for }JS(C): FT(S)\le2tB &\iff C\text{ has a 3-partition},\\ \exists S\text{ non-preemptive for }JS(C): FT(S)\le2tB &\iff C\text{ has a 3-partition}. \end{aligned}$$

The milestones follow the source's proof text: the schedule supplied by a solution in Lemma 7(a), the timing forced on the final job, the exclusion of short preemptive schedules in Lemma 7(b), and the preemptive equivalence stated in the proof. The final-job milestone describes the occupied time slots of the paper's Figure 4, independently of how many adjacent pieces a formal schedule uses.

Significance

The equivalence transfers the distinction between solvable and unsolvable 3-PARTITION inputs to an exact finish-time threshold in a job shop with only two machines. It also establishes the non-preemptive decision equivalence for this construction, because a solution yields a non-preemptive schedule while an unsolvable input rules out even the more permissive preemptive schedules. These facts supply the scheduling part of the paper's strong NP-completeness claim; membership in NP is handled separately by Lemma 6 (pp. 44–45).

The result is proved in the source paper. The work proposed here is a machine-checked development of its explicit reduction equivalence and the finite-piece scheduling model needed to state it. The milestone theorems expose statements that can be reused when formalizing other preemptive scheduling reductions. The shared job-shop instance and 3-PARTITION input are already published definitions; the particular reduction instance and preemptive schedule predicate are new local definitions.

Difficulty

Preemption makes a task's processing time distributable across intervals. Merely checking that each machine has enough total capacity does not characterize feasible schedules: every job's operations must still occur in order, and pieces of different jobs must avoid one another on each machine. The converse direction must constrain every preemptive schedule that meets the threshold, not only a schedule having the visual pattern in Figure 4. A schedule can also represent one uninterrupted interval as several adjacent pieces, so piece count alone cannot express the source's timing claim.

Formalization scope

Machines are Fin 2, with $P_1$ numbered $0$ and $P_2$ numbered $1$. Jobs are Fin (3t+1); the final job is index $3t$. Its zero-based operation $i$ uses machine $1$ for even $i$ and machine $0$ for odd $i$. The definition uses the published JobShopLTAS.Core.Instance for ordered operations, machines, real processing times, and non-preemptive feasibility. It uses the published ResourceScheduling.Chain.ThreePartition for $t,B,a_i$, validity, and solutions. Those objects have the same conventions as the paper here. The local preemptive model uses finitely many positive-length pieces per task, whose durations sum exactly to that task's processing time. The threshold is the explicit real cast of $2tB$; no real infimum or division by a possibly zero optimum appears.

The goal is specific to the instance the paper constructs from each valid input. A free job-shop instance, a freely chosen schedule, or an extra hypothesis that the input has a solution would erase the reduction's content. Validity carries $B>0$, total $tB$, and both strict bounds on each $a_i$. The case $t=0$ remains in scope: the constructed job has no tasks and its finish-time threshold is zero. All existing tasks have positive length whenever the input is valid, so the published non-preemptive predicate's treatment of zero-length tasks does not affect this mission.

The paper states “3-Partition $\alpha$ preemptive JOFT with $m=2$” and connects it to NP-completeness for preemptive and non-preemptive scheduling when complexity is measured by the sum of task lengths. The Lean theorem states the proof's two decision equivalences with constant $2tB$ and machine count $2$. It does not formalize $\alpha$ as a polynomial-time many-one reduction, the unary task-length measure, NP-completeness, or Lemma 6's NP-membership argument. Contributions that establish the reduction statements, the schedule construction, or general finite-piece scheduling facts are within scope.

Selected references

• Teofilo Gonzalez and Sartaj Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 1978, pp. 36–52. DOI: 10.1287/opre.26.1.36.

Motivation

Flow shops and job shops are the basic models of multi-stage production: every job passes through several machines, and each machine handles one task at a time. Gonzalez and Sahni (Operations Research 26(1), 1978) showed that minimizing the finish time of such shops is NP-complete even with preemption, and then asked how well simple heuristics do. One of the two objectives they study is the mean flow time, the average completion time of the jobs, which measures how long a job spends in the shop on average.

Their Lemma 9 analyses the most natural rule for that objective, shortest processing time first (SPT): process the jobs in order of nondecreasing total work. For a single machine SPT is optimal (Smith 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 76, which the paper cites). Lemma 9 shows that with $m$ processors the same rule loses at most a factor $m$, and the paper's Example 2 shows that the factor $m$ is attained in the limit.

Setting

A job shop has $m\ge1$ processors $P_1,\dots,P_m$ and $n$ jobs. Job $i$ is a finite sequence of tasks; each task names the processor that must process it and a processing time $p\ge0$. The tasks of a job are processed in their order: a task may start only after the job's previous task has completed. A flow shop is the special case in which every job has $m$ tasks and its $k$-th task runs on $P_k$.

A non-preemptive schedule gives every task a start time $s\ge0$; the task then occupies its processor during $[s,s+p)$, and two distinct tasks on one processor never overlap. The finish time $f_i(S)$ of job $i$ in schedule $S$ is the time at which all tasks of job $i$ have been completed, and the mean flow time is

$$\mathrm{MFT}(S)=\frac1n\sum_{i=1}^n f_i(S).$$

An OMFT schedule $S^*$ is a feasible schedule of least mean flow time.

Let $L_i$ be the sum of the task times of job $i$. An SPT order is a listing $\sigma(0),\dots,\sigma(n-1)$ of the jobs with $L_{\sigma(0)}\le\dots\le L_{\sigma(n-1)}$, ties broken arbitrarily. The SPT schedule processes the jobs in that order: each job in turn, each positive-time task starting at the later of the completion of the job's previous task and the latest completion of a task already placed on its processor. A zero-time task completes when its preceding task completes and leaves the processor available.

Formalization targets

Goal: Lemma 9

For every job shop, every SPT order $\sigma$ with SPT schedule $S$, and every feasible non-preemptive schedule $\tau$,

$$\mathrm{MFT}(S)\le m\cdot\mathrm{MFT}(\tau),$$

so that $\mathrm{MFT}(S)/\mathrm{MFT}(S^*)\le m$ for an OMFT schedule $S^*$. A separate item states the same bound for flow shops.

Milestones

The milestones follow the paper's proof of Lemma 9 on p. 47:

1. the SPT schedule is a feasible schedule;
2. the job in position $k$ of the SPT schedule finishes by $\sum_{j\le k}L_{\sigma(j)}$;
3. in any feasible schedule, if $i_1,\dots,i_n$ is the order in which the jobs finish, then $f_{i_k}\ge\sum_{j\le k}L_{i_j}/m$;
4. a prefix sum of any listing of the $L_i$ is at least the corresponding prefix sum of the sorted listing;
5. $\mathrm{MFT}(S^*)\ge\frac1n\sum_{k=1}^n\sum_{j=1}^k L_j/m$.

Significance

Lemma 9 is one of the earliest performance guarantees for a shop-scheduling heuristic under a sum objective. It shows that a rule computable by one sort, $O(n\log n)$ plus a linear pass, is within a factor equal to the number of machines, independently of the number of jobs. This is better than the factor $n$ that Lemma 8 of the same paper gives for an arbitrary busy schedule, whenever $m<n$. Example 2 of the paper shows that the factor cannot be improved for SPT. Lower bounds of the work-per-machine type used here recur in later approximation results for total completion time in shops and on parallel machines.

The result has been proved since 1978. As far as a search of the Prove2Me catalogue shows, it has not been machine-checked. This mission adds a machine-checked statement of the SPT schedule as an algorithm, not as an arbitrary schedule with a property. It also adds the guarantee for job shops with arbitrary task sequences, of which flow shops are a special case.

Difficulty

The arithmetic of the proof is short. The work is in two places. The SPT schedule is a concrete construction, a fold over jobs and tasks that updates processor availability, so the bound on its finish times has to be carried through an invariant of that construction. The lower bound on every feasible schedule needs a packing argument: tasks on one processor that complete by a given time have total length at most that time. That argument is not available in Mathlib in a form that applies here. The tempting shortcut of comparing the two schedules job by job fails: the optimal schedule need not finish jobs in SPT order, so the comparison must go through sums of sorted prefixes.

Formalization scope

• Instance and feasibility. The job data come from the published JobShopLTAS.Core.Instance (jobs Fin n, processors Fin m, tasks Fin (μ j), real processing times $\ge0$). The local IsPaperFeasibleSchedule requires nonnegative starts, in-job order, and no overlap of positive-time tasks on the same processor. Zero-time tasks occupy no processor interval. The paper assumes $m\ge1$, and the scheduling theorems carry that hypothesis.
• Finish time and MFT. $f_i$ is the maximum completion time over the tasks of job $i$, with baseline $0$; MFT divides by $n$, and for $n=0$ both sides are $0$.
• The SPT schedule is the list schedule constructed by the heuristic, for every SPT order, so ties are broken in every possible way. Zero-time tasks do not advance processor availability. It is not "any feasible schedule whose jobs finish in SPT order", a reading under which an optimal schedule would qualify and the goal would be trivial.
• The optimum. The paper's "Let $S^*$ be an OMFT schedule" is stated as "for every feasible non-preemptive schedule $\tau$". This is equivalent and does not assume that an optimum exists.
• Ratios multiplied out. $\mathrm{MFT}(S)/\mathrm{MFT}(S^*)\le m$ is stated as $\mathrm{MFT}(S)\le m\cdot\mathrm{MFT}(\tau)$, and the proof's bounds divided by $m$ are multiplied by $m$. No division by a possibly zero quantity occurs.
• Constants. The only constant is the factor $m$, the number of processors.
• Not formalized. The running time of SPT, the comparison with Lemma 8 and its remark "it is assumed that $m<n$" (not a hypothesis of Lemma 9), and the tightness Example 2.
• Milestones 2 and 4 are stated for every listing $\sigma$ and every pair of listings; they are combinatorial facts about list schedules and sorted sums that are reusable beyond this mission. Proofs of any milestone, and a reusable packing lemma for non-overlapping intervals, are welcome.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106
• K. Jansen, R. Solis-Oba, M. Sviridenko, Makespan Minimization in Job Shops: A Linear Time Approximation Scheme, SIAM J. Discrete Math. 16(2), 288–300, 2003 (source of the job-shop definition reused here). https://doi.org/10.1137/S0895480199363908

Motivation

A flow shop is the simplest model of a production line: every job passes through the same sequence of machines in the same order. Minimizing the time at which the last job leaves the last machine (the finish time, or makespan) is easy for two machines, where Johnson's rule gives an optimal schedule in time $O(n\log n)$ (Johnson 1954), and NP-hard from three machines on (Garey, Johnson, Sethi 1976; Gonzalez, Sahni 1978, §1, for preemptive schedules). For three or more machines the practical question is therefore how far a fast heuristic can be from the optimum in the worst case.

Gonzalez and Sahni (1978, §2) first show that any busy schedule, one that never leaves a processor idle while a task is available for it, has finish time at most $m$ times the optimum (their Lemma 10), and that the natural "longest job first" order does no better. They then give a heuristic, H, that uses Johnson's two-machine algorithm as a subroutine and has the better worst-case ratio $\lceil m/2\rceil$ (Lemma 11). This mission formalizes that bound.

Setting

A flow shop has $m$ processors $P_1,\dots,P_m$ and $n$ jobs. Job $i$ consists of $m$ tasks; task $j$ runs on processor $P_j$ and needs processing time $t_{j,i}\ge 0$ (zero is allowed). A non-preemptive schedule gives every task a start time $s_{j,i}$, and the task occupies $P_j$ during $[s_{j,i},s_{j,i}+t_{j,i})$. It is feasible when all start times are nonnegative, when task $j+1$ of a job starts only after task $j$ of that job has completed ($s_{j,i}+t_{j,i}\le s_{j+1,i}$), and when no processor runs two tasks of positive length at the same time. Its finish time $\mathrm{FT}(s)$ is the latest completion time $s_{j,i}+t_{j,i}$ (and $0$ if there is no task). An optimal finish time (OFT) schedule $S^*$ is a feasible schedule of least finish time.

Heuristic H (p. 48) divides the processors into $\lceil m/2\rceil$ groups: group $g$ consists of $P_{2g-1}$ and $P_{2g}$, and when $m$ is odd the last group is $P_m$ alone. The flow shop $F_g$ on group $g$ has the same jobs, with task times $t_{2g-1,i},t_{2g,i}$ only. For each group an OFT schedule $R(g)$ of $F_g$ is computed (by Johnson's algorithm), with finish time $f(R(g))$. The schedule $S$ generated by H runs these schedules one after another: every task of group $g$ starts at its time in $R(g)$ plus the offset $\sum_{h<g}f(R(h))$.

Formalization targets

Goal: Lemma 11 (p. 49)

For every flow shop with $m$ processors and $n$ jobs, every choice of OFT schedules $R(g)$ of the group flow shops, the schedule $S$ generated by H, and every feasible non-preemptive schedule $\tau$ of the flow shop (in particular an OFT schedule $S^*$),

$$\mathrm{FT}(S)\le\Big\lceil\frac m2\Big\rceil\,\mathrm{FT}(\tau).$$

The paper writes this as $\mathrm{FT}(S)/\mathrm{FT}(S^*)\le\lceil m/2\rceil$.

Milestones

1. Every group flow shop $F_g$ has an OFT schedule (p. 48; the paper obtains it with Johnson's algorithm).
2. The concatenation of feasible group schedules is a feasible schedule of the $m$-processor flow shop (p. 48).
3. $\mathrm{FT}(S^*)\ge\max_g f(R(g))$ (proof of Lemma 11, p. 49).
4. $\mathrm{FT}(S)\le\sum_g f(R(g))\le\lceil m/2\rceil\max_g f(R(g))$ (proof of Lemma 11, p. 49).

Significance

The result gives a polynomial-time heuristic, running in time $O(mn\log n)$, whose finish time is within a factor $\lceil m/2\rceil$ of the optimum on every instance, half the factor $m$ that every busy schedule already achieves. The paper's Example 4 (p. 49) shows that for $m=3$ the factor $2=\lceil 3/2\rceil$ is approached, so the analysis cannot be improved in general.

Formalizing it produces a reusable, machine-checked model of the $m$-processor flow shop with non-preemptive schedules, its restriction to blocks of consecutive processors, and the concatenation of schedules of disjoint blocks. Lemma 11 has a short paper proof; to our knowledge it has no machine-checked proof. The model's careful treatment of zero task times, of odd $m$, and of the restriction of a schedule to a processor group is itself part of the value: these are the points at which an informal argument is silent.

Difficulty

The arithmetic of the bound is short; the content lies in two structural facts about a precise model: that the concatenated object is a feasible schedule of the whole flow shop, including across the boundary between consecutive groups and for a final group of a single processor, and that the optimum of the whole flow shop is at least the optimum of each group flow shop, whose first processor has no predecessor. Informal arguments are silent on exactly these points. A naive formalization that leaves the offsets free, or that does not require the $R(g)$ to be optimal, makes the statement false; one that lets $S$ be any schedule with the right restrictions makes it witnessed by $S^*$ itself.

The existence of OFT schedules for the group flow shops (milestone 1) is a separate matter: the paper takes it from Johnson's algorithm, and proving it requires an optimality argument for two-machine flow shops (or a compactness argument over finitely many processing orders).

Formalization scope

• Representation. Processors are Fin m and jobs Fin n, both 0-based; times are real numbers. A flow shop is a matrix t : Fin m → Fin n → ℝ with t ≥ 0. A schedule is a matrix of start times. Group $g$ (0-based, g : Fin ((m + 1) / 2)) contains the processors $2g$ and $2g+1$ that exist, min 2 (m - 2g) of them.
• Finish time. A fold of max with baseline $0$ over all tasks; it is $0$ for $m=0$ or $n=0$. The maximum of the group finish times is also a fold of max with baseline $0$. No supremum over an unbounded or empty set is taken.
• Zero task times. A zero-length task occupies no processor time (it is exempt from the non-overlap condition) but still respects the job's task order and counts in the finish time when it is placed late; optimal schedules are unaffected.
• The optimum. "OFT schedule $S^*$" is replaced by a universally quantified feasible schedule $\tau$, which is stronger and needs no existence assumption for $S^*$. Optimality of $R(g)$ is the predicate "feasible, and finish time at most that of every feasible schedule of the same group flow shop".
• Constants. $\lceil m/2\rceil$ is (m + 1) / 2 in $\mathbb N$, cast to $\mathbb R$; the two agree for every $m\ge 0$. The ratio is multiplied out, so a zero optimum does not divide by zero.
• Not formalized. Johnson's algorithm and the running times $O(n\log n)$ and $O(mn\log n)$. The goal quantifies over every family of optimal group schedules, which includes the one Johnson's algorithm computes; the paper's proof uses only optimality. The preemptive comparison on p. 50 and the tightness examples are outside the mission.
• Trivialization ruled out. The schedule $S$ is a function of the $R(g)$ with the fixed offsets $\sum_{h<g}f(R(h))$, and each $R(g)$ must be optimal for its group flow shop; neither the offsets nor $S$ are free.
• Infrastructure. Elementary facts about Finset.fold max and sums over Fin; nothing beyond Mathlib. Contributions proving milestone 1 by formalizing Johnson's rule for this model are welcome and reusable.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117

Motivation

In a store-and-forward network, messages are cut into packets that travel from node to node along wires, one wire per time step, and wait in buffers between moves. Routing such traffic splits into two problems: choosing a path for each packet, and scheduling the packets along their paths, deciding at every step which packets move and which wait. Leighton, Maggs and Rao showed that the second problem always has an essentially optimal solution: once paths are fixed, two simple parameters of the paths determine the routing time up to a constant factor, on every network.

The result separates path selection from timing in the design of routing algorithms for parallel machines, and it reaches beyond networks: a job-shop problem in which every operation takes one unit of time and no job visits a machine twice is the same problem with jobs as packets and machines as edges.

Timeline.

• 1988: Leighton, Maggs and Rao, extended abstract at FOCS, Universal packet routing algorithms.
• 1994: the full paper in Combinatorica 14, with the existence theorem of an $O(c+d)$ schedule with constant queues (Theorem 3.4) and a randomized on-line algorithm.
• 1999: Leighton, Maggs and Richa, Fast algorithms for finding O(congestion + dilation) packet routing schedules, make the construction algorithmic, using the algorithmic Local Lemma of Beck.

Setting

A network is a directed multigraph: a type $V$ of nodes, a type $E$ of edges, and maps $\mathrm{src},\mathrm{tgt}:E\to V$. A path is a list of edges $e_0,\dots,e_{\ell-1}$ with $\mathrm{tgt}(e_k)=\mathrm{src}(e_{k+1})$; it is edge-simple if no edge occurs twice. A finite set $P$ of packets is given, each with its path.

The dilation $d$ is the largest number of edges on a path; the congestion $c$ is the largest number of paths through one edge. Since a packet crosses at most one edge per step and an edge carries at most one packet per step, every schedule needs at least $\max(c,d)$ steps.

A schedule assigns to every packet $p$ and every index $k$ of its path the step $\tau(p,k)\ge1$ at which $p$ crosses its $k$-th edge, strictly increasing in $k$. Its length is the last crossing step. A packet waits in its initial queue before its first crossing, in the edge queue at the head of the edge it last crossed between two crossings, and in its final queue after its last crossing. Only edge queues count for queue size: the other two are fixed by the instance. A schedule is valid if at most one packet crosses each edge at each step.

For the proof, the paper measures schedules that are not yet valid through frames: a $T$-frame is a run of $T$ consecutive steps, and the relative congestion of a frame is the largest number of packets crossing one edge in it, divided by $T$.

Formalization targets

Goal: Theorem 3.4 (p. 11)

There are absolute constants $K$ and $Q$ such that every finite set of packets with edge-simple paths of congestion at most $c$ and dilation at most $d$, on any network, has a valid schedule with

$$\text{length}\le K\,(c+d),\qquad \text{every edge queue}\le Q \text{ at every step}.$$

The constants are not fixed: the paper proves existence, and any constants are a valid answer.

Milestones, in the order the proof uses them

1. Lemma 3.1 (p. 8), the Lovász Local Lemma: events of probability at most $p$ with dependence at most $b\ge1$ and $4pb<1$ all fail together with positive probability.
2. Lemma 3.2 (p. 8): with congestion and dilation at most $d$, a schedule of length $O(d)$ with no waiting in edge queues and at most $T$ packets per edge in every frame of size $T\ge\log_2 d$.
3. The recurrences (pp. 12–13): $I^{(1)}=\log d$, $I^{(i+1)}=\log^5 I^{(i)}$, $r^{(1)}=1$, $r^{(i+1)}=r^{(i)}(1+\kappa/\sqrt{\log I^{(i)}})$ stop at some $j=O(\log^* d)$ with $r^{(j)}=O(1)$.
4. Lemma 3.5 (p. 14): frame bounds for all sizes from $T$ to $2T-1$ imply them for all sizes $\ge T$.
5. The final simulation (pp. 12–13): a schedule with relative congestion $O(1)$ in frames of constant size, in which every packet waits at most once every $k_1\ge2$ steps, becomes a valid schedule, a constant factor longer, with constant edge queues.

Significance

The theorem shows that congestion and dilation, two quantities read off the paths alone, determine the optimal schedule length up to a constant factor on every network, with buffers of constant size. Path-selection algorithms that minimize $c+d$ therefore yield near-optimal routing, and the same bound holds for unit-time job shops without repeated machines. It is also an often-cited application of the Local Lemma beyond a single round of random choices: the proof applies it $O(\log^* d)$ times in succession.

The result has been proved since 1994, and the algorithmic version since 1999. As far as is known, no part of it is machine-checked. The mission produces a formal model of store-and-forward schedules with edge queues and frames, a formal statement of the theorem that excludes the degenerate readings, and formal versions of the steps of its proof.

Difficulty

The naive approach gives each packet a random initial delay and then lets it move without waiting. That gives $O(\log(Nd))$ packets per edge per step, and $O(c+d\log(Nd))$ steps after slowing down. Lemma 3.2 does better only in frames of size $\log d$, not in single steps. Recursing on frames, as in Theorem 3.3, loses a constant factor per level and gives $(c+d)2^{O(\log^* (c+d))}$.

Removing that factor is the central difficulty. Each refinement must keep the relative congestion nearly unchanged, $r^{(i+1)}=r^{(i)}(1+O(1)/\sqrt{\log I^{(i)}})$, which requires second-order terms in the tail estimates, delays spread over the block rather than inserted at its start, and careful handling of block boundaries. The constant queue bound needs an invariant: every packet waits at most once every $I^{(i)}$ steps. The Local Lemma gives existence only; the construction is non-constructive.

Formalization scope

Conventions committed to in Lean:

• The network is arbitrary: V E : Type with src tgt : E → V, no finiteness or degree bound. Packets form a Fintype P; paths are List E with matching endpoints (List.IsChain) and List.Nodup.
• Congestion and dilation are bounds (CongestionLE path c, DilationLE path d), equivalent to exact values because every bound is monotone.
• A schedule is a Timetable: time p k : ℕ, the step at which packet p crosses its k-th edge, at least 1 and strictly increasing in k. Length at most L means every crossing step is ≤ L. Valid means two different crossings of one edge happen at different steps.
• The edge-queue size of edge g at the end of step t counts crossings of g at a step ≤ t whose packet crosses its next edge at a step > t. Initial and final queues are not counted.
• Frames: frameCount τ g t T counts the packets that cross g at a step in [t, t+T). Relative congestion at most r in frames of size ≥ T₀ is frameCount ≤ r·T for all T ≥ 1 with T₀ ≤ T.
• log is Real.logb 2. Every O(1) and "sufficiently large" is a constant quantified before the instance, and in the goal ∃ K Q comes before the network.
• Lemma 3.1 is stated on an arbitrary probability space with measurable events. Dependence uses independence from the generated σ-algebra, and the statement adds 1 ≤ b, without which the page's statement is false.

These choices rule out the trivial formalizations: constants chosen after the instance would make $K=cd$ suffice; a schedule without edge exclusivity would make the greedy schedule of length $d$ a solution; a missing queue bound drops half of the theorem; and a statement without its length bound is solved by sending one packet at a time.

Not stated: Lemmas 3.6–3.10 and the summary of the refinement step (p. 20). They concern the block decomposition and delay-insertion rules of pp. 13–14 and 17–18, which the paper defines only in prose. Contributions are welcome on the Local Lemma (finite or general), the probabilistic estimates of Lemma 3.2, Lemma 3.5, the elementary simulation step, and formal definitions of the block operations from which Lemmas 3.6–3.10 can be stated. The schedule model is reusable for other routing results, such as the on-line algorithm of §2 or the $O(c+d)$ results for leveled networks.

Selected references

• F. T. Leighton, B. M. Maggs, S. B. Rao, Packet routing and job-shop scheduling in O(congestion + dilation) steps, Combinatorica 14 (1994) 167–186. https://doi.org/10.1007/BF01215349 (this mission cites the authors' manuscript).
• F. T. Leighton, B. M. Maggs, S. B. Rao, Universal packet routing algorithms, Proc. 29th IEEE FOCS (1988) 256–269.
• F. T. Leighton, B. M. Maggs, A. W. Richa, Fast algorithms for finding O(congestion + dilation) packet routing schedules, Combinatorica 19 (1999) 375–401. https://doi.org/10.1007/s004930050061
• P. Erdős, L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions, in Infinite and Finite Sets, Colloq. Math. Soc. János Bolyai 10 (1975) 609–627.
• J. Spencer, Ten Lectures on the Probabilistic Method, SIAM (1987), pp. 57–58. https://doi.org/10.1137/1.9780898719918

Motivation

A flexible manufacturing system is a set of machines through which parts of several types travel along fixed routes; each machine serves several buffers and must pay a set-up time whenever it switches from one buffer to another. Real-time scheduling decides, as the system evolves, which buffer each machine works on. Perkins and Kumar (IEEE Trans. Automat. Control 34, 1989) introduced simple distributed policies for this problem, of which the most natural is the clearing policy: a machine keeps working on a buffer until it is empty, and only then switches. They proved that every clear-a-fraction policy, a subclass of clearing policies, keeps every buffer bounded on acyclic systems whenever each machine has spare capacity, and left open whether clear-a-fraction policies stabilize all systems in which material flows around cycles.

Kumar and Seidman (IEEE Trans. Automat. Control 35(3), 1990, doi:10.1109/9.50339) answered no. Their Example 1 is a single part type that visits two machines in the order 1, 2, 2, 1. Every machine has spare capacity, yet under the clearing policy the buffer levels grow without bound, and they do so even when all set-up times are zero, so the instability comes from machines starving each other rather than from time lost to set-ups. Until then, instability had been suspected to require positive set-up times. Shortly afterwards Lu and Kumar exhibited instability of a static buffer-priority rule in a re-entrant network (IEEE Trans. Automat. Control 36, 1991); together these examples started the study of stability of multiclass queueing networks.

Setting

A manufacturing system has part types $p$ arriving at rates $d_p > 0$. Parts of type $p$ follow a route of length $n_p$: their $i$-th operation is at machine $\mu_{p,i}$, and they wait for it in buffer $b_{p,i}$, where each part needs processing time $\tau_{p,i} > 0$. Machine $m$ serves the buffers $B_m = \{b : \mu_b = m\}$, and switching from $b$ to $b'$ costs set-up time $\delta_{b,b'} \ge 0$.

Flows are continuous (fluid). The level of buffer $b$ at time $t \ge 0$ is $x_b(t) = x_b(0) + u_b(t) - y_b(t) \ge 0$, where $y_b(t)$ is its cumulative output and $u_b(t)$ its cumulative input: $d_p t$ for the first buffer of a route, and the output of the preceding buffer otherwise. Each machine works in runs: run $k$ is a set-up phase of length $\delta_{\beta_{k-1},\beta_k}$ followed by a processing phase on buffer $\beta_k$, during which the buffer is drained at rate $1/\tau_b$ while it is nonempty and passed through at its inflow rate when it is empty. The system is stable if $\sup_{0 \le t < \infty} x_b(t) < \infty$ for every buffer.

A clearing policy (Definition 1) is one in which a machine processing $b$ continues until the first time that $b$ is empty and some other buffer of the same machine is nonempty, and then commences a set-up for one of the nonempty buffers.

Example 1. One part type arrives at rate $d = 1$ and visits machine 1, machine 2, machine 2 and machine 1; its buffers are $1, 2, 3, 4$, so $B_1 = \{1, 4\}$ and $B_2 = \{2, 3\}$. Processing times are $\tau_1, \dots, \tau_4 > 0$, and $\delta_k$ is the time to set up to buffer $k$. The parameters satisfy the critical condition and the capacity condition

$$\tau_2 + \tau_4 > 1, \qquad \tau_1 + \tau_4 < 1, \qquad \tau_2 + \tau_3 < 1. \tag{3–5}$$

The initial state is $x(0) = (\xi, 0, 0, 0)$, with machine 1 set up for buffer 4 and machine 2 set up for buffer 3. Write

$$\lambda = \frac{\tau_4}{1-\tau_2} > 1, \quad \alpha = \frac{(\tau_4+1)(\delta_1+\delta_2)}{1-\tau_2} + \delta_3(\tau_4+1) + \delta_4, \quad \beta = \frac{\tau_4(\delta_1+\delta_2)}{1-\tau_2} + \tau_4\delta_3 + \delta_4.$$

Formalization targets

Goal: Example 1, both cases

Assume (3)–(5).

1. If $\delta_1, \dots, \delta_4 > 0$, there is $\xi_0$ such that for every $\xi \ge \xi_0$ ($\xi > 0$) a clearing trajectory from $(\xi, 0, 0, 0)$ exists, and every such trajectory has

$$\sup_{0 \le t < \infty} x_1(t) = +\infty.$$

2. If $\delta_1 = \dots = \delta_4 = 0$, the same holds for every $\xi > 0$.

Milestone: the Case 1 cycle map

For $\xi$ large enough, every clearing trajectory from $(\xi, 0, 0, 0)$ reaches, at $T_1 = (\lambda + \tau_2/(1-\tau_2))\xi + \alpha$,

$$x(T_1) = (\lambda\xi + \beta, 0, 0, 0),$$

with machines 1 and 2 again set up for buffers 4 and 3.

Milestone: the Case 2 magnification

With zero set-up times and any $\xi > 0$, every clearing trajectory reaches, at $t_5 = (\tau_2+\tau_4)\xi/(1-\tau_2)$,

$$x(t_5) = (\lambda\xi, 0, 0, 0),$$

with machines 1 and 2 again set up for buffers 4 and 3.

Significance

The example shows that the condition $\rho_m < 1$ on every machine, which is necessary for stability and sufficient for the existence of some stabilizing policy, does not make natural distributed policies stable once material flows around a cycle. The throughput of the line falls to $1/(\tau_2+\tau_4) < 1$ part per unit time although each machine could handle the demand. This motivates the paper's two positive results: sufficient conditions under which clear-a-fraction policies are stable (Theorem 1), and a supervisory mechanism that stabilizes any policy (Theorem 2), which are the subjects of the other missions of this series. The example is also an early instance of the phenomenon later studied as instability of multiclass fluid networks under work-conserving policies.

The paper's argument is a stage-by-stage computation of piecewise linear trajectories. No machine-checked version of it exists. A formal proof has to make precise what the paper leaves to the reader: that the clearing rule determines the trajectory, that the stage formulas are what that trajectory does, and that the cycle can be restarted. The formal model of runs, set-ups and the clearing rule built here is the same as in the other missions of the series.

Difficulty

The arithmetic of each cycle is routine once the trajectory is known. The difficulty is in the universal quantifier: the claim covers every clearing trajectory, and the clearing rule is defined implicitly, through "the first time thereafter" at which a buffer is empty and another one is nonempty. At several switching instants the buffer a machine switches to is empty and only starts to fill at that instant, and with zero set-up times a machine may begin a run at an instant where the switching condition already holds. Showing that each switch happens exactly when the paper says, and that the fluid levels then follow the printed formulas (including the reduced rate of a machine working on an empty buffer), is a uniqueness argument for a hybrid system, not a simulation. The existence half asks for the converse: an explicit trajectory, defined for all time, with infinitely many runs whose start times tend to infinity.

Formalization scope

• Time is real ($t \ge 0$); flows are fluid; there are no transport delays or assembly.
• The system is a general structure (part types Fin P, machines Fin M, buffers ⟨p, i⟩ with i : Fin (n p), paper index $i$ = Lean index $i+1$), instantiated as Example 1 with $d = 1$, route $(1,2,2,1)$, and $\delta_{b,b'} = \delta_{b'}$ for $b \ne b'$; staying on a buffer costs nothing.
• A trajectory is a schedule of runs per machine (possibly finitely many, the last lasting forever), with only finitely many run starts in any bounded interval. Processing obeys a rate cap ($y_b$ grows at most at rate $1/\tau_b$, and only while machine $\mu_b$ is in a processing phase of $b$) and runs at full rate while the buffer is nonempty.
• In Definition 1, a target buffer counts as "nonempty" when it is demanding: positive level, or inflow starting at that instant. The no-early-exit condition is imposed on the open processing interval. Under the literal reading (positive level) or a closed interval, the paper's own trajectories are not clearing, and the goal would hold vacuously; the existence clause in the goal rules out that trivialization.
• "Set up for buffer $b$ at time $T$" means the run in force on $(s_k, s_{k+1}]$.
• Unboundedness is stated for buffer 1: for every $C$ there is $t \ge 0$ with $x_1(t) > C$; "$\xi$ large enough" is $\exists \xi_0, \forall \xi \ge \xi_0$.

Useful contributions include lemmas about fluid trajectories that do not depend on the example (continuity of levels, the pass-through rate on an empty buffer, restarting a trajectory at a run boundary), which also serve the other missions of the series.

Selected references

• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Trans. Automat. Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Trans. Automat. Control 34, 139–148, 1989 (reference [18] of the paper).
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Trans. Automat. Control 36, 1991.

Motivation

In a flow shop every job passes through the same machines in the same order. Choosing the order in which jobs enter the shop so that the last job finishes as early as possible (minimizing the makespan) is one of the oldest problems of scheduling theory. For two machines Johnson (1954) gave an exact sorting rule; for three machines his rule is exact only in special cases, and the general problem was later shown to be NP-hard (Garey, Johnson and Sethi, 1976). Exact methods for three or more machines therefore enumerate sequences, and the question is how to enumerate as few of them as possible.

Ignall and Schrage (1965), at the same time as Lomnicki (Operational Research Quarterly, 1965), introduced branch and bound for the three-machine permutation flow shop. Their lower bound, which adds to the time each machine becomes free the work that remains on it and the least work that must follow on later machines, became the template for the machine-based bounds used in flow-shop branch and bound ever since.

Timeline. 1954: Johnson proves the two-machine rule and shows that for three machines a common job order on all machines loses nothing for the makespan. 1960: Land and Doig introduce branch and bound for integer programs. 1965: Ignall–Schrage and Lomnicki apply it to the three-machine flow shop. 1976: Garey, Johnson and Sethi prove the three-machine makespan problem NP-hard, so exact enumeration with good bounds remains the method for exact solutions.

Setting

There are $n\ge1$ jobs and three machines $A$, $B$, $C$. Job $i$ needs time $a_i$ on $A$, then $b_i$ on $B$, then $c_i$ on $C$. Following Johnson, only permutation schedules are considered: a full sequence is a permutation $\sigma$ of the jobs, processed in that order on all three machines, each operation starting as early as possible. Its makespan is the time machine $C$ finishes the last job.

A node $J_r$ is a partial sequence: an ordered list of $r$ distinct jobs. Its unscheduled set $\bar J_r$ is the set of the other $n-r$ jobs. The attributes $\mathrm{TIMEA}(J_r)$, $\mathrm{TIMEB}(J_r)$, $\mathrm{TIMEC}(J_r)$ are the times at which machines $A$, $B$, $C$ finish the jobs of $J_r$ processed in order. A full sequence begins with $J_r$ when its first $r$ positions are $J_r$. The lower bound of a node with $\bar J_r\neq\emptyset$ is

$$LB(J_r)=\max\Big[\mathrm{TIMEA}(J_r)+\sum_{\bar J_r}a_i+\min_{\bar J_r}(b_i+c_i),\ \mathrm{TIMEB}(J_r)+\sum_{\bar J_r}b_i+\min_{\bar J_r}c_i,\ \mathrm{TIMEC}(J_r)+\sum_{\bar J_r}c_i\Big].$$

The branch-and-bound procedure keeps a list of nodes ranked by $LB$, starting from the root (no job scheduled). At each step it removes the first node, creates one child per unscheduled job by appending that job, and inserts the children ranked into the list, a new node going before old nodes of equal bound. It stops when the first node of the list is terminal, i.e. has scheduled $n-1$ jobs, so that its last job is forced.

Formalization targets

Goal: the stopping rule certifies an optimal sequence

$$\exists k:\ \text{the first node of } \mathrm{run}(k) \text{ is terminal},\qquad\text{and}\qquad \text{first node } P \text{ terminal} \ \Longrightarrow\ \mathrm{makespan}(\sigma_P)\le\mathrm{makespan}(\sigma)\ \ \forall\sigma ,$$

where $\sigma_P$ is $P$ followed by its one unscheduled job. This is the paper's "the problem is solved: that node's sequence is an optimal one" (p. 402), for any real processing times.

Milestones

1. Validity of the bound (p. 401): $LB(J_r)\le\mathrm{makespan}(\sigma)$ for every $\sigma$ beginning with $J_r$, $r<n$.
2. Exactness at depth $n-1$ (general form of an observation on p. 403): for $r=n-1$, $LB(J_{n-1})$ equals the makespan of the completed sequence.
3. Node counts (p. 403): at least $\tfrac12n(n+1)$ nodes are created before stopping, at most $1+n+n(n-1)+\cdots+n!$ are ever created, and the list never holds more than $n!$ nodes.
4. Dominance (pp. 403–404): if $J_r$ and $I_r$ contain the same jobs, $\mathrm{TIMEA}(J_r)=\mathrm{TIMEA}(I_r)$; if also $\mathrm{TIMEB}(J_r)\le\mathrm{TIMEB}(I_r)$ and $\mathrm{TIMEC}(J_r)\le\mathrm{TIMEC}(I_r)$, replacing $I_r$ by $J_r$ at the beginning of any sequence does not increase its makespan, and $LB(J_r)\le LB(I_r)$ (p. 404).
5. The 4-job example (pp. 402–403): the run stops after 6 steps with node 231 first, whose bound 62 is the optimal makespan.
6. The refined bound (p. 409): the strengthened bound used in the paper's computations is still a lower bound.

Significance

The goal is the correctness theorem of the Ignall–Schrage algorithm: best-first search over partial sequences, with a machine-based bound, returns an optimal permutation. Milestone 1 is the bound's validity, which every later machine-based flow-shop bound generalizes; milestone 4 is the dominance rule that justifies discarding nodes; milestone 3 brackets the effort of the search between the best case $\tfrac12n(n+1)$ and full enumeration.

The paper's arguments are short and informal: validity of the bound is asserted with a one-line reason, and optimality at stopping is argued on the example. None of these results has a machine-checked proof. The formalization makes the procedure itself a precise object (list, insertion rule, stopping rule) and turns the paper's claims into statements about it, so that the correctness of the search is proved rather than illustrated.

Difficulty

Each inequality is elementary, but the goal is a statement about an iterated list-manipulating procedure. The obvious argument "the first node has the smallest bound and the bound is valid" needs an invariant that the paper does not state: at every step, every full sequence begins with some node on the list, and the list is sorted. Both must be proved to survive one step of removal and ranked insertion. Termination is likewise not stated: it needs a measure that strictly decreases, for instance the set of nodes that remain to be created, which requires showing that no node is created twice. A tempting shortcut, proving optimality only among the sequences whose nodes were created, is not the theorem.

Formalization scope

Jobs are Fin n (the paper's job $i$ is $i-1$), processing times are arbitrary reals with no sign condition, and full sequences are Equiv.Perm (Fin n). The makespan is the machine-$C$ completion time of Johnson's as-soon-as-possible schedule, taken from the published definition JohnsonFlowShop.ThreeStage.asapSchedule. Nodes are lists of jobs, and the node attributes are the same recursion folded over the list. Minima over $\bar J_r$ are Finset.inf'; on an empty set the auxiliary minimum returns a placeholder $0$ that no statement evaluates.

Explicit readings of the paper's phrases:

• "is a lower bound … for any node that emanates from node $P$" is "$\le$ the makespan of every permutation whose first $r$ positions are $J_r$";
• "a node that has scheduled all $n$ jobs" is read as a node with $n-1$ jobs, whose sequence is completed by the forced last job. The example (stop at node 231 of a 4-job problem), the node counts and the formula for $LB$ all require this reading;
• "the problem is solved: that node's sequence is an optimal one" is termination together with optimality over all $n!$ permutations;
• "cannot be hurt by replacing $I_r$ with $J_r$" compares the completions of $J_r$ and $I_r$ by the same ordering of the remaining jobs;
• children are inserted one at a time in increasing job index, each before every node with an equal bound; this reproduces the paper's LIST table;
• dominance discarding is not part of the procedure in the goal.

A formalization in which the optimality claim ranges only over sequences the run created, or one that asserts optimality without termination, would be trivial or vacuous and is ruled out by the goal's statement.

Not formalized: the reduction from general schedules to permutation schedules (Johnson's Lemma 3, proved on the platform as JohnsonFlowShop.ThreeStage.same_ordering_dominant), the dominance bookkeeping and its percentages, the two-machine mean-completion problem (a separate mission of this series), the computational tables, and the TIMEB/TIMEC columns of the example's LIST table. No platform item treats flow-shop lower bounds or branch and bound over sequences; the nearest branch-and-bound mission, BiconvexProg.BranchBound (Al-Khayyal and Falk), concerns biconvex programs and is unrelated.

The lemmas a solver will want (the invariant of the list, monotonicity of the completion recursion in its start times, validity of the bound) are reusable for the two-machine mission and for any other machine-based bound. Proofs of the milestones, and of the goal from them, are welcome in any order.

Selected references

• E. Ignall and L. Schrage, Application of the branch and bound technique to some flow-shop scheduling problems, Operations Research 13(3), 400–412, 1965. https://doi.org/10.1287/opre.13.3.400
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
• A. H. Land and A. G. Doig, An automatic method of solving discrete programming problems, Econometrica 28(3), 497–520, 1960. https://doi.org/10.2307/1910129
• M. R. Garey, D. S. Johnson and R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117