Graph Theory

Motivation

A matching in a graph is a set of edges no two of which share a node. Given a real weight on every edge, the maximum-weight matching problem asks for a matching of largest total weight. It is one of the basic problems of combinatorial optimization: assignment, pairing and scheduling problems reduce to it, and it is the standard example of a combinatorial problem that is solvable in polynomial time although it is not obviously a linear program.

For bipartite graphs the problem is a linear program in disguise: the polytope cut out by nonnegativity and the node-degree inequalities has only 0–1 vertices (the Birkhoff–von Neumann theorem in the square case; Mathlib has it as extremePoints_doublyStochastic). For general graphs this fails already on a triangle, where the vector with every coordinate $1/2$ satisfies all degree inequalities but is not a combination of matchings. Edmonds' 1965 paper (DOI 10.6028/jres.069b.013) adds one family of inequalities, one for each odd set of nodes, and proves that the resulting polyhedron has exactly the matching vectors as its vertices. The companion paper Paths, trees, and flowers gives the cardinality algorithm on which the weighted algorithm of §7 is built.

Timeline:

• 1931: König and Egerváry prove the min–max theorems for bipartite matching; 1946: Birkhoff shows that the doubly stochastic matrices are the convex hull of the permutation matrices (the bipartite perfect-matching polytope).
• 1947: Tutte characterizes graphs with a perfect matching.
• 1965: Edmonds, Paths, trees, and flowers: the blossom algorithm for maximum-cardinality matching.
• 1965: Edmonds, this paper: Theorem (P) (the matching polyhedron) and Theorem (M) (blossom-shrinking optimality certificates), with a weighted matching algorithm.

Setting

Let $G$ be a finite graph with node set $V$ and edge set $E$; each edge meets two different nodes, its ends. Real variables $x_e$ correspond to the edges $e\in E$. The polyhedron $C\subseteq\mathbb R^E$ is the set of vectors $x$ satisfying

1. $x_e\ge 0$ for every edge $e$;
2. $\sum_{e \text{ meets } v} x_e\le 1$ for every node $v$;
3. $\sum_{e \text{ has both ends in } S} x_e\le r$ for every set $S$ of $2r+1$ nodes, $r$ a strictly positive integer.

The matching vectors $P$ are the vectors with every component $0$ or $1$ that satisfy (2); they are the incidence vectors of matchings. For edge weights $c\in\mathbb R^E$, the linear form (4) is $W(c,x)=\sum_e c_e x_e$.

The dual program has a variable $y_v$ for each node and $z_S$ for each odd set $S$ ($|S|=2r_S+1$, $r_S\ge1$). Its objective is (5) $U(y,z)=\sum_v y_v+\sum_S r_S z_S$, subject to (6) $y,z\ge0$ and (7) $y_{v_1}+y_{v_2}+\sum_{S\ni v_1,v_2}z_S\ge c_e$ for every edge $e$ with ends $v_1,v_2$. For a matching $M$, conditions (8)–(10) are the complementary slackness conditions: $y_v=0$ at nodes not covered by $M$, equality in (7) on $M$, and every odd set with $z_S>0$ contains exactly $r_S$ edges of $M$.

A blossom sequence $\{G_i\}_{i=0}^n$ (Theorem (M)) starts from $G_0=G$ with matching $M_0=M$ and repeatedly shrinks an odd circuit $B_i$ (a blossom, $2a_i+1$ edges of which $a_i$ are matched) to a single node, carrying node weights $w(v^i)$ and edge weights $w(e^i)$ that obey conditions (a)–(k) of p. 127.

In the Lean development these are Graph, IsMatching, incidence, matchingPolyhedron ($C$), matchingVectors ($P$), W, U, DualFeasible ((6)–(7)), CompSlack ((8)–(10)) and BlossomSequence, all in the namespace EdmondsMatching65.Polyhedron.

Formalization targets

Goal: Theorem (P)

$$\operatorname{ext}(C)=P.$$

The vertices (extreme points) of $C$ are exactly the matching vectors of $G$. Hence the maximum weight of a matching equals $\max\{W(c,x):x\in C\}$ for every $c$.

Milestones

1. $P\subseteq\operatorname{ext}(C)$ (§2, p. 126).
2. If for every $c$ some 0–1 point of $C$ maximizes $W(c,\cdot)$ over $C$, then $\operatorname{ext}(C)=P$ (§2, p. 126).
3. Weak duality: $W(c,x)\le U(y,z)$ for $x\in C$ and $\langle y,z\rangle$ satisfying (6)–(7) (§3, p. 126).
4. If $M$ is a matching and $\langle y,z\rangle$ satisfies (6)–(10), then $W(c,\chi^M)=U(y,z)$ (§3, p. 127).
5. A blossom sequence for $M$ yields $\langle y,z\rangle$ satisfying (6)–(10) (§5, pp. 127–128).
6. For every $c$ some maximum matching has a blossom sequence (§6, p. 128).
7. Theorem (M): a matching is maximum if and only if a blossom sequence for it exists (§4, p. 127).
8. For every $c$ there are a matching $M$ and $\langle y,z\rangle$ satisfying (6)–(10) (§3, p. 127).

Significance

