Combinatorics

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:

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$:

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

An integer program in standard form, $\max c\cdot x$ subject to $Ax=b$, $x\ge 0$, $x$ integer, is easy to state and hard to solve. Its linear programming relaxation is solved by the simplex method, which ends at an optimal basis $B$. The difference between the two problems is the integrality of $x$, and R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2, 451–558, doi:10.1016/0024-3795(69)90017-2) measures that difference with a finite Abelian group. Dropping only the nonnegativity of the basic variables leaves a problem whose feasible set has a simple structure: its convex hull is the corner polyhedron, and its integer points are the solutions of an equation in the group $\mathbb Z^m/B\mathbb Z^m$.

The first section of the paper uses this to explain when the integer program reduces to the group problem. Its asymptotic theorem says that if $b$ lies far enough inside the cone where $B$ is LP-optimal, then an optimal solution of the group problem gives an optimal integer solution. Gomory first proved this in 1965 (On the relation between integer and noninteger solutions to linear programs, PNAS 53, 260–265, doi:10.1073/pnas.53.2.260) by a counting argument on group solutions. The 1969 paper proves it again through the geometry of the corner polyhedron. The vertices of that polyhedron are irreducible, and an irreducible point is small. This is the version formalized here.

Setting

Let $A=(B,N)$ be an integer $m\times(m+n)$ matrix, with $B$ a nonsingular $m\times m$ matrix (the first $m$ columns) and $N$ the $m\times n$ matrix of the remaining columns $N_1,\dots,N_n$. As on p. 452 of the paper, $A$ contains an $m\times m$ unit matrix. Let $b\in\mathbb Z^m$ and $c=(c_B,c_N)\in\mathbb R^{m+n}$. The integer program (2) is

The relative prices are $c_N^*=-c_N+c_BB^{-1}N$, with components $c^*_{m+i}$. $B$ is an optimal LP basis when $B^{-1}b\ge0$ and every $c^*_{m+i}\ge0$.

The group is $\mathcal G=M(I)/M(B)$, where $M(I)=\mathbb Z^m$ and $M(B)$ is the lattice of integer combinations of the columns of $B$. Let $f$ be the quotient map. $\mathcal G$ is finite of order $D=|\det B|$. Let $\mathcal N$ be the set of nonzero elements among $fN_1,\dots,fN_n$, and put $g_0=fb$. The group equation is

and $P(\mathcal G,\mathcal N,g_0)$ is the convex hull of its solutions in $\mathbb R^{\mathcal N}$. A nonnegative integer $t$ is irreducible if any two integer vectors $s,r$ with $0\le s,r\le t$ and $\sum s(g)\cdot g=\sum r(g)\cdot g$ are equal.

The group costs are $c^*(g)=\min_{i:\,fN_i=g}c^*_{m+i}$. Problem (8) minimizes $\sum_g c^*(g)t(g)$ over the solutions of the group equation. A corresponding vertex of a point $t^*$ (Remark 1) is a nonnegative integer $x_N^*$ with three properties: $t^*(g)=\sum_{i:\,fN_i=g}x^*_{m+i}$; at most one positive $x^*_{m+i}$ per group element; and $x^*_{m+i}=0$ when $fN_i=\bar0$. It uses only least cost columns when $x^*_{m+i}>0$ only if $c^*_{m+i}=c^*(fN_i)$.

The cone $K_B=\{y\in\mathbb R^m:B^{-1}y\ge0\}$ is where $B$ is LP-optimal. $K_B(d)$ is the set of its points at Euclidean distance at least $d$ from its frontier, and $l_{\max}$ is the largest Euclidean length of a column $N_i$.

Formalization targets

Goal: THEOREM 4 (p. 462)

If $b\in K_B\bigl(l_{\max}(D-1)\bigr)$, $t^*$ is a vertex of $P(\mathcal G,\mathcal N,fb)$ minimizing (8), and $x_N^*$ is a corresponding vertex using only least cost columns, then

Milestones

