Combinatorics

Motivation

Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: $n$ items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.

The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.

Timeline.

• 1954: Johnson proves the two-machine rule (Theorem 1) and, for three machines, the reduction to a common ordering (Lemma 3), a closed form for the elapsed time, and optimality of the rule on $A_i + B_i$, $B_i + C_i$ when $\min A_i \ge \max B_j$ (Theorem 2), with the mirror case $\min C_i \ge \max B_j$ asserted.
• 1976: Garey, Johnson and Sethi show that minimizing makespan in a three-machine flow shop is strongly NP-hard in general, so some restriction of Theorem 2's kind is unavoidable for an exact ordering rule.

Setting

There are $n$ items and three machines. Item $i$ needs processing time $A_i > 0$ on machine 1, $B_i > 0$ on machine 2 and $C_i > 0$ on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.

A schedule assigns each item start times $s^1_i, s^2_i, s^3_i$. It is feasible when all start times are at least $0$ on machine 1, the processing intervals of distinct items on the same machine do not overlap, and $s^1_i + A_i \le s^2_i$, $s^2_i + B_i \le s^3_i$. The three machines may process the items in different orders. The total elapsed time (makespan) is $\max_i (s^3_i + C_i)$.

An ordering $\sigma$ lists the items, $\sigma(k)$ being the item in position $k$. Its as-soon-as-possible schedule processes the items in the order $\sigma$ on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions $1, \dots, n$, Johnson defines

$$K_u = \sum_{i=1}^{u} A_i - \sum_{i=1}^{u-1} B_i, \qquad H_v = \sum_{i=1}^{v} B_i - \sum_{i=1}^{v-1} C_i,$$

the sums running over the items in the first $u$ (resp. $v$) positions.

Johnson's three-stage rule says that item $i$ definitely precedes item $j$ when

$$\min(A_i + B_i,\ C_j + B_j) < \min(A_j + B_j,\ C_i + B_i) \tag{IV}$$

and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.

Formalization targets

Goal: Theorem 2 (p. 67)

If every $A_i$ is at least every $B_j$, then an ordering consistent with (IV) exists, and for every such ordering $\sigma$ the as-soon-as-possible schedule of $\sigma$ is feasible and satisfies

$$\operatorname{makespan}(\text{as-soon-as-possible schedule of } \sigma) \le \operatorname{makespan}(s) \quad \text{for every feasible schedule } s .$$

Milestones

1. Lemma 3 (p. 65). Every feasible schedule is matched or beaten by the as-soon-as-possible schedule of some single ordering.
2. Closed form (p. 66). For every ordering, the total idle time of machine 3 is $\sum_i Y_i = \max_{1 \le u \le v \le n}(H_v + K_u)$, so that

$$\operatorname{makespan} = \sum_{i=1}^{n} C_i + \max_{1 \le u \le v \le n} (K_u + H_v),$$

the "maximum walk" of p. 68. 3. Special case (p. 67). If $\min A_i \ge \max B_j$ then $\max_{u \le v} K_u = K_v$, so the makespan is $\sum_i C_i + \max_v (H_v + K_v)$. 4. (III) $\Leftrightarrow$ (IV) (p. 67). Interchanging the items in positions $j, j+1$ changes $H$ and $K$ only at $j, j+1$, and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every $C_i$ is at least every $B_j$.

Significance

The result. Theorem 2 gives an $O(n \log n)$ exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.

Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).

Difficulty

The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves $\max_{u \le v}(H_v + K_u)$, and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis $\min A \ge \max B$ is what makes $K$ nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.

Formalization scope

Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with $0$, so the empty instance has makespan $0$. An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's $K_{u+1}$, $H_{v+1}$. Statements with maxima over positions assume $n \ge 1$.

Hypotheses made explicit or corrected:

• $\min A_i \ge \max B_i$ is read globally, $B_j \le A_i$ for all $i, j$, as in the section heading. The pointwise reading $B_i \le A_i$ makes Theorem 2 false (an instance with five items is recorded in the Formalization Note of the goal).
• Consistency with (IV) is required for all pairs of positions, not only adjacent ones.
• Lemma 4 carries Lemma 2's exception for an item indifferent to both others; without it the statement is false.
• Lemma 3's proof cites "Lemma 2" where Lemma 1 is meant.
• The interchange equivalence (milestone 4) is stated for arbitrary reals, which is stronger than the page needs.

Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form $\sum C + \max(K_u + H_v)$, would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.

A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.

Selected references

• 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

