Graph Theory

Motivation

The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges have capacities. It is a basic model in operations research (transportation, scheduling, bipartite matching) and a standard subroutine in combinatorial optimization.

Classical algorithms, from Ford and Fulkerson (1956) through Edmonds–Karp and Dinic (1970–1972) and Karzanov (1974), increase a feasible flow along augmenting paths or blocking flows. Goldberg and Tarjan, A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988, doi:10.1145/48014.61051), replaced this global view by a local one: the push-relabel method maintains a preflow, which may violate conservation at intermediate vertices, and moves excess along edges toward vertices with smaller distance labels. The generic method, with the basic operations applied in any order, is the starting point of the FIFO, highest-label and dynamic-tree implementations analysed later in the same paper, and push-relabel codes remain among the fastest practical maximum-flow solvers.

This mission formalizes §2–§3 of the paper: the generic algorithm is correct, and it stops after a number of basic operations bounded by an explicit polynomial in the numbers of vertices and edges, whatever order of operations is chosen.

Setting

A flow network has a finite vertex set $V$ with $n = |V|$, a source $s$ and a sink $t \ne s$, and a capacity $c(v,w) \ge 0$ for every ordered pair of vertices, positive exactly on the edges $E = \{(v,w) : c(v,w) > 0\}$; $m = |E|$, and there are no loops, $c(v,v) = 0$.

Flows are real functions on all vertex pairs. A function $f$ satisfies the capacity constraint if $f(v,w) \le c(v,w)$ and antisymmetry if $f(v,w) = -f(w,v)$ for all pairs. The excess of $v$ is $e(v) = \sum_{u} f(u,v)$. A flow also has $e(v) = 0$ for $v \notin \{s,t\}$; a preflow only $e(v) \ge 0$ for $v \ne s$. The value of a flow is $|f| = \sum_v f(v,t)$, and a maximum flow is a flow of maximum value.

The residual capacity is $r_f(v,w) = c(v,w) - f(v,w)$; pairs with $r_f(v,w) > 0$ are the edges of the residual graph $G_f$. A valid labeling is $d : V \to \mathbb{N} \cup \{\infty\}$ with $d(s) = n$, $d(t) = 0$ and $d(v) \le d(w) + 1$ on every residual edge. A vertex $v$ is active if $v \notin \{s,t\}$, $d(v) < \infty$ and $e(v) > 0$.

The two basic operations (Fig. 1 of the paper) are:

• Push$(v,w)$, applicable when $v$ is active, $r_f(v,w) > 0$ and $d(v) = d(w)+1$: send $\delta = \min(e(v), r_f(v,w))$, i.e. $f(v,w) \mathrel{+}= \delta$, $f(w,v) \mathrel{-}= \delta$. It is saturating if $r_f(v,w) = 0$ afterwards and nonsaturating otherwise.
• Relabel$(v)$, applicable when $v$ is active and $d(v) \le d(w)$ for every residual edge $(v,w)$: set $d(v) \leftarrow \min\{d(w)+1 : (v,w) \in E_f\}$ ($\infty$ if there is none).

The generic algorithm (Fig. 2) starts from the preflow that saturates every edge leaving $s$ and is zero elsewhere, with the simple labeling $d(s) = n$, $d(v) = 0$ otherwise, and applies applicable basic operations in any order while one exists. An execution with $K$ basic operations is a sequence of states $(f_0,d_0),\dots,(f_K,d_K)$ from the initial state, each obtained from the previous one by one applicable operation.

Formalization targets

Goal: Theorems 3.11 and 3.4

Assume the paper's standing assumption $m \ge n-1$. For every execution with $K$ basic operations,

$$K \le (2n-1)(n-2) + 2nm + 4n^2 m,$$

and if no basic operation applies in the final state, then $f_K$ is a maximum flow. The paper states the bound as $O(n^2m)$ and proves it as "immediate from Lemmas 3.8, 3.9, and 3.10"; the goal states the sum of those three printed bounds. Since every execution is this short, no order of operations runs forever.

Milestones

In the order the proof uses them: Lemma 2.1 (at an active vertex a push or a relabel applies); Lemma 3.1 (the labeling stays valid); Theorem 3.2 (Ford–Fulkerson: a flow is maximum iff $t$ is unreachable from $s$ in $G_f$); Lemma 3.3 (under a valid labeling $t$ is unreachable from $s$); Lemma 3.5 (from any vertex with positive excess, $s$ is reachable); Lemma 3.6 (labels never decrease; a relabeling increases the label); Lemma 3.7 ($d(v) \le 2n-1$ throughout); Theorem 3.4 (termination with finite labels gives a maximum flow); Lemma 3.8 ($\le 2n-1$ relabelings per vertex, $\le (2n-1)(n-2) < 2n^2$ in total); Lemma 3.9 ($\le 2nm$ saturating pushes); Lemma 3.10 ($\le 4n^2m$ nonsaturating pushes, under $m \ge n-1$). A further, non-milestone item states the unnumbered invariant that every $f_k$ is a preflow.

Significance

The generic bound shows that push-relabel terminates in a polynomial number of steps without any rule for choosing the next operation; the specific orderings of §4–§5 of the paper (first-in first-out, $O(n^3)$; dynamic trees, $O(nm\log(n^2/m))$) refine only the count of nonsaturating pushes, and reuse Lemmas 3.1–3.9 unchanged. The correctness argument, a valid labeling excludes augmenting paths, is the template for the push-relabel minimum-cost flow and assignment algorithms that followed.

These results are proved in the paper and are textbook material. Their machine-checked counterparts are, as far as is known here, not on the Prove2Me platform: the platform's network-flow statements (from Introduction to Linear Optimization, e.g. LinearOptimization.max_flow_min_cut) use a different model, with arc-indexed nonnegative flows and extended-real capacities, and contain nothing about preflows, labels or operation counts. This mission produces a formal account of the antisymmetric-flow model, of Ford–Fulkerson in that model, and of the amortized counting arguments, with the constants the paper prints.

Difficulty

The correctness half is short once the invariants are in place; the difficulty is in the counting. The label bound (Lemma 3.7) is a statement about the whole execution, and it depends on a structural fact about preflows (Lemma 3.5) whose truth rests on antisymmetry and on the nonnegativity of excesses. The obvious first idea for the push counts, bounding pushes per edge or per vertex locally, fails for nonsaturating pushes: flow pushed across a pair can be pushed back later, and nothing local limits how often this happens, so Lemma 3.10 holds only as an amortized statement over the entire execution and depends on both earlier counts. Saturating pushes on a pair can also recur, in both directions, and Lemma 3.9 has to control the interaction between the two directions.

Formally, all of this is reasoning about arbitrary interleavings of operations, with labels in $\mathbb{N} \cup \{\infty\}$ and real-valued flows.

Formalization scope

• Vertices form a finite type with decidable equality; $n$ is its cardinality, $s \ne t$, so $n \ge 2$ and the natural-number subtractions $2n-1$ and $n-2$ are exact. Capacities are a real function on all pairs, nonnegative, zero on the diagonal; $E$ is its support and $m$ its cardinality.
• Flows and preflows are antisymmetric real functions on all pairs (not nonnegative arc flows); the excess is computed from $f$, never stored. A maximum flow is a flow whose value is at least that of every flow.
• Labels live in ℕ∞, with $\infty + 1 = \infty$; the relabel value is an infimum, which is $\infty$ on the empty set.
• An execution is a sequence of states σ : ℕ → State V with a length $K$, starting at the Fig. 2 state with the simple labeling (the paper's own assumption for its proofs), each step an applicable push or relabel. "Terminates" means that no basic operation applies, the loop guard of Fig. 2. The three counts are cardinalities of the sets of step indices of each kind.
• Explicit constants: $2n-1$ per-vertex relabelings, $(2n-1)(n-2) < 2n^2$ total relabelings, $2nm$ saturating pushes, $4n^2m$ nonsaturating pushes, label bound $2n-1$, and the total $(2n-1)(n-2)+2nm+4n^2m$. The standing assumption $m \ge n-1$ appears only on Lemma 3.10 and the goal.
• A trivializing formalization is ruled out: the step relation fixes the pushed amount $\delta = \min(e(v), r_f(v,w))$ and the new label exactly as in Fig. 1, termination is the loop guard rather than "the result is a flow", and a sorry-free check exhibits a concrete network $s \to a \to t$ with a two-step execution (relabel $a$, then push $(a,t)$), so the run hypotheses are satisfiable.

Welcome contributions: proofs of the invariants (preflow, valid labeling, label monotonicity), of Ford–Fulkerson for antisymmetric flows (reusable beyond this mission), and of the counting lemmas. The FIFO bound of §4 is the subject of a companion mission.

Selected references

• A. V. Goldberg, R. E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4):921–940, 1988. doi:10.1145/48014.61051
• L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19(2):248–264, 1972. doi:10.1145/321694.321699
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows: Theory, Algorithms, and Applications, Prentice Hall, 1993.