1. THEOREM 1 (p. 459): an irreducible $t$ satisfies $\prod_{g\in\mathcal N}(1+t(g))\le|\mathcal G|$.
2. p. 459: $|M(I)/M(B)|=|\det B|$.
3. THEOREM 2 (p. 460): every vertex of $P(\mathcal G,\mathcal N,g_0)$ is an irreducible integer point.
4. Proof of THEOREM 4 (p. 462): an irreducible $t$ has $\sum_g t(g)\le|\mathcal G|-1$.
5. THEOREM 3 (p. 461): a corresponding vertex of a minimizing vertex is optimal for (2) whenever $B^{-1}(b-Nx_N^*)\ge0$.
6. Proof of THEOREM 4: $\|Nx_N^*\|\le l_{\max}(D-1)$.
7. Proof of THEOREM 4: $y\in K_B(d)$ and $\|v\|\le d$ imply $y-v\in K_B$.
8. Display (10), p. 464: the optimal $x^*$ of THEOREM 4 satisfies $\prod_{i=1}^n(1+x^*_{m+i})\le D$.

Significance

THEOREM 4 explains why integer programs with large right-hand sides are often easy. For $b$ outside a band of width $l_{\max}(D-1)$ along the boundary of the cone $K_B$, the integer optimum is the LP solution $B^{-1}b$ plus a correction that depends only on the class of $b$ modulo the lattice of $B$. That correction is periodic in $b$ and can be tabulated once for the $D$ group elements. The vertex form adds a structural statement: the correction can be read off a vertex of the corner polyhedron, so the faces and vertices of corner polyhedra (the subject of the rest of the paper) bear directly on integer programming. Display (10) shows such optimal solutions are small: their nonbasic parts satisfy $\prod(1+x_{m+i})\le D$.

All results here are proved in the paper. None of them is formalized yet. The 1965 version of the asymptotic theorem, posed as THEOREM 1 of the mission on Gomory (1965), is in the same family of statements. Its hypothesis is that the group solution is optimal; here the hypothesis is that it is a vertex of $P(\mathcal G,\mathcal N,g_0)$. Its counting lemma (a short optimal group solution) and its bound $\|Ny\|\le(D-1)l$ have counterparts in milestones 4 and 6.

Difficulty

An optimal solution of the group problem need not be short. Group solutions can be made longer without changing their cost (add a zero-cost cycle), and a long nonbasic part $x_N$ can push $b-Nx_N$ out of the cone $K_B$, making $x_B$ negative. The goal must therefore use the vertex hypothesis. Vertices are irreducible (THEOREM 2), and irreducibility bounds their size through a pigeonhole count in the finite group (THEOREM 1). The formal work is spread across three settings: the convex geometry of the hull of an infinite integer set, the arithmetic of the quotient $\mathbb Z^m/B\mathbb Z^m$ and its order, and the linear algebra connecting $B^{-1}$, the cone $K_B$ and its frontier.

Formalization scope

Vectors on $\mathcal N$ are functions on the subtype of a Finset of the group. Integer solutions are $\mathbb N$-valued, and $P(\mathcal G,\mathcal N,g_0)$ is convexHull ℝ of their real images. THEOREMS 1 and 2 are stated for an arbitrary finite Abelian group and any finite $\mathcal N$ not containing $0$, as in the paper. The integer program uses the basis as the first $m$ columns, Fin m ⊕ Fin n. $B^{-1}$ is the real matrix inverse, and every statement assumes $\det B\ne0$. Optimality of $x$ means feasibility plus $c\cdot y\le c\cdot x$ for every feasible integer $y$; no supremum is taken. The loose phrases of the paper are read as follows.

• "Vertex" means an extreme point.
• "Every vertex is irreducible" means every vertex is the image of an integer solution, and that solution is irreducible.
• "Optimal linear programming basis" means $B^{-1}b\ge0$ and $c^*\ge0$.
• "Corresponding vertex $x^*$ of $P_x(B,N,b)$" means conditions (i)–(iii) of Remark 1, which the paper calls easily verified, taken as the definition.
• "Minimizing (8)" means minimizing over the integer solutions of the group equation.
• "Euclidean distance from the frontier" is explicit: $\sqrt{\sum_k v_k^2}$, frontier in the usual topology, so $K_B(0)=K_B$.