A b-matching with upper bounds in a graph $G=(V,E)$ assigns a nonnegative integer $x_e\le d_e$ to every edge so that the edges at each node $i$ carry at most $b_i$ in total. Maximizing a linear objective over such assignments is an integer program that contains ordinary matching ($b\equiv 1$, $d\equiv 1$) and appears in assignment, transportation and scheduling models with capacities on both nodes and arcs. Edmonds and Johnson showed that the integer hull of this system is described by adding the blossom (matching) inequalities to the linear relaxation (Edmonds–Johnson 1970; cited in the paper as [8], [13]). There are exponentially many blossom inequalities, so a cutting-plane method needs a separation procedure: given a fractional point $\bar x$, find a violated blossom inequality or certify that none exists.

M. W. Padberg and M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7 (1982), gave this procedure. Section 1 of the paper computes a minimum-capacity cut with an odd number of odd-labelled nodes in polynomial time; Sections 2 and 3 reduce blossom separation to that computation. This mission formalizes Section 3, the case with upper bounds $d$. The companion mission Odd Minimum Cut-Sets and b-Matchings 1 formalizes Section 1.

Timeline: Edmonds (1965) describes the perfect matching polytope; Edmonds and Johnson (1970) extend the description to capacitated $b$-matching; Gomory and Hu (1961) give the cut-tree that Section 1 of Padberg–Rao relies on; Padberg and Rao (1982) reduce separation to odd minimum cuts. Later work (Letchford, Reinelt and Theis, 2008) shortened the resulting algorithms; the reduction itself is the one stated here.

Setting

Let $G=(V,E)$ be a finite simple undirected graph, $b\in\mathbb Z_{>0}^V$ and $d\in\mathbb Z_{>0}^E$. The system is

$$Ax\le b,\qquad x\le d,\qquad x\ge 0, \tag{3.1}$$

with $A$ the node–edge incidence matrix. For $W\subseteq V$ write $E(W)$ for the edges with both ends in $W$ and $(W:V-W)$ for the cut-set of $W$, the edges with exactly one end in $W$. For $T\subseteq (W:V-W)$ with $b(W)+d(T)=\sum_{i\in W}b_i+\sum_{e\in T}d_e$ odd, the blossom inequality is

$$x(W)+x(T)=\sum_{e\in E(W)}x_e+\sum_{e\in T}x_e\le \tfrac12\bigl(b(W)+d(T)-1\bigr). \tag{3.3}$$

Let $\bar x$ be a real point feasible for (3.1) and $\bar s=b-A\bar x$ its node slacks. Let $E(\bar x)$ be the edges with $\bar x_e>0$. The labelled weighted graph $G(\bar x,d)$ has nodes $V$, a special node $S$, and one new node $i_e$ for each $e\in E(\bar x)$. For each such edge $e=[i,j]$, where $i$ is the end the construction scans first, it has an edge $[i,i_e]$ of weight $d_e-\bar x_e$ and an edge $[i_e,j]$ of weight $\bar x_e$. Each $i\in V$ is joined to $S$ with weight $\bar s_i$. There are no other edges. A node $i_e$ is odd iff $d_e$ is odd; $S$ is odd iff $b(V)$ is odd; a node $i\in V$ is odd iff $b_i$ plus the $d_e$ of the subdivided edges scanned from $i$ is odd. A node set $U$ is odd when it contains an odd number of odd nodes, and $\bar y(U:\tilde V-U)$ denotes the total weight of the edges leaving $U$ (its cut capacity).

Formalization targets

Goal: Theorem 3.1

For every feasible $\bar x$ and every scan order,

$$\exists\,W\subseteq V,\ T\subseteq (W:V-W):\ b(W)+d(T)\text{ odd},\ \bar x(W)+\bar x(T)>\tfrac12\bigl(b(W)+d(T)-1\bigr)$$ $$\Longleftrightarrow\quad \exists\,U\subseteq \tilde V \text{ odd}:\ \bar y(U:\tilde V-U)<1 .$$

The paper's closing sentence, that $W$ and $T$ can be obtained constructively from the proof of Lemma 3.2, describes the proof and is not part of the formal statement.

Milestones

1. Eq. (3.6): $2x(W)+x(W:V-W)+x(T)+s(W)+t(T)=b(W)+d(T)$ for $T\subseteq(W:V-W)$, with $t=d-x$.
2. Eq. (3.7): $\bar x$ violates (3.3) for $(W,T)$ iff $\bar x(W:V-W)+d(T)-2\bar x(T)+\bar s(W)<1$.
3. Lemma 3.1: if $T\subseteq (W:V-W)\cap E(\bar x)$ and $b(W)+d(T)$ is odd, some odd $U$ with $S\notin U$ has $\bar y(U:\tilde V-U)$ equal to the left side of (3.7) (Eq. (3.8)).
4. Lemma 3.2: every odd $U$ with $S\notin U$ and capacity $<1$ arises this way from some $(W,T)$ with $b(W)+d(T)$ odd.

Significance