The result. Theorem (P) turns maximum-weight matching in general graphs into a linear program over an explicitly described polyhedron, and Theorem (M) with the §5 translation gives a short certificate of optimality for every maximum matching. Together they established the template of polyhedral combinatorics: describe the convex hull of the combinatorial objects by inequalities, and prove the description through linear programming duality and an algorithm. The matching polytope underlies the analysis of the weighted blossom algorithm, separation over odd-set inequalities (Padberg–Rao), and many later integrality results; Edmonds' own §8 states the extension to degree-constrained subgraphs.

Formalizing it. The theorem has been proved since 1965 and appears in every text on combinatorial optimization; this mission asks for a machine-checked proof of the polytope statement for general finite graphs, including parallel edges, together with the duality certificate and the blossom-sequence characterization. The prove2me platform has a proved form of Edmonds' perfect matching polytope theorem on complete graphs in convex-decomposition form (MetricTSP.pm_polytope_decomposition), a different polytope with a different conclusion; nothing states Theorem (P) or Theorem (M).

Difficulty

The inclusion $P\subseteq\operatorname{ext}(C)$ and weak duality are routine. The difficulty is the reverse inclusion: showing that no fractional point of $C$ is a vertex. The bipartite argument (a fractional point has a cycle of fractional edges along which it can be perturbed both ways) breaks on odd cycles: perturbing along an odd circuit violates a degree inequality, and the odd-set inequalities that cut off the half-integral points are exponentially many and overlap. The paper's route needs, for every weight vector, an optimal matching together with a dual solution satisfying (6)–(10), and the existence of that certificate is the substance of the weighted matching algorithm: the blossom sequence of Theorem (M) must be constructed, and the translation (11)–(16) from node and edge weights of the contracted graphs to $\langle y,z\rangle$ must be verified through the whole shrinking history.

Formalization scope

• The graph is a finite node type V, a finite edge type E and an end map ends : E → Sym2 V with no loops. Parallel edges are allowed: the contracted graphs of Theorem (M) have them, and Theorem (P) holds for multigraphs; simple graphs are the case of an injective end map.
• Vectors are E → ℝ, one coordinate per edge. Vertices are Mathlib's Set.extremePoints ℝ. Odd sets carry an explicit r : ℕ with 1 ≤ r and |S| = 2r + 1; even sets and singletons carry no inequality.
• Edge weights are arbitrary reals; matchings need not be perfect and may be empty. No connectivity, no parity of |V|.
• The dual variable z is a function on all node sets of which only odd sets are read.
• A contracted graph Gᵢ is a partition of V into blocks; an edge of G is an edge of Gᵢ when its ends lie in different blocks. Each Mᵢ must be a matching of Gᵢ, and all of (a)–(k) appear as fields of BlossomSequence; a sequence missing any of them would make milestone 6 trivial or milestone 5 false.
• A trivializing formalization is ruled out: coordinates indexed by node pairs (Sym2 V → ℝ) leave non-edge coordinates free and give a polyhedron with no extreme points, and the goal is stated as equality of extreme points, not as a convex-hull identity or as the existence of a dual certificate.
• Needed infrastructure: extreme points of polyhedra as unique maximizers of linear forms, finite LP weak duality over these index sets, and the weighted blossom algorithm (or another proof of milestone 8). The polyhedral lemmas are reusable for other integrality results; contributions on any milestone are welcome.

Selected references

• J. Edmonds, Maximum Matching and a Polyhedron With 0,1-Vertices, J. Res. Nat. Bur. Standards Sect. B 69B (1965), 125–130. https://doi.org/10.6028/jres.069b.013
• J. Edmonds, Paths, Trees, and Flowers, Canad. J. Math. 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
• W. T. Tutte, The Factorization of Linear Graphs, J. London Math. Soc. 22 (1947), 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
• M. W. Padberg, M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Math. Oper. Res. 7 (1982), 67–80. https://doi.org/10.1287/moor.7.1.67
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 25.

Motivation

Routing and network optimization often require the length of the best route between every ordered pair of points. Robert W. Floyd's Algorithm 97 gives a compact procedure for this task: it receives a matrix of direct-link lengths and changes the matrix in place until each entry is meant to represent a shortest-path length. The procedure is a small historical source for an algorithm now used as a standard all-pairs shortest-path routine. Its published text consists of the ALGOL code and a short explanatory comment, without a correctness proof.

The same page contains Floyd's Algorithm 96, a Boolean procedure for ancestor relations. Its output records whether a chain of parent links connects two individuals. Floyd cites Warshall's theorem on Boolean matrices in both comments. The Boolean procedure and the length procedure use the same order of three loops; together they expose the distinction between discovering that a route exists and determining its best length. This mission formalizes both claims from Floyd's published page, with the shortest-path statement as its goal.

Setting

A directed network has $n$ numbered points. Its length matrix $w$ assigns a real number $w(i,j)$ to a direct link from $i$ to $j$. The value $\infty$ means that the direct link is absent. Links may have negative lengths, and the initial diagonal entries $w(i,i)$ are unrestricted. The paper's matrix index range is $1,\ldots,n$; the Lean development uses $0,\ldots,n-1$ in the same order.

A path from $i$ to $j$ is a sequence $p_0=i,p_1,\ldots,p_L=j$ with $L\ge1$ links. The points $p_0,\ldots,p_{L-1}$ are distinct, as are $p_1,\ldots,p_L$. Thus a path between different points has no repeated point, while a path from a point to itself is a simple closed path with at least one link. Its length is $\ell_w(p)=\sum_{t=0}^{L-1}w(p_t,p_{t+1})$; a missing link gives length $\infty$. Write $d_w(i,j)$ for the minimum length among these paths, taking $d_w(i,j)=\infty$ when there is no finite-length path. Since $L\le n$, this is a minimum over a finite family.