The printed slip on p. 462 ($\sum(1+t^*(g))$ for THEOREM 1's product) is corrected in the Lean. Dropping the vertex hypothesis from the goal is not a valid formalization (the statement becomes false in general), and neither is defining irreducibility with real $r,s$ (THEOREM 1 then fails). The existence of a minimizing vertex, which the paper takes for granted, is not posed.

A complete development needs the finiteness and order of $\mathbb Z^m/B\mathbb Z^m$ (Mathlib's AddSubgroup.index_eq_natAbs_det), extreme points of convex hulls (extremePoints_convexHull_subset), and an argument that a closed cone with $y$ deep inside it contains the ball around $y$. The group-polyhedron definitions and THEOREMS 1–2 apply to any finite Abelian group and are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. https://doi.org/10.1016/0024-3795(69)90017-2
• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Nat. Acad. Sci. USA 53 (1965), 260–265. https://doi.org/10.1073/pnas.53.2.260
• R. E. Gomory, Faces of an integer polyhedron, Proc. Nat. Acad. Sci. USA 57 (1967), 16–18. https://doi.org/10.1073/pnas.57.1.16
• B. L. van der Waerden, Modern Algebra, English translation of the 2nd German edition, Ungar, New York, 1949–1950 (computation of $f$, cited p. 456).

Motivation

Scheduling work on several identical processors creates a plausible expectation: completing tasks sooner, removing constraints, or adding a processor should not delay the overall finish. A fixed priority-list rule defeats that expectation. When a task becomes ready earlier, it can occupy a processor that would otherwise have run another task; that decision changes later availability. Graham gives explicit schedules in which changing only the list raises the finishing time from 12 to 14, removing two precedence constraints raises it to 16, shortening every task raises it to 13, or adding one processor raises it to 15. These examples establish that the effect is a property of the scheduling rule, rather than of a change in the total set of tasks. See Graham, §2, pp. 417–419.

This mission concerns the upper limit of that effect. An operations researcher comparing a list schedule before and after a change in available processors or task data needs a bound that survives all four changes at once. The result is also a compact benchmark for formalizing algorithms whose behavior depends on changing availability: the model must describe when tasks become ready, when processors are idle, and which ready task a processor takes next. Graham's Theorem 1, proved in the 1969 paper, supplies the bound.

Setting

There are $r$ tasks $T_1,\ldots,T_r$ and $n$ identical processors. Each task $T_j$ has a positive processing time $\mu(T_j)$. A strict precedence order $\prec$ specifies tasks that must be completed first: $T_i\prec T_j$ means $T_j$ cannot start before $T_i$ ends. A priority list $L$ orders all tasks once each. It may place a successor before a predecessor, because the processor skips any task that is not ready. These conventions are those of Graham's system in §2, p. 416.

A schedule gives each task a processor and a start time $S_j\ge0$. Once started, the task occupies that processor continuously on $[S_j,S_j+\mu(T_j))$. Two tasks on one processor cannot overlap, while tasks may meet at an endpoint. Precedence means $S_i+\mu(T_i)\le S_j$ whenever $T_i\prec T_j$. The finishing time $\omega$ is the largest completion time $S_j+\mu(T_j)$. The paper's list rule starts the first currently ready task in $L$ whenever a processor can take a task. A ready task that has not started cannot coexist with an idle processor. If one task starts while another ready task waits, the started task is earlier in $L$.

The same task set is run a second time, with processing times $\mu'$, order $\prec'$, list $L'$, processor count $n'$, and finishing time $\omega'$. The data satisfy $\mu'(T_j)\le\mu(T_j)$ for every $j$ and $\prec'\subseteq\prec$. Thus the second run may have shorter tasks and fewer precedence relations; both lists may differ arbitrarily. Both runs obey the same list-scheduling rule Graham, §3, p. 419.

Formalization targets

General anomaly bound

For $r,n,n'\ge1$, positive processing times in both runs, and the two list schedules just described, the target is Graham's Theorem 1:

The numerator and denominator refer to the actual runs, with potentially different lists and processor counts. The conclusion does not require the new schedule to finish earlier. Its factor permits the anomalies shown in §2 while preventing an arbitrarily large increase for fixed $n,n'$. The supporting targets follow the proof's numbered displays: a precedence chain covering idle times in the second run (1), an idle-time estimate for that chain (2), a comparison of its length with the first run (3)–(4), and the work-volume bound used in (5) Graham, pp. 419–420.

Significance

The theorem places a quantitative limit on the damage caused by a list rule after simultaneous changes in task durations, precedence, ordering, and capacity. When $n'=n$, the factor is $2-1/n$; when the first run has one processor, it is $1$. The statement applies to every finite task set and every pair of lists, so it can be reused when a scheduling method produces a list without additional structural guarantees. Graham states that the bound is best possible, citing earlier examples; this mission formalizes the inequality in this paper and does not claim to formalize those external examples Graham, p. 420.

The result is proved in the source paper. The work here is to give its objects precise Lean definitions and to supply machine-checked proofs of the bound and its supporting claims. A formal development needs to account for continuous real start times, processor assignments, half-open execution intervals, and the behavior of the list rule when several tasks or processors become available together. The resulting model of a nonpreemptive list schedule and the basic volume and chain estimates can serve later formalizations of parallel scheduling. The present proposal contains statements and definitions; its theorem bodies are open proof obligations.

Difficulty

Total work alone does not control the anomaly: processors can be idle while precedence keeps available work from starting, and changing precedence can alter which tasks occupy the processors later. A direct comparison of corresponding task completion times between the two runs also fails in Graham's §2 examples. The central difficulty is expressing the second run's idle periods through work on a single precedence chain and then relating that chain to the first run's finishing time. In Lean, the chain and the time intervals must be represented without silently changing endpoint conventions or treating a ready but unstarted task as running.

Formalization scope

Tasks are Fin r and processors are Fin n, with zero-based Lean indices corresponding to Graham's one-based subscripts. Processing times and start times are real. A priority list is a bijection between positions and tasks, so it contains every task exactly once and need not respect precedence. The order is strict. Feasible schedules are nonpreemptive and use half-open running intervals. The finishing time is a finite maximum of completion times; for no tasks it is defined as zero, while the ratio theorem assumes $r>0$ so its denominator is positive. Both processor counts are positive. The strict positivity of both time functions is inherited from the paper's $\mu:T\to(0,\infty)$ convention.

The model captures Graham's rule by no unforced idleness and list priority. It does not encode the smaller-index tie rule for identical processors, since the tie affects only processor labels and not start times or $\omega$. The covering-chain milestone represents Graham's set $B$ as times before $\omega'$ when not all processors are busy; all-idle times before the finish cannot occur under the list rule. The idle-time milestone writes the total duration of empty tasks as $n'\omega'-\sum_j\mu'(T_j)$ using display (5). Natural-number subtraction is not used in the constants: $n-1$ and $n'-1$ are real differences. The companion existence statement and a concrete two-task sanity check rule out a vacuous list-schedule predicate. Contributions can address that existence theorem, the chain construction, interval accounting, the volume bound, and the final ratio.

Selected references

• R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

Motivation

Shop scheduling asks how to sequence jobs that each need processing on several machines. In an open shop, a job's operations may be executed in any order, as in testing stations, repair bays, or classroom and examination timetables, where the order in which a candidate visits the stations is irrelevant. The objective studied here is the makespan $C_{\max}$, the time at which the last operation finishes.

The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) introduced the three-field notation $\alpha|\beta|\gamma$ that the scheduling literature still uses, and classified the complexity of the problems it names. For the open shop, its §5.2.1 presents a simplified exposition of the result of Gonzalez and Sahni (J. ACM 23, 1976): with two machines and no preemption, the obvious lower bound on the makespan is always achieved. The same page records that the three-machine case $O3\|C_{\max}$ is binary NP-hard, so two machines is exactly where the problem is easy.

Timeline. Gonzalez and Sahni (1976) gave the linear-time algorithm for $O2\|C_{\max}$, proved NP-hardness for $O3\|C_{\max}$, and gave a polynomial algorithm for the preemptive problem $O|pmtn|C_{\max}$. Graham et al. (1979, §5.2.1) gave the shorter construction formalized here, and observed (§5.2.2) that it implies preemption brings no advantage for $m = 2$. Lenstra (cited as forthcoming in the survey) showed $O2|r_j|C_{\max}$, $O2|tree|C_{\max}$ and $O\|C_{\max}$ unary NP-hard.

Setting

There are $n$ jobs $J_1, \dots, J_n$ and two machines $M_1$, $M_2$. Job $J_j$ has an operation on $M_1$ of length $a_j \ge 0$ and an operation on $M_2$ of length $b_j \ge 0$. There is no preemption, and every job is available at time $0$. A schedule assigns start times $s_1(j)$ and $s_2(j)$ to the two operations of $J_j$, which then occupy $[s_1(j), s_1(j)+a_j)$ on $M_1$ and $[s_2(j), s_2(j)+b_j)$ on $M_2$.

A schedule is feasible if

1. all start times are nonnegative;
2. each machine processes at most one job at a time: the intervals of distinct jobs on the same machine do not overlap;
3. each job is processed on at most one machine at a time: the two intervals of the same job do not overlap, in either order.

Write $T_1 = \sum_j a_j$ and $T_2 = \sum_j b_j$ for the two machine loads. The survey's construction uses the sets

two distinct jobs $J_r$, $J_l$ with $a_r \ge \max_{J_j \in A} b_j$ and $b_l \ge \max_{J_j \in B} a_j$, and $A' = A - \{J_r, J_l\}$, $B' = B - \{J_r, J_l\}$.

Formalization targets

Goal: the optimal makespan

and the optimum is attained. Formally, for every $T \ge 0$: a feasible schedule completing every operation by $T$ exists if and only if $T_1 \le T$, $T_2 \le T$ and $a_j + b_j \le T$ for all $j$. The goal mentions neither $A$, $B$, $J_r$, $J_l$ nor the case analysis; those are the milestones.

Milestones (in the order of the argument)

1. Two distinct jobs $J_r$, $J_l$ with the required bounds exist when $n \ge 2$.
2. Fig. 5.1: the blocks $B' \cup \{J_l\}$ and $A' \cup \{J_r\}$, with $A'$ and $B'$ in arbitrary order, have feasible staircase schedules without idle time.
3. Fig. 5.2: if $T_1 - a_l \ge T_2 - b_r$, the blocks combine into a feasible schedule of all jobs ending by $T_1 + b_r$.
4. Case (1): if moreover $a_r \le T_2 - b_r$, some feasible schedule has length at most $\max\{T_1, T_2\}$.
5. Case (2): if moreover $a_r > T_2 - b_r$, some feasible schedule has length at most $\max\{T_1, a_r + b_r\}$.
6. The symmetric case $T_1 - a_l < T_2 - b_r$: some feasible schedule has length at most $\max\{T_1, T_2, a_l + b_l\}$.
7. The lower bound: every feasible schedule has $C_{\max} \ge \max\{T_1, T_2, \max_j(a_j + b_j)\}$.

Significance

The result. The theorem gives a closed form for the optimal makespan of a two-machine open shop, together with a linear-time construction of an optimal schedule. The survey uses it immediately: since the bound is also a lower bound for preemptive schedules, $O2|pmtn|C_{\max}$ is solved by the same schedules, so preemption gives no advantage on two machines (§5.2.2). It is the standard example of a shop problem whose trivial lower bound is tight, and the contrast with the binary NP-hard $O3\|C_{\max}$ marks the complexity boundary for nonpreemptive open shops.

Formalizing it. The result is classical and proved on paper; no machine-checked proof is known to exist on this platform. The mission produces a reusable model of nonpreemptive two-machine open-shop schedules with real processing times, a verified lower bound, and a verified constructive argument. Unlike many existence-of-schedule results, the survey's construction is explicit (orders and start times), so it can be formalized directly rather than through an abstract existence argument.

Difficulty

The lower bound is the easy half. The difficulty is the construction: a schedule must meet the bound simultaneously on both machines and for every job. The natural first idea, running every job on $M_1$ then $M_2$ in some order (a flow-shop schedule), fails: Johnson's rule then gives a makespan that can exceed $\max\{T_1, T_2, \max_j(a_j+b_j)\}$, because the open shop needs some job to visit $M_2$ first. The survey's construction moves exactly one job, $J_r$, to the front of $M_2$, and its correctness depends on the choice of $J_r$ and $J_l$ and on the case split on $T_1 - a_l$ versus $T_2 - b_r$. Figures 5.3 and 5.4 are drawn for $T_1 \ge T_2$; in the other subcases the start times shown in the figures need adjustment, and the formal statements of the cases assert lengths rather than the figures' exact start times.

Formalization scope

All declarations live in the namespace SchedSurvey.O2. Jobs are Fin n, 0-based ($J_j$ is index $j-1$). Processing times and start times are real numbers with $a_j, b_j \ge 0$; the survey's integer data are a special case, and every claim of §5.2.1 holds over the reals. A schedule is a pair of start-time functions s₁ s₂ : Fin n → ℝ. Interval non-overlap is s + p ≤ s' ∨ s' + p' ≤ s, so touching intervals are allowed and a zero-length operation occupies nothing. Feasibility (IsFeasible) contains both disjointness constraints of §2.1, the machine constraint and the job constraint, with the two operations of a job in either order. The job constraint is essential: without it the optimum would be $\max\{T_1, T_2\}$ and the goal false.

"Length at most $L$" is CompletesBy a b S L: every operation ends by $L$. Optimality is stated in threshold form, which avoids taking a supremum or infimum over a possibly empty set and is equivalent to "$C^*_{\max}$ equals the maximum and is attained". A maximum over $A$ or $B$ appears as a bound on every member, which is also correct for empty $A$ or $B$. The orders of $A'$ and $B'$ are duplicate-free lists whose members are exactly those sets; back-to-back start times are given by contigStart.

The milestone on the choice of $J_r$, $J_l$ assumes $n \ge 2$, which the page presupposes; the goal does not, and covers $n \le 1$ as well. The lower bound assumes $T \ge 0$, which matters only for $n = 0$.

A trivializing formalization is ruled out: feasibility includes both disjointness constraints and nonnegative start times, the threshold is quantified over all $T \ge 0$, and no constant is fixed.

Contributions welcome: proofs of the lower bound (a sum of disjoint intervals inside $[0, T]$), of the list-based block lemmas, of the case lemmas, and of the goal from them. The interval and back-to-back-schedule lemmas are reusable for other shop problems.

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(4) (1976) 665–679. https://doi.org/10.1145/321978.321985
• S.M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110

Motivation

Parallel processing poses a basic allocation question: given tasks of known lengths and several identical processors, how much time is lost when tasks are assigned by a simple list rule instead of an optimal allocation? The finishing time is the moment the last processor completes its work. For independent tasks, a list rule starts each next task on a processor that becomes free first. Such a rule is easy to execute, but the resulting allocation can be worse than the best partition of tasks among processors. Graham's 1969 paper studies precise worst-case ratios for this model. Its Theorem 3 asks what guarantee follows when the first $k$ tasks of the list are chosen among the longest and scheduled optimally before the remaining tasks are appended.

The paper also notes two endpoints of this family. With $k=0$, the rule is ordinary list scheduling and has ratio at most $2-1/n$. With $k=n$, the $n$ longest tasks can start one per processor, giving ratio at most $3/2-1/(2n)$. Theorem 3 expresses these as instances of one bound, including the integer jump at each multiple of $n$ Graham, pp. 427–428.

Setting

There are $r>0$ independent tasks, indexed by $jin\{0,\ldots,r-1\}$, and $n>0$ identical processors, indexed by $p\in\{0,\ldots,n-1\}$. Task $j$ takes a strictly positive time $\mu_j$. A priority list $L$ contains every task exactly once. Its first $k$ tasks are $k$ of the longest tasks; equal lengths may be ordered either way. As a processor becomes available, it takes the next task in the list. Once started, a task runs without interruption. With no precedence constraints, every unstarted task is ready, so a processor runs its assigned tasks consecutively from time zero.

An assignment $\sigma$ records the processor that executes each task. The load $\ell_p(\sigma)$ of processor $p$ is the sum of its assigned task lengths. The finishing time is the largest load, $\omega(k)=\max_p\ell_p(\sigma)$. For a list assignment, each task is assigned to a processor whose load from earlier list tasks is smallest at that step. If two processors are tied, either can be selected without changing the finishing time. For any assignment $\tau$, let $\omega_k(\tau)$ be the largest load contributed by only the first $k$ list tasks. The algorithm requires its own first $k$ assignments to minimize $\omega_k(\tau)$ over all assignments $\tau$; the remaining tasks may occur in any list order.

Write $\omega_0$ for the smallest finishing time achievable for all $r$ tasks. The paper introduces it as the minimum over possible lists and later describes the same problem as minimizing the largest part sum over partitions of the task lengths Graham, pp. 421, 428. The formalization uses the partition or assignment form of $\omega_0$.

Formalization targets

Theorem 3

For $0\le k\le r$, when the first $k$ longest tasks have an optimal prefix schedule, Graham's bound is

Here $\lfloor k/n\rfloor$ is the greatest integer at most $k/n$. The theorem also says the bound is best possible when $k$ is divisible by $n$ Graham, Theorem 3, p. 427. The equality examples are a separate companion statement in this mission.

Source milestones

The milestones state the finite-volume lower bound on $\omega_0$, the case in which completing all tasks takes no longer than completing the first $k$, and the paper's numbered inequalities (14), (15), and (16). They use $\alpha^*$ for the greatest task length after the first $k$ positions. These are individual mathematical claims from the proof on p. 427, with their original wording and formulas recorded alongside the formal statements.

Significance

The theorem gives a quantitative tradeoff between work spent optimizing a prefix and the worst-case finishing time of the full list. Its denominator is $1+\lfloor k/n\rfloor$, so the guarantee improves when the optimized prefix contains another full processor's worth of long tasks. The example at multiples of $n$ shows that the stated coefficient cannot be uniformly reduced for the algorithm as specified Graham, p. 427.

The result is proved in the paper. This mission's remaining work is a machine-checked proof of its exact statement and the source's intermediate inequalities. The published identical-machine makespan definition is reused, while the list-assignment rule, optimal prefix, and longest-remaining-task quantity are made explicit here. Those definitions can also support later work on list scheduling without precedence constraints. No machine-checked proof of Theorem 3 is claimed by this proposal.

Difficulty

An optimal schedule for the first $k$ long tasks does not make the entire list optimal: short tasks appended later can affect which processor finishes last. A bound based only on average total work ignores this final imbalance; a bound based only on the largest remaining task ignores how many long tasks every assignment must place together. The proof must relate both constraints to one finishing time while preserving the floor $\lfloor k/n\rfloor$. Replacing that floor with the real quotient changes the claim, and allowing an arbitrary prefix arrangement loses the algorithm's required optimality.

Formalization scope

Tasks and processors are finite indexed sets Fin r and Fin n; their zero-based indices correspond to the paper's one-based $T_j$ and $P_i$. Task lengths are positive real numbers, and both $r$ and $n$ are positive. The list is a permutation, not merely a sequence that might omit or repeat a task. The condition $k\le r$ is explicit because choosing $k$ tasks from $r$ requires it; the paper treats $r>k$ inside the proof and the case $k=r$ is covered by the theorem. There is no precedence relation in this mission.

The list rule is a predicate on assignments: each next task goes to a processor with least current load. It omits the paper's smaller-index tie convention, since tied identical processors can be interchanged without changing the finishing time. The first $k$ positions must contain $k$ longest tasks, and their assignment must minimize the prefix finishing time among all assignments of those tasks. Those conditions are part of the goal; the inequalities (14)–(16) are conclusions to establish, not assumptions of the goal. A separate existence statement and a checked concrete instance ensure the list predicate is satisfiable.

All maxima and minima range over finite nonempty processor or assignment sets. The optimum is a minimum over assignments, equivalent to the paper's minimum over lists in the independent-task model. The quantity $\alpha^*$ is the largest duration outside the prefix when $k<r$, and is defined as zero when none remains; statements using it require $k<r$. Division is by $n>0$ and by $\omega_0>0$. Lean's natural-number quotient represents $\lfloor k/n\rfloor$; real subtraction is used for coefficients such as $n-1$. Contributions toward the finite load identities, the optimum-over-lists equivalence, and proofs of the listed bounds are within scope.

Selected references

• R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

Motivation

The cutting stock problem asks how to cut standard stock rolls of length $L$ into pieces of demanded lengths $l_1,\dots,l_m$ so that the demands are met at least cost. Gilmore and Gomory solved its linear programming relaxation by column generation (Part I, Opns. Res. 9 (1961)): every cutting pattern is a column, and the column to bring into the basis is found by solving an integer knapsack problem whose objective is given by the current dual prices. In Part II (Opns. Res. 11 (1963)) they replaced the dynamic-programming knapsack solver of Part I by a lexicographic enumeration with a bound test, the Knapsack Method, and reported it to be about five times as fast as dynamic programming on their problem set (p. 866). The method is an early enumeration-with-bounds (branch-and-bound type) procedure for the integer knapsack, and the same pricing problem remains the inner loop of column generation for cutting stock, bin packing and their many variants.

Setting

There are $m$ demanded lengths $l_1,\dots,l_m>0$ with linear programming prices $b_1,\dots,b_m\ge0$, and $k$ standard stock lengths $L_1,\dots,L_k$ with costs $c_1,\dots,c_k$. A column for $L_j$ is a vector $(\alpha)_m=(a_1,\dots,a_m)$ of nonnegative integers with $\sum_i l_ia_i\le L_j$. The knapsack problem (1) for $L_j$ is

and the quantity to compute is $M_j=\max(c_j,\bar M_j)$: a column improves the linear program exactly when $\bar M_j>c_j$.

For a prefix $(\alpha)_s=(a_1,\dots,a_s)$ write $\lambda\cdot(\alpha)_s=\sum_{i\le s}l_ia_i$ and $\beta\cdot(\alpha)_s=\sum_{i\le s}b_ia_i$. Step (1) sorts the data, $b_1/l_1\ge\dots\ge b_m/l_m$ and $L_1>\dots>L_k$, and appends a slack item $a_{m+1}$ with $b_{m+1}=0$, $l_{m+1}=1$. The method then generates vectors in decreasing lexicographic order:

• Steps (2) and (7) fill the coefficients after a prefix greedily, $a_i=[(L-\text{used})/l_i]$, for $L=L_1$ at the start and $L=L_t$ later.
• Step (3) records $\beta\cdot(\alpha)_m$ as the new $M_j$ for each $j\ge t$ with $L_j\ge\lambda\cdot(\alpha)_m$ and $\beta\cdot(\alpha)_m>M_j$.
• Step (4) finds the last nonzero coefficient $a_s$.
• Step (5) lowers $a_s$ by one and looks for the smallest $j$ with $L_j\ge\lambda\cdot(\alpha)_s$ and $(L_j-\lambda\cdot(\alpha)_s)b_{s+1}>(M_j-\beta\cdot(\alpha)_s)l_{s+1}$. This is the bound obtained by relaxing the integrality of $a_{s+1}$.
• Step (6) backs up to the previous nonzero coefficient when no such $j$ exists, and stops when there is none.