Motivation

The maximum flow problem asks how much of a commodity can be sent from a source to a sink through a network whose arcs have capacities. It underlies bipartite matching, transportation, scheduling and many reductions in combinatorial optimization. The classical method for it, the labeling method of Ford and Fulkerson (Flows in Networks, 1962), repeatedly finds an augmenting path and pushes flow along it. With integer capacities it terminates, but the number of augmentations can be as large as the maximum flow value itself, and Edmonds and Karp exhibit a four-node network on which this happens (p. 250). With irrational capacities the method need not terminate at all.

Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2):248–264, 1972 (doi:10.1145/321694.321699), showed that two simple rules for choosing the augmenting path repair this. The first, augmenting along a path with fewest arcs, is the subject of mission 1 of this series. This mission covers the second (§1.3): augment along a path that gives the largest possible augmentation. For integer capacities the number of augmentations then grows only logarithmically in the maximum flow value.

Setting

A network $N$ has a finite set $V$ of nodes, a source $s$ and a sink $t \neq s$, and a set of arcs, ordered pairs $(u,v)$ with $u \neq v$, at most one from each node to another. One arc is the return arc $(t,s)$; the other arcs form the set $A$, and each $(u,v) \in A$ has a capacity $c(u,v) > 0$. A flow is a nonnegative function $f$ on the arcs of $N$ with $f(u,v) \le c(u,v)$ on $A$ and flow conservation at every node, $s$ and $t$ included. Its value is $f(t,s)$, the flow returned along the return arc; a maximum flow has the largest value among all flows, and $f^*(t,s)$ denotes that value.

The residual network $N^f$ has an arc $(u,v)$ whenever $(u,v) \in A$ and $c(u,v) - f(u,v) > 0$, or $(v,u) \in A$ and $f(v,u) > 0$. An augmenting path is a directed path $s = u_1, \dots, u_p = t$ of distinct nodes in $N^f$. Each of its arcs $(u,v)$ has a residual amount $e(u,v)$, equal to $c(u,v) - f(u,v)$, $f(v,u)$, or $c(u,v) - f(u,v) + f(v,u)$ according to which of $(u,v)$, $(v,u)$ lie in $A$, and the path's augmentation is $\varepsilon = \min e(u_i, u_{i+1})$. Augmenting increases $f(t,s)$ by $\varepsilon$ and changes the flow on the arcs of the path accordingly, with the paper's own rule when both $(u,v)$ and $(v,u)$ are arcs. The labeling method produces flows $f^0, f^1, \dots$ by augmenting along a path relative to $f^k$ as long as one exists.

The rule studied here chooses, at every step, an augmenting path whose $\varepsilon$ is at least that of every other augmenting path relative to the current flow. The bound involves an integer $M > 1$ such that every partition of the nodes into $X \ni s$ and $\bar X \ni t$ has at most $M$ arcs of $N$ with one end on each side.

Formalization targets

Goal: Theorem 2 (p. 253)

For a network with integer capacities, $M$ as above, and a run $f^0, \dots, f^K$ of the labeling method with maximum augmentations started from an integer-valued flow,

$$K \;\le\; 1 + \log_{M/(M-1)} f^*(t,s),$$

and if no augmenting path relative to $f^K$ exists, then $f^K$ is a maximum flow.

Milestones

The milestone list follows the paper's argument:

1. augmentation produces a flow of value $f(t,s) + \varepsilon$ (§1.1, p. 249);
2. a flow is maximum if and only if it has no augmenting path (§1.1, pp. 249–250);
3. with integer capacities, $\varepsilon$ is a positive integer and the flows of the method stay integer-valued (§1.1, p. 250);
4. the cut inequality $c(X,\bar X) \ge f(X,\bar X) - f(\bar X,X) = f(t,s)$ (p. 254);
5. $f^*(t,s) - f^k(t,s) \le \varepsilon^k M$, where $\varepsilon^k = f^{k+1}(t,s) - f^k(t,s)$ (p. 254);
6. $f^*(t,s) - f^{k+1}(t,s) \le [f^*(t,s) - f^k(t,s)](1 - M^{-1})$ (p. 254);
7. $f^*(t,s) - f^k(t,s) \le f^*(t,s)(1 - M^{-1})^k$ (p. 254).

Significance

Theorem 2 was among the first bounds showing that a maximum flow algorithm can be made polynomial in the size of the numbers rather than in their values: since $M \le n^2/2$ and $f^*(t,s)$ is at most $n^2$ times the average capacity, the bound is $O(n^2 \log(n^2 \bar c))$ in terms of the number of nodes $n$ and the average capacity $\bar c$ (p. 254). The largest-augmentation rule, often called the fattest-path or maximum-capacity augmenting path rule, is a standard textbook variant, and its geometric-decrease argument is the model for later capacity-scaling methods, including the scaling algorithm for the Hitchcock problem in §2 of the same paper (mission 3 of this series).

The theorem has been proved since 1972 and appears in standard texts. As far as a platform search shows (2026-09-26), no machine-checked proof of it exists on Prove2Me. The platform does contain LinearOptimization.max_flow_min_cut and LinearOptimization.max_flow_ford_fulkerson_integer_termination, which state max-flow min-cut and termination of the generic method in a different network model (parallel arcs, extended nonnegative capacities, no return arc); they give no count of augmentations and are related work only. This mission would contribute a formal proof of the counting bound together with the general labeling-method facts (milestones 1–3), which mission 1 needs as well.

Difficulty

The obvious argument, that each augmentation raises the value by at least 1, gives only the bound $f^*(t,s)$, and on the four-node example of p. 250 that bound is attained by an arbitrary choice of paths. The logarithmic bound needs a lower bound on the size of the largest augmentation in terms of the remaining gap $f^*(t,s) - f^k(t,s)$. The largest augmentation is defined by comparison with all augmenting paths relative to the current flow, while the gap is a global quantity of the network, and neither integrality nor the maximum-augmentation rule alone controls it. Milestone 2's converse, that a non-maximum flow always admits an augmenting path, is itself the max-flow min-cut theorem in this model, and the formal proof has to establish it for the paper's return-arc model rather than import it from a different one.

Formalization scope