The no-negative-cycle condition says that every closed path has nonnegative length. Individual links can still be negative. This condition matters because, in a network with a negative cycle, repeated travel around that cycle can keep reducing a walk's length. Floyd's comment does not state the condition, although the claimed output needs it.

Algorithm 97 scans a pivot $i$, then row $j$, then column $k$, each in increasing order. It enters the column scan when the current $m(j,i)$ is finite; if the current $m(i,k)$ is also finite, it computes $s=m(j,i)+m(i,k)$ and replaces $m(j,k)$ when $s<m(j,k)$. Every replacement affects subsequent reads of the same matrix. Algorithm 96 makes the corresponding Boolean update: when $m(j,i)$ and $m(i,k)$ are true, it sets $m(j,k)$ to true.

Formalization targets

Reachability and missing paths

For Algorithm 96, let $b^+$ be the transitive closure of the initial parent relation $b$, using chains of one or more links. Its comment asserts

$$\operatorname{ancestor}(b)(i,j)=\mathrm{true}\quad\Longleftrightarrow\quad i\mathrel{b^+}j.$$

For Algorithm 97, the separate unreachable-pair sentence asserts that, whenever no finite-length path runs from $i$ to $j$,

$$\operatorname{shortestPath}(w)(i,j)=\infty.$$

This second target needs no condition on cycle lengths. Both statements are milestones because they are claims printed in the two algorithm comments, rather than lemmas invented for the formalization.

Complete shortest-path matrix

The goal is the whole output claim of Algorithm 97. For every $n$, every matrix $w$ with no negative cycle, and all points $i,j$,

$$\operatorname{shortestPath}(w)(i,j)=d_w(i,j).$$

The equality includes paths with negative individual links, diagonal entries, and unreachable pairs. It fixes the entire final matrix, rather than only an upper or lower bound.

Significance

The goal connects an explicit in-place matrix program with a route-based definition of shortest length. Once established, it permits later formal developments to use the procedure as a justified all-pairs distance computation, including networks whose individual links have negative lengths. The Boolean milestone similarly identifies the final state of an ancestor procedure with the transitive closure of the initial relation. Neither assertion requires treating an implementation's output as the definition of the mathematical answer.

Floyd's 1962 paper states these outcomes but supplies no proof. This mission supplies precise Lean statements and definitions for a proof to target. A completed machine-checked development would establish the published procedure's correctness under the missing necessary premise. The statements in this proposal are currently open theorem targets; compiling their declarations checks syntax and types, not their proofs. Supporting work on finite paths, cycle decompositions, and matrix updates can be reused in other finite directed-network arguments.

Difficulty

The array is changed in place. During a pivot's sweep, an entry used in a later update may already differ from its value at the start of that pivot. The test on $m(j,i)$ is evaluated before the column loop, but the same entry is read again within every column iteration. A proof based only on a simultaneous, out-of-place matrix recurrence does not directly describe these reads. Negative individual links also prevent arguments that rely on every update decreasing only through a nonnegative segment. The no-negative-cycle condition must control what happens when a proposed route returns to a point already visited.

Formalization scope

Points are Fin n, including the empty network at $n=0$ and the single-point network at $n=1$. Lengths are WithTop ℝ, where ⊤ represents the paper's ₁₀10 sentinel as mathematical infinity. The paper's literal sentinel is $10^{10}$; a finite bound cannot represent arbitrarily long paths, so this mission uses infinity in its goal. The ALGOL real operations are represented by exact real arithmetic. The printed procedure's loop order, strict comparison, two finiteness guards, and immediate assignments are part of the Lean definition.

The initial diagonal is not normalized. Therefore a path from $i$ to itself has at least one link, and the final diagonal denotes a shortest closed-path length when one exists. The Boolean comment's “is true if” is read as an equivalence, supported by its following explanation of the final matrix; chains have one or more links, matching Lean's Relation.TransGen.

The sole added hypothesis in the main goal is absence of negative cycles. It is necessary: with one point and self-link length $-1$, the procedure changes that entry to $-2$, although the shortest simple closed path has length $-1$. No nonnegative-link or zero-diagonal premise is imposed. The unreachable-pair milestone omits the cycle hypothesis because its claim holds without it. The benchmark $d_w$ is a finite minimum of summed link lengths, defined independently of Algorithm 97; defining it from the procedure or its recurrence would empty the goal of its intended content. Contributions proving the printed algorithms' statements, or establishing reusable finite-path and update results needed for them, fit this scope.

Selected references

• Robert W. Floyd, Algorithm 97: Shortest Path, Communications of the ACM 5(6), 1962, p. 345. DOI 10.1145/367766.368168.
• Robert W. Floyd, Algorithm 96: Ancestor, Communications of the ACM 5(6), 1962, pp. 344–345, in the same published Algorithms department scan.

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