Theorem 3.1 is what makes the blossom inequalities of capacitated $b$-matching usable in a linear-programming based cutting-plane method: combined with the odd minimum cut algorithm of Section 1, it separates them in polynomial time. By the equivalence of separation and optimization, it also yields a polynomial-time algorithm for capacitated $b$-matching through the ellipsoid method. The paper notes the further consequence that every odd cut-set of capacity less than one, not only a minimum one, gives a violated inequality.

The results are proved in the 1982 paper; none of them has a machine-checked proof that this mission is aware of. What the mission adds is a formal statement of the graph $G(\bar x,d)$ and of the reduction, and a checked proof of it. The definitions of the capacitated $b$-matching system, its blossom inequalities and the subdivided graph are reusable for later work on matching polytopes and on the uncapacitated case of Section 2.

Difficulty

The identities (3.6) and (3.7) are bookkeeping over incidences. The substance is the correspondence between node sets $W$ with complemented edge sets $T$ and odd node sets $U$ of $G(\bar x,d)$. In one direction the right $U$ must pick, for every cut edge, the side of $i_e$ that makes the edge contribute $\bar x_e$ or $d_e-\bar x_e$ as (3.7) requires, and its parity must be computed through the orientation-dependent labels. In the other direction an arbitrary odd cut of capacity below one must be shown to have this shape; this uses $d_e\ge 1$ to exclude every other position of a new node $i_e$, and it uses the evenness of the total label to pass from an odd set containing $S$ to its complement. A point $\bar x$ whose blossom violation uses an edge $e\in T$ with $\bar x_e=0$ has no new node for $e$. Such a $T$ has to be ruled out, and the argument uses the capacity bound. It is not an assumption of the theorem.

Formalization scope

The graph is a Mathlib SimpleGraph V on a finite type with decidable adjacency; edges are elements of G.edgeFinset : Finset (Sym2 V). The data are b : V → ℕ and d : Sym2 V → ℕ, positive on nodes and on edges, and a real point x : Sym2 V → ℝ. Feasibility means the linear relaxation of (3.1); integrality of $\bar x$ is not assumed. All halves and differences are computed in ℝ. When $W=V$ the cut-set is empty, so the paper's convention "$T$ is empty" holds automatically.