• Nodes form a finite type V with decidable equality. A : Finset (V × V) contains no loops and not $(t,s)$. Capacities are real, c : V → V → ℝ, positive on A. Integrality is the hypothesis IntegralCaps N, and for the initial flow IsIntegralOn N (f 0) (integer values on the arcs of $N$, the return arc included).
• Flows are functions V → V → ℝ constrained only on the arcs of $N$. A maximum flow is the predicate IsMaxFlow, comparing $f(t,s)$ with every flow, not a supremum. The goal takes a maximum flow g as a hypothesis and sets $f^*(t,s) = g(t,s)$; every network has one.
• Augmenting paths are duplicate-free node lists whose consecutive pairs are arcs of $N^f$. The page prints Case (b) of the definition of $\varepsilon_i$ with the same hypothesis as Case (c); the corrected Case (b), $(u,v) \notin A$ and $(v,u) \in A$, is used, as the definition of $N^f$ (p. 251) and the list for $e(u,v)$ (p. 253) confirm.
• A run is IsMaxAugRun N K f P. Its initial flow is arbitrary except for integrality, and each later flow is the augmentation of the previous one along a path of maximum $\varepsilon$ among all augmenting paths.
• The crossing bound CrossArcsBounded N M counts the arcs of $N$, return arc included, with one end on each side of every $s$–$t$ partition. This is the literal reading of p. 253.
• Explicit constants. The bound is exactly $1 + \log_{M/(M-1)} f^*(t,s)$, written (K : ℝ) ≤ 1 + Real.logb ((M : ℝ) / ((M : ℝ) - 1)) (g N.t N.s) with $M > 1$ a natural number. When $f^*(t,s) = 0$, Real.logb gives $0$ and the bound reads $K \le 1$. The contraction factor is 1 - (M : ℝ)⁻¹.
• A statement that bounds only runs of an unsatisfiable step predicate, drops the integrality of $f^0$ or of the capacities (the bound is false without them), or compares $\varepsilon$ only among paths of some restricted class does not formalize Theorem 2. A sorry-free check exhibits a four-node network with integer capacities and a valid maximum-augmentation step.
• Reusable beyond this mission: the return-arc network model, the augmentation step with the paper's opposite-arc rule, the integrality lemma, and the cut inequality. Proofs of any milestone are welcome, as are proofs of the converse in milestone 2 that could later be shared with mission 1.

Selected references

• J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
• L. R. Ford, D. R. Fulkerson, Flows in Networks, RAND report R-375-PR, 1962; Princeton University Press, 1962. https://www.rand.org/pubs/reports/R375.html

Motivation

The Steiner problem in graphs asks for the cheapest way to connect a prescribed set of nodes of a network, where intermediate nodes may be used freely. It is the network version of the classical Euclidean Steiner tree problem surveyed by Gilbert and Pollak (SIAM J. Appl. Math. 16, 1968), and it arises wherever a few sites must be joined through an existing network at minimum total cost: communication and pipeline layout, VLSI routing, and phylogenetics. With two terminals it is the shortest-path problem; with all nodes as terminals it is the minimum spanning tree problem; in between it is NP-hard.

Dreyfus and Wagner (Networks 1(3):195–207, 1971) gave the first exact algorithm whose running time is exponential only in the number $k$ of terminals and polynomial in the number $n$ of nodes. The paper states it, as Algorithm A, together with its proof of correctness and an exact count of its elementary operations.

Timeline. 1968: Gilbert and Pollak survey Steiner minimal trees. 1971: Dreyfus and Wagner, a dynamic program over subsets of terminals running in time proportional to $n^3/2 + n^2(2^{k-1}-k-1) + n(3^{k-1}-2^k+3)/2$. 1987: Erickson, Monma and Veinott give the same subset recursion for general network flow problems. 2007: Björklund, Husfeldt, Kaski and Koivisto (STOC 2007) improve the exponential dependence on $k$ for small integer weights. The Dreyfus–Wagner recursion remains the standard exact method and the basis of the fixed-parameter tractability of the problem in $k$.

Setting

A graph $G = (N, A)$ has a finite set $N$ of nodes and a set $A$ of undirected arcs, each arc $a$ having a positive length $|a|$; $G$ is connected. For a set $S \subseteq A$ of arcs, $|S| = \sum_{s \in S} |s|$. A set $S$ connects a node set $X$ if all members of $X$ are joined by paths composed only of arcs in $S$.

Given $Y \subseteq N$, a Steiner path (or Steiner tree) connecting $Y$ is a set $S \subseteq A$ that connects $Y$ with $|S|$ minimum. Its length is the Steiner length $\operatorname{St}(Y)$. For nodes $i, j$, $D(i,j)$ is the length of a shortest path from $i$ to $j$; $D(i,j) = \operatorname{St}(\{i,j\})$.

Algorithm A fixes a linear order of $N$ (so that each nonempty set $D$ has a first element $D[1]$), picks $q \in Y$, sets $C = Y - \{q\}$, and fills a table $S[D, I]$ for nonempty $D \subsetneq C$ and $I \in N$:

$$S[\{t\}, I] = D(t, I), \qquad S[D, I] = \min_{J \in N}\Big(D(I,J) + \min_{D[1] \in E \subsetneq D}\big(S[E,J] + S[D-E,J]\big)\Big),$$

and returns

$$v = \min_{J \in N}\Big(D(q,J) + \min_{C[1] \in E \subsetneq C}\big(S[E,J] + S[C-E,J]\big)\Big).$$

A minimum over an empty set is $+\infty$. In the Lean development these objects are steinerLength, pathDist, tableA and algorithmA in the namespace DreyfusWagner.Steiner.

Formalization targets

Goal: Algorithm A is exact

For every finite connected graph with positive arc lengths, every linear order on its nodes, every $Y$ with $\|Y\| \ge 3$ and every $q \in Y$,

$$v = \operatorname{St}(Y).$$

This is the caption of Algorithm A ("Computes the length of the Steiner tree connecting $Y$", p. 203). The statement is an equality, not a bound.

Milestones

In the order the proof uses them:

1. A Steiner path is a tree (§1, p. 197): a minimum connecting arc set contains no cycle.
2. The two-node case (Appendix A, p. 205): $\operatorname{St}(\{i,j\}) = D(i,j)$.
3. Theorem 1 (Appendix A, p. 206): for a Steiner tree $S$, a node $x$ on it, and a set $C$ of arcs of $S$ at $x$, the arcs of $S$ connecting $x$ to the terminals reached through $C$ form a Steiner tree for those terminals together with $x$.
4. Optimal Decomposition Theorem (Appendix A, p. 206): if $\|Y\| \ge 3$ and $q \in Y$, a Steiner tree for $Y$ splits into three disjoint Steiner paths, for $\{p,q\}$, $\{p\} \cup D$ and $\{p\} \cup (Y - D - \{q\})$, where $p \in N$ and $\emptyset \ne D \subsetneq Y - \{q\}$.
5. The recurrence (§2, pp. 199–200): for $\|D\| \ge 2$ and any node $m$,

$$\operatorname{St}(\{m\} \cup D) = \min_{k \in N}\Big(D(m,k) + \min_{\emptyset \ne E \subsetneq D}\big(\operatorname{St}(\{k\} \cup E) + \operatorname{St}(\{k\} \cup (D - E))\big)\Big).$$

6. The table invariant (§2, p. 200): $S[D, I] = \operatorname{St}(\{I\} \cup D)$ for every nonempty $D$ and every $I$.

Two companion items accompany the goal: the numerical illustration of §3 (seven nodes, $\operatorname{St}(Y) = 5$, Algorithm A returns $5$), and the exact count of elementary statements of §5, $n^2(2^{k-1}-k-1) + n(3^{k-1}-2^k+3)/2$.

Significance

The result turns the Steiner problem with few terminals into a polynomial computation in the size of the network: for fixed $k$ the running time is $O(n^3)$ including all-pairs shortest paths. It is the reference exact algorithm against which heuristics and approximation algorithms for Steiner trees are evaluated, a standard example of dynamic programming over subsets, and the origin of the fixed-parameter tractability of the Steiner tree problem parameterized by the number of terminals. The subset recurrence reappears in group Steiner, prize-collecting and directed Steiner variants.

The paper's proof is complete and the result is classical; it has not, to our knowledge, been machine-checked. This mission produces a checked account of the exactness of the recursion: the structural facts about minimum connecting arc sets (acyclicity, optimality of branches, the three-way decomposition) and the passage from these to the algorithm's table. These facts about weighted graphs, minimum connecting arc sets and shortest paths are reusable well beyond this paper.

Difficulty