The traveling-salesman problem (TSP) asks for a cheapest cycle through all vertices of a weighted complete graph. Exact algorithms for it are branch-and-bound searches, and their size depends almost entirely on the quality of the lower bounds used to prune the search. In 1970 Held and Karp introduced the 1-tree bound: a Lagrangian relaxation of the degree-2 constraints of a tour, whose value can be evaluated by one minimum-spanning-tree computation (Held & Karp, Part I, 1970). Part II (Held & Karp, 1971) replaces the ascent procedure of Part I by an iterative method related to the relaxation method for linear inequalities of Agmon and of Motzkin and Schoenberg (1954), and with it solved to proven optimality every instance presented to it, up to 64 cities. The iteration is the prototype of what is now called the subgradient method with Polyak-type step sizes, and the 1-tree bound remains a standard lower bound in exact TSP codes.

Timeline:

• 1954 — Agmon; Motzkin and Schoenberg: the relaxation method for systems of linear inequalities, and convergence of Féjer-monotone sequences relative to full-dimensional sets.
• 1970 — Held and Karp (Part I): the 1-tree bound $\max_\pi w(\pi)$ and a column-generation / ascent method for it.
• 1971 — Held and Karp (Part II): the iteration $\pi^{m+1} = \pi^m + t_m v_{k(\pi^m)}$, its relaxation-method analysis (Lemmas 1–3) and the constant-step guarantee (Theorem 1).
• 1974 — Held, Wolfe and Crowder validate the method as general subgradient optimization.

Setting

Let $n \ge 3$ and let $(c_{ij})$ be a symmetric real $n\times n$ matrix of weights on the edges of the complete graph $K_n$ with vertex set $\{1,\dots,n\}$; weights may be negative and need not satisfy the triangle inequality. A subgraph has weight equal to the sum of its edge weights. A tour is a cycle through every vertex exactly once; $C^*$ is the weight of a minimum tour.

A 1-tree is a tree on the vertex set $\{2,\dots,n\}$ together with two distinct edges at vertex $1$. Index the 1-trees by $k$; let $c_k$ be the weight of the $k$-th 1-tree, $d_{ik}$ the degree of vertex $i$ in it, and $v_k \in \mathbb R^n$ the degree-excess vector with components $d_{ik}-2$. For $\pi \in \mathbb R^n$ define

$$w(\pi) = \min_k\,[c_k + \pi\cdot v_k].$$

A tour is a 1-tree with $v_k = 0$, so $C^* \ge w(\pi)$ for every $\pi$ (Eq. (2)); the best bound is $\max_\pi w(\pi)$. For a point $\pi$, $k(\pi)$ denotes a minimum-weight 1-tree at $\pi$, a 1-tree attaining the minimum defining $w(\pi)$. The ascent iteration (3) is

$$\pi^{m+1} = \pi^m + t_m\,v_{k(\pi^m)}.$$

For a target value $\bar w$, $P_{\bar w}$ is the polyhedron of solutions of $\bar w \le c_k + \pi\cdot v_k$ for all $k$ (system (5)). All norms $\|\cdot\|$ are Euclidean.

Formalization targets

Goal: Theorem 1

With constant step $t_m = \bar t > 0$, any starting point and any choice of minimum-weight 1-trees,

$$\sup_m w(\pi^m) \;\ge\; \max_\pi w(\pi) - \tfrac12\,\bar t\,\limsup_{m\to\infty}\|v_{k(\pi^m)}\|^2 .$$

Milestones

1. Eq. (2): $C^* \ge w(\pi)$ for every $\pi$.
2. Lemma 1: if $w(\bar\pi) \ge w(\pi)$ then $(\bar\pi-\pi)\cdot v_{k(\pi)} \ge w(\bar\pi) - w(\pi) \ge 0$.
3. Lemma 2: if $0 < t < 2(w(\bar\pi)-w(\pi))/\|v_{k(\pi)}\|^2$ then $\|\bar\pi - (\pi + t v_{k(\pi)})\| < \|\bar\pi-\pi\|$.
4. Féjer-monotone convergence (Motzkin–Schoenberg, quoted in the proof of Lemma 3): a sequence whose distance to every point of a set with nonempty interior is nonincreasing converges.
5. Lemma 3, Case 1: for $\bar w < \max_\pi w$ and the relaxation iteration

$$\pi^{m+1} = \pi^m + \lambda_m\,\frac{\bar w - w(\pi^m)}{\|v_{k(\pi^m)}\|^2}\,v_{k(\pi^m)} \qquad (6)$$

with $0<\varepsilon<\lambda_m\le 2$, the iterates enter $P_{\bar w}$ or converge to a boundary point of $P_{\bar w}$. 6. Lemma 3, Case 2: with $\lambda_m = 2$ the iterates enter $P_{\bar w}$. 7. §3 bound: the restricted minimum $w_{X,Y}(\pi)$ over 1-trees containing the edges $X$ and avoiding the edges $Y$ is a lower bound on every tour of the derived problem.

Milestones 1–5 are the steps of the paper's proof of Theorem 1; 6 and 7 are further results of the paper on the same objects.

Significance

Theorem 1 is the paper's justification of the step rule actually used in its computations: a fixed step $\bar t$ loses at most $\tfrac12\bar t$ times the asymptotic squared deviation of the generated 1-trees from being tours. Since $\|v_k\|^2$ is an even integer that vanishes exactly on tours, and the paper observes it is typically small in practice, the bound explains why the constant-step ascent reaches bounds sharp enough for branch-and-bound. Lemmas 1–3 are the first analysis of a subgradient-type method for a nonsmooth concave function, cast as the relaxation method for the (exponentially large) system (5).