$G(\bar x,d)$ is fixed by definitions from $(G,b,d,\bar x)$ and an orientation tail choosing the end of each edge scanned first; every theorem quantifies over the orientation. The node type is Option V ⊕ {e // e ∈ E(x̄)}, with none the special node $S$. Weights are a symmetric function on nodes with $0$ meaning "no edge". The labels are given in closed form. The paper assigns them by a sequential scan that flips the parity of the scanned end by $d_e$, and addition mod 2 does not depend on the order of the scan. "The cut capacity of an odd minimum cut-set is less than one" is stated as "some odd cut has capacity less than one"; the two agree, and the formulation avoids a minimum over a possibly empty family.

Two trivializing formalizations are ruled out: $G(\bar x,d)$ is constructed, not an arbitrary labelled graph assumed to satisfy (3.8); and no infimum over odd cuts is taken, since a real sInf of an empty family is $0$ and would make the right side true when no odd cut exists.

Contributions welcome: proofs of the milestones, lemmas on cut capacities of symmetric weight functions on finite types, and parity bookkeeping for labelled node sets.

Selected references

• M. W. Padberg, M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7(1), 67–80, 1982. https://doi.org/10.1287/moor.7.1.67
• J. Edmonds, E. L. Johnson, Matching: a well-solved class of integer linear programs, in Combinatorial Structures and Their Applications, Gordon and Breach, 89–92, 1970; reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, 27–30, 2003. https://doi.org/10.1007/3-540-36478-1_3
• R. E. Gomory, T. C. Hu, Multi-terminal network flows, Journal of the SIAM 9(4), 551–570, 1961. https://doi.org/10.1137/0109047
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
• A. N. Letchford, G. Reinelt, D. O. Theis, Odd minimum cut sets and b-matchings revisited, SIAM Journal on Discrete Mathematics 22(4), 1480–1487, 2008. https://doi.org/10.1137/060664793

Motivation

Edmonds showed that the convex hull of the matchings of a graph is described by the degree constraints together with the blossom inequalities, one for every odd set of nodes (Edmonds 1965). There are exponentially many of them, so any cutting-plane method for matching and b-matching problems must answer a separation question: given a fractional point, find a violated blossom inequality or certify that none exists. Padberg and Rao (1982) reduced this question to a purely graph-theoretic one, the odd minimum cut-set problem, and solved that problem in polynomial time with a single Gomory–Hu computation. The same subroutine underlies separation for many other odd-set constraints (for example the 2-matching and comb-type constraints of the travelling salesman polytope), and later work refined its running time (Letchford, Reinelt and Theis 2008).

This mission covers Section 1 of the paper: the combinatorial theorem about odd cuts, independent of matchings. A companion mission covers the reduction from capacitated b-matching separation (Section 3).

Setting

Let $G = (V, E)$ be a finite undirected graph without loops and multiple edges, with edge weights $c_e \ge 0$. Write $c_{ij}$ for the weight of the edge $[i, j]$, with $c_{ij} = c_{ji}$, and $c_{ij} = 0$ if there is no such edge. For $W \subseteq V$ the cut-set $(W : V - W)$ is the set of edges with exactly one end in $W$, and its capacity is

$$c(W : V - W) = \sum_{i \in W} \sum_{j \in V - W} c_{ij}.$$

A nonempty set $V_1 \subseteq V$ of nodes is labelled odd, the rest even. For $U \subseteq V$ the label $\lambda(U)$ is odd if $|U \cap V_1|$ is odd, and even otherwise; $\lambda(\emptyset)$ is even. The paper assumes throughout that $\lambda(V)$ is even, i.e. $|V_1|$ is even. A cut-set $(U : V - U)$ is odd if $\lambda(U)$ is odd, and an odd minimum cut-set is a solution $X$ of

$$c(X : V - X) = \min\{ c(U : V - U) : U \subseteq V,\ \lambda(U) \text{ odd} \}. \qquad (1.1)$$

A cut-set $(M : V - M)$ is a minimum cut-set with respect to all pairs of odd nodes if it separates two odd nodes and no cut-set separating two odd nodes has smaller capacity.

A cut-tree $G_T = (N, F)$ for the odd nodes is the output of the Gomory–Hu algorithm applied to all pairs of odd nodes (Gomory and Hu 1961). Each tree node contains exactly one odd node and possibly some even ones, so $N$ is identified with $V_1$, and each node $v$ of $G$ belongs to one tree node $\pi(v)$. Removing a tree edge $f = [r, s]$ splits $G_T$ into two subtrees; the nodes of $G$ in the tree nodes of the $r$-side subtree form a set $M$, and the weight of $f$ is $d_f = c(M : V - M)$. The defining property (Hu, Theorem 9.2) is that for every tree edge $f = [r, s]$ the cut-set $(M : V - M)$ is a minimum cut-set of $G$ separating $r$ and $s$. The cardinality of a subtree is its number of tree nodes.

Formalization targets

Goal: Theorem 1.1 (p. 70)

For every cut-tree $G_T$ of $G$ for the odd nodes:

1. some edge of $G_T$ decomposes it into two subtrees of odd cardinality; and
2. if $f^* = [r, s]$ is such an edge of minimum weight among all such edges, and $M$ is the $r$-side shore of $f^*$, then

$$c(M : V - M) = \min\{ c(U : V - U) : U \subseteq V,\ \lambda(U) \text{ odd} \}.$$

Because $|N| = |V_1|$ is even, the two subtrees have the same parity, so the condition is checked on one side.

Milestones

• Lemma 1.1 (p. 68). If $(M : V - M)$ is a minimum cut-set with respect to all pairs of odd nodes, there is an odd minimum cut-set $(X : V - X)$ with $X \subseteq M$ or $X \subseteq V - M$.
• Section 1, p. 70. If $f^*$ has minimum weight among all edges of $G_T$, its shore $M$ gives a minimum cut-set with respect to all pairs of odd nodes.

Significance

Theorem 1.1 turns problem (1.1), a minimization over exponentially many odd sets, into $|V_1| - 1$ maximum-flow computations followed by a scan of the tree edges. Combined with Section 3 of the paper, this gives a polynomial separation algorithm for the blossom inequalities of b-matching polytopes, and hence, by the equivalence of separation and optimization, a polynomial-time route to weighted b-matching through linear programming. The odd-cut routine is also used for separating the odd-set constraints of other polytopes.

The theorem has been proved since 1982 and is textbook material. What this mission adds is a machine-checked proof on a precise encoding of cut-trees. As far as the platform's corpus shows, neither the Gomory–Hu cut-tree property nor any odd-cut theorem has been formalized in Lean; Mathlib has trees and reachability in simple graphs but no cut-tree theory.

Difficulty

The obvious argument fails at the minimum. Every tree-edge shore separates two odd nodes, so a minimum-weight odd-splitting edge certainly yields an odd cut, but showing that no odd set $U$, however it cuts across the tree nodes, has smaller capacity requires relating an arbitrary odd $U$ to a tree edge whose shore is also odd and whose endpoints $U$ separates. The cut-tree only certifies minimality for cuts separating the two ends of a tree edge; an odd set $U$ may split many tree nodes and cross many shores at once, and nothing in the cut-tree property speaks about parity. Parity bookkeeping between odd labels in $G$ and odd cardinality of subtrees is the other place where care is needed: the two notions agree only because each tree node holds exactly one odd node.

Formalization scope

The graph is a weight function c : V → V → ℝ on a Fintype V, with hypotheses that it is symmetric and nonnegative; a missing edge has weight 0 and the diagonal never enters a cut. Node sets are Finset V and $V - W$ is the complement Wᶜ. The odd nodes form a Finset odd with odd.Nonempty and Even odd.card on every statement. The cut-tree is a SimpleGraph on the subtype {v // v ∈ odd} together with a map π : V → {v // v ∈ odd}; IsOddCutTree requires that the graph is a tree, that π fixes every odd node, and the Gomory–Hu minimality for every tree edge. The tree-edge weight $d_f$ is computed from the shore, not supplied as data. Minimality is always stated as ≤ against every competitor; no real infimum is taken.

The existence of a cut-tree (the Gomory–Hu theorem) is a hypothesis-side object and is not part of this mission; the theorems hold for every tree satisfying the cut-tree property. A statement in which the cut-tree assumption already says that the chosen edge's shore is an odd minimum cut, or in which "odd minimum cut" is minimized only over tree-edge shores, would make Theorem 1.1 definitional; both are ruled out, since IsOddMinCut ranges over every node set with odd label.

A complete development needs: submodularity-type identities for cut capacities (reusable for any cut problem), the structure of fundamental cuts of a tree (the two sides of a removed edge are complementary and the parities of $U \cap V_1$ along tree edges combine), and Lemma 1.1. Proofs of the milestones, alternative arguments for the goal that avoid the recursion, and a formal Gomory–Hu existence theorem are all welcome contributions.

Selected references

• M. W. Padberg and M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7(1), 67–80, 1982. https://doi.org/10.1287/moor.7.1.67
• R. E. Gomory and T. C. Hu, Multi-Terminal Network Flows, Journal of the SIAM 9(4), 551–570, 1961. https://doi.org/10.1137/0109047
• T. C. Hu, Integer Programming and Network Flows, Addison-Wesley, 1969 (Chapter 9, Theorem 9.2).
• J. Edmonds, Maximum Matching and a Polyhedron with 0,1-Vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
• A. N. Letchford, G. Reinelt and D. O. Theis, Odd Minimum Cut Sets and b-Matchings Revisited, SIAM Journal on Discrete Mathematics 22(4), 1480–1487, 2008. https://doi.org/10.1137/060664793

Motivation

The capacitated vehicle routing problem (CVRP) asks for minimum-cost routes, starting and ending at a depot, that serve every customer exactly once without any vehicle carrying more than its capacity. It is one of the central problems of operations research and logistics, and exact algorithms for it have been built on branch-and-cut for three decades: a linear programming relaxation is strengthened at every node of a search tree by adding valid inequalities that the current LP solution violates.

The most important of these inequalities are the capacity inequalities. Deciding whether an LP solution violates one of them is strongly NP-hard, so practical codes rely on heuristics, and most heuristics first shrink the support graph: groups of customers are contracted into single supervertices so that the search runs on a smaller graph. Shrinking is only useful if it is safe, meaning it cannot hide a violated inequality. Before the work of Lysgaard, Letchford and Eglese, the standard safe rule allowed shrinking a single edge whose LP value is at least one (Augerat et al. 1998; Ralphs et al. 2003). Lysgaard, Letchford & Eglese (2004), whose separation routines were released as the widely used CVRPSEP package, generalized the rule to customer sets of any size in their Proposition 1, the only numbered result of the paper.

Setting

Let $G = (V, E)$ be the complete undirected graph on $V = \{0, 1, \dots, n\}$. Vertex $0$ is the depot and $V_c = \{1, \dots, n\}$ are the customers. Vehicles have capacity $Q > 0$ and each customer $i$ has an integer demand $q_i$ with $0 < q_i \le Q$. An LP point is a vector $x = (x_e)_{e \in E}$; $x_{ij}$ and $x_{ji}$ are the same variable, and LP solutions satisfy $x \ge 0$.

For a vertex set $S$, $\delta(S)$ is the set of edges with exactly one end-vertex in $S$ (edges to the depot included), and $x(\delta(S)) = \sum_{e \in \delta(S)} x_e$ is its cut value. For a customer set $S \subseteq V_c$:

• $q(S) = \sum_{i \in S} q_i$ is its total demand;
• $r(S)$, the bin-packing number, is the minimum number of bins of capacity $Q$ into which the items of sizes $q_i$, $i \in S$, can be packed;
• $k(S) = \lceil q(S)/Q \rceil \le r(S)$ is the rounded capacity bound.

The capacity inequalities and the rounded capacity inequalities (RCIs) are

$$x(\delta(S)) \ge 2r(S) \quad\text{and}\quad x(\delta(S)) \ge 2k(S), \qquad S \subseteq V_c,\ |S| \ge 2 .$$

The violation of such an inequality at $x$ is $2r(S) - x(\delta(S))$ (resp. $2k(S) - x(\delta(S))$); it is violated when this is positive.

Shrinking a customer set $S$ contracts it to one supervertex. The supervertices of the shrunk graph are then $S$ and the single customers outside $S$, so a union of supervertices is a customer set $T'$ with $S \subseteq T'$ or $S \cap T' = \emptyset$. Shrinking $S$ is safe if for every customer set $T$ with $|T| \ge 2$ whose inequality is violated, there is such a union $T'$ with $|T'| \ge 2$ and at least the same violation.

Formalization targets

Goal: Proposition 1

For every $x \ge 0$ and every customer set $S$ with

$$x(\delta(S)) \le 2 \qquad\text{and}\qquad x(\delta(R)) \ge 2 \ \text{ for every nonempty proper subset } R \subsetneq S,$$

shrinking $S$ is safe for the capacity inequalities $x(\delta(T)) \ge 2r(T)$.

Milestones (proof of Proposition 1, p. 426)

1. Monotonicity of the bin-packing number: $2r(S \cup T) - 2r(T) \ge 0$.
2. Submodularity of the cut function, in the paper's arrangement: $x(\delta(T)) - x(\delta(S \cup T)) \ge x(\delta(S \cap T)) - x(\delta(S))$ for $x \ge 0$.
3. The crossing-set inequality: if $T$ crosses $S$ ($T \cap S$, $T \setminus S$, $S \setminus T$ all nonempty), then $2r(T) - x(\delta(T)) \le 2r(S \cup T) - x(\delta(S \cup T))$.

Further statements on the same page

4. The same shrinking condition is safe for the rounded capacity inequalities $x(\delta(T)) \ge 2k(T)$, which are the inequalities the algorithm separates.
5. The paper's first separation heuristic checks the RCI for each connected component $S_i$ of the support graph on the customers, for each complement $V_c \setminus S_i$, and for the union of the components with no support edge to the depot. At an integer point satisfying the degree equations $x(\delta(\{i\})) = 2$ and the bounds $x_{ij} \in \{0,1\}$, $x_{0j} \in \{0,1,2\}$, this heuristic finds a violated RCI whenever one exists. This claim is stated in the paper without proof and is not needed for the goal.

Significance

Proposition 1 justifies contracting whole groups of customers before running separation heuristics, which shrinks the graph those heuristics work on while preserving every violated capacity inequality up to its violation. The rule is part of the separation routines of CVRPSEP and of later branch-and-cut and branch-cut-and-price codes for vehicle routing that reuse them.

The result is proved in the paper; to the best of the platform's records, none of it is formalized. The mission produces a reusable formal layer for the two-index CVRP formulation: cut values on the complete graph with a depot, the bin-packing number, the rounded capacity bound, and the notion of safe shrinking. Submodularity of the cut function (target 2) is a classical fact that the paper cites rather than proves; the platform already has a related statement for symmetric weight matrices on Boolean regions (EmergentGeometry.cutWeight_submodular), in a different representation. Target 5 records a claim of the paper that it asserts without proof.

Difficulty

When the violated set $T$ contains $S$ or misses it, $T$ itself is a union of supervertices and there is nothing to show. The difficulty is a set $T$ that crosses $S$: no union of supervertices is obviously as violated as $T$, because enlarging $T$ can raise its cut value — $x(\delta(S \cup T))$ can be smaller or larger than $x(\delta(T))$ depending on the edges leaving $S \setminus T$ — and the hypotheses on $S$ say nothing about $T$ directly. Both hypotheses on $S$ and the sign condition $x \ge 0$ matter here; for signed $x$ the statement fails. A violated $T$ strictly inside $S$ is not a crossing set in the paper's sense and has to be handled as well.

On the formal side, the bin-packing number is an optimum of a combinatorial problem; its properties must be derived from a definition by assignments to bins, and it is well defined only because every demand fits in one vehicle. Target 5 needs a structural understanding of integer points satisfying the degree equations, which the paper does not supply.

Formalization scope

Vertices are Fin (n+1), the depot is 0, and a customer set is a Finset (Fin (n+1)) not containing 0. The edge vector is a function x : Sym2 (Fin (n+1)) → ℝ on unordered pairs, and the cut value is ∑ i ∈ S, ∑ j ∈ Sᶜ, x s(i, j), which includes the edges to the depot. The capacity $Q$ is real (the paper does not say it is an integer) and demands are natural numbers with $0 < q_i \le Q$ for customers. The bin-packing number is the least number of bins over assignments of the customers of $S$ to bins of total demand at most $Q$; under $q_i \le Q$ this minimum exists. Of the LP point only $x \ge 0$ is assumed in Proposition 1 and targets 1–4, which is at least as strong as the paper's setting. The hypothesis "$x(\delta(R)) \ge 2$ for all $R \subset S$" ranges over nonempty proper subsets.

A formalization that lets $R = \emptyset$ in that hypothesis is vacuous, because $x(\delta(\emptyset)) = 0$; one that drops the condition "$S \subseteq T'$ or $S \cap T' = \emptyset$" from safe shrinking is trivial (take $T' = T$); and one that defines $r$ as $k$, as an arbitrary monotone function, or with a junk value $0$, or that omits the depot edges from the cut, states a different result. None of these is the mission's statement.

Needed infrastructure: finite sums over cuts of Sym2-indexed vectors, a working API for the bin-packing number, and, for target 5, connected components of the support graph (SimpleGraph.Reachable). The cut-function lemmas and the bin-packing number are reusable for any later formalization of CVRP polyhedra (framed capacity, comb and multistar inequalities). Contributions of general lemmas about cut functions on complete graphs are welcome as separate theorems.

Selected references

• J. Lysgaard, A. N. Letchford, R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming Ser. A 100 (2004) 423–445. https://doi.org/10.1007/s10107-003-0481-8
• G. L. Nemhauser, L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
• P. Augerat, J. M. Belenguer, E. Benavent, A. Corberán, D. Naddef, Separating capacity constraints in the CVRP using tabu search, European Journal of Operational Research 106 (1998) 546–557. https://doi.org/10.1016/S0377-2217(97)00290-7
• T. K. Ralphs, L. Kopman, W. R. Pulleyblank, L. E. Trotter, On the capacitated vehicle routing problem, Mathematical Programming 94 (2003) 343–359. https://doi.org/10.1007/s10107-002-0323-0

Motivation

A two-machine flow shop is the simplest multi-stage production system: every job visits machine 1 and then machine 2, each machine works on one job at a time, and the goal is to finish all jobs as early as possible. S. M. Johnson's 1954 paper (Naval Research Logistics Quarterly 1(1):61–68, doi:10.1002/nav.3800010110) answered this question, posed by R. Bellman, with an exact rule, now called Johnson's rule. It is one of the first exact results in machine scheduling. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) the problem is written $F2\,\|\,C_{\max}$. The rule is the standard polynomial case against which the NP-hardness of the three-machine flow shop (Garey, Johnson and Sethi 1976) is contrasted, and it is still used inside heuristics for larger shops.

Timeline:

• 1954. Johnson proves the two-machine rule and a three-machine special case (the latter is the second mission of this series).
• 1976. Garey, Johnson and Sethi prove that the three-machine flow shop is NP-hard in the strong sense, so the two-machine case marks the boundary of tractability.

Setting

There are $n$ items $i = 1, \dots, n$. Item $i$ needs $A_i > 0$ units of time on machine 1 and then $B_i > 0$ units on machine 2. Each time is setup time plus work time, and the times are otherwise arbitrary. A schedule assigns start times $s^1_i$ and $s^2_i$. It is feasible when all start times are nonnegative, the intervals $[s^1_i, s^1_i + A_i]$ of distinct items do not overlap on machine 1, the intervals $[s^2_i, s^2_i + B_i]$ do not overlap on machine 2, and $s^1_i + A_i \le s^2_i$ for every item. The total elapsed time $T(s) = \max_i (s^2_i + B_i)$ is the time at which the last item leaves machine 2.

An order is a permutation $\sigma$, where $\sigma(k)$ is the item in position $k$. The as-soon-as-possible schedule $a_\sigma$ of an order processes the items in the order $\sigma$ on both machines, with no delay on machine 1. Each item starts on machine 2 as soon as it has left machine 1 and machine 2 is free.

Relation (II). Item $i$ is definitely preferred to item $j$ when

$$\min(A_i, B_j) < \min(A_j, B_i),$$

and the two items are indifferent when equality holds. An order is consistent with all the definite preferences when no item is definitely preferred to an item placed earlier.

For an order $\sigma$ the paper uses the quantities

$$K_u = \sum_{l \le u} A_{\sigma(l)} - \sum_{l < u} B_{\sigma(l)}, \qquad F(\sigma) = \max_u K_u .$$

Formalization targets

Goal: Theorem 1 (p. 63)

For positive $A, B$:

$$\exists\, \sigma \text{ consistent with (II)}, \qquad\text{and}\qquad \forall\, \sigma \text{ consistent with (II)},\ \forall\, s \text{ feasible}:\quad a_\sigma \text{ is feasible and } T(a_\sigma) \le T(s).$$

The comparison is against every feasible schedule, including those whose two machines follow different orders.

Milestones

1. Lemma 1 (p. 61). Every feasible schedule can be replaced, at no greater total elapsed time, by a feasible schedule that follows one common order on both machines.
2. As soon as possible (p. 62). For a fixed common order, $a_\sigma$ is feasible and minimizes $T$ among the feasible schedules that follow $\sigma$.
3. Closed form (p. 62). $T(a_\sigma) = \sum_i B_i + F(\sigma)$, i.e. the total idle time of machine 2 is $\max_u K_u$.
4. Adjacent interchange (p. 63). Interchanging the items in positions $j, j+1$ leaves every other $K_u$ unchanged. Moreover, $\max(K_j, K_{j+1}) < \max(K'_j, K'_{j+1})$ holds if and only if (II) holds for the pair.
5. Interchanges do not increase $F$ (p. 63). If the pair in positions $j, j+1$ satisfies (II) non-strictly, then $F(\sigma) \le F(\sigma')$.
6. Lemma 2 (p. 64). Relation (II) is transitive, except when the middle item is indifferent to both others.
7. Worked example (p. 65). For $A = (4,4,30,6,2)$ and $B = (5,1,4,30,3)$, the order $(5,1,4,3,2)$ takes 47 units with 4 units of idle time. The reversed order takes 78 units, and every order takes between 47 and 78 units.

Significance

The theorem reduces an optimization over a continuum of start-time vectors, and over $n!$ orders, to sorting with respect to a pairwise relation. The paper's working rule computes an optimal order in $O(n \log n)$ time. The two-machine rule is the building block of Johnson's three-machine result, of the Campbell–Dudek–Smith heuristic for $m$ machines, and of lower bounds in branch-and-bound methods for flow shops. The closed form $T(a_\sigma) = \sum_i B_i + \max_u K_u$ reappears across flow-shop theory as a longest-path formula.

The result is classical and proved. This mission contributes a machine-checked proof in Lean 4 against Mathlib. As far as a search of the platform shows, no formal statement of the flow-shop model or of Johnson's rule exists there. The mission also fixes a reusable Lean model of a two-machine schedule: start times, feasibility, total elapsed time and the as-soon-as-possible schedule of an order.

Difficulty

The paper's argument leaves two steps informal, and a formal proof must supply both. First, Lemma 1 is justified by a picture and the phrase "successive interchanges". The page does not show that each interchange keeps the schedule feasible and does not delay the last completion on machine 2, and this is where most of the modelling work sits. Second, relation (II) is not a strict weak order when there are ties, so the obvious sorting argument fails. Consistency on adjacent pairs does not imply optimality: the items $(A, B) = (5,2), (1,1), (2,5)$, in that order, satisfy (II) non-strictly on both adjacent pairs, yet take 13 units against an optimum of 10. Lemma 2's exception is exactly this case.

Formalization scope

Items are Fin n (0-based) and times are real numbers. Positivity $A_i > 0$, $B_i > 0$ is a hypothesis of the goal and of Lemma 1, the as-soon-as-possible step and the closed form, as on p. 61. Lemma 2 and the interchange statements are pure min/sum algebra and carry no positivity. An order is σ : Equiv.Perm (Fin n) with σ k the item in position k. Interchanging positions $j, j+1$ is σ * Equiv.swap j (j+1). The total elapsed time is Finset.univ.fold max 0 of the machine-2 completion times, so it is $0$ when $n = 0$. $K_u$ is indexed by 0-based positions (Lean's $K_u$ is the paper's $K_{u+1}$), and $F$ requires $n \ge 1$.

Conventions made explicit or corrected:

• "Consistent with all the definite preferences" is imposed on all pairs of positions $k < l$ as the non-strict inequality $\min(A_{\sigma(k)}, B_{\sigma(l)}) \le \min(A_{\sigma(l)}, B_{\sigma(k)})$. The goal also asserts that such an order exists, so its main clause is not vacuous.
• The display of $K'_u$ on p. 63 prints the upper limit $u$ on the $B'$-sum. The definition of $K_u$ on p. 62 and the reduction of (I) to (II) require $u-1$, and the formalization uses $u-1$.
• Lemma 2 keeps the page's exception (item 2 indifferent to both items); without it the statement is false.

Measuring the objective by $F(\sigma)$, or comparing only against schedules that follow one common order, would drop Lemma 1 and change the theorem. The goal compares against every feasible start-time schedule. The working rule of p. 64 (a procedure) is not formalized.

Proofs of any milestone are welcome, as are further lemmas about the as-soon-as-possible schedule and a formalization of the working rule. The schedule definitions are the basis for the three-machine mission of this series.

Selected references

• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. doi: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. doi:10.1287/moor.1.2.117
• 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:287–326, 1979. doi:10.1016/S0167-5060(08)70356-X
• H. G. Campbell, R. A. Dudek, M. L. Smith, A heuristic algorithm for the n job, m machine sequencing problem, Management Science 16(10):B630–B637, 1970. doi:10.1287/mnsc.16.10.B630