The upper bound $v \ge \operatorname{St}(Y)$ is routine: each term of each minimum is the length of some connecting arc set, so no term can beat the optimum. The content is the reverse inequality, which needs the Optimal Decomposition Theorem: one must show that some optimal tree actually splits at a single node $p$ into a shortest path to $q$ and two optimal subtrees whose terminal sets partition $Y - \{q\}$ into two nonempty parts. The naive choice $p = q$ fails when $q$ is a leaf, and the choice of the first branching node fails when the path from $q$ meets another terminal first; the paper handles these as separate cases. A second difficulty is the passage from arc sets to trees: minimum connecting sets are forests only because lengths are positive, and "the arcs of $S$ involved in connecting" a set of terminals must be identified with a subtree. Finally the table recursion must be matched with the recurrence, including the restriction $D[1] \in E$ that enumerates each splitting once.

Formalization scope

Nodes are a finite type V with a LinearOrder (the paper's "(ordered) set"; the goal holds for every order). The graph is a SimpleGraph V with decidable adjacency, arcs are unordered pairs Sym2 V, and lengths are ℓ : Sym2 V → ℝ. Every theorem assumes the paper's standing hypotheses of p. 195: all arcs of $G$ have positive length (∀ e ∈ G.edgeSet, 0 < ℓ e) and $G$ is connected. The paper allows several arcs between the same two nodes; the simple-graph model keeps one, which does not change any Steiner length since an optimal set uses only the shortest of parallel arcs. Connecting means reachability in the graph formed by the arcs of $S$. Steiner lengths, $D(i,j)$ and all minima of the algorithm take values in WithTop ℝ, where ⊤ is $+\infty$, ⊤ + x = ⊤ and an empty minimum is ⊤; no real-valued infimum with a junk value is used. $D(i,j)$ is a minimum over paths of $G$.

The goal assumes $\|Y\| \ge 3$, the paper's own hypothesis (Appendix A, p. 205). For $\|Y\| = 2$ Algorithm A as printed returns $+\infty$ because line (18) admits no set $E$; the two-node case is covered by milestone 2. The algorithm is defined from $D(i,j)$, addition and minima only: a formalization in which tableA or algorithmA refers to Steiner lengths, or in which the goal only asserts $v \ge \operatorname{St}(Y)$, would be trivial and is ruled out. The loop order of lines (4)–(14) is replaced by recursion on $\|D\|$, which the paper states is immaterial (p. 203).

Useful infrastructure: sums of lengths along walks and paths, reachability in edge-subgraphs, acyclicity of minimum connecting sets, and splitting a tree at a node. Contributions of these as reusable lemmas are welcome, as are proofs of individual milestones in any order. Tree reconstruction (§2, p. 200) and the empirical running times (p. 205) are out of scope.

Selected references

• S. E. Dreyfus, R. A. Wagner, The Steiner Problem in Graphs, Networks 1(3):195–207, 1971. https://doi.org/10.1002/net.3230010302
• E. N. Gilbert, H. O. Pollak, Steiner Minimal Trees, SIAM Journal on Applied Mathematics 16(1):1–29, 1968. https://doi.org/10.1137/0116001
• R. W. Floyd, Algorithm 97: Shortest Path, Communications of the ACM 5(6):345, 1962. https://doi.org/10.1145/367766.368168
• R. E. Erickson, C. L. Monma, A. F. Veinott Jr., Send-and-Split Method for Minimum-Concave-Cost Network Flows, Mathematics of Operations Research 12(4):634–664, 1987. https://doi.org/10.1287/moor.12.4.634
• A. Björklund, T. Husfeldt, P. Kaski, M. Koivisto, Fourier Meets Möbius: Fast Subset Convolution, STOC 2007, 67–74. https://doi.org/10.1145/1250790.1250801

Motivation

Connecting a set of terminals by a network of direct links of least total length is one of the oldest problems of combinatorial optimization. R. C. Prim's 1957 paper in the Bell System Technical Journal (DOI) was motivated by the rate structure for Bell System leased-line services, in which the charge for connecting a set of terminals depends on the length of a shortest network connecting them. The paper states two local construction principles, P1 and P2, and shows that any sequence of their applications produces a shortest network, first for points in the plane and then for arbitrary connected labelled graphs with arbitrary real edge lengths. The paper's §V specialization of the principles, growing a single fragment, is what is now called Prim's algorithm, and its §IV statement is the form of the minimum spanning tree theorem used throughout network design, clustering and approximation algorithms.

Timeline. O. Borůvka (1926) solved the problem for an electrical network in Moravia; V. Jarník (1930) gave the single-fragment procedure; J. B. Kruskal (1956, Proc. AMS 7, 48–50) proved that adding globally shortest links avoiding cycles yields a shortest spanning tree; Prim (1957) gave the more permissive principles P1 and P2, which contain both the Jarník procedure and Kruskal's rule as special orders of application; E. W. Dijkstra (1959) rediscovered the single-fragment procedure.

Setting

Let $V$ be a finite set of $N$ terminals and $G$ a simple graph on $V$, the labelled graph whose edges are the possible links. Each edge $e$ carries a real length $w(e)$; lengths may be negative, zero, or tie. For a finite set $F$ of links, $H(F)$ denotes the graph on $V$ whose edges are the links of $F$.

• A spanning subtree of $G$ is a set $F$ of edges of $G$ such that $H(F)$ is a tree on $V$. Its length is $\ell_w(F) = \sum_{e \in F} w(e)$.
• A shortest spanning subtree (SSS) is a spanning subtree of least length among all spanning subtrees of $G$. Prim's dictionary is "shortest connection network (SCN) ↔ shortest spanning subtree (SSS)". $L(G,w)$ denotes that least length.
• Given the links $F$ made so far, the connected components of $H(F)$ are the isolated terminals (one terminal) and isolated fragments (two or more terminals).
• Principle 1: any isolated terminal $t$ can be connected to a nearest neighbor, a $G$-neighbor $n$ with $w(\{t,n\}) \le w(\{t,m\})$ for all $G$-neighbors $m$ of $t$.
• Principle 2: any isolated fragment $C$ can be connected to a nearest neighbor $n \notin C$ by a shortest available link $\{u,n\}$, $u \in C$; equivalently $\{u,n\}$ is a shortest edge of $G$ with one end in $C$ and the other outside.
• A construction is a sequence of links $e_0, e_1, \dots$, each an application of P1 or P2 with respect to the links before it. It is complete when it has $N-1$ links.

Only edges of $G$ are possible links; in Prim's distance table a missing edge has length $\infty$.

Formalization targets

Goal (§IV, p. 1396)

For every finite connected graph $G$ and every $w$,

$$\Bigl(\exists\ \text{a complete construction}\Bigr) \ \wedge\ \Bigl(\forall\ \text{complete constructions } e_0,\dots,e_{N-2}:\ \{e_0,\dots,e_{N-2}\} \text{ is a SSS of } G\Bigr).$$

This is the sentence "P1 and P2 will provide a SSS for any connected labelled graph with any set of real edge lengths." It fixes nothing about the order of applications, the component chosen, or the tie-breaking.

Milestones

1. Counting (§II, p. 1392): after any construction with $k$ links, $H(F)$ is acyclic with $N-k$ components; a complete construction is a spanning subtree; a construction with fewer than $N-1$ links can be extended.
2. Necessary Condition 1 (p. 1392): every terminal of a SSS is linked in it to at least one nearest neighbor.
3. Necessary Condition 2 (p. 1392): every fragment $S$ of a SSS, $\emptyset \ne S \ne V$, is linked in it to a nearest neighbor by a shortest available link.
4. Distinct lengths (§III, p. 1393): if the edge lengths are pairwise distinct, every link of every construction belongs to every SSS.
5. Continuity (§III, p. 1394): $w \mapsto L(G,w)$ is continuous.

Significance

The goal is the correctness theorem of a whole family of greedy minimum spanning tree procedures at once: Jarník–Prim (one growing fragment), Kruskal (globally shortest link first) and Borůvka-style interleavings all produce sequences of P1/P2 applications. Because lengths are arbitrary reals, it also covers maximum spanning trees by a sign change (p. 1397) and graphs that are not complete.

The result is classical and fully proved in the literature. What this mission adds is a machine-checked statement in exactly Prim's generality. Mathlib has spanning trees of connected graphs (SimpleGraph.Connected.exists_isTree_le) and the edge count of trees, but no minimum spanning tree theory. Existing Prove2Me items on minimum spanning trees are either restricted to complete graphs with distance matrices or state a cut property in existence form at a single vertex; none states Prim's principles or his necessary conditions.

Difficulty

The obvious argument, "each link P1 or P2 adds belongs to the shortest network", uses a unique shortest network, and that fails with ties: when two links tie, a P1/P2 link need not lie in a given SSS. Prim's own treatment of ties (§III) is an informal perturbation argument; the formal statement must hold for every tie-breaking choice made during a construction, not only for a generic perturbed instance. Negative lengths remove the easy reading "shortest connected spanning subgraph": the minimum must range over trees only. The statements also involve the component structure of $H(F)$ as it changes during a construction, and tree paths in an arbitrary, not necessarily complete, graph.

Formalization scope

Namespace ShortestConnection.Principles, Mathlib SimpleGraph. Conventions:

• $V$ is a Fintype with decidable equality; $G$ is a SimpleGraph V (at most one link per pair, no loops, which is Prim's setting). Lengths are w : Sym2 V → ℝ; only values on edges of $G$ matter.
• Link sets are Finset (Sym2 V); linkGraph F is SimpleGraph.fromEdgeSet F. A spanning subtree requires ↑F ⊆ G.edgeSet and (linkGraph F).IsTree.
• An isolated fragment is a whole connected component of linkGraph F; the P2 condition is a single inequality against every $G$-edge leaving it, which is equivalent to "nearest neighbor and shortest link" in Prim's sense.
• A construction is a List (Sym2 V) checked entrywise against l.take i; complete means length Fintype.card V - 1 (natural subtraction, used only for nonempty $V$).
• $L$ is sInf of the lengths of spanning subtrees; continuity is in the product topology.

Implicit hypotheses made explicit: $G$ connected (hence $V \ne \emptyset$) wherever an SSS or a complete construction is involved; at least two terminals for Necessary Condition 1; $S$ nonempty and $S \ne V$ for Necessary Condition 2; pairwise distinct edge lengths only in milestone 4, as in the paper's temporary assumption.

The goal's existence clause rules out a vacuous formalization in which no complete construction exists; the step predicates are defined from lengths and components only, never through shortest spanning subtrees, and they are not restricted to one growing fragment or to the globally shortest link.

Needed infrastructure: tree exchange (adding an edge to a spanning tree creates one cycle; removing any other cycle edge yields a spanning tree), component counts under edge addition, and minima of finitely many continuous functions. The exchange and counting lemmas are reusable for any matroid-greedy or spanning-tree mission. Contributions of intermediate lemmas, and proofs of the milestones in any order, are welcome.

Selected references

• R. C. Prim, Shortest Connection Networks And Some Generalizations, Bell System Technical Journal 36 (1957), 1389–1401. https://doi.org/10.1002/j.1538-7305.1957.tb01515.x
• J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proceedings of the AMS 7 (1956), 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7
• V. Jarník, O jistém problému minimálním, Práce Moravské Přírodovědecké Společnosti 6 (1930), 57–63.
• O. Borůvka, O jistém problému minimálním, Práce Moravské Přírodovědecké Společnosti 3 (1926), 37–58.
• R. L. Graham, P. Hell, On the history of the minimum spanning tree problem, Annals of the History of Computing 7 (1985), 43–57. https://doi.org/10.1109/MAHC.1985.10011

Motivation

A maximal independent set (MIS) of a graph is a set of vertices, no two adjacent, to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be found fast in parallel was a central question of parallel complexity in the early 1980s: an MIS algorithm is a subroutine for maximal matching, vertex colouring with $\Delta + 1$ colours, and many other symmetry-breaking tasks.

• Karp and Wigderson (STOC 1984; J. ACM 32, 1985) gave the first fast parallel algorithms for MIS: a randomized one and a deterministic one, both with running time $O((\log n)^4)$, placing MIS in NC$^4$.
• Luby (SIAM J. Comput. 15(4), 1986) gave the Monte Carlo algorithms analysed in this mission, together with a derandomization that yields a deterministic EREW P-RAM algorithm with $O((\log n)^2)$ running time, placing MIS in NC$^2$. Alon, Babai and Itai (J. Algorithms 7, 1986) independently found a Monte Carlo algorithm similar to Algorithm B.

Luby's algorithm is the standard textbook example of a randomized parallel algorithm and remains the basis of distributed MIS algorithms in the LOCAL model. Its analysis rests on one statement, Theorem 1 of the paper, which this mission formalizes.

Setting

All algorithms in the paper run the same loop on a finite simple undirected input graph $G = (V, E)$ with $n = |V|$ vertices. The current graph is $G' = (V', E')$, initially $G$. For $W \subseteq V'$ the neighbourhood is $N(W) = \{ i \in V' : \exists j \in W,\ (i,j) \in E' \}$. One execution of the loop body selects a set $I' \subseteq V'$ independent in $G'$, adds it to the output, and replaces $G'$ by the subgraph induced on $V' - (I' \cup N(I'))$. The loop stops when $G'$ is empty.

For $i \in V'$ write $\mathrm{adj}(i)$ for its neighbours and $d(i) = |\mathrm{adj}(i)|$ for its degree. The two Monte Carlo select steps are:

• Algorithm A. Every vertex draws a priority $\pi(i)$ uniformly from $\{1, \dots, n^4\}$, independently. A vertex enters $I'$ when its priority is strictly smaller than the priority of each of its neighbours.
• Algorithm B. Every vertex independently sets $\mathrm{coin}(i) = 1$ with probability $1/(2d(i))$, or always if $d(i) = 0$. Let $X$ be the set of vertices with coin $1$. A vertex of $X$ enters $I'$ when each of its neighbours in $X$ has strictly smaller degree.

Let $Y_k$ be the number of edges of $E'$ before the $k$-th execution of the loop body. The number of edges eliminated by that execution is $Y_k - Y_{k+1}$: exactly the edges of $G'$ with at least one endpoint in $I' \cup N(I')$. For $d(i) \ge 1$ the paper uses the weight $\mathrm{sum}(i) = \sum_{j \in \mathrm{adj}(i)} 1/d(j)$.

Formalization targets

Goal: Theorem 1

For the current graph $G'$ and $n \ge \max(1, |V'|)$,

$$E\big[Y_k^A - Y_{k+1}^A\big] \ge \tfrac18\, Y_k^A - \tfrac1{16}, \qquad E\big[Y_k^B - Y_{k+1}^B\big] \ge \tfrac18\, Y_k^B .$$

The constants are those printed in the paper. No connectivity, degree or size condition on $G'$ is assumed.

Milestones

1. §3.2, p. 1040. The priorities of Algorithm A are pairwise distinct with probability at least $1 - 1/(2n^2)$.
2. TECHNICAL LEMMA, p. 1043. For $p_1 \ge \dots \ge p_n \ge 0$ and $c > 0$, with $\alpha_l = \sum_{j \le l} p_j$, $\beta_l = \sum_{j < k \le l} p_j p_k$ and $\gamma_l = \alpha_l - c\beta_l$,

$$\max_{1 \le l \le n} \gamma_l \ge \tfrac12 \min\{\alpha_n, 1/c\}.$$

3. LEMMA A (Beame), p. 1041. For Algorithm A and $d(i) \ge 1$,

$$\Pr[i \in N(I')] \ge \big[\tfrac14\min\{\mathrm{sum}(i), 1\}\big]\big(1 - \tfrac{1}{2n^2}\big).$$

4. LEMMA B, p. 1042. For Algorithm B and $d(i) \ge 1$,

$$\Pr[i \in N(I')] \ge \tfrac14 \min\{\mathrm{sum}(i)/2, 1\}.$$

5. Proof of Theorem 1, first display, p. 1041. For any random choice of $I'$,

$$E[Y_k - Y_{k+1}] \ge \tfrac12 \sum_i d(i)\Pr[i \in I' \cup N(I')] \ge \tfrac12 \sum_i d(i) \Pr[i \in N(I')].$$

6. Proof of Theorem 1, closing chain, p. 1041.

$$\tfrac12 \sum_{\mathrm{sum}(i) \le 2} d(i)\,\mathrm{sum}(i) + \sum_{\mathrm{sum}(i) > 2} d(i) \ge |E'|.$$

Significance

Theorem 1 says that each round removes, in expectation, a constant fraction of the remaining edges. From it the paper derives that the expected number of rounds of either algorithm is $O(\log n)$, and hence that MIS has a Monte Carlo algorithm running in $O(\log n)$ expected time on a CRCW P-RAM and $O((\log n)^2)$ on an EREW P-RAM with $O(m)$ processors. Algorithm B and the proof of part (2) are also the basis of the paper's deterministic algorithm: the analysis of Lemma B uses only pairwise independence of the coins. The companion mission (A Simple Parallel Algorithm for the Maximal Independent Set Problem II) formalizes that derandomization and reuses the statements of milestones 2, 5 and 6.

The results are proved in the paper and reproduced in textbooks (e.g. Motwani and Raghavan, Randomized Algorithms), but not formalized: no statement of Theorem 1, Lemma A or Lemma B was found on the platform. A formal proof would make the per-round analysis of a standard parallel randomized algorithm reusable. That includes the degree-weighted counting of milestone 6 and the Bonferroni-type bound of the Technical Lemma, both of which recur in later analyses of distributed symmetry breaking.

Difficulty

The obvious argument tries to show that a fixed vertex enters $I'$ with good probability. That fails, because a high-degree vertex rarely wins against all its neighbours. The analysis instead bounds the probability that a vertex is removed, i.e. lands in $N(I')$. This event is a union over neighbours of dependent events, so the first Bonferroni inequality alone does not give a lower bound: the pairwise-intersection terms must be controlled. The union bound can also be very lossy when $\mathrm{sum}(i)$ is large, which is why the conclusion involves a minimum with a constant.

A second obstacle is the passage from vertices to edges: vertices of small $\mathrm{sum}(i)$ can have high degree while contributing little probability. The per-vertex bounds therefore have to be summed with degree weights and redistributed over edges. For Algorithm A there is an additional complication: priorities from $\{1, \dots, n^4\}$ can collide, so the argument about a uniformly random order holds only on the event that $\pi$ is injective. That event appears as the factor $1 - 1/(2n^2)$.

Formalization scope

• Graph. The current graph $G'$ is a SimpleGraph V on a finite type with decidable adjacency, and $V' = V$. The degree is SimpleGraph.degree, $\mathrm{adj}(i)$ is neighborFinset, and $Y_k = |E'|$ is edgeFinset.card.
• Conditional form. Theorem 1 is stated for a fixed current graph $G'$, i.e. conditionally on the first $k - 1$ rounds, as in the paper's proof. The unconditional statement follows by averaging.
• Input size. $n$ is a parameter with $1 \le n$ and $|V'| \le n$. It is not fixed to $|V'|$, which would cover only the first round.
• Select steps. Both endpoints' ALGEDGE runs are applied to every edge, since $E'$ contains each edge in both orientations. Hence Algorithm A keeps $i$ iff $\pi(i) < \pi(j)$ for all neighbours $j$. Algorithm B keeps $i \in X$ iff $d(j) < d(i)$ for all neighbours $j \in X$. Algorithm B's $I'$ starts at $X$; the page leaves $I'$ uninitialized in §3.3, and Algorithm D's code (p. 1047) has $I' \leftarrow X$.
• Laws. Probabilities and expectations are explicit finite sums: uniform over the $(n^4)^{|V|}$ priority vectors, and the product law over the $2^{|V|}$ coin vectors. A coin of an isolated vertex is $1$ with probability $1$, as on the page.
• Milestones. Milestone 5 is stated for an arbitrary finite distribution of $I'$, which contains both algorithms' laws. Milestone 6 divides out the common factor $\tfrac18$ of the printed chain.

Theorem 1 is false for arbitrary distributions of priorities or coins. A formalization that takes "Pr" as an unconstrained parameter, conditions on the event of interest, or replaces $n$ by $|V'|$ does not state the paper's theorem.

A complete development needs finite product probability spaces, inclusion–exclusion (Bonferroni) inequalities for finite unions, the symmetry of uniform priorities conditioned on injectivity, and degree-sum identities (SimpleGraph.sum_degrees_eq_twice_card_edges). The Technical Lemma and milestones 5 and 6 are reusable beyond this mission. Proofs of any milestone, and alternative proofs of Lemmas A and B, are welcome.

Selected references

• M. Luby, A Simple Parallel Algorithm for the Maximal Independent Set Problem, SIAM J. Comput. 15(4):1036–1053, 1986. https://doi.org/10.1137/0215074
• R. M. Karp and A. Wigderson, A Fast Parallel Algorithm for the Maximal Independent Set Problem, J. ACM 32(4):762–773, 1985. https://doi.org/10.1145/4221.4226
• N. Alon, L. Babai and A. Itai, A Fast and Simple Randomized Parallel Algorithm for the Maximal Independent Set Problem, J. Algorithms 7(4):567–583, 1986. https://doi.org/10.1016/0196-6774(86)90019-2
• R. Motwani and P. Raghavan, Randomized Algorithms, Cambridge University Press, 1995. https://doi.org/10.1017/CBO9780511814075

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

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

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

Selected references

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

Motivation

A matching of a graph is a set of edges no two of which share a vertex. A matching with as many edges as possible is a basic object of combinatorial optimization. Assignment problems, pairing and scheduling problems, and the Chinese postman problem reduce to it, and it is the standard example of a problem with a polynomial-time algorithm that is not an instance of linear programming over a bipartite structure.

For bipartite graphs the problem was settled by the 1950s, through the theorems of König and Hall and the Hungarian method of Kuhn, whose correctness rests on linear programming duality. As Berge notes on p. 842, that duality "no longer subsists when the graph is not bipartite". C. Berge's three-page note of 1957 (doi:10.1073/pnas.43.9.842) gave the criterion that works for every graph: a matching is maximum exactly when it admits no augmenting chain.

Timeline.

• 1931–1935: König and Hall characterize maximum matchings and systems of distinct representatives in bipartite graphs.
• 1947: Tutte characterizes graphs with a perfect matching (doi:10.1112/jlms/s1-22.2.107).
• 1950: Gallai studies the structure of graphs with respect to their maximum matchings (cited by Berge as the source of his Lemma 1).
• 1955: Kuhn gives the Hungarian method for the bipartite assignment problem (doi:10.1002/nav.3800020109).
• 1957: Berge proves that a matching is maximum if and only if no alternating chain joins two neutral points (Theorem 1 of this paper).
• 1965: Edmonds turns the criterion into a polynomial-time algorithm for general graphs by shrinking odd cycles ("blossoms") (doi:10.4153/CJM-1965-045-4).

Setting

Let $G = (X, U)$ be a finite graph without loops or multiple edges, with vertex set $X$ and edge set $U$. A matching is a set $V_0 \subseteq U$ of edges no two of which have a vertex in common. Its size $|V_0|$ is its number of edges. A matching is maximum if no matching of $G$ has more edges. This is a statement about cardinality: a matching to which no edge can be added (maximal under inclusion) need not be maximum.

Fix a matching $V_0$. Its edges are strong, all other edges weak. A vertex is neutral if no strong edge contains it, and $N$ is the set of neutral points. An alternating chain is a walk in $G$ that does not use the same edge twice and in which, of any two consecutive edges, one is strong and the other weak. Vertices may repeat.

For the milestones, Berge adds a new vertex $\bar a$ joined by strong edges to every neutral point, which gives a graph $\bar G$. Whenever an alternating chain of $\bar G$ runs from $\bar a$ to a vertex $x$, its last edge $(z, x)$ carries an arrow from $z$ to $x$. The non-neutral vertices then fall into four classes:

• $I$, the inaccessible points, at which no edge carries an arrow;
• $W$, the weak points, which receive arrows on weak edges only;
• $S$, the strong points, which receive arrows on strong edges only;
• the medium points, which receive both kinds.

The mission's Lean development uses the same names: IsNeutral, IsAlternatingChain, IsMaximumMatching, barGraph, Arrow, IsInaccessible, IsWeakPt, IsStrongPt, IsMedium.

Formalization targets

Goal: Theorem 1 (p. 843)

$$V_0 \text{ is maximum} \iff \text{no alternating chain connects a neutral point } a \text{ to a neutral point } a' \ne a .$$

The statement fixes nothing beyond finiteness: the graph need not be connected, and no bound on its size is assumed.

Milestones

1. Proof of Theorem 1, first paragraph. An alternating chain $W$ between distinct neutral points makes $(V_0 \setminus W) \cup (W \setminus V_0)$ a larger matching.
2. Lemma 5. If $|N| \le 1$, then $V_0$ is maximum.
3. Lemma 2. If $\bar a$ is inaccessible, then $S \cup N$ is internally stable (an independent set).
4. Lemma 3. If $\bar a$ is inaccessible and there are no medium and no inaccessible points, then $S \cup N$ is a maximum internally stable set, $W$ is a minimum cover, and $V_0$ is maximum.
5. Lemma 4. If $\bar a$ is inaccessible, the edges leaving a connected component $Z$ of $I$ are weak and carry no arrow, the outside neighbours of $Z$ are weak points, and $|Z| \ge 2$.
6. Lemma 1 (Gallai), corrected. If $\bar a$ is inaccessible, the components of the medium points, enlarged by the neutral points that receive a weak arrow, have exactly one strong edge entering them, have all other boundary edges weak and directed outward, and have at least three vertices.

Significance

Theorem 1 reduces the optimality of a matching, a statement about all matchings of the graph, to the absence of one kind of local structure. Its consequences include:

• correctness of every augmenting-path algorithm for maximum matching, including Edmonds' blossom algorithm and the Hopcroft–Karp and Micali–Vazirani refinements;
• the standard proofs of the Tutte–Berge formula and of the Gallai–Edmonds structure theorem, which start from it.

A matching that is not maximum can be certified by exhibiting the chain, and a maximum matching is certified by the labelling of Lemmas 1–4.

Theorem 1 has been proved since 1957 and appears in every textbook on matching theory. It is not formalized in Mathlib at the revision this mission uses. Mathlib has matchings as subgraphs, perfect matchings, alternating cycles and Tutte's theorem, but no augmenting-path characterization. This mission adds a formal statement of the theorem, together with the labelling of Berge's proof in a form that later missions on Edmonds' algorithm can reuse.

Difficulty

The "only if" direction is a local computation: the symmetric difference along an augmenting chain is again a matching, with one more edge. Even this needs care, because an alternating chain is only a trail and may a priori revisit vertices, while the augmentation needs a path.

The converse is the substance. In bipartite graphs, a search from the neutral points that alternates weak and strong edges labels each vertex at most one way, and its failure yields a cover of the same size as the matching. In general graphs an odd cycle lets a vertex be reached both through a strong and through a weak edge (the medium points). The bipartite labelling then fails, and no cover of size $|V_0|$ need exist: in a triangle the maximum matching has one edge and the minimum cover two. The proof has to treat these odd structures separately, and that is what Lemmas 1 and 4 do.

Formalization scope

• Graphs and matchings. The graph is a Mathlib SimpleGraph V on a Fintype V. The paper's "unoriented graph (or 1-dimensional regular complex)" may have parallel edges, but a matching uses at most one edge of a parallel class, so nothing is lost. The matching is a subgraph M with M.IsMatching, and its size is M.edgeSet.ncard. Maximum means cardinality-maximum over all matching subgraphs. Internally stable sets and covers are Mathlib's IsIndepSet and IsVertexCover.
• Alternating chains. An alternating chain is a walk that is a trail (no repeated edge; vertices may repeat), with alternation between consecutive edges.
• $\bar G$ and arrows. $\bar G$ lives on Option V, with $\bar a$ = none. An arrow needs an alternating chain of positive length from $\bar a$.
• Readings of ambiguous phrases.
  • "$\bar a$ is inaccessible" means that no arrow is directed to $\bar a$. Read literally ("not adjacent to a directed edge"), the phrase fails whenever $N \neq \emptyset$.
  • "Edges adjacent to $Z$" (and to $Y$) are the edges with exactly one endpoint in the set.
  • The paper's medium class $M$ is IsMedium in Lean, because M names the matching.
• Results not formalized.
  • Lemma 1 is false as printed. On a triangle with one matched edge, the two medium points form $Y$ with $|Y| = 2$, and their neighbour is neutral. The mission states a corrected form, labelled as such, in which neutral blossom bases are added to $Y$.
  • Lemma 6 (shrinking) is false. On the path $u$–$x$–$y$–$v$ with extra edges $y$–$t$, $t$–$q$, the set $A = \{x, y, t\}$ and $V_0 = \{xy, tq\}$, the matching is maximum on $A$ and on the shrunk graph, yet $\{ux, yv, tq\}$ is larger.
  • Theorem 2 (a minimum cover built from the labels) is false. Take a neutral vertex joined to the stems of two triangles, with the stems and the triangles matched. The construction yields a cover of 6 vertices, while one of 5 exists.
  • Neither false result is formalized, and the cases of the proof of Theorem 1 that rest on them are not milestones. The algorithmic remarks on p. 844 are procedures, not claims, and are not formalized either.
• Ruled-out trivializations. None of the following is a faithful encoding:
  • reading "maximum" as inclusion-maximal;
  • allowing an alternating chain to join a neutral point to itself (the one-vertex chain would then always exist);
  • reading "$\bar a$ is inaccessible" in a way that is never or always true;
  • imposing alternation on only some pairs of edges.

Any proof of the goal is welcome, whether it follows Berge's induction, uses the symmetric difference of two matchings, or goes through the Tutte–Berge formula. Reusable infrastructure is especially welcome: augmentation along a path, the symmetric difference of two matchings as a union of paths and cycles, and trails that alternate with respect to a matching.

Selected references

• C. Berge, Two theorems in graph theory, Proc. Natl. Acad. Sci. USA 43(9) (1957), 842–844. doi:10.1073/pnas.43.9.842
• W. T. Tutte, The factorization of linear graphs, J. London Math. Soc. 22 (1947), 107–111. doi:10.1112/jlms/s1-22.2.107
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955), 83–97. doi:10.1002/nav.3800020109
• J. Edmonds, Paths, trees, and flowers, Canadian J. Math. 17 (1965), 449–467. doi:10.4153/CJM-1965-045-4

Motivation

The question behind this mission was posed by T. E. Harris to L. R. Ford, Jr. and D. R. Fulkerson at RAND, in the setting of rail transport: given a rail network linking two cities, with a capacity on every link, find the largest steady flow from one city to the other. Ford and Fulkerson's answer, the minimal cut theorem, published in the Canadian Journal of Mathematics in 1956 (DOI 10.4153/CJM-1956-045-5), says that the obvious upper bound, the total capacity of a set of links whose removal separates the two cities, is always achieved by some flow.

The theorem became the starting point of network flow theory, and through it of a large part of combinatorial optimization and operations research: transportation, assignment, scheduling and network reliability problems are routinely reduced to it.

Timeline.

• 1927: K. Menger proves that the minimum number of vertices separating two vertex sets of a graph equals the maximum number of disjoint paths joining them (Fund. Math. 10), the unit-capacity ancestor of the theorem.
• 1955: Harris and Ross study the Soviet rail network as a capacity problem in a RAND report; Harris formulates the maximal flow problem (Schrijver's historical account: Math. Program. 91, 2002).
• 1956: Ford and Fulkerson publish the minimal cut theorem for undirected networks, with a non-constructive proof based on maximal flows (this paper). Independently, Elias, Feinstein and Shannon state and prove the max-flow min-cut theorem for directed networks (IRE Trans. Inf. Theory 2, 1956), and Dantzig and Fulkerson obtain it from linear programming duality.
• 1956–1962: Ford and Fulkerson's labelling (augmenting path) algorithm, collected in Flows in Networks (Princeton, 1962).
• 1972: Edmonds and Karp give polynomial bounds for augmenting-path methods (J. ACM 19).

Setting

A network $N$ consists of a finite set of vertices $V$, a finite set of arcs $E$, two distinct vertices, the source $a$ and the sink $b$, and a positive capacity $c(e)>0$ on every arc. Each arc $e$ has two distinct end vertices; arcs are undirected, and several arcs may join the same pair of vertices.

A chain joining $u$ and $w$ is a set of distinct arcs that can be arranged as $\alpha_1(v_0v_1),\alpha_2(v_1v_2),\dots,\alpha_m(v_{m-1}v_m)$ with $v_0=u$, $v_m=w$ and the vertices $v_0,\dots,v_m$ pairwise distinct; each arc may be traversed in either direction. The null chain ($m=0$) joins $u$ to itself.

A flow $f$ assigns a number $f(C)\ge 0$ to each chain $C$ joining $a$ and $b$ (and $0$ to every other set of arcs) such that the load $\ell_f(e)=\sum_{C\ni e}f(C)$ satisfies $\ell_f(e)\le c(e)$ for every arc. Its value is $\mathrm{val}(f)=\sum_C f(C)$. An arc is saturated by $f$ if $\ell_f(e)=c(e)$. A maximal flow is a flow of largest value.

A set $D$ of arcs is a disconnecting set if every chain joining $a$ and $b$ contains an arc of $D$; its value is $v(D)=\sum_{e\in D}c(e)$. A cut is a disconnecting set no proper subset of which is disconnecting.

The proof introduces two further objects: the set $S$ of arcs saturated by every maximal flow, and the set $L\subseteq S$ of left arcs, those arcs of $S$ whose left vertex (the end vertex met first by a positive chain flow of a maximal flow, travelling from $a$) can be reached from $a$ by a chain with no arc saturated by some maximal flow.

Formalization targets

Goal: Theorem 1 (Minimal cut theorem), p. 400

$$\exists\, m\in\mathbb R:\quad m=\max_{f\ \text{flow}}\mathrm{val}(f)=\min_{D\ \text{disconnecting}}v(D),$$

with both the maximum and the minimum attained. The statement mentions only flows and disconnecting sets, not the proof objects $S$ and $L$.

Milestones, in the order of the paper's proof

1. A maximal flow exists, and the set of maximal flows is convex (p. 400).
2. Lemma 1: $S$ is a disconnecting set (p. 400).
3. Every arc of $S$ receives the same orientation from all positive chain flows of all maximal flows: its left vertex is unique (pp. 400–401).
4. Lemma 2: $L$ is a disconnecting set (p. 401).
5. Lemma 3: no positive chain flow of a maximal flow contains more than one arc of $L$ (p. 401).
6. $\mathrm{val}(f)\le v(D)$ for every flow $f$ and every disconnecting set $D$ (p. 402).
7. $L$ is a cut of minimal value, and every maximal flow has value $v(L)$ (p. 402).

Two further statements of the paper are included as items without being milestones: the remark that a disconnecting set of minimal value is a cut (p. 400), and the Corollary (p. 402): if a set $A$ of arcs meets every cut in exactly one arc, adding $k$ to the capacity of each arc of $A$ raises the maximal flow value by $k$.

Significance

The minimal cut theorem turns a maximization over flows into a minimization over finite sets of arcs, so an optimal flow comes with a short certificate of optimality. It implies Menger's theorem (unit capacities), and through it König's theorem on bipartite matchings and Hall's marriage theorem. The Corollary is the tool behind the paper's own computing procedure for source–sink planar networks (§2, formalized in a companion mission).

The theorem is classical and proved. What this mission adds is a machine-checked proof of the paper's own formulation: undirected arcs, parallel arcs, flows decomposed along chains (path flows, with no circulations), and the minimum taken over arc sets meeting every chain, together with the proof's intermediate claims. Max-flow min-cut theorems already on the platform (Applied Combinatorics VIII, AppliedComb.Flows.max_flow_min_cut; Introduction to Linear Optimization X, LinearOptimization.max_flow_min_cut) concern directed networks with edge flows obeying conservation and cuts given by vertex sets. They are related results, not this statement, and connecting the two models is itself welcome work.

Difficulty

Weak duality (milestone 6) is immediate; the content is the reverse inequality. The obvious first step, taking a maximal flow and observing that its saturated arcs separate $a$ from $b$, does not finish the proof: a positive chain flow may pass through several saturated arcs, so the total capacity of the saturated arcs can exceed the flow value. One has to single out a disconnecting subset that every positive chain flow crosses exactly once, and there is no canonical choice from a single flow. The paper's sets $S$ and $L$ are defined from all maximal flows at once, and the work consists in showing that these sets are well behaved. The orientation claim in particular needs an exchange argument on two chains that cross at an arc, where the recombined arc sequences may revisit vertices and must be reduced to chains. In a formal development this "a walk contains a chain" step and the averaging of maximal flows over finitely many chains are the main bookkeeping costs.

Formalization scope

• A network is a structure on a vertex type V and an arc type E, both Fintype with decidable equality, with end-vertex maps tail, head (labels only, no direction), tail e ≠ head e, a source and a sink with source ≠ sink, and capacities cap : E → ℝ with 0 < cap e. These are the paper's standing assumptions; there are no others in §1. In particular, no planarity is assumed and an arc may join $a$ and $b$ directly.
• A chain is a Finset E that is the arc set of some arrangement (list of arcs, list of pairwise distinct vertices, each arc joining consecutive vertices in either order).
• A flow is a function f : Finset E → ℝ, non-negative, zero off the chains joining source and sink, with every arc load at most the capacity. A collection of chain flows that lists a chain twice merges into this form without changing the value or any load.
• "Maximal" means of maximum value. The goal is stated with IsGreatest and IsLeast on the sets of flow values and of values of disconnecting sets, so no supremum of a real set appears and both extrema must be attained.
• A trivializing formalization is ruled out: chains must be self-avoiding and must join the source and the sink, the disconnecting condition quantifies over exactly these chains, and the minimum ranges over all disconnecting sets rather than over a family chosen to match a given flow.
• Needed infrastructure: finite sums over Finset (Finset E), convexity in Finset E → ℝ, compactness of the flow polytope (for existence), and lemmas on lists (extracting a chain from a walk). The walk-to-chain lemma and weak duality are reusable for the companion mission and for any path-flow model.

Selected references

• L. R. Ford, Jr. and D. R. Fulkerson, Maximal Flow Through a Network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• P. Elias, A. Feinstein and C. E. Shannon, A note on the maximum flow through a network, IRE Transactions on Information Theory 2 (1956), 117–119. https://doi.org/10.1109/TIT.1956.1056816
• K. Menger, Zur allgemeinen Kurventheorie, Fundamenta Mathematicae 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115
• L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• J. Edmonds and R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19 (1972), 248–264. https://doi.org/10.1145/321694.321699
• A. Schrijver, On the history of the transportation and maximum flow problems, Mathematical Programming 91 (2002), 437–445. https://doi.org/10.1007/s101070100259