All results are proved in the paper (except the Féjer-monotone convergence and Case 2 of Lemma 3, which it cites from Motzkin and Schoenberg). None is formalized: the platform has the 1-tree lower bound only under a metric assumption on the weights (SupplyChainTheory.held_karp_bound, SupplyChainTheory.one_tree_lower_bound), and the subtour-LP bound MetricTSP.held_karp_le_opt, a different object. This mission produces the bound for arbitrary real weights, the supergradient property of $v_{k(\pi)}$, and a machine-checked convergence analysis of the relaxation iteration.

Difficulty

Lemmas 1 and 2 and Eq. (2) are short once the finite minimum defining $w$ is handled. The difficulty is in Lemma 3 and Theorem 1. The iteration is not monotone in $w$, so no descent argument applies; progress is measured by the Euclidean distance to the target polyhedron $P_{\bar w}$, and turning distance decrease into convergence requires the Féjer-monotonicity theorem, which in turn needs $P_{\bar w}$ to have nonempty interior (from $\bar w < \max_\pi w$). In Theorem 1 the step is constant rather than of the relaxation form (6), and the target polyhedron is not given in advance: the relevant relaxation parameters are admissible only eventually and must be kept away from zero, which requires controlling degenerate directions $v_{k(\pi^m)} = 0$ and the behaviour of $w$ along an iteration that is not known a priori to stay bounded. A direct argument that $w(\pi^m)$ increases fails, since single steps can decrease $w$.

Formalization scope

Vertices are Fin n, the paper's vertex 1 is 0 : Fin n, and graphs are SimpleGraph (Fin n). Weights are c : Sym2 (Fin n) → ℝ, arbitrary reals. A 1-tree is a graph whose restriction to the vertices other than 0 is a tree and in which 0 has degree 2; a tour is a connected graph with all degrees 2. w(π) is the minimum of weight c G + ∑ i, π i * (deg G i − 2) over 1-trees, written as an sInf over a finite set that is nonempty for n ≥ 3; every theorem assumes 3 ≤ n. Euclidean norms and inner products are written as coordinate sums of squares and products, never Mathlib's sup norm on Fin n → ℝ. The minimum-weight 1-tree $k(\pi^m)$ is a hypothesis at every step, and ties may be broken arbitrarily. The goal is stated as "for every $\pi^*$ and $\delta>0$ some iterate has $w(\pi^m) > w(\pi^*) - \tfrac12\bar t L - \delta$", which is equivalent to the printed inequality; $L$ is the limsup of a sequence with finitely many values, a genuine real.

The statements exclude trivializing readings: the 1-tree predicate rejects graphs without exactly two edges at vertex 1; w is never a minimum over an empty set under the standing hypothesis 3 ≤ n; no ⨆ of a possibly unbounded family is used; the step size $\bar t$ and the parameter $\varepsilon$ are strictly positive.

A complete development needs finite minima of affine functions (concavity, attainment), 1-tree and tour combinatorics on simple graphs, and Féjer-monotone sequences in $\mathbb R^n$; the last two are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3, are welcome.

Selected references

• M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
• M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees, Operations Research 18 (1970) 1138–1162. https://doi.org/10.1287/opre.18.6.1138
• T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 393–404. https://doi.org/10.4153/CJM-1954-038-x
• S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 382–392. https://doi.org/10.4153/CJM-1954-037-2
• M. Held, P. Wolfe and H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223

Motivation

Two optimization problems on weighted networks sit at the base of operations research and algorithm design. The first asks for the cheapest way to connect every node of a network, such as a cable, pipeline or communication network. The answer is a minimum weight spanning tree. The second asks for the shortest route from a depot to every other node of a road or data network, the single-source shortest path problem. Chapter 12 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) treats both. It proves the structural lemmas behind the greedy spanning tree algorithms of Kruskal (1956) and Prim (1957), and the correctness of the shortest path algorithm of Dijkstra (1959).

The minimum spanning tree problem goes back to Borůvka (1926), who designed an electrical network for Moravia. Kruskal and Prim gave the two greedy algorithms taught today, and Dijkstra's 1959 note treated both problems. Dijkstra's shortest path method, with heap-based refinements such as Fredman and Tarjan (1987), remains the standard solver for non-negative lengths and a building block of routing, scheduling and network flow codes.

Setting

A graph $G = (V, E)$ has a finite vertex set $V$ and a set $E$ of 2-element subsets of $V$. A weight $w(e) \in \mathbb N_0$ is attached to each edge, and a set $S$ of edges has weight $w(S) = \sum_{e \in S} w(e)$. A spanning forest of $G$ is an acyclic graph $H = (V, S)$ with $S \subseteq E$. A spanning tree is a spanning forest that is connected. The weight of a spanning tree is the weight of its edge set. In Lean these are SimpleGraph V with [Fintype V], IsSpanningForest G H ($H \le G$ and acyclic), IsSpanningTree G T ($T \le G$ and a tree), and weight w T for a weight w : Sym2 V → ℕ.

A digraph $G = (V, E)$ has $E \subseteq V \times V$ with $x \ne y$ for every directed edge $(x, y)$. Each directed edge has a length $w(x, y) \in \mathbb N_0$. The length is extended by $w(x, y) = \infty$ for non-edges. A directed path from $a$ to $b$ is a sequence $(a = u_0, \dots, u_t = b)$ of distinct vertices in which consecutive pairs are directed edges. Its length is $\sum_{i<t} w(u_i, u_{i+1})$. The distance $\operatorname{dist}(a, b) \in \mathbb N_0 \cup \{\infty\}$ is the minimum length of a directed path from $a$ to $b$, and is $\infty$ when no such path exists. A shortest path is a directed path attaining it. In Lean this is WeightedDigraph V with ext, IsDirPath, pathLength, dist and IsShortestPath.

Dijkstra's algorithm (Algorithm 12.14) with root $r$ and $n = |V|$ keeps a sequence $\sigma$ of permanent vertices, a value $\delta(x) \in \mathbb N_0 \cup \{\infty\}$ and a sequence $P(x)$ for each vertex. Step 1 sets $\delta(r) = 0$, $P(r) = (r)$, $\sigma = (r)$, and $\delta(x) = w(r, x)$, $P(x) = (r, x)$ for $x \ne r$. Step $i$ with $1 < i < n$ scans from the last permanent vertex $v_i$. For every temporary $x$ it sets $\delta(x) \leftarrow \min\{\delta(x), \delta(v_i) + w(v_i, x)\}$, and on a strict decrease it replaces $P(x)$ by $P(v_i)$ followed by $x$. Each step ends by appending to $\sigma$ a temporary vertex of minimum $\delta$, chosen arbitrarily among ties. The algorithm halts at Step $n$. DijkstraRun G r i s holds when some sequence of admissible choices leads to state s at the start of Step $i$.

Formalization targets

Goal: correctness of Dijkstra's algorithm (Theorem 12.18)

For every halted state of every run, and every vertex $x$,

$$\delta(x) = \operatorname{dist}(r, x), \qquad \operatorname{dist}(r, x) < \infty \implies P(x) \text{ is a shortest path from } r \text{ to } x.$$

Milestones

1. Proposition 12.3. A spanning forest $H = (V, S)$ of a graph on $n \ge 1$ vertices has $|S| \le n - 1$ and exactly $n - |S|$ components. It is a spanning tree if and only if $|S| = n - 1$.
2. Proposition 12.4 (Exchange Principle). Let $T$ be a spanning tree and $xy \in E \setminus T$. Then $T$ contains a unique path $x = x_0, \dots, x_t = y$, and replacing any edge $x_i x_{i+1}$ of it by $xy$ gives a spanning tree.
3. Lemma 12.6. In a connected weighted graph, let $F$ be a spanning forest and $C$ a component of $F$. A minimum weight edge leaving $C$ lies in some spanning tree that has minimum weight among the spanning trees containing $F$.
4. Proposition 12.16. Every prefix and every suffix of a shortest path is a shortest path.
5. Proposition 12.17. When the algorithm halts, $\delta(v_1) \le \delta(v_2) \le \cdots \le \delta(v_n)$.

Milestones 4 and 5 are the two statements the book's proof of the goal rests on. Milestones 1–3 are the spanning tree half of the chapter. Lemma 12.6 is the result from which the book derives the correctness of Kruskal's and Prim's algorithms.

Significance

Theorem 12.18 certifies that one pass of $n$ steps computes all distances from $r$ and a shortest path tree, with no condition on the digraph beyond non-negative lengths. Lemma 12.6 is the cut property. Every greedy minimum spanning tree method (Kruskal, Prim, Borůvka) is an instance of it, and the exchange principle is the matroid basis-exchange axiom specialised to the graphic matroid.

All of these results are classical and proved. None is formalized in this form on the platform. Mathlib has spanning trees of connected graphs, uniqueness of paths in acyclic graphs, and the edge count $n - 1$ of a tree. It has no edge–component count for forests, no exchange principle, no weighted spanning trees, and no Dijkstra. On Prove2Me, FamousTheorems.tree_card_edges_6b and ClassicalGaps.isAcyclic_edges_eq_card_sub_one_imp_connected cover only the tree case of Proposition 12.3. KServer.mst_cut_property is a cut property for complete graphs encoded by parent maps, a different statement. The label-correcting algorithm of Dynamic Programming and Optimal Control II (BertsekasDP.label_correcting_*) is a different algorithm: it keeps an open list and scans in arbitrary order, not by minimum label.

Difficulty

The goal is a statement about the final state of a run, but the facts it depends on only become visible across steps: a permanent vertex's $\delta$ and $P$ never change again, and $\delta(x)$ is always the length of the current $P(x)$. None of this is recorded in the final state itself. An argument over the steps of the run has to show that each $P(x)$ remains a path with distinct vertices, including when edges of length $0$ allow ties. It also has to handle the value $\infty$, where $\infty + a = \infty$ and a comparison between two infinite values never counts as a decrease. Tie-breaking is arbitrary, so no argument may depend on which minimum is chosen. For Lemma 12.6 the difficulty is the exchange step: removing an edge of a tree path and adding a crossing edge must again give a tree that still contains the forest $F$, and this is a statement about cycles and components, not about counts.

Formalization scope

• Graphs are SimpleGraph V over a Fintype V. Weights are Sym2 V → ℕ (the book's $w : E \to \mathbb N_0$; values off $E$ are never used). Acyclic, tree and connected components are Mathlib's. In Proposition 12.3, $|S| = n - k$ is written $|S| + k = n$ and $n \ge 1$ is assumed, which the bound $n - 1$ presupposes.
• Lemma 12.6 assumes $G$ connected, the section's standing assumption (p. 239). The page's "to avoid trivialities, we assume $n \ge 3$" is not imposed, because the statement holds for every $n$. The crossing edge may have either endpoint in $C$.
• Lengths in the digraph are ℕ, and $\delta$ and distances are ℕ∞, where $\infty$ is ⊤, never a large finite number. A version with real or ℝ≥0 lengths would be a generalization and is not what is asked.
• Dijkstra's algorithm is defined step by step exactly as on pp. 246–247, including $\delta(x) = w(r, x) = \infty$ and $P(x) = (r, x)$ for non-neighbours at Step 1. The goal quantifies over every halted state, so it holds for every tie-breaking. A halted state always exists; a sorry-free check of this is in the workspace. For a vertex not reachable from $r$ the book is silent. The distance there is read as $\infty$, and the shortest-path conclusion is asserted only at finite distance.
• A trivializing formalization is ruled out: $\delta$ is computed by the update rule of Algorithm 12.14, not defined as the distance, and the theorem is not stated for an arbitrary procedure satisfying its own conclusion.
• The book uses no $O(\cdot)$ bounds or approximate constants in these statements, so there are no constants to instantiate.
• Reusable infrastructure: a list-based theory of directed paths and distances in ℕ∞, the invariants of Dijkstra's algorithm, and forest edge counting. Contributions of general lemmas (walks shortcut to paths without increasing length, component counts under edge insertion) are welcome.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 12. https://www.appliedcombinatorics.org/
• E. W. Dijkstra, "A note on two problems in connexion with graphs", Numerische Mathematik 1 (1959) 269–271. https://doi.org/10.1007/BF01386390
• J. B. Kruskal, "On the shortest spanning subtree of a graph and the traveling salesman problem", Proc. AMS 7 (1956) 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7
• 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
• M. L. Fredman and R. E. Tarjan, "Fibonacci heaps and their uses in improved network optimization algorithms", J. ACM 34 (1987) 596–615. https://doi.org/10.1145/28869.28874
• O. Borůvka, "O jistém problému minimálním", Práce Moravské přírodovědecké společnosti 3 (1926) 37–58. https://dml.cz/handle/10338.dmlcz/500114

Motivation

Insertion heuristics build a traveling salesman tour one city at a time: start from a single city, and at each step choose a city not yet on the subtour and splice it into the subtour where it lengthens the subtour least. Local search heuristics start from a tour and repeatedly replace a few of its edges by others while this shortens the tour. Both families are standard in practice, and a natural engineering idea is to combine them: run an insertion heuristic, then polish the result by local search. The question this mission formalizes is whether local optimality of the insertion tour certifies anything about its quality.

Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) answered this for graphs satisfying the triangle inequality. Their §4 proves that nearest and cheapest insertion always return a tour of length at most $2(1-1/n)$ times the optimal length, and their Theorem 5 shows this bound is attained. Their §7 then shows that the very tour attaining the bound is $k$-optimal for every $k\le n/4$: no exchange of $k$ edges shortens it. So the insertion bound is tight even for tours that local search with $k$-changes cannot improve.

Timeline, as far as this mission is concerned:

• 1965: Lin (Bell System Tech. J. 44) defines $k$-optimal tours and uses 3-optimal local search.
• 1973: Lin and Kernighan (Oper. Res. 21) generalize the edge-exchange neighbourhoods.
• 1977: Rosenkrantz, Stearns and Lewis prove the $2(1-1/n)$ upper bound for nearest and cheapest insertion (Theorem 4 and its corollary), its tightness for $n\ge 6$ (Theorem 5), the existence of $k$-optimal tours with the same ratio (Theorem 6, stated for $n\ge 8$), and the Corollary combining the two.

Setting

A traveling salesman graph on $n$ nodes is the node set $N=\{1,\dots,n\}$ with a distance $d(i,j)\ge 0$ that is symmetric and satisfies the triangle inequality $d(i,k)\le d(i,j)+d(j,k)$. A tour is a Hamiltonian circuit; its length is the sum of its edge lengths; OPTIMAL is the least length of a tour. As in the paper, the identically zero distance is excluded, so OPTIMAL $>0$.

A subtour is a circuit on a subset of the nodes (a single node is a subtour without edges). For a subtour $T$ and a node $k\notin T$, TOUR$(T,k)$ is obtained by deleting an edge $(x,y)$ of $T$ minimizing $d(x,k)+d(k,y)-d(x,y)$ and adding $(x,k)$ and $(k,y)$; COST$(T,k)$ is the resulting increase in length. An insertion method chooses nodes $a_0,a_1,\dots,a_{n-1}$, starts from $T_1=\{a_0\}$ and sets $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$; INSERT is the length of $T_n$. Nearest insertion chooses $a_i$ minimizing $d(T_i,x)=\min_{y\in T_i}d(y,x)$ over $x\notin T_i$; cheapest insertion chooses $a_i$ minimizing COST$(T_i,x)$. Ties are broken arbitrarily.

A $k$-change of a tour deletes $k$ of its edges and adds $k$ other edges so that another tour is obtained. A tour is $k$-optimal if no $k$-change produces a strictly shorter tour.

The extremal instance is the circle $(N_n,d_n)$: $n$ cities equally spaced on a circular road, with $d_n(i,j)$ the smallest $m\ge 0$ with $i-j\equiv m$ or $j-i\equiv m \pmod n$. The insertion run of Theorem 5 inserts the cities in the order $1,2,\dots,n$ and produces the zig-zag tour $T_n$: city 1, then the even cities in increasing order, then the odd cities in decreasing order.

Formalization targets

Goal: the Corollary to Theorem 6

For $n\ge 6$ and $4k\le n$ there is a traveling salesman graph with OPTIMAL $>0$ on which some run of nearest insertion, and some run of cheapest insertion, return a $k$-optimal tour with

$$\frac{\mathrm{INSERT}}{\mathrm{OPTIMAL}}=2\left(1-\frac1n\right).$$

Milestones

1. The insertion run on the circle: the subtours $T_i$ and nodes $a_i=i+1$ form an insertion run that obeys both the nearest and the cheapest rule (proof of Theorem 5).
2. On the circle, $T_n$ has length $2(n-1)$ and OPTIMAL $=n$ (proof of Theorem 5).
3. Theorem 5: for $n\ge 6$ there is a graph with INSERT/OPTIMAL $=2(1-1/n)$ for both methods.
4. Equation (7.4): the length of a tour of the circle is the sum over unit edges $e$ of COUNT$(e,T)$, the number of times $e$ is traversed when each tour edge is replaced by a shortest arc.
5. Every tour of the circle is odd or even (all counts of one parity), eq. (7.5).
6. $T_n$ is the shortest even tour, so every tour shorter than $T_n$ is odd.
7. $T_n$ is $k$-optimal for every $k\le n/4$.
8. Theorem 6: for $n\ge 8$ there is a graph with a tour that is $k$-optimal for all $k\le n/4$ and has LOCALOPT/OPTIMAL $=2(1-1/n)$.

Significance

The result. The Corollary shows that the $2(1-1/n)$ worst-case guarantee of nearest and cheapest insertion cannot be improved by requiring that the returned tour survive $k$-change local search, for $k$ up to a quarter of the number of cities. Theorem 6 says more generally that $k$-optimality with $k\le n/4$ does not bound the ratio to the optimum below $2(1-1/n)$. Together with the paper's upper bound, the insertion guarantee is exact, and it stays exact after local polishing with small neighbourhoods.

Formalizing it. All statements are proved in the paper; none, to our knowledge, has been machine-checked. The platform has an upper bound for nearest insertion (SupplyChainTheory, Theorem 10.7, ratio at most 2) but no tightness example and no notion of $k$-optimality. This mission produces a reusable definition of $k$-changes against arbitrary tours, the circle metric, and the parity-counting argument on a cycle, and it supplies the calculations the paper omits ("We omit these calculations but note that they require the assumption $n\ge 6$").

Difficulty

Two steps carry the weight. First, the omitted calculations for the insertion run: at each stage one must show that inserting $a_i$ between $i-1$ and $i$ minimizes the insertion increase over every edge of the zig-zag subtour, and that no other outside city can be inserted for less than 2; the claim fails for $n=4$ and $n=5$, so the verification must use $n\ge 6$ in an essential way. Second, $k$-optimality is a statement about every tour at edge difference $k$, not about 2-opt segment reversals or any specific move family. A search over moves of a special form does not establish it; the argument must bound the length of an arbitrary tour at edge difference $k$ from below.

Formalization scope

Nodes are Fin n, so the paper's node $m$ is index $m-1$ and $a_i=i+1$ is index $i$; subtour indices stay 1-based ($T_1=[a_0]$, approximation $T_n$). A distance is d : Fin n → Fin n → ℝ with the structure IsTSPDist (symmetric, nonnegative, triangle inequality, and $d(i,i)=0$; the last is a normalization absent from the paper that changes no length). A tour is an Equiv.Perm (Fin n), a subtour a list read cyclically; OPTIMAL is Finset.univ.inf' over permutations, the true minimum. TOUR$(T,k)$ is insertion at a position minimizing the new length; COST is a minimum over positions; the nearest-insertion distance (4.1) takes values in WithTop ℝ, so no junk value arises. $k$-optimality compares the tour with every permutation whose edge set (unordered pairs) misses exactly $k$ of the tour's edges. Ratios are multiplied out.

COUNT$(e,T)$ needs a choice of shortest arc for antipodal pairs when $n$ is even; the formalization takes the arc through $\min(x,y),\dots,\max(x,y)$. The paper's argument does not depend on this choice.

Deviations from the printed text: the Corollary is stated for $n\ge 6$ (the printed statement says only $4k\le n$, but its proof uses the example of Theorem 5, which exists for $n\ge 6$; for $k=0$, $n=3$ the printed statement is false). Theorem 6 keeps its printed $n\ge 8$. In the proof of Theorem 5 the paper writes "(4.2) holds" where the cheapest-insertion condition (4.3) is meant; the formal statement uses (4.3).

The existence statements carry OPTIMAL $>0$, the paper's standing assumption (1.1). Without it, the zero distance would make every length zero and every tour $k$-optimal, which would satisfy the ratio equations trivially; that formalization is ruled out.

Contributions welcome: proofs of any milestone, in particular the omitted insertion calculations and the parity lemma, and reusable lemmas on cyclic lists and edge sets of permutations.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• S. Lin, Computer solutions of the traveling salesman problem, Bell System Tech. J. 44:2245–2269, 1965. https://doi.org/10.1002/j.1538-7305.1965.tb04146.x
• S. Lin, B. W. Kernighan, An effective heuristic algorithm for the traveling-salesman problem, Oper. Res. 21(2):498–516, 1973. https://doi.org/10.1287/opre.21.2.498