Combinatorics

Completed

Graph Theory Operations Research Optimization+1·Captain: mikedeng1

An Analysis of Several Heuristics for the Traveling Salesman Problem III: Nearest and Cheapest Insertion Are Within a Factor of TwoResearch Paper

Motivation

The traveling salesman problem (TSP) asks for a shortest closed route through a finite set of points. It is NP-hard, and in practice tours are built by fast constructive heuristics whose output is then improved or used as is. A central question in the analysis of algorithms, raised in this form by Rosenkrantz, Stearns and Lewis in 1977, is how far such a heuristic can be from optimal in the worst case, as a function of the number of points $n$ , when the distances satisfy the triangle inequality.

The paper (SIAM J. Comput. 6(3), 1977) answers this for several heuristics. For the general class of insertion methods it proves a logarithmic bound (Theorem 3); for two specific rules, nearest insertion and cheapest insertion, it proves a bound that does not grow with $n$ : the tour is less than twice the optimal (Theorem 4), and more precisely at most $2(1-1/n)$ times the optimal (Corollary, eq. (4.12)). Theorem 5 of the same paper shows the constant $2(1-1/n)$ is attained, so this is the exact worst case of both rules. These results, with Christofides' 3/2 bound of 1976, are the classical reference points for approximation ratios of TSP construction heuristics and appear in standard OR and approximation-algorithm texts.

Setting

A traveling salesman graph $(N,d)$ has a finite node set $N$ with $|N| = n$ and a distance $d : N\times N\to\mathbb R$ that is symmetric, nonnegative and satisfies the triangle inequality $d(i,k)\le d(i,j)+d(j,k)$ . A tour is a circuit visiting every node exactly once; its length is the sum of its edge lengths, and OPTIMAL is the least tour length.

A subtour $T$ is a tour on a subset of $N$ (a one-node subtour has no edges). For $k\notin T$ , $\mathrm{TOUR}(T,k)$ inserts $k$ into $T$ where it is cheapest: if $T$ has at least two nodes, choose an edge $(x,y)$ of $T$ minimizing $d(x,k)+d(k,y)-d(x,y)$ and replace it by $(x,k),(k,y)$ ; if $T=\{i\}$ , form the two-node tour on $i,k$ . $\mathrm{COST}(T,k)$ is the length of $\mathrm{TOUR}(T,k)$ minus the length of $T$ .

An insertion method builds subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some $a_i\notin T_i$ , $1\le i<n$ ; INSERT is the length of $T_n$ . With $d(T,p)=\min_{x\in T}d(x,p)$ :

nearest insertion chooses each $a_i$ with $d(T_i,a_i)=\min\{d(T_i,x): x\in N-T_i\}$ ;
cheapest insertion chooses each $a_i$ with $\mathrm{COST}(T_i,a_i)=\min\{\mathrm{COST}(T_i,x): x\in N-T_i\}$ .

The start node $a_0$ and every tie (between candidate nodes, and between candidate edges) are arbitrary. TREE denotes the length of a minimal spanning tree of $(N,d)$ .

Formalization targets

Goal: Corollary to Theorem 4, eq. (4.12)

For every traveling salesman graph on $n\ge1$ nodes and every run of nearest insertion or of cheapest insertion,

\mathrm{INSERT}\;\le\;2\Bigl(1-\frac1n\Bigr)\cdot\mathrm{OPTIMAL}.

Milestones

Lemma 2, (3.3): $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for $k\notin T$ , $j\in T$ .
Eq. (3.7): for every insertion method, $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$ .
Eqs. (4.9)–(4.10): nearest insertion satisfies $\mathrm{COST}(T_i,a_i)\le 2\,d(p,q)$ for all $p\in T_i$ , $q\notin T_i$ (4.5).
Proof of Theorem 4: cheapest insertion satisfies (4.5) as well.
Lemma 3: every insertion run satisfying (4.5) has $\mathrm{INSERT}\le 2\cdot\mathrm{TREE}$ (4.6).
Eq. (4.11): $\mathrm{TREE}\le(1-1/n)\cdot\mathrm{OPTIMAL}$ .

Theorem 4 itself, $\mathrm{INSERT}<2\cdot\mathrm{OPTIMAL}$ when $d$ is not identically zero, is included as a companion statement.

Significance

The bound says that two simple $O(n^2)$ and $O(n^2\log n)$ construction rules are never worse than a factor $2(1-1/n)$ from optimal on any metric instance, a guarantee independent of $n$ , in contrast with nearest neighbor and with arbitrary insertion orders, whose ratios the same paper shows can grow logarithmically. Lemma 3 is reusable on its own: any insertion rule satisfying the local inequality (4.5) inherits the bound $2\cdot\mathrm{TREE}$ , and the paper notes that similar arguments apply to nearest addition and nearest merger.

The result has been proved since 1977. The Prove2Me library has a machine-checked proof of the weaker statement for nearest insertion only with constant $2$ (SupplyChainTheory.nearest_insertion_bound, from Snyder–Shen, Theorem 10.7) and of $\mathrm{TREE}\le\mathrm{OPTIMAL}$ (SupplyChainTheory.mst_lower_bound). This mission asks for the paper's full statement: both rules, the exact constant $2(1-1/n)$ , and the general Lemma 3 via its correspondence between insertion steps and spanning-tree edges. Paired with the tightness result of the companion mission (Theorem 5), it would give a formally verified exact worst-case ratio for both heuristics.

Difficulty

Lemma 2 and inequality (4.5) are local consequences of the triangle inequality; the difficulty is global. The obvious attempt at Lemma 3 charges step $i$ to the tree edge joining $a_i$ to its nearest node of $T_i$ , but distinct steps can then be charged to the same tree edge, and the sum of the charges no longer bounds $2\cdot\mathrm{TREE}$ . Any correct argument must control how the insertion order interacts with the structure of an arbitrary spanning tree, which in Lean means reasoning about paths in SimpleGraph together with the evolving subtours. For cheapest insertion the chosen node need not be a nearest node, so (4.5) is not immediate from the rule. Finally, the goal's constant $2(1-1/n)$ is sharper than the bound $2\cdot\mathrm{OPTIMAL}$ obtained from $\mathrm{TREE}\le\mathrm{OPTIMAL}$ , so the weaker spanning-tree bound already in the library does not suffice.

Formalization scope

Nodes are Fin n with $n\ge1$ (the paper's nodes $1,\dots,n$ shifted to $0,\dots,n-1$ ). The distance satisfies the paper's three axioms plus the normalization $d(i,i)=0$ , which never affects a tour, subtour or tree length. Tours are permutations; OPTIMAL is a minimum over all of them (Finset.inf'). Subtours are lists of distinct nodes with closed length. $\mathrm{TOUR}(T,k)$ is encoded as insertion of $k$ at a list position whose resulting length is minimal over all $|T|+1$ positions, which is the minimization of (3.1) over the edges of $T$ ; COST is the corresponding minimum increase. The subtour index is 1-based as printed ( $T_1=\{a_0\}$ , $T_n$ final). The distance $d(T,p)$ is taken in $\mathbb R\cup\{+\infty\}$ , so no default value enters the nearest rule. Spanning trees are SimpleGraph (Fin n) with IsTree; statements about TREE are phrased over every spanning tree (upper bounds) or some spanning tree (bounds on TREE), which is equivalent. Ratios are multiplied out, so the goal needs no nontriviality hypothesis; Theorem 4's strict form carries the paper's exclusion of the identically zero distance (p. 564).

A formalization in which TOUR inserts at an arbitrary rather than a cheapest position, or in which the run fixes the start node or the tie-breaking, would state a different (and, for arbitrary positions, false) theorem; the statements here quantify over every run.

A complete development needs subtour-length lemmas for List.insertIdx, the telescoping identity (3.7), and a spanning-tree edge-assignment argument on Mathlib's SimpleGraph paths; the last two are reusable for other insertion rules and for the companion missions of this series. Proofs of any milestone are welcome independently.

Selected references

D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, GSIA, Carnegie Mellon University, 1976. https://doi.org/10.1007/s43069-021-00101-z (reprint in Operations Research Forum 3, 2022)
L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 10 (Theorem 10.7). https://doi.org/10.1002/9781119584445

10 thms2 active usersReviewed

Probability·Captain: mikedeng1

Limits of Permutation Sequences II: Convergence Is Equivalent to Being Cauchy in the Rectangular DistanceResearch Paper

Motivation

For dense graphs, convergence of subgraph densities was shown by Lovász and Szegedy (2006) to have graphons as limit objects, and Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) proved that the same convergence is metric: a graph sequence converges exactly when it is Cauchy in the cut distance. The metric view is what makes the space of graphons compact and connects limit theory with regularity lemmas and property testing.

Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) developed the corresponding theory for permutations. Besides the existence of limits (the subject of mission I of this series), they introduced a rectangular distance $d_\square$ between permutations, a normalized version of Cooper's discrepancy (Cooper, J. Combin. Theory Ser. A, 2004; reference [7] of the paper), and proved in Theorem 1.8 that convergence of a permutation sequence is the same as being Cauchy for $d_\square$ . This mission formalizes that theorem.

Timeline:

2004. Cooper introduces the discrepancy of a permutation as a measure of quasirandomness.
2006–2008. Lovász–Szegedy and Borgs et al. establish graph limits and the cut-distance characterization of convergence.
2011–2013. Hoppen et al. prove the permutation analogues, including Theorem 1.8 (this paper).

Setting

For $n \ge 1$ , $S_n$ is the set of permutations of $[n]=\{1,\dots,n\}$ , $|\pi| = n$ for $\pi\in S_n$ , and $\mathcal S=\bigcup_n S_n$ . For $\tau\in S_k$ and $\pi\in S_n$ , $\Lambda(\tau,\pi)$ counts the increasing $k$ -tuples $x_1<\dots<x_k$ in $[n]$ with $\pi(x_i)<\pi(x_j)\iff\tau(i)<\tau(j)$ , and the subpermutation density is $t(\tau,\pi)=\Lambda(\tau,\pi)/\binom nk$ for $k\le n$ and $0$ for $k>n$ . A permutation sequence $(\sigma_n)$ is convergent if $t(\tau,\sigma_n)$ converges for every fixed $\tau\in\mathcal S$ .

A limit permutation is a Lebesgue measurable $Z:[0,1]^2\to[0,1]$ such that $Z(x,\cdot)$ is a cdf (non-decreasing, right-continuous, $Z(x,1)=1$ ) for every $x$ and $\int_0^1 Z(x,y)\,dx=y$ for every $y$ ; the set of them is $\mathcal Z$ . Each $Z$ has an associated random point $(X,Y)$ with $X\sim U[0,1]$ and conditional cdf $Z(X,\cdot)$ , joint distribution function $F(x,y)=\int_0^x Z(t,y)\,dt$ , and pattern densities $t(\tau,Z)$ (the probability that $k$ independent copies of $(X,Y)$ form the pattern $\tau$ ).

For $\sigma\in S_n$ , the step limit permutation $Z_\sigma$ spreads the permutation matrix of $\sigma$ uniformly over the corresponding $n\times n$ grid cells. The rectangular distance of $Z_1,Z_2\in\mathcal Z$ is

d_\square(Z_1,Z_2)=\sup_{x_1<x_2,\ y_1<y_2}\left|\int_{x_1}^{x_2}\big(Z_1(x,y_2)-Z_1(x,y_1)\big)dx-\int_{x_1}^{x_2}\big(Z_2(x,y_2)-Z_2(x,y_1)\big)dx\right|,

the largest difference between the probabilities the two random points give to an axis-parallel rectangle, and $d_\infty(Z_1,Z_2)=\sup_{x,y}|F_1(x,y)-F_2(x,y)|$ . On permutations of possibly different lengths, $d_\square(\sigma,\pi):=d_\square(Z_\sigma,Z_\pi)$ . A sequence is Cauchy with respect to $d_\square$ if for every $\varepsilon>0$ there is $n_0$ with $d_\square(\sigma_n,\sigma_m)<\varepsilon$ for all $n,m\ge n_0$ .

Formalization targets

Goal: Theorem 1.8, under $|\sigma_n|\to\infty$

|\sigma_n|\to\infty\ \Longrightarrow\ \Big((\sigma_n)\ \text{convergent}\iff(\sigma_n)\ \text{is } d_\square\text{-Cauchy}\Big).

Milestones

In the order the proof uses them:

Lemma 3.5: $|t(\tau,\sigma)-t(\tau,Z_\sigma)|\le\frac1n\binom k2$ for $\tau\in S_k$ , $\sigma\in S_n$ , $k\le n$ .
Eq. (49): for $|\sigma_n|\to\infty$ , $\sigma_n\to Z\iff Z_{\sigma_n}\xrightarrow{t}Z$ .
Eq. (34): $d_\infty\le d_\square\le 4\,d_\infty$ on $\mathcal Z$ .
Lemma 2.1: for uniform marginals, weak convergence is equivalent to uniform convergence of joint distribution functions.
Lemma 2.2 (a): every law on $[0,1]^2$ with uniform marginals has a limit permutation as its conditional cdf.
Lemma 5.3: weak, $d_\square$ - and density convergence on $\mathcal Z$ coincide.
Theorem 1.6 (i): a convergent sequence with $|\sigma_n|\to\infty$ converges to some $Z\in\mathcal Z$ .
Claim 2.4: a convergent sequence with $|\sigma_n|\not\to\infty$ is eventually constant.
Theorem 1.8 ( $\Rightarrow$ ): every convergent sequence is $d_\square$ -Cauchy, with no condition on lengths.

Significance

Theorem 1.8 identifies density convergence, defined through infinitely many pattern counts, with a single metric condition. With Theorem 1.6 it shows that the completion of $(\mathcal S,d_\square)$ is $\mathcal Z$ modulo almost-everywhere equality, which is compact; permutations are isolated points of it (Claim 2.4). This is the permutation counterpart of the cut-distance theory of graph limits, and it is the metric in which the paper's testability and sampling results (Lemma 4.2) are quantitative.

The theorem is proved in the paper. To the best of current knowledge neither it nor the underlying permuton theory is formalized in any proof assistant. The mission produces machine-checked statements of the rectangular distance, its comparison with the sup-norm distance of distribution functions, and the Cauchy characterization, all reusable for quasirandom permutations and permutation property testing.

Difficulty

The direction "convergent $\Rightarrow$ Cauchy" needs a limit permutation for the sequence and the equivalence of density and $d_\square$ convergence on $\mathcal Z$ (Lemma 5.3), which is not formal: density convergence involves every pattern, $d_\square$ a supremum over rectangles. For "Cauchy $\Rightarrow$ convergent", completeness of bounded functions under the sup norm gives a uniform limit $F$ of the distribution functions, but a uniform limit of distribution functions of limit permutations is not visibly the distribution function of a limit permutation. Identifying it needs weak compactness, Lemma 2.1 and the regular conditional cdf of Lemma 2.2.

The literal statement also fails for sequences whose lengths do not tend to infinity, as explained under Formalization scope; the reduction "we may assume $|\sigma_n|\to\infty$ " covers only one direction.

Formalization scope

$[0,1]$ is Mathlib's unitInterval with Lebesgue measure; a limit permutation is a curried real function Z : I → I → ℝ, almost-everywhere measurable on the square, with the cdf and integral conditions for every $x$ and every $y$ . $S_n$ is Equiv.Perm (Fin n) (0-based) and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n).
$d_\square$ on $\mathcal Z$ is the integral form of the paper's Eq. (32); $d_\infty$ is Eq. (33) with $F_i(x,y)=\int_0^x Z_i(t,y)\,dt$ . Both are real suprema of bounded families. $Z_\sigma$ is in closed form, with the first row used at $x=0$ (a null-set choice).
$d_\square$ on permutations is defined for every pair of lengths as $d_\square(Z_\sigma,Z_\pi)$ , the paper's extension (Sect. 4.1); the same-length formula (31) is not needed. A definition that returned $0$ or junk for different lengths would make every sequence with growing lengths Cauchy and is ruled out.
Correction. The paper states Theorem 1.8 for all sequences. Without $|\sigma_n|\to\infty$ , "Cauchy $\Rightarrow$ convergent" is false: interleaving $\sigma=(1,2)$ with permutations $\tau_k$ , $|\tau_k|\to\infty$ , $d_\square(Z_{\tau_k},Z_\sigma)\to0$ , gives a Cauchy sequence along which $t(\sigma,\cdot)$ alternates between $1$ and values tending to $3/4$ . The goal carries $|\sigma_n|\to\infty$ ; the true direction without it is milestone 9.
"Convergent" is the paper's Definition 1.2 (all densities converge), not the existence of a limit $Z$ . The Cauchy condition uses the explicit $\varepsilon$ – $n_0$ form with strict inequality, not a metric-space instance.
Theorem 1.6 (i) is also the goal of mission I; it is restated here in this mission's namespace.

Needed infrastructure: Prokhorov compactness of probability measures on the square, the Portmanteau theorem, completeness of bounded functions under the sup norm, and conditional cdfs (ProbabilityTheory.condCDF). Contributions on any milestone, and alternative proofs of the Cauchy characterization, are welcome.

Selected references

C. Hoppen, Y. Kohayakawa, C. G. Moreira, B. Ráth, R. M. Sampaio, Limits of permutation sequences, arXiv:1103.5844v2, 2012; J. Combin. Theory Ser. B 103 (2013). https://arxiv.org/abs/1103.5844v2
J. N. Cooper, Quasirandom permutations, J. Combin. Theory Ser. A 106 (2004) no. 1, 123–143 (cited as [7] in arXiv:1103.5844v2).
L. Lovász, B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96 (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002
C. Borgs, J. T. Chayes, L. Lovász, V. T. Sós, K. Vesztergombi, Convergent sequences of dense graphs I: Subgraph frequencies, metric properties and testing, Adv. Math. 219 (2008) 1801–1851. https://doi.org/10.1016/j.aim.2007.08.004
P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962

19 thms2 active usersReviewed

Completed

Theoretical Computer Science·Captain: mikedeng1

A Faster Algorithm Computing String Edit Distances 2: Discrete Edit Costs Are NecessaryResearch Paper

Motivation

The edit distance between two strings is the least total cost of a sequence of single-character insertions, deletions and replacements that turns one string into the other. It underlies spelling correction, sequence alignment in computational biology, and file comparison. Wagner and Fischer (J. ACM 21, 1974) computed it for strings of length $n$ in time $O(n^2)$ by filling an $(n+1) \times (n+1)$ matrix. Masek and Paterson (J. Comput. System Sci. 20, 1980) lowered this to $O(n^2/\log n)$ with a "Four Russians" block method: the matrix is cut into $m \times m$ blocks, and the effect of every possible block is tabulated in advance.

The tabulation only pays off if the number of possible blocks is small. The paper guarantees this under two hypotheses: the alphabet is finite, and the edit costs are discrete, that is, all integer multiples of one constant. Its §4 asks whether discreteness can be dropped, and answers no with an explicit example whose costs are $0$ , $1$ , $\pi$ and $5$ . This mission formalizes that example.

Timeline:

1974, Wagner and Fischer: the $O(|A|\,|B|)$ matrix algorithm and its recurrence, for nonnegative costs.
1980, Masek and Paterson: the $O(n^2/\log n)$ algorithm for a finite alphabet and discrete costs (§2, Lemma 4), and the example of §4 showing the discreteness hypothesis cannot simply be removed (Theorem 5).
2015, Backurs and Indyk (STOC 2015): no strongly subquadratic algorithm under the Strong Exponential Time Hypothesis, which places the gap the paper left open in context.

Setting

Let $\Sigma$ be an alphabet and $\lambda$ the null string. An edit operation $a \to b$ is a pair of strings of length at most one other than $(\lambda, \lambda)$ : a replacement when both are symbols, a deletion when $b = \lambda$ , an insertion when $a = \lambda$ . $B$ results from $A$ by $a \to b$ if $A = \sigma a \tau$ and $B = \sigma b \tau$ . A cost function $\gamma$ assigns a nonnegative real to each edit operation; $R_{a,b} = \gamma(a \to b)$ , $D_a = \gamma(a \to \lambda)$ , $I_a = \gamma(\lambda \to a)$ . The edit distance $\delta(\gamma, A, B)$ is the minimum of $\sum_i \gamma(s_i)$ over sequences $s_1, \dots, s_m$ of edit operations taking $A$ to $B$ . For fixed strings, $\delta_{i,j} = \delta(\gamma, A^i, B^j)$ , where $A^i = A_1 \cdots A_i$ ; this is the edit matrix. A step is the difference of two horizontally or vertically adjacent entries, $\delta_{i,j} - \delta_{i-1,j}$ or $\delta_{i,j} - \delta_{i,j-1}$ , and the possible steps of $\gamma$ are the steps of all edit matrices of all pairs of strings. The cost set $\Omega = \{D_a\} \cup \{I_a\} \cup \{R_{a,b}\}$ is discrete if some $r > 0$ has every element of $\Omega$ as an integer multiple.

An edit path is a sequence of matrix cells $(p, q)$ in which each cell increases $p$ , $q$ or both by one: a deletion of $A_{p+1}$ (cost $D_{A_{p+1}}$ ), an insertion of $B_{q+1}$ (cost $I_{B_{q+1}}$ ), or a replacement of $A_{p+1}$ by $B_{q+1}$ (cost $R_{A_{p+1},B_{q+1}}$ ). The eccentricity of $(i, j)$ is $|i - j|$ .

The example. $\Sigma = \{a, b, c\}$ with

R_{\sigma,\sigma} = 0,\quad R_{a,b} = R_{b,a} = 1,\quad R_{c,a} = R_{c,b} = R_{a,c} = R_{b,c} = \pi,\quad I_\sigma = D_\sigma = 5.

Let $\mu_{2k} = \mu_{2k+1} = \lfloor 2k/(2\pi+1) \rfloor$ . The infinite strings $A$ and $B$ are $baba\ldots$ and $abab\ldots$ with a $c$ written into both, at each even position $i$ where $\mu_i > \mu_{i-1}$ , so that $A^i$ and $B^i$ each contain exactly $\mu_i$ letters $c$ . The first $c$ is at position $8$ . $P^*(i, j, k)$ is the minimum cost of an edit path from $(i, j)$ to $(i+k, j+k)$ through points all of eccentricity at least $|i-j|$ .

Formalization targets

Goal (Theorem 5, as its proof establishes it)

For the example's $\gamma$ , $A$ and $B$ ,

k \mapsto \delta_{k,k+1} - \delta_{k,k} \ \text{ is injective on } \mathbb{N}, \qquad \text{and the set of possible steps of } \gamma \text{ is infinite.}

The first part gives at least $n$ distinct steps in the edit matrix of $A^n$ and $B^n$ ; the second is the negation of the conclusion of the paper's Lemma 4. The goal fixes no constants and no growth rate beyond "at least one new step per diagonal position".

Milestones

§2.3: for every nonnegative normalized cost function and all strings, $\delta_{i,j}$ equals the minimum cost of an edit path from $(0,0)$ to $(i,j)$ .
Lemma 5: $P^*(i,j,k) \ge k - \mu_{i+k} + \mu_i$ if $i - j$ is even, and $P^*(i,j,k) \ge (\mu_{i+k} - \mu_i + \mu_{j+k} - \mu_j)\pi$ if $i - j$ is odd.
Lemma 6: for $0 \le k' \le k$ , $P^*(0,0,k') + 5 + P^*(k'+1, k', k-k') \ge 5 + (\mu_{k+1} + \mu_k)\pi$ .
Lemma 7: $\delta_{k,k} = k - \mu_k$ and $\delta_{k,k+1} = \delta_{k+1,k} = 5 + (\mu_{k+1} + \mu_k)\pi$ .

A further item records that the example satisfies every other condition of the paper: its costs are nonnegative and normalized ( $\gamma(a \to b) = \delta(\gamma, a, b)$ ), but $\Omega = \{0, 1, \pi, 5\}$ is not discrete.

Significance

The block algorithm precomputes one table entry per block and per pair of initial step vectors, so its preprocessing is polynomial in $n$ only when the number of possible steps is bounded independently of the strings. The example shows that without discreteness the steps can grow with $n$ even over a three-letter alphabet with nonnegative normalized costs, so the table size becomes of order $(kn)^m$ and the method gives no speedup. It explains why the finite-alphabet, non-discrete case is left open in the paper's conclusion.

The paper's result is proved on paper; no machine-checked version is known to exist, and Mathlib has no edit distance at the pinned revision. The formalization produces exact closed forms for three diagonals of a nontrivial edit matrix with irrational entries, a formal link between edit distance over arbitrary edit sequences and minimum-cost paths, and a verified counterexample to the naive generalization of the algorithm. The sibling mission of the series formalizes the algorithm and Lemma 4.

Difficulty

The central difficulty is Lemma 5: a lower bound on the cost of every path confined to a band of eccentricity, not only the straight diagonal. A path may leave its diagonal, pay $10$ for a deletion and an insertion, and travel along another diagonal whose $c$ 's may or may not line up. The bound must hold uniformly in $i$ , $j$ and $k$ , and it depends on the floor function $\mu$ and on precise inequalities between $\mu_{r+s} - \mu_r$ and $s/(2\pi+1)$ . Checking that the straight diagonals are optimal for small $k$ does not suffice: the $c$ -densities are chosen so that even and odd diagonals cost almost exactly the same per step, and a periodic placement of $c$ 's would let one diagonal eventually undercut another.

Formalization scope

Strings are Lists; the infinite strings $A$ , $B$ are functions $\mathbb{N} \to \Sigma$ read from index $1$ , and $A^n$ is the list of their first $n$ symbols. An edit operation is a pair of Option values other than $(\text{none}, \text{none})$ . The edit distance and $P^*$ are real infima (sInf) of nonempty sets of nonnegative reals, so they coincide with the paper's minima. $\delta_{i,j}$ has $i$ indexing $A$ and $j$ indexing $B$ (the paper's Figure 4 prints $A$ across the columns). $\mu_i$ is $\lfloor 2\lfloor i/2 \rfloor/(2\pi+1) \rfloor$ . The constraint of $P^*$ applies to every point of the path, endpoints included. Costs use Real.pi itself.

Pinned statements: the paper states Theorem 5 about the running time of Algorithm Y ("Discreteness is a necessary condition for Algorithm Y to run in time $O(k^m)$ on length $m$ strings and step sequences"); its proof establishes that the number of distinct steps grows linearly with the string length, which is what the goal states. Running time is not formalized. The §2.3 milestone is stated, as in the paper, for all strings and every nonnegative cost function satisfying the §1.1 normalization $\gamma(a \to b) = \delta(\gamma, a, b)$ ; both standing assumptions are hypotheses. The paper's standing assumption $|A| \ge |B|$ is used only for running times and is omitted.

The example must be the paper's: replacing $\pi$ by a rational, or quantifying over "some" cost function or "some" strings, makes the goal false or empty, and the edit distance must be the minimum over edit sequences, not a recurrence.

Needed infrastructure: edit sequences and their costs, the reduction of edit sequences to edit paths, and bounds on $\lfloor \cdot \rfloor$ with $\pi$ (Mathlib's irrational_pi and Real.pi_gt_d2). The edit-distance definitions are shared in shape with the sibling mission and are reusable. Proofs of any milestone are welcome.

Selected references

W. J. Masek, M. S. Paterson, A Faster Algorithm Computing String Edit Distances, J. Comput. System Sci. 20 (1980), 18–31. https://doi.org/10.1016/0022-0000(80)90002-1
R. A. Wagner, M. J. Fischer, The String-to-String Correction Problem, J. ACM 21 (1974), 168–173. https://doi.org/10.1145/321796.321811
A. Backurs, P. Indyk, Edit Distance Cannot Be Computed in Strongly Subquadratic Time (unless SETH is false), STOC 2015, 51–58. https://doi.org/10.1145/2746539.2746612

9 thms2 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Maximizing Non-Monotone Submodular Functions III: Guarantees of Deterministic Local SearchResearch Paper

Motivation

Many optimization problems ask for a subset of a finite ground set that maximizes a function with diminishing returns: the cut of a graph or a directed graph, the value of a facility-location configuration, the entropy of a set of random variables, or a welfare function in combinatorial auctions. These functions are submodular but typically non-monotone: adding elements can decrease the value. Max Cut and Max Directed Cut are the textbook special cases. Unconstrained maximization of a nonnegative non-monotone submodular function is NP-hard, and before Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) no constant-factor approximation was known for general such functions in the value-oracle model.

The paper gives several algorithms. A uniformly random set achieves $1/4$ of the optimum (a separate mission of this series). This mission concerns the paper's first deterministic algorithm: a local search that repeatedly adds or removes a single element while the value improves by a factor larger than $1 + \epsilon/n^2$ , and returns the better of the final set and its complement. The key structural fact behind it, that a local optimum of a submodular function dominates all its subsets and supersets, goes back to Cherenin (1962) and Goldengorin, Tijssen and Tso (1999).

Timeline. Cherenin (1962) and Goldengorin–Tijssen–Tso (1999): local optima dominate comparable sets. Schäffer and Yannakakis (SIAM J. Comput. 1991): finding an exact local optimum of Max Cut is PLS-complete, which is why the algorithm here uses an approximate improvement threshold. Feige–Mirrokni–Vondrák (FOCS 2007; SIAM J. Comput. 2011): the $1/3$ and $1/2$ guarantees of this mission, and $2/5$ for a randomized "smooth" local search. Buchbinder, Feldman, Naor and Schwartz (SIAM J. Comput. 2015): a randomized double-greedy $1/2$ -approximation, which is optimal in the value-oracle model by the lower bound of the same 2011 paper.

Setting

Let $X$ be a finite ground set with $n = |X|$ elements. A set function assigns a real number $f(S)$ to every $S \subseteq X$ . It is submodular (Definition 1.1) if

f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X,

and symmetric if $f(X \setminus S) = f(S)$ for all $S$ . Throughout the section of the paper formalized here, $f$ is nonnegative. The algorithm may query $f(S)$ for any $S$ (a value oracle). The optimum is $\mathrm{OPT} = \max_{S \subseteq X} f(S)$ .

A set $S$ is a local optimum if $f(S \cup \{a\}) \le f(S)$ for every $a \notin S$ and $f(S \setminus \{a\}) \le f(S)$ for every $a \in S$ . It is a $(1+\alpha)$ -approximate local optimum (Definition 3.2) if $(1+\alpha)f(S) \ge f(S \setminus \{v\})$ for $v \in S$ and $(1+\alpha)f(S) \ge f(S \cup \{v\})$ for $v \notin S$ .

Algorithm LS with parameter $\epsilon > 0$ and $c = 1 + \epsilon/n^2$ :

Let $S := \{v\}$ , where $f(\{v\})$ is the maximum over all singletons.
If some $a \in X \setminus S$ has $f(S \cup \{a\}) > c\,f(S)$ , let $S := S \cup \{a\}$ and repeat step 2.
If some $a \in S$ has $f(S \setminus \{a\}) > c\,f(S)$ , let $S := S \setminus \{a\}$ and go back to step 2.
Return $\max\{f(S), f(X \setminus S)\}$ .

In Lean these are Submodular, SymmetricSetFun, OPT, IsLocalOptimum, IsApproxLocalOptimum, lsStep, IsLSRun, IsLSTerminal and lsOutput in NonmonotoneSubmod.LocalSearch.

Formalization targets

Goal: Theorem 3.4 (p. 1141)

For nonnegative submodular $f$ on a nonempty $X$ and $\epsilon > 0$ , every run of Algorithm LS, with any choice of starting singleton and of improving elements, satisfies:

\text{at termination at } S:\qquad \max\{f(S), f(X\setminus S)\} \ge \Big(\frac13 - \frac{\epsilon}{n}\Big)\mathrm{OPT};

\text{if } f \text{ is symmetric, at termination at } S:\qquad f(S) \ge \Big(\frac12 - \frac{\epsilon}{n}\Big)\mathrm{OPT};

\text{if } n \ge 2, \text{ after any } k \text{ steps}:\qquad \Big(1 + \frac{\epsilon}{n^2}\Big)^k \le n.

The last line is the explicit content of the printed bound of $O(\frac1\epsilon n^3 \log n)$ oracle calls: it gives $k = O(\frac1\epsilon n^2 \log n)$ steps of at most $2n$ queries each, and in particular termination.

Milestones, in attack order

Lemma 3.1: a local optimum $S$ of a submodular $f$ satisfies $f(T) \le f(S)$ whenever $T \subseteq S$ or $T \supseteq S$ .
Lemma 3.3: for a $(1+\alpha)$ -approximate local optimum, $f(T) \le (1 + n\alpha) f(S)$ for such $T$ .
Termination bridge (sentence after Algorithm LS): a set at which LS has terminated is a $(1+\epsilon/n^2)$ -approximate local optimum.
First display of the proof: $2(1+n\alpha)f(S) + f(X\setminus S) \ge f(C)$ for every $C$ .
Second display, symmetric case: $2(1+n\alpha)f(S) \ge f(C)$ for every $C$ .
$\mathrm{OPT} \le n f(\{v\})$ for a maximum-value singleton, when $n \ge 2$ .
Growth along a run: $f(S_k) \ge (1+\epsilon/n^2)^k f(\{v\})$ .

Significance

The result. Theorem 3.4 is the deterministic constant-factor approximation of the paper that first gave guaranteed approximation factors for maximizing general nonnegative submodular functions ("Prior to our work, to the best of our knowledge, no guaranteed approximation factor was known", p. 1135), and the $1/2$ bound for symmetric functions matches the value-oracle lower bound proved in the same paper (so it is optimal for symmetric functions among algorithms using polynomially many queries). Local search with a multiplicative acceptance threshold was subsequently used for constrained non-monotone submodular maximization (matroid and knapsack constraints, Lee–Mirrokni–Nagarajan–Sviridenko 2010).

Formalizing it. The result is proved; to our knowledge neither the theorem nor Lemmas 3.1 and 3.3 has a machine-checked proof. The mission produces a reusable finite model of set functions and single-element local search over Finset, with the algorithm stated as a nondeterministic step relation, so that the guarantee is proved for every tie-breaking rule. The same model is the starting point for formalizing other local-search guarantees.

Difficulty

The natural first idea, to argue from an exact local optimum via Lemma 3.1, does not apply: LS stops at an approximate local optimum, and the error $\alpha$ per element must be accumulated along a chain of up to $n$ single-element changes between $S$ and $S \cap C$ or $S \cup C$ . This accumulation is where the nonnegativity of $f$ enters (the lemma fails for negative-valued $f$ ), and where the factor $n\alpha = \epsilon/n$ in the final ratio comes from. The running-time bound requires relating $\mathrm{OPT}$ to the best singleton, which uses submodularity on sets of all sizes and breaks down on a one-element ground set. A further bookkeeping difficulty is the algorithm itself: its steps are ordered (removals only when no addition applies), and the termination bridge must use that order.

Formalization scope

Ground set: X : Type with [Fintype X] [DecidableEq X]; subsets are Finset X; $f$ is Finset X → ℝ; complements are Sᶜ. $n$ is (Fintype.card X : ℝ).
Nonnegativity is the hypothesis ∀ S, 0 ≤ f S (standing assumption of §3); Lemma 3.1 and the termination bridge are stated without it, as they need none.
$\mathrm{OPT}$ is the maximum over all subsets (Finset.sup'), never a supremum with a default value.
The algorithm is a relation: a run is a sequence S : ℕ → Finset X with S 0 = {v} for any maximum-value singleton v and consecutive sets related by an LS step; the theorems quantify over all runs. Steps use strict inequalities, termination their negation, exactly as printed.
Added hypotheses, each disclosed in the item statements: $\epsilon > 0$ (implicit in the paper); $X \neq \emptyset$ for the goal; $\alpha \ge 0$ and $f \ge 0$ for Lemma 3.3 and the displays; $n \ge 2$ for $\mathrm{OPT} \le n f(\{v\})$ and the step bound (both false for $n = 1$ : $f(\emptyset) = 5$ , $f(\{v\}) = 0$ ). The displays are stated for every set $C$ , not only an optimal one.
The printed $O(\frac1\epsilon n^3 \log n)$ oracle-call bound, an asymptotic statement with an unquantified constant, is replaced by the explicit step bound $(1+\epsilon/n^2)^k \le n$ that its proof establishes.
Ruling out trivialization: the goal names the algorithm (its start at a maximum singleton, its ordered step rules, termination, and the returned maximum). A statement "for every $(1+\alpha)$ -approximate local optimum" is a milestone, not the theorem; an exact local optimum ( $\alpha = 0$ ) is a different algorithm.
Not in scope: the tight example of pp. 1141–1142, the randomized local search of §3.2, and the hardness results of §4.

Contributions welcome: proofs of the milestones, general lemmas about chains of single-element changes in Finset, and the derivation of the goal from them.

Selected references

U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
V. Cherenin, Solving some combinatorial problems of optimal planning by the method of successive calculations, Novosibirsk, 1962 (in Russian).
B. Goldengorin, G. Tijssen, M. Tso, The Maximization of Submodular Functions: Old and New Proofs for the Correctness of the Dichotomy Algorithm, SOM report, University of Groningen, 1999.
A. A. Schäffer, M. Yannakakis, Simple local search problems that are hard to solve, SIAM J. Comput. 20(1):56–87, 1991. https://doi.org/10.1137/0220004
J. Lee, V. S. Mirrokni, V. Nagarajan, M. Sviridenko, Maximizing nonmonotone submodular functions under matroid or knapsack constraints, SIAM J. Discrete Math. 23(4):2053–2078, 2010. https://doi.org/10.1137/090750020
N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A tight linear time (1/2)-approximation for unconstrained submodular maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

14 thms2 active usersReviewed

Completed

Graph Theory Linear Optimization Operations Research·Captain: mikedeng1

On Certain Polytopes Associated with Graphs III: The Stable Set Polytope after Substituting a Graph for a VertexResearch Paper

Motivation

Many combinatorial optimization problems on graphs are linear programs over a polytope whose inequality description is unknown. The stable set polytope is the standard example: maximizing a linear function over it is the maximum weight stable set problem, which is NP-hard, and no complete inequality description is known for general graphs. A productive line of work, begun in V. Chvátal's 1975 paper On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154), asks instead how such descriptions behave under graph operations: if descriptions are known for small graphs, can one write one down for a graph built from them?

Section 5 of that paper answers this for substitution, the operation that replaces a vertex of one graph by a whole second graph. Substitution contains three familiar constructions as special cases: duplicating a vertex, forming the join of two graphs, and forming the lexicographic product (composition). Duplication is one of the two ingredients of Lovász's proof of the perfect graph theorem (Lovász 1972); substitution in general is the operation under which perfection is preserved, and graphs built from simple pieces by substitution are a recurring source of classes with tractable stable set polytopes.

Setting

All graphs are finite, undirected and loopless. A stable set of a graph $G=(V,E)$ is a set of vertices no two of which are adjacent. Write $S(G)\subseteq\mathbb R^V$ for the set of incidence vectors of stable sets (the zero–one vectors $x$ with $\{u:x_u=1\}$ stable), and

P(G)=\operatorname{conv}S(G)

for the stable set polytope. A finite system of linear inequalities in the variables $(x_u:u\in V)$ is a defining linear system of $P(G)$ when its set of solutions is exactly $P(G)$ .

Let $G_1=(V_1,E_1)$ and $G_2=(V_2,E_2)$ be graphs with $V_1\cap V_2=\emptyset$ , and let $v\in V_1$ . The graph $G$ obtained from $G_1$ by substituting $G_2$ for $v$ has vertex set $(V_1-\{v\})\cup V_2$ . Its edges are the edges of $G_1-v$ , the edges of $G_2$ , and every edge joining a vertex of $G_2$ to a neighbour of $v$ in $G_1$ . In Lean the vertex type is the disjoint sum {u : V₁ // u ≠ v} ⊕ V₂ and the graph is substitute G₁ v G₂.

Formalization targets

Goal: Theorem 5.1

For $k\in\{1,2\}$ let

-x_u\le 0\ (u\in V_k),\qquad \sum_{u\in V_k}a_{iu}x_u\le b_i\ (i\in J_k)

be a defining linear system of $P(G_k)$ , with $J_1,J_2$ finite index sets and real coefficients, and put $a^+_{iv}=\max\{a_{iv},0\}$ for $i\in J_1$ . Then

-x_u\le 0\ \ (u\in V_2\cup(V_1-\{v\})),\qquad a^+_{iv}\sum_{u\in V_2}a_{ju}x_u+b_j\sum_{u\in V_1-\{v\}}a_{iu}x_u\le b_ib_j\ \ (i\in J_1,\ j\in J_2)\tag{5.1}

is a defining linear system of $P(G)$ . The statement fixes no particular system for $G_1$ or $G_2$ : any defining systems of the two pieces produce one for $G$ , with $|J_1|\cdot|J_2|$ rows besides nonnegativity.

Milestones

Validity of (5.1) (§5, p. 145): every $x\in S(G)$ satisfies (5.1), hence so does every point of $P(G)$ .
Proposition 2.1 (pp. 139–140): for a finite nonempty set $S$ of solutions of a system with nonnegativity rows $-x_u\le 0$ , the solution set equals $\operatorname{conv}S$ if and only if for every integer vector $c$ the value $\max\{cx:x\in S\}$ equals the minimum of the associated dual linear program, the minimum being attained.
Decomposition of the optimum (§5, pp. 145–146): for an integer vector $c$ on $V_2\cup W$ , $W=V_1-\{v\}$ , with $d_u=\max\{c_u,0\}$ ,

\max\{cx:x\in S(G)\}=\max\{m_0,\ m_1+m_2\},

where $m_0$ and $m_1$ are the maxima of $\sum_{u\in W}d_ux_u$ over $x\in S(G_1)$ with $x_v=0$ and $x_v=1$ respectively, and $m_2$ is the maximum of $\sum_{u\in V_2}d_ux_u$ over $S(G_2)$ .

Significance

Theorem 5.1 gives an explicit construction: from a polyhedral description of $P(G_1)$ and $P(G_2)$ it writes one of $P(G)$ , row by row, with no loss. Specialized to $G_1=K_2$ it gives Corollary 5.2 of the paper, a defining linear system for the join $G_1+G_2$ ; applied repeatedly it gives defining systems for lexicographic products, and applied with $G_2=\overline{K_2}$ it describes the effect of duplicating a vertex. Applied to clique systems, whose coefficients are 0 and 1, the rows of (5.1) are again clique inequalities of $G$ , so the class of graphs whose stable set polytope is described by nonnegativity and clique inequalities is closed under substitution.

The result has been proved in print since 1975. As far as a search of the Prove2Me catalogue shows, none of it, including Proposition 2.1 and the substitution operation itself, has a machine-checked statement or proof. The mission asks for a formal proof of the theorem and of the two combinatorial and polyhedral steps it rests on. The definitions of $S(G)$ , $P(G)$ and graph substitution, and the LP characterization of Proposition 2.1, are reusable by every other mission on stable set polytopes and on polyhedral descriptions of 0–1 sets.

Difficulty

That every point of $P(G)$ satisfies (5.1) is a short case check on stable sets of $G$ . The difficulty is the reverse inclusion: that no point outside $P(G)$ satisfies (5.1). The first idea, taking a point that satisfies (5.1) and splitting it directly into a point of $P(G_1)$ and a point of $P(G_2)$ , fails: (5.1) couples the two input systems through products of their coefficients and right-hand sides, and a fractional solution of (5.1) carries no evident decomposition into the two pieces. Nothing is assumed about the signs of the input coefficients, so the rows of (5.1) can mix positive and negative terms, and the positive part $a^+_{iv}$ in place of $a_{iv}$ is what keeps the system valid when $a_{iv}<0$ .

The polyhedral step behind Proposition 2.1, relating a convex hull of finitely many points to an inequality system through linear programming duality, is not available in Mathlib in this form and has to be built.

Formalization scope

Graphs are SimpleGraph on a Fintype with decidable equality; the substituted graph lives on {u : V₁ // u ≠ v} ⊕ V₂, which builds in $V_1\cap V_2=\emptyset$ .
$S(G)$ is the set of real incidence vectors of finite stable sets (IsIndepSet); $P(G)$ is convexHull ℝ (S G), never the solution set of an inequality system.
A linear system is a finite index type $J$ with real a : J → V → ℝ, b : J → ℝ. The nonnegativity rows $-x_u\le0$ are kept as a separate conjunct ∀ u, 0 ≤ x u everywhere; Proposition 2.1 is false without them. "Defining linear system" is set equality of the solution set with $P(G)$ .
No sign conditions on the $a_{iu}$ or $b_i$ are assumed; the paper assumes none.
Implicit hypothesis made explicit: $V_2\ne\emptyset$ ([Nonempty V₂]) in Theorem 5.1. The paper's graphs have nonempty vertex sets and its proof picks a vertex of $G_2$ ; with $V_2=\emptyset$ , $J_2=\emptyset$ and $V_1\ne\{v\}$ , (5.1) is just $x\ge0$ and the theorem fails. The validity milestone does not need it.
In Proposition 2.1 the set $S$ is assumed nonempty, which the paper's $\max\{cx:x\in S\}$ presupposes. "max = min" is stated as a lower bound for every feasible dual vector plus a feasible dual vector attaining the maximum.
In the decomposition milestone each maximum is a real sSup over a finite set that always contains the zero vector or the incidence vector of $\{v\}$ , so no junk value of sSup can occur.
A trivializing formalization is excluded: $P(G)$ is the convex hull of stable-set vectors rather than a set defined through the same inequalities, and the goal is the full set equality, not the validity inclusion alone.

Contributions welcome: a proof of Proposition 2.1 (the reusable core), the combinatorial decomposition, the validity case check, and the assembly of the goal.

Selected references

V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
F. Harary, Graph Theory, Addison-Wesley, 1969.

6 thms2 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Local Search Heuristics for k-Median and Facility Location Problems II: p-Swap Local Search for k-Median Has Locality Gap 3 + 2/pResearch Paper

Motivation

The k-median problem asks to open $k$ facilities among a set of candidate sites so that the total distance from clients to their nearest open facility is as small as possible. It is a basic model of facility location and of clustering, and it is NP-hard, so the question studied in approximation algorithms is how close a polynomial-time method can get to the optimum.

Local search is the method most used in practice: start from any $k$ facilities and repeatedly replace a few of them by others whenever this lowers the cost. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first analysis of a local search for k-median with a bounded performance guarantee using only $k$ medians. For single swaps they proved a locality gap of $5$ (Theorem 3.2, the subject of the first mission of this series); allowing up to $p$ facilities to be exchanged at once improves the gap to $3 + 2/p$ , which the paper notes improves on the $4$ -approximation of Charikar and Guha. That $p$ -swap bound is the result this mission formalizes.

Timeline (as recounted in §1 of the paper):

Shmoys, Tardos and Aardal, and Charikar, Guha, Tardos and Shmoys: LP rounding gives a $6\tfrac23$ -approximation for k-median.
Jain and Vazirani: primal–dual schema and Lagrangian relaxation give a $6$ -approximation; Charikar and Guha improve it to $4$ .
Korupolu, Plaxton and Rajaraman: local search with add, delete and swap moves gives a solution with $k(1+\epsilon)$ facilities and service cost at most $3 + 5/\epsilon$ times the optimum.
Arya et al.: locality gap $5$ for single swaps and $3 + 2/p$ for $p$ -swaps with exactly $k$ facilities, with a tight example.
Later work (Li and Svensson, 2013/2016) goes below $3$ with methods other than local search.

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality; $c_{ji} = d(j,i)$ is the cost of serving client $j$ by facility $i$ .

For a nonempty set $S \subseteq F$ of open facilities, each client is served by its nearest open facility, and

\mathrm{cost}(S) = \sum_{j \in C} \min_{i \in S} c_{ji}.

Fix an integer $p \ge 1$ . A $p$ -swap $\langle A, B\rangle$ deletes a set $A \subseteq S$ of at most $p$ facilities and adds a set $B \subseteq F$ of the same size. The $p$ -swap neighbourhood of $S$ is

\mathcal B(S) = \{(S \setminus A) \cup B \mid A \subseteq S,\ B \subseteq F,\ |A| = |B| \le p\},

and $S$ is locally optimum when $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$ . The locality gap is the supremum, over instances, of the ratio between the cost of a locally optimum solution and the cost of a global optimum.

In Lean the instance is MetricInstance Cl Fa with the distance on Cl ⊕ Fa, the cost is kmCost I S hS (defined only for nonempty S), and local optimality is IsPSwapLocalOpt I p S hS, all in the namespace LocalSearchFL.MultiSwap.

Formalization targets

Goal: locality gap at most $3 + 2/p$

For every metric instance, every integer $p \ge 1$ , every $k \ge 1$ , every locally optimum $S$ with $|S| = k$ , and every nonempty $O \subseteq F$ with $|O| \le k$ ,

\mathrm{cost}(S) \le \left(3 + \frac{2}{p}\right)\mathrm{cost}(O).

This is the bound concluded at the end of §3.4 (p. 553, announced p. 551). The comparison solution $O$ is arbitrary, not only an optimum, which is the strongest form printed.

Milestones

§3.4, p. 551: for sets $X, Y \subseteq S$ , disjoint sets have disjoint captures, and $X \subseteq Y$ implies $\mathrm{capture}(X) \subseteq \mathrm{capture}(Y)$ , where $\mathrm{capture}(A) = \{o \in O \mid |N_S(A) \cap N_O(o)| > |N_O(o)|/2\}$ .
Claim 3.1, p. 552: when $|S| = |O|$ , there are partitions $A_1,\dots,A_r$ of $S$ and $B_1,\dots,B_r$ of $O$ with $|A_i| = |B_i|$ , $B_i = \mathrm{capture}(A_i)$ and exactly one bad facility in $A_i$ for $i < r$ , and only good facilities in $A_r$ .
§3.4, pp. 552–553: a family of swaps of size at most $p$ with positive weights, such that each $o \in O$ is swapped in with total weight exactly $1$ , each $s \in S$ is swapped out with total weight at most $(p+1)/p$ , and $\mathrm{capture}(A) \subseteq B$ for every swap $\langle A, B\rangle$ .
Property 3.2, p. 553: a bijection $\pi$ of $N_O(o)$ with $\pi(P) \cap P = \emptyset$ for every class $P$ of a partition of $N_O(o)$ with $|P| \le \tfrac12|N_O(o)|$ .

Significance

The bound shows that the simplest optimization heuristic, stopped at any local optimum, is within a constant factor of optimal for metric k-median, and that the factor tends to $3$ as the neighbourhood grows; the paper's tight example (§3.5, given for $p = 2$ and stated to generalize to every $p$ ) shows that the analysis cannot be improved for this neighbourhood. Combined with the standard $\varepsilon$ -improvement rule (p. 548), it yields a polynomial-time $(3 + 2/p + \varepsilon)$ -approximation. The analysis template (charging each client's reassignment through a bijection of $N_O(o)$ , and averaging the local-optimality inequalities of carefully chosen swaps) was reused for facility location, capacitated variants and k-means.

The result has been proved since 2001. What this mission adds is a machine-checked proof: no formalization of the k-median problem or of any locality-gap bound is known to exist in Mathlib or on this platform. The combinatorial milestones (capture, the partition of Claim 3.1, the weighted swaps, the bijection of Property 3.2) are independent of the metric and are reusable in any local-search analysis of clustering objectives.

Difficulty

For single swaps each facility of $O$ is paired with one facility of $S$ and a direct counting argument suffices. With $p$ -swaps, a facility of $S$ may capture several facilities of $O$ at once, and a group of facilities of $S$ may jointly capture a facility of $O$ that none of them captures alone. Pairing facilities one by one then fails: the clients of a captured facility cannot be reassigned cheaply unless the capturing set is swapped out together with everything it captures. Swapping whole groups is only allowed when a group has at most $p$ members; larger groups must be split into single swaps, and the weights must be chosen so that every facility of $O$ is counted exactly once while no facility of $S$ is counted more than $(p+1)/p$ times. Getting the constant $3 + 2/p$ (rather than a weaker one) depends on this exact accounting.

Formalization scope

Clients and facilities are types Cl, Fa with Fintype and DecidableEq; solutions are Finset Fa. The distance is real-valued on Cl ⊕ Fa; d x x = 0 is not assumed (the paper neither states nor uses it).
The cost is the nearest-facility cost of a nonempty set; the empty set has no cost, so no junk value enters. The bound is stated multiplied out, kmCost I S hS ≤ (3 + 2 / (p : ℝ)) * kmCost I O hO, with the constant computed in $\mathbb R$ .
$|S| = k$ is required; $O$ ranges over all nonempty sets with $|O| \le k$ . §3.3 introduces multiswaps with $p > 1$ ; the statement takes $p \ge 1$ , where $p = 1$ is Theorem 3.2 (bound $5$ ).
Local optimality is over the whole neighbourhood (3), including sets $B$ that meet $S$ , not only over the swaps used in the analysis. Restricting it to those swaps would state a theorem with a stronger hypothesis.
The milestones state Claim 3.1, the swap construction and Property 3.2 in existence form; the procedure of Figure 8 is not formalized. Capture, good and bad are computed against the original $S$ and $O$ . The client assignments in the milestones are arbitrary functions; nearest-facility assignments are a special case. Milestone 3 also records that the deleted sets of two swaps are equal or disjoint, which is immediate from the construction and is what makes Property 3.2 applicable.
The per-swap reassignment inequality is not a milestone: the paper describes it only as "similar to the one presented for the single-swap heuristic" and prints no inequality.
Out of scope: the tight example (§3.5), the polynomial-time wrapper, and arbitrary client demands.

Needed infrastructure: finite sums over clients, Finset.inf', permutations (Equiv.Perm), and a weighted double-counting argument over the swaps. Proofs of the combinatorial milestones and alternative routes to the goal are welcome.

Selected references

V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
M. Charikar, S. Guha, É. Tardos, D. Shmoys, A Constant-Factor Approximation Algorithm for the k-Median Problem, J. Comput. System Sci. 65(1):129–149, 2002. https://doi.org/10.1006/jcss.2002.1882
K. Jain, V. Vazirani, Approximation Algorithms for Metric Facility Location and k-Median Problems Using the Primal-Dual Schema and Lagrangian Relaxation, J. ACM 48(2):274–296, 2001. https://doi.org/10.1145/375827.375845
M. Korupolu, C. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
S. Li, O. Svensson, Approximating k-Median via Pseudo-Approximation, SIAM J. Comput. 45(2):530–547, 2016. https://doi.org/10.1137/130938645

8 thms2 active usersReviewed

Completed

Machine Learning·Captain: mikedeng1

On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities I: The Growth Function DichotomyResearch Paper

Motivation

Statistical learning theory asks when the empirical frequencies of a whole class of events converge to their probabilities uniformly over the class. Vapnik and Chervonenkis answered this question in 1971 (Theory Probab. Appl. 16 (1971) 264–280) by attaching to every class of sets a single combinatorial quantity, the growth function, and bounding the probability of a large uniform deviation in terms of it. For that bound to be useful, the growth function must grow more slowly than an exponential. The first result of the paper, Theorem 1, shows that the growth function of any class is either exactly $2^r$ or bounded by a polynomial. This dichotomy is the reason finite VC dimension (the size of the largest fully shattered sample) became the central complexity measure of learning theory.

Timeline of the combinatorial core:

1971–1972. The same polynomial bound appeared in three independent papers: Vapnik and Chervonenkis (this paper; announced in Dokl. Akad. Nauk SSSR 181 (1968)), N. Sauer, On the density of families of sets, J. Combin. Theory Ser. A 13 (1972) 145–147, and S. Shelah, A combinatorial problem; stability and order for models and theories in infinitary languages, Pacific J. Math. 41 (1972) 247–261. The bound $\sum_{k=0}^{n} \binom{r}{k}$ of Lemma 1 below is now called the Sauer–Shelah lemma.
1989. Blumer, Ehrenfeucht, Haussler and Warmuth, Learnability and the Vapnik–Chervonenkis dimension, J. ACM 36 (1989) 929–965, made finite VC dimension the characterization of PAC learnability.

Setting

Let $X$ be a set and $S$ a collection of subsets of $X$ . A sample of size $r$ is a finite sequence $x_1, \dots, x_r$ of elements of $X$ ; repetitions are allowed. Each $A \in S$ induces in the sample the subsample of the terms that lie in $A$ , which is determined by the set of positions $\{i : x_i \in A\}$ .

The index $\Delta^S(x_1, \dots, x_r)$ is the number of different subsamples induced by the sets of $S$ , i.e. the number of distinct sets of positions $\{i : x_i \in A\}$ with $A \in S$ . It is at most $2^r$ . The growth function is

m^S(r) = \max_{x_1, \dots, x_r} \Delta^S(x_1, \dots, x_r),

the maximum over all samples of size $r$ . For the rays $\{y \le a\}$ on the line $m^S(r) = r + 1$ ; for the open subsets of $[0,1]$ , $m^S(r) = 2^r$ .

The function $\Phi(n, r)$ on pairs of natural numbers is defined by the recurrence (1) of the paper,

\Phi(n, r) = \Phi(n, r-1) + \Phi(n-1, r-1), \qquad \Phi(0, r) = 1, \qquad \Phi(n, 0) = 1 .

In the Lean development these are index S x for x : Fin r → X, growthFunction S r, and Phi n r in the namespace VapnikChervonenkis.GrowthFunction.

Formalization targets

Goal: Theorem 1 (p. 267)

For a nonempty class $S$ , either $m^S(r) = 2^r$ for every $r$ , or, with $n \ge 1$ the first value of $r$ at which $m^S(r) = 2^r$ fails,

m^S(r) \le r^n + 1 \qquad \text{for all } r \ge 0 .

The exponent $n$ is pinned down by minimality: $m^S(n) \ne 2^n$ and $m^S(r) = 2^r$ for every $r < n$ .

Milestones, in the order the proof uses them

The index is at most $2^r$ (p. 265): $\Delta^S(x_1, \dots, x_r) \le 2^r$ .
The closed form of $\Phi$ (p. 266): $\Phi(n, r) = \sum_{k=0}^{n} \binom{r}{k}$ for $r > n$ , and $\Phi(n, r) = 2^r$ for $r \le n$ .
The polynomial bound (p. 266): $\Phi(n, r) \le r^n + 1$ for $n > 0$ , $r \ge 0$ .
Lemma 1 (p. 266): if $1 \le n \le i$ and $\Delta^S(x_1, \dots, x_i) \ge \Phi(n, i)$ , some subsample $x_{i_1}, \dots, x_{i_n}$ of size $n$ satisfies $\Delta^S(x_{i_1}, \dots, x_{i_n}) = 2^n$ .
The first display of the proof of Theorem 1 (p. 268): if $m^S(n) \ne 2^n$ , then $\Delta^S(x_1, \dots, x_r) < \Phi(n, r)$ for every sample of size $r > n$ .

Significance

Theorem 1 converts the distribution-free bound $\mathbf P\{\pi^{(l)} > \varepsilon\} \le 4 m^S(2l) e^{-\varepsilon^2 l/8}$ of Theorem 2 of the same paper into a convergence statement: whenever the growth function is not identically $2^r$ , the right-hand side is a polynomial times a decaying exponential, so relative frequencies converge to probabilities uniformly over $S$ . The same dichotomy underlies sample-complexity bounds for PAC learning, covering-number bounds for VC classes, and the notion of VC dimension itself; the exponent $n$ is the VC dimension plus one.

The results are classical and proved. Mathlib contains the Sauer–Shelah lemma for finite set families (Finset.card_shatterer_le_sum_vcDim in Mathlib/Combinatorics/SetFamily/Shatter.lean). The platform has several open formal statements of Sauer's lemma for growth functions over finite point sets (ComputationalLearning.sauer_lemma, FoundationsML.RademacherVC.sauer_lemma, HighDimProb.Chaining.sauer_shelah) and a closed form for Kearns–Vazirani's $\Phi$ (ComputationalLearning.phi_closed_form, the same recurrence). No statement of Theorem 1, and none over the paper's sequence model of samples, is formalized. This mission formalizes the paper's own route: Lemma 1 in the paper's form, the polynomial bound on $\Phi$ , and the dichotomy with the minimal exponent. It also provides the growth function over sequences that the companion missions (Theorem 2, and the entropy criterion Theorem 4) are stated with.

Difficulty

The obvious argument has two steps: bound $\Delta^S$ by $\Phi(n, r)$ whenever no subsample of size $n$ is fully split, then bound $\Phi(n, r)$ by $r^n + 1$ . The first step is the Sauer–Shelah lemma, and it does not follow from counting alone. A class can induce many subsamples on $r$ points without inducing all $2^n$ on any fixed $n$ of them, and no counting of subsamples one position at a time rules this out. The second step is elementary but must hold uniformly for all $r$ , including $r \le n$ , where $\Phi(n, r) = 2^r$ and the bound $2^r \le r^n + 1$ uses $r \le n$ .

Samples are sequences, not sets. With repeated points, two positions carrying the same point can never be separated, so Lemma 1 must be applied to position sets rather than point sets. Transferring Mathlib's set-family lemma to this setting is a bookkeeping step that does not reduce to a citation.

Formalization scope

A sample of size $r$ is x : Fin r → X with positions $0, \dots, r-1$ ; repetitions are allowed. A subsample of size $n$ is x ∘ e with e : Fin n → Fin i strictly increasing.
index S x counts distinct Finset (Fin r) of positions {i | x i ∈ A} with A ∈ S. Counting point sets A ∩ {x_1, …, x_r} instead would be a different object when points repeat; the growth function over finite sets of points (as in ComputationalLearning_VC) differs from $m^S$ when $X$ has fewer than $r$ elements.
growthFunction S r is the supremum in ℕ of index S x over all samples; the family is bounded by $2^r$ , so it is a maximum. When $X$ is empty and $r \ge 1$ its value is $0$ ; $m^S(0) = 1$ exactly when $S$ is nonempty.
Phi is defined by the recurrence (1). The paper introduces $\Phi(n, r)$ as the maximal number of components into which $r$ hyperplanes cut $n$ -space; that geometric identity (Example 3) is not part of this mission.
Hypothesis added to Theorem 1: $S$ nonempty. The paper calls $n$ "a positive constant"; for $S = \emptyset$ every index is $0$ , the first violation is at $r = 0$ and $n$ is not positive.
Corrections of the printed text. (a) The closed form of $\Phi$ is printed with summand $\binom{r}{n}$ ; it is formalized with $\binom{r}{k}$ (the printed version already fails at $\Phi(1, 2) = 3$ ). (b) The proof of Theorem 1 ends "for $r > 0$ , $\Phi(n, r) < r^n + 1$ ", which fails at $n = r = 1$ ; the milestone is the non-strict bound stated on p. 266. The milestone texts are verbatim from the page.
Milestone 5 states the first display of the proof of Theorem 1 with its hypothesis as printed: $n$ is the first value of $r$ with $m^S(r) \ne 2^r$ .
The goal keeps the minimality of $n$ . A version stating $m^S(r) \le r^n + 1$ for an arbitrary $n$ with $m^S(n) \ne 2^n$ would be a different theorem, and a version that drops the first disjunct or allows $n = 0$ would trivialize.

No measure, σ-algebra or probability appears: the class $S$ is an arbitrary collection of subsets of a bare type. Needed infrastructure: basic API for index (monotonicity in the sample, behaviour under restriction to a subsample) and a bridge between samples and Mathlib's set families (Finset.Shatters, Finset.vcDim). Both are reusable by the two companion missions of this paper, and contributions of either are welcome.

Selected references

V. N. Vapnik and A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and Its Applications 16(2) (1971) 264–280 (English translation by B. Seckler). https://doi.org/10.1137/1116025
N. Sauer, On the density of families of sets, Journal of Combinatorial Theory, Series A 13 (1972) 145–147. https://doi.org/10.1016/0097-3165(72)90019-2
S. Shelah, A combinatorial problem; stability and order for models and theories in infinitary languages, Pacific Journal of Mathematics 41 (1972) 247–261. https://doi.org/10.2140/pjm.1972.41.247
A. Blumer, A. Ehrenfeucht, D. Haussler and M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4) (1989) 929–965. https://doi.org/10.1145/76359.76371

9 thms2 active usersReviewed

Linear Optimization Operations Research Theoretical Computer Science·Captain: mikedeng1

Santa Claus Schedules Jobs on Unrelated Machines: The Configuration LP Has Integrality Gap at Most 33/17Research Paper

Motivation

Scheduling jobs on unrelated machines so as to minimize the makespan (the time at which the last machine finishes) is one of the central problems of approximation algorithms. For the general problem, Lenstra, Shmoys and Tardos (1990) gave a 2-approximation and showed that no polynomial-time algorithm achieves a factor below $3/2$ unless P = NP; closing the gap between $3/2$ and $2$ has been open since.

The restricted assignment problem is the special case in which every job $j$ has a single size $p_j$ and may only run on a given set $\Gamma(j)$ of machines. The $3/2$ hardness already holds here, and the best known algorithms were still $2$ -approximations. Every linear program previously used for the problem has integrality gap $2$ , so a better LP lower bound was the natural target.

Svensson (2011) showed that the configuration LP of Bansal and Sviridenko (2006), whose variables assign whole sets of jobs to machines, has integrality gap at most $33/17 \approx 1.9412$ . Its optimum therefore gives a polynomial-time estimate of the optimal makespan within a factor strictly better than $2$ .

1990: Lenstra, Shmoys, Tardos, 2-approximation for unrelated machines, and $3/2$ hardness already for restricted assignment.
2006: Bansal and Sviridenko introduce the configuration LP for the max–min variant (the Santa Claus problem).
2008: Feige shows the configuration LP has constant integrality gap for restricted Santa Claus, and Asadpour, Feige and Saberi (2008) give a local search proof of a factor-4 gap.
2011: Svensson adapts that local search to makespan and proves the gap $33/17$ for restricted assignment (arXiv:1011.1168).

Setting

An instance consists of finite sets $J$ (jobs) and $M$ (machines), sizes $p_j \ge 0$ , and for each job a set $\Gamma(j) \subseteq M$ . A schedule is a map $\sigma : J \to M$ with $\sigma(j) \in \Gamma(j)$ . The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$ , and the makespan is the largest load. $\mathrm{OPT}$ is the least makespan of a schedule.

For a target makespan $T$ , a configuration for machine $i$ is a set $C \subseteq J$ of jobs that may all run on $i$ ( $i \in \Gamma(j)$ for $j \in C$ ) with $p(C) = \sum_{j \in C} p_j \le T$ . Write $\mathcal C(i,T)$ for the set of configurations. The configuration LP asks for $x_{i,C} \ge 0$ with

\text{[C-LP]}\qquad \sum_{C \in \mathcal C(i,T)} x_{i,C} \le 1 \quad (i \in M), \qquad \sum_{i \in M}\ \sum_{C \in \mathcal C(i,T),\ C \ni j} x_{i,C} \ge 1 \quad (j \in J).

Its dual has variables $y_i, z_j \ge 0$ and constraints $y_i \ge \sum_{j \in C} z_j$ for all $i$ and $C \in \mathcal C(i,T)$ . $\mathrm{OPT}_{LP}$ is the least $T$ at which [C-LP] is feasible, and $\mathrm{OPT}_{LP} \le \mathrm{OPT}$ .

In the Lean development these are configs Γ p T i, CLPFeasible Γ p T, CLPDualFeasible Γ p T y z and schedLoad p σ i, in the namespace RestrictedAssignment.Svensson.

Formalization targets

Goal: Theorem 4.1

For every instance with $p \ge 0$ and every $T \ge 0$ ,

\text{[C-LP] feasible at } T \ \Longrightarrow\ \exists\, \sigma : J \to M,\ \ \sigma(j) \in \Gamma(j)\ \forall j,\quad \sum_{j : \sigma(j) = i} p_j \le \tfrac{33}{17}\, T \ \ \forall i .

Equivalently $\mathrm{OPT} \le \tfrac{33}{17}\,\mathrm{OPT}_{LP}$ . The statement is scale-free and does not define $\mathrm{OPT}_{LP}$ .

Milestones

The milestones follow the paper's proof, which normalizes $\mathrm{OPT}_{LP} = 1$ and sets $R = 16/17$ :

a dual solution with $\sum_i y_i < \sum_j z_j$ makes [C-LP] infeasible;
the local search, Algorithm 2 (ExtendSchedule), keeps its partial schedule valid (load at most $1 + R$ , at most one big job per machine);
when the algorithm has no potential move, an explicit pair $(y^*, z^*)$ is dual feasible (Claim 4.7) and has $\sum y^* < \sum z^*$ (Claim 4.8);
hence, if [C-LP] is feasible, a potential move always exists (Lemma 4.6);
the algorithm has no infinite run (Lemma 4.9);
[C-LP] feasible at $T = 1$ gives a schedule of makespan at most $1 + 16/17$ .

Three facts from Section 2 complete the list: normalization by scaling, $\mathrm{OPT}_{LP} \le \mathrm{OPT}$ , and monotonicity of feasibility in $T$ .

Significance

The theorem shows that the configuration LP is a strictly stronger relaxation than those behind the factor- $2$ algorithms. With the known polynomial-time approximate solvability of the LP, it gives a polynomial-time algorithm that estimates the optimal makespan of restricted assignment within $33/17 + \epsilon$ . The local search in the proof finds a schedule of the same quality, but it is not known to run in polynomial time. Later work lowered the constant to $11/6$ (Jansen and Rohwedder, 2017) along the same lines.

The result is proved on paper. As far as known, no part of it has a machine-checked proof. Formalizing it gives:

a reusable definition of the configuration LP and its dual certificate;
a precise, nondeterministic model of a local search whose termination rests on a lexicographic potential;
a check of a proof that has many cases. The formalization already exposed two edge cases:
- Claim 4.8 fails when $j_{\mathrm{new}}$ has size $0$ and no admissible machine;
- the termination proof needs positive job sizes. With a job of size $0$ , the algorithm can move it back and forth between two tied machines forever.

The milestones are stated with the corresponding hypotheses.

Difficulty

The obvious approach, rounding a fractional configuration solution, loses a factor $2$ . If each machine takes one configuration and the collisions of jobs chosen twice or not at all are repaired, the repair can double a load. This is where every earlier LP-based bound stalls.

The milestones along the paper's route are hard for two reasons. First, the dual pair $(y^*, z^*)$ rounds job sizes down by class (big to $11/17$ , medium to $9/17$ ). Proving $\sum y^* < \sum z^*$ requires a case analysis over how each blocked machine came to be blocked. The two claims are therefore false for arbitrary states of the search and hold only for states the algorithm actually reaches, so the invariants of reachable states have to be formalized too. Second, the search both adds and removes blockers, so no simple quantity decreases at every step. Termination needs a potential defined on the whole history of the search.

Formalization scope

Jobs and machines are finite types with decidable equality, sizes are real numbers with $p_j \ge 0$ , and admissible machines are a Finset per job. Schedules are total maps $J \to M$ with $\sigma(j) \in \Gamma(j)$ stated explicitly. Partial schedules are maps $J \to$ Option M. Constants are exact rationals in $\mathbb R$ . Values of moves live in Lex (ℝ × ℝ).

Algorithm 2 is a step relation Step, not a function. The move of minimum lexicographic value is a hypothesis on the chosen pair, so every tie-breaking rule is covered. The blocker tree is stored as its list of blockers in insertion order. Claims 4.7, 4.8 and Lemma 4.6 quantify over states reachable from the initial state, as their proofs require. Lemma 4.9 asserts that no infinite run exists.

Three statements would trivialize the goal, and the formalization rules them out:

a schedule allowed to use machines outside $\Gamma(j)$ ;
a target $T < 0$ ;
an LP missing either constraint row.

Theorem 1.1 (polynomial time), the separation oracle, and Section 3's two-size case are not part of the mission.

Useful contributions include:

the weak-duality certificate;
the scaling and monotonicity facts;
the invariants of reachable states (each job lies in at most one blocker, blockers on a machine are never reassigned while present);
the two claims and the termination argument.

The configuration LP definitions are reusable for the Santa Claus problem and for bin packing.

Selected references

O. Svensson, Santa Claus Schedules Jobs on Unrelated Machines, arXiv:1011.1168v2, 2011; SIAM J. Comput. 41(5), 2012. https://arxiv.org/abs/1011.1168
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Math. Programming 46, 1990. https://doi.org/10.1007/BF01585745
N. Bansal, M. Sviridenko, The Santa Claus problem, STOC 2006. https://doi.org/10.1145/1132516.1132522
A. Asadpour, U. Feige, A. Saberi, Santa Claus meets hypergraph matchings, APPROX 2008; ACM Trans. Algorithms 8(3), 2012. https://doi.org/10.1145/2229163.2229168
K. Jansen, L. Rohwedder, On the configuration-LP of the restricted assignment problem, SODA 2017. https://arxiv.org/abs/1611.01934

13 thms2 active usersReviewed

Completed

Graph Theory Linear algebra Probability+1·Captain: mikedeng1

Matching Is as Easy as Matrix Inversion: Steps 1–3 Find a Minimum Weight Perfect Matching with Probability at Least 1/2Research Paper

Motivation

Deciding whether a graph has a perfect matching, and finding one, are basic problems of combinatorial optimization; Edmonds' blossom algorithm solves them sequentially in polynomial time. The question behind this paper is whether they can also be solved in parallel, in polylogarithmic time on polynomially many processors (the class NC, or RNC when random bits are allowed).

The algebraic route to that question goes through the Tutte matrix. Tutte (1947) showed that a graph has a perfect matching if and only if its Tutte matrix, a skew-symmetric matrix of indeterminates, has a nonzero determinant. Substituting random numbers for the indeterminates turns this into a randomized parallel decision procedure, but it does not say which perfect matching exists, and a graph may have exponentially many.

Mulmuley, Vazirani and Vazirani (Combinatorica 7 (1987) 105–113) resolve this with the isolating lemma: random small integer weights make the minimum weight member of an arbitrary set family unique with probability at least one half. Once a single perfect matching is isolated, one determinant and one adjugate of an integer matrix reveal it. The isolating lemma has since become a standard tool in randomized algorithms and complexity theory, well beyond matchings.

Timeline:

1947, Tutte: a graph has a perfect matching iff the determinant of its Tutte matrix is a nonzero polynomial (doi:10.1112/jlms/s1-22.2.107).
1979, Lovász: random substitution into the Tutte matrix gives a randomized algorithm for deciding whether a perfect matching exists (Fundamentals of Computation Theory, LNCS 1979).
1986, Karp, Upfal and Wigderson: the first RNC algorithm that finds a perfect matching, with RNC³ running time (Combinatorica 6 (1986) 35–48).
1987, Mulmuley, Vazirani and Vazirani: the isolating lemma and an RNC² algorithm that inverts one integer matrix (this paper).
2016–2017, Fenner, Gurjar and Thierauf (arXiv:1601.06319) for bipartite graphs, and Svensson and Tarnawski (arXiv:1704.01929) for general graphs, partially derandomize the isolation step and place perfect matching in quasi-NC. Whether perfect matching is in NC remains open.

Setting

A set system $(S, F)$ is a finite set $S$ of elements together with a family $F$ of subsets of $S$ . Given a weight $w_x \in \mathbb{N}$ for each element $x$ , the weight of $T \subseteq S$ is $w(T) = \sum_{x \in T} w_x$ , and $F$ has a unique minimum weight set if one member of $F$ is strictly lighter than every other member.

A graph $G$ has vertices $v_1, \dots, v_n$ (in Lean, Fin n, in their natural order) and edge set $E$ , with $m = |E|$ . A perfect matching is a set $M \subseteq E$ such that every vertex lies in exactly one edge of $M$ . The edges and the perfect matchings of $G$ form a set system.

Given edge weights $w_{ij} \in \mathbb{N}$ , the integer matrix $B$ is obtained from the Tutte matrix by substituting $2^{w_{ij}}$ for its indeterminates:

b_{ij} = 2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i < j; \qquad b_{ij} = -2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i > j; \qquad b_{ij} = 0 \ \text{otherwise}.

$|B|$ is its determinant, $B_{ij}$ the submatrix with row $i$ and column $j$ removed, and $\operatorname{adj}(B)$ its adjugate, whose $(j, i)$ entry is $\pm|B_{ij}|$ .

The algorithm of §4 is:

Step 1. Compute $|B|$ and obtain $w$ , the exponent for which $2^{2w}$ is the highest power of 2 dividing $|B|$ .
Step 2. Compute $\operatorname{adj}(B)$ .
Step 3. Output every edge $(v_i, v_j)$ for which the integer $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.

Formalization targets

Goal: Steps 1–3 find a minimum weight perfect matching with probability at least 1/2

For every graph $G$ that has a perfect matching, with edge weights drawn uniformly and independently from $\{1, \dots, 2m\}$ ,

\Pr\bigl[\text{the output of Steps 1–3 is a perfect matching of } G \text{ of minimum weight}\bigr] \ \ge\ \tfrac12 .

This is the correctness half of the paper's Theorem (p. 109). The probability is a fraction of the $(2m)^m$ weight functions.

Milestones

Lemma 1 (isolating lemma): for a nonempty family $F$ over an $n$ -element set, weights uniform in $[1, 2n]$ give a unique minimum weight set with probability $\ge 1/2$ .
Isolation for perfect matchings (§4): with edge weights uniform in $[1, 2m]$ , the minimum weight perfect matching is unique with probability $\ge 1/2$ .
Odd-cycle cancellation (proof of Lemma 2): for a skew-symmetric integer matrix, only permutations all of whose cycles have even length contribute to the determinant.
Lemma 2: if the minimum weight perfect matching is unique, of weight $w$ , then $|B| \neq 0$ and $2^{2w}$ is the highest power of 2 dividing $|B|$ .
Lemma 3: under the same hypothesis, $(v_i, v_j) \in M$ iff $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.
Steps 1–3, deterministic core: under the same hypothesis, Step 1 obtains the weight of $M$ and Steps 2–3 output exactly $M$ .

Two companion items are included but are not on the goal's path: the maximum weight version of Lemma 1 (the remark after its proof, p. 107) and Lemma 4 (p. 110): the lexicographically largest matching set, for vertices sorted by decreasing weight, is a heaviest matching set.

Significance

The isolating lemma is a statement about arbitrary set families with no structure assumed, which is why it transfers: it is used for isolating satisfying assignments, for parallel algorithms for exact matching and minimum weight matchings with small weights, and in the derandomization program that led to the quasi-NC matching algorithms cited above. Lemmas 2 and 3 are the bridge from a combinatorial object (a unique minimum weight perfect matching) to arithmetic facts about one integer matrix (2-adic valuations of its determinant and adjugate entries), which is what makes the algorithm reducible to matrix inversion.

All results of this mission are proved in the paper. What the mission adds is machine-checked proofs: Mathlib at the pinned revision contains Tutte's barrier theorem but neither the isolating lemma nor the Tutte-matrix determinant arguments, and a search of Prove2Me (September 2026) found no formalization of them. A complete development yields a reusable isolating lemma for finite set systems and a reusable determinant expansion for skew-symmetric matrices.

Difficulty

The probabilistic step is a union bound over elements, but the event bounded for each element, "the element is ambiguous", is defined through a threshold that depends on all the other weights; the argument needs independence of that threshold from the element's own weight, which is a product-space (Fubini-type) counting statement rather than a one-line estimate. In a counting formalization over $\{1, \dots, 2n\}^S$ , each fibre must be handled separately.

The determinant steps require a genuine combinatorial involution on permutations: reversing an odd cycle must be well defined (a canonical choice of cycle) and self-inverse, preserve the sign, negate the value, and in Lemma 3 also preserve the constraint $\sigma(i) = j$ , which is where "since $n$ is even, there are at least two odd cycles" enters. Relating a permutation with only even cycles to a pair of perfect matchings whose union is its trail is the second nontrivial bijection. Divisibility must be tracked exactly: $2^{2w}$ divides every term, and every term other than the one of $M$ is divisible by $2^{2w+1}$ .

Formalization scope

Vertices are Fin n and the graph is G : SimpleGraph (Fin n) with decidable adjacency. Edge weights are functions G.edgeSet → ℕ; perfect matchings are Finset G.edgeSet in which every vertex lies in exactly one edge. The matrix is weightedTutteMatrix G w : Matrix (Fin n) (Fin n) ℤ, with the positive entry above the diagonal. Probabilities are ratios of counts over Fintype.piFinset (fun _ => Finset.Icc 1 (2m)), stated without division as $(2m)^m \le 2 \cdot \#\{\dots\}$ ; the weight range is exactly $[1, 2m]$ (resp. $[1, 2n]$ in Lemma 1). " $x/2^k$ is odd" means $2^k \mid x$ and $x/2^k$ is an odd integer. The minor $|B_{ij}|$ is taken as Mathlib's signed cofactor adjugate B j i; parity and divisibility do not see the sign. Step 1's $w$ is $\lfloor \nu_2(|B|)/2\rfloor$ .

Added hypotheses: Lemma 1 and its maximum version assume $F$ nonempty (the printed lemma omits it and is false for $F = \emptyset$ ); the goal and the isolation milestone assume $G$ has a perfect matching, which is the paper's own input assumption. Lemmas 2 and 3 allow arbitrary natural weights, as printed.

The algorithm's output is defined from $B$ , $|B|$ , $\operatorname{adj}(B)$ , the 2-adic valuation and parity only; a definition of the output that refers to perfect matchings or to minimality would trivialize the goal and is ruled out. The complexity half of the Theorem (RNC², $O(n^{3.5}m)$ processors), which rests on Pan's matrix-inversion algorithm, is not formalized, nor are §5a–b and §6.

Contributions welcome: proofs of the milestones in any order, general lemmas about the permutation expansion of skew-symmetric determinants, and a counting form of the union bound over product spaces, all of which are reusable outside this mission.

Selected references

K. Mulmuley, U. V. Vazirani, V. V. Vazirani, Matching is as easy as matrix inversion, Combinatorica 7(1) (1987) 105–113. https://doi.org/10.1007/BF02579206
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
R. M. Karp, E. Upfal, A. Wigderson, Constructing a perfect matching is in random NC, Combinatorica 6(1) (1986) 35–48. https://doi.org/10.1007/BF02579407
L. Lovász, On determinants, matchings, and random algorithms, Fundamentals of Computation Theory (FCT '79), 1979, 565–574.
S. Fenner, R. Gurjar, T. Thierauf, Bipartite perfect matching is in quasi-NC, STOC 2016. https://arxiv.org/abs/1601.06319
O. Svensson, J. Tarnawski, The matching problem in general graphs is in quasi-NC, FOCS 2017. https://arxiv.org/abs/1704.01929

10 thms2 active usersReviewed

Completed

Convex Optimization Graph Theory Operations Research·Captain: mikedeng1

Cones of Matrices and Set-Functions and 0–1 Optimization IV: Clique, Odd Hole, Odd Wheel and Odd Antihole Constraints Hold after One Round of N₊Research Paper

Motivation

The stable set problem (find a largest, or maximum-weight, set of pairwise non-adjacent nodes in a graph) is NP-hard, and its linear programming relaxations have been studied since the 1970s as a test bed for polyhedral combinatorics. Lovász and Schrijver (SIAM J. Optim. 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation to a cone of $(n+1)\times(n+1)$ matrices, impose conditions every 0–1 solution satisfies, and project back. Its semidefinite version, the operator $N_+$ , is one of the first systematic uses of positive semidefinite constraints in combinatorial optimization, and it is the ancestor of the Sherali–Adams, Lasserre and sum-of-squares hierarchies used today in approximation algorithms and proof complexity.

For the stable set problem the paper measures the strength of the operators by an index: how many rounds are needed before a given valid inequality is implied. This mission formalizes the paper's result that one round of $N_+$ already implies four of the classical families of facets of the stable set polytope.

Timeline:

1975: Chvátal shows that the rank constraint of a connected α-critical graph defines a facet of its stable set polytope (Chvátal 1975); clique, odd hole and odd antihole constraints are special rank constraints.
1981–88: Grötschel, Lovász and Schrijver show that the weighted stable set problem is solvable in polynomial time for perfect and $h$ -perfect graphs, through the theta body $\mathrm{TH}(G)$ (Grötschel, Lovász, Schrijver 1988).
1991: Lovász and Schrijver define the operators $N$ and $N_+$ and prove Corollary 2.15: clique, odd hole, odd wheel and odd antihole constraints have $N_+$ -index 1.

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$ . The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \ \forall x \in K\}$ . Let $Q$ be the cone spanned by the 0–1 vectors with $x_0 = 1$ . For a convex cone $K \subseteq Q$ , the matrix cone $M_+(K)$ consists of the symmetric positive semidefinite matrices $Y = (y_{ij})$ with $y_{ii} = y_{0i}$ for $1 \le i \le n$ and $u^{\mathsf T}Yv \ge 0$ for all $u \in K^*$ , $v \in Q^*$ . The operator is

N_+(K) = \{Ye_0 : Y \in M_+(K)\},

and $N_+^0(K) = K$ , $N_+^t(K) = N_+(N_+^{t-1}(K))$ .

Let $G = (V, E)$ be a finite graph with no isolated nodes (the paper's standing assumption for Section 2). $\mathrm{STAB}(G)$ is the convex hull of incidence vectors $\chi^A$ of stable sets $A$ . $\mathrm{FRAC}(G)$ is the polytope given by $x_i \ge 0$ and $x_i + x_j \le 1$ for $ij \in E$ . $\mathrm{FR}(G) \subseteq \mathbb R^{V\cup\{0\}}$ is the cone $x_i \ge 0$ , $x_i + x_j \le x_0$ . The relaxations are

N_+^r(G) = \{x \in \mathbb R^V : (1, x) \in N_+^r(\mathrm{FR}(G))\},

so $N_+^0(G) = \mathrm{FRAC}(G) \supseteq N_+^1(G) \supseteq \dots \supseteq \mathrm{STAB}(G)$ . The $N_+$ -index of an inequality $a^{\mathsf T}x \le b$ valid for $\mathrm{STAB}(G)$ is the least $r$ with $a^{\mathsf T}x \le b$ valid for $N_+^r(G)$ .

The four constraint families are:

clique: $\sum_{i\in B} x_i \le 1$ for a clique $B$ ;
odd hole: $\sum_{i\in C} x_i \le \frac12(|C|-1)$ for $C$ inducing a chordless odd cycle;
odd wheel: $\sum_{i\in U\setminus\{u_0\}} x_i + \frac{|U|-2}{2}x_{u_0} \le \frac{|U|-2}{2}$ for $U$ inducing an odd wheel with center $u_0$ (an odd hole plus a node adjacent to all of it);
odd antihole: $\sum_{i\in D} x_i \le 2$ for $D$ inducing a chordless odd cycle in the complement of $G$ .

The contraction of a node $v$ turns $a^{\mathsf T}x \le b$ into the inequality with the coefficients of $v$ and its neighbours removed and right-hand side $b - a_v$ .

Formalization targets

Goal: Corollary 2.15

For every graph $G$ without isolated nodes, each clique constraint (clique of size at least 3), odd hole constraint, odd wheel constraint and odd antihole constraint has $N_+$ -index exactly 1:

a^{\mathsf T}x \le b \text{ holds on } N_+^1(G) \quad\text{and fails somewhere on } \mathrm{FRAC}(G).

Milestones

Lemma 1.5: for a closed convex cone $K \subseteq Q$ and $a$ with $a_i \le 0$ ( $i \ge 1$ ), $a_0 \ge 0$ , if $a^{\mathsf T}x \ge 0$ holds on $K \cap G_i$ (where $G_i = \{x_i = x_0\}$ ) for every $i$ with $a_i < 0$ , then it holds on $N_+(K)$ .
Lemma 2.14: if $a^{\mathsf T}x \le b$ is valid for $\mathrm{STAB}(G)$ , and the contraction of every node with positive coefficient is valid for $N_+^r(G)$ , then $a^{\mathsf T}x \le b$ is valid for $N_+^{r+1}(G)$ .
Bipartite support (Section 2.c): an inequality valid for $\mathrm{STAB}(G)$ whose nonzero-coefficient nodes induce a bipartite graph is valid for $\mathrm{FRAC}(G)$ .
Contraction property (Section 2.d): contracting a node with positive coefficient in any of the four constraints leaves positive-coefficient nodes that induce a bipartite subgraph.

Further result

Corollary 2.19 (first sentence): the $N_+$ -index of a $\mathrm{STAB}(G)$ -valid inequality $a^{\mathsf T}x \le b$ is at most the independence number of the subgraph induced by the nodes with positive coefficient.

Significance

Corollary 2.15 shows that a single round of $N_+$ , a relaxation over which one can optimize in polynomial time for each fixed number of rounds (the paper's Theorem 2.1), captures all clique, odd hole, odd wheel and odd antihole inequalities at once. Consequently $N_+(G) = \mathrm{STAB}(G)$ for every $h$ -perfect graph, in particular for perfect and $t$ -perfect graphs. The result is a standard reference point when comparing lift-and-project hierarchies, and the lemmas behind it (Lemma 1.5 and Lemma 2.14) are the paper's general tools for bounding $N_+$ -ranks.

The theorem was proved in 1991. To our knowledge it has not been machine-checked: this mission would produce the first formal development of the Lovász–Schrijver $N_+$ operator, its iterates, and the stable set relaxations $\mathrm{STAB}$ , $\mathrm{FRAC}$ , $\mathrm{FR}$ in Lean.

Difficulty

The lower bound (each constraint fails on $\mathrm{FRAC}(G)$ ) is a direct computation; the upper bound is where the work lies. The obvious approach, deriving each constraint from the linear conditions on the lifted matrix $Y$ alone, cannot succeed: those conditions define the linear operator $N$ , and the goal is specifically about what positive semidefiniteness adds. The general lemmas are stated for arbitrary cones and require a working theory of polar cones and closedness in $\mathbb R^{n+1}$ , including closedness of the iterates $N_+^r(\mathrm{FR}(G))$ , which the paper uses without comment. The graph-theoretic steps require facts about the stable set and fractional stable set polytopes of bipartite graphs and a careful case analysis of chordless odd cycles in a graph and in its complement, none of which is in Mathlib.

Formalization scope

Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι, with none the special coordinate $x_0$ . For graphs, ι := V.
$M$ is defined by condition (iii) with polar cones, not by its reformulations. Only $M_+$ , $N_+$ and their iterates are defined; the linear operator $N$ is not used.
Lemma 1.5 carries the hypothesis that $K$ is closed. The paper takes it tacitly (all its cones are polyhedral); without it the lemma fails, since $N_+(K)$ depends only on the closure of $K$ .
$\mathrm{FR}(G)$ is defined by its constraints, which agree with the paper's "cone spanned by the vectors $(1,x)$ , $x \in \mathrm{FRAC}(G)$ " because $G$ has no isolated nodes. Every graph statement carries the no-isolated-nodes hypothesis.
Contraction is written on the same graph $G$ as a zeroed coefficient vector, rather than on the subgraph $G - \Gamma(v) - v$ .
Odd holes include triangles; odd antiholes have at least 5 nodes (a 3-node "antihole" is a stable set, for which the constraint is false); odd wheels are an odd hole plus a center adjacent to all its nodes.
Clique constraints in the goal are restricted to cliques with at least 3 nodes: cliques of size 1 or 2 give inequalities already valid on $\mathrm{FRAC}(G)$ , of index 0.
" $N_+$ -index at most $r$ " is stated as validity on $N_+^r(G)$ ; the index itself is stated with IsLeast, never with an infimum that would default to 0 on an empty set.

A formalization asserting only validity on $N_+^1(G)$ , or only for one fixed graph, would be weaker than the paper's statement and is ruled out: the goal states the exact index for all graphs without isolated nodes and all four families.

Not formalized: the linear operator $N$ and its results, the polynomial-time separation results (Theorem 2.1, Corollaries 2.20–2.21), the theta-body results (Lemma 2.17, Corollary 2.18), graph indices (Corollary 2.16), and the second sentence of Corollary 2.19.

Reusable infrastructure includes the polar cone, the matrix cone $M_+$ and the $N_+$ operator (usable for any 0–1 program), the polytopes $\mathrm{STAB}$ and $\mathrm{FRAC}$ , and odd holes, antiholes and wheels as finite-set predicates. Contributions proving closedness of the iterates, the integrality of $\mathrm{FRAC}$ for bipartite graphs, or the $M$ -cone reformulations (iii′)–(iii″) are welcome.

Selected references

L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2), 1991, 166–190. https://doi.org/10.1137/0801013
M. Grötschel, L. Lovász and A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988 (2nd ed. 1993). https://doi.org/10.1007/978-3-642-78240-4
V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory B 18, 1975, 138–154. https://doi.org/10.1016/0095-8956(75)90041-6

8 thms2 active usersReviewed

Graph Theory Linear Optimization Operations Research·Captain: mikedeng1

Cones of Matrices and Set-Functions and 0–1 Optimization III: The Defect of a Stable Set Inequality Bounds Its N-IndexResearch Paper

Motivation

Many 0–1 optimization problems can be written as linear programs over the convex hull of the 0–1 points of a polytope, but that hull usually has no manageable description by inequalities. Lift-and-project methods approximate it by a sequence of convex sets. Each set comes from a linear or semidefinite system in more variables, followed by a projection. Lovász and Schrijver introduced the operator $N$ in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim. 1(2), 1991). For any polytope $K$ in the unit cube, $n$ rounds of $N$ reach the 0–1 hull (their Theorem 1.4), and each round keeps linear optimization tractable.

The stable set problem is the paper's main test case, and the question is quantitative: how many rounds does a given valid inequality need? Section 2.c answers it with a single number read off a linear program. Later work on the rank of lift-and-project hierarchies uses this measure: Balas, Ceria and Cornuéjols's lift-and-project cuts (1993), the Sherali–Adams and Lasserre comparisons of Laurent (2003), and the rank lower bounds for stable set relaxations in the decades since.

Setting

Let $G = (V, E)$ be a finite graph with no isolated nodes, which is the paper's standing assumption for Section 2. For $A \subseteq V$ let $\chi^A \in \mathbb R^V$ be its incidence vector.

The stable set polytope is $\mathrm{STAB}(G) = \operatorname{conv}\{\chi^A : A \text{ stable}\}$ .
The fractional stable set polytope $\mathrm{FRAC}(G)$ is the solution set of $x_i \ge 0$ ( $i \in V$ ) and $x_i + x_j \le 1$ ( $ij \in E$ ).

Homogenize with a new coordinate $x_0$ . Let $Q \subseteq \mathbb R^{V \cup\{0\}}$ be the cone spanned by the 0–1 vectors with $x_0 = 1$ , and let $\mathrm{FR}(G)$ be the cone given by $x_i \ge 0$ and $x_i + x_j \le x_0$ . For a convex cone $K$ with polar cone $K^* = \{u : u^{\mathsf T}x \ge 0 \ \forall x \in K\}$ , the matrix cone $M(K)$ is the set of symmetric matrices $Y$ that satisfy two conditions:

$y_{ii} = y_{0i}$ for every $i$ ;
$u^{\mathsf T} Y v \ge 0$ for all $u \in K^*$ and $v \in Q^*$ .

The operator is $N(K) = \{Y e_0 : Y \in M(K)\}$ . Its iterates are $N^0(K) = K$ and $N^t(K) = N(N^{t-1}(K))$ . On the graph side, $N^t(G) = \{x : \binom1x \in N^t(\mathrm{FR}(G))\}$ , so $N^0(G) = \mathrm{FRAC}(G)$ and $\mathrm{STAB}(G) \subseteq N^t(G)$ for every $t$ .

Let $a^{\mathsf T}x \le b$ be valid for $\mathrm{STAB}(G)$ , with $a \in \mathbb Z_+^V$ and $b \in \mathbb Z_+$ . Two numbers are attached to it:

its N-index $k$ is the least $t$ such that $a^{\mathsf T}x \le b$ is valid for $N^t(G)$ ;
its defect is $r = 2\max\{a^{\mathsf T}x - b : x \in \mathrm{FRAC}(G)\}$ , which is an integer.

For a node $v$ with neighbourhood $\Gamma(v)$ , the deletion of $v$ zeroes $a_v$ . The contraction of $v$ zeroes $a$ on $\{v\}\cup\Gamma(v)$ and lowers the right-hand side to $b - a_v$ .

Formalization targets

Goal: Theorem 2.13

For every such inequality with defect $r \ge 0$ and N-index $k$ ,

\frac{r}{b} \;\le\; k \;\le\; r,

formalized as $r \le k\,b$ and $k \le r$ . The goal holds for every graph without isolated nodes and every valid inequality with nonnegative integer coefficients and nonnegative defect.

Milestones

Lemma 2.11. Let $a \ge 0$ and $\max_{\mathrm{STAB}} a^{\mathsf T}x < \max_{\mathrm{FRAC}} a^{\mathsf T}x$ . Then the edges $ij$ with $y_i + y_j = 1$ at every FRAC-maximizer $y$ form a nonbipartite graph.
Lemma 2.12. Under the same hypothesis, some node $i$ has $y_i = \tfrac12$ at every FRAC-maximizer $y$ .
The defect-decrease claim (proof of Theorem 2.13). For such a node $i$ , the deletion and the contraction of $i$ both have defect smaller than $r$ .
Lemma 2.2. If the deletion and the contraction of some node are valid for $K$ , where $K \subseteq \mathrm{FR}(G)$ is a closed convex cone, then $a^{\mathsf T}x \le b$ is valid for $N(K)$ .
Lemma 2.7. $\frac{1}{k+2}\mathbb 1 \in N^k(G)$ for every $k \ge 0$ .

Further result

Corollary 2.8. Let $G$ have $n$ nodes, stability number $\alpha$ and graph N-index $k$ . Then

\frac n\alpha - 2 \le k \le n - \alpha - 1.

Significance

Theorem 2.13 turns the N-index, which is defined through an infinite family of matrix-cone projections, into a quantity computable by one linear program over $\mathrm{FRAC}(G)$ . Some consequences:

Odd hole constraints have defect 1 and hence N-index 1.
An odd antihole on $2k+1$ nodes has index exactly $k$ ; the paper notes that the lower bound is tight for odd antihole constraints.
Inequalities of large defect relative to their right-hand side need many rounds. With Lemma 2.7 this yields Corollary 2.8 and the unboundedness of the N-index of line graphs, the stable set side of Yannakakis's matching-polytope question.

The result is proved in the paper; the mission's work is to formalize it. Nothing on Prove2Me or in Mathlib covers stable set polytopes, the Lovász–Schrijver operator or its index, and no machine-checked version of Theorem 2.13 is known. A formal proof would give the first verified rank bound for a lift-and-project hierarchy. It would also build a reusable library for $\mathrm{STAB}$ , $\mathrm{FRAC}$ , half-integrality of $\mathrm{FRAC}$ vertices, and the $N$ operator.

Difficulty

The upper bound is an induction on the defect, and it needs several facts about $\mathrm{FRAC}(G)$ :

its vertices are half-integral;
the defect is therefore an integer;
a node $\tfrac12$ at every optimum exists, which is a statement about the whole optimal face and not about one optimal vertex.

The last is the heart of Lemmas 2.11 and 2.12. The induction also climbs through $N^t(\mathrm{FR}(G))$ for every $t$ , so Lemma 2.2 must hold for an arbitrary closed convex cone inside $\mathrm{FR}(G)$ , not only for polytopes given by inequalities.

The lower bound is where the obvious argument fails. The printed proof tests $a^{\mathsf T}x \le b$ at $\frac1{k+2}\mathbb 1$ and obtains $k \ge a^{\mathsf T}\mathbb 1/b - 2$ . That equals $r/b$ only when $r = a^{\mathsf T}\mathbb 1 - 2b$ , which Lemma 2.10 gives for facets alone. For a general valid inequality $r$ can exceed $a^{\mathsf T}\mathbb 1 - 2b$ , so the uniform vector does not suffice. The theorem is stated, as printed, for every valid inequality, and a complete proof must supply the missing step.

Formalization scope

Coordinates of $\mathbb R^{V\cup\{0\}}$ are indexed by Option V, with none as $x_0$ . Graphs are finite SimpleGraphs with the hypothesis that every node has a neighbour.
$\mathrm{FR}(G)$ is defined by its two constraint families. This equals the cone over $\mathrm{FRAC}(G)$ because there are no isolated nodes.
$M$ is defined by condition (iii) itself.
The defect and the N-index are never suprema or infima. They are values $r$ , $k$ with IsGreatest and IsLeast hypotheses, so no default value such as $\sup\emptyset = 0$ can make a statement vacuous.
Coefficients are natural numbers cast to $\mathbb R$ . Lemmas 2.11–2.12 take real $a \ge 0$ , as printed.
Deletion and contraction are zero-extended coefficient vectors on the same graph $G$ , with defects taken over $\mathrm{FRAC}(G)$ . Subgraphs with isolated nodes never arise.
The goal adds the hypothesis $r \ge 0$ . Without it the upper bound is false: for $x_1 \le 2$ on one edge, $r = -2$ but $k = 0$ . The paper's proof presumes it.
The lower bound is stated as $r \le kb$ , which avoids Lean's $r/0 = 0$ convention.
Lemma 2.2 is stated for a closed convex cone $K \subseteq \mathrm{FR}(G)$ . The paper tacitly takes $K$ closed, and the Section 1 lemma it rests on is false for non-closed cones. Its hypothesis " $K$ contains $\mathrm{STAB}(G)$ " is dropped, which makes the lemma stronger.
Corollary 2.8 uses the least $k$ with $N^k(G) = \mathrm{STAB}(G)$ . This is equivalent to the paper's "largest N-index of a facet" and avoids a facet notion.
The goal is the two-sided bound for all graphs and inequalities. A version for one fixed graph, a version with a facet hypothesis, or "valid for $N^r(G)$ " alone would each be a different, weaker theorem.
Not formalized: Lemma 2.10 (facets), Corollaries 2.6 and 2.9 (graph index via facets), and the polynomial-time results.

The work needs half-integrality of $\mathrm{FRAC}(G)$ , Lemma 1.3 of the paper ( $N(K) \subseteq (K\cap H_i) + (K \cap G_i)$ ) and monotonicity of $N$ . Each of these is reusable and welcome as a separate contribution.

Selected references

L. Lovász, A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2) (1991) 166–190. https://doi.org/10.1137/0801013
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4
E. Balas, S. Ceria, G. Cornuéjols, A lift-and-project cutting plane algorithm for mixed 0–1 programs, Mathematical Programming 58 (1993) 295–324. https://doi.org/10.1007/BF01581273
M. Laurent, A comparison of the Sherali–Adams, Lovász–Schrijver, and Lasserre relaxations for 0–1 programming, Mathematics of Operations Research 28(3) (2003) 470–496. https://doi.org/10.1287/moor.28.3.470.16391
M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43 (1991) 441–466. https://doi.org/10.1016/0022-0000(91)90024-Y

10 thms2 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems IV: Greedy Set Cover C1 Has Worst-Case Ratio H(k) on SC(k)Research Paper

Motivation

Set covering asks for the fewest members of a family of sets whose union is everything the family covers. It models crew scheduling, facility siting, test-suite reduction, logic minimization and fault testing; Johnson names the last two as its practical applications. Karp showed in 1972 that the decision version is NP-complete (Karp 1972), so in practice one runs a heuristic and asks how far from optimal it can be.

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (JCSS 9, 256–278) is one of the founding papers of the worst-case analysis of approximation algorithms. For set covering it analyses the obvious greedy rule, repeatedly take a set that covers the most still-uncovered points, and proves that on families whose sets have at most $k$ elements its output is never more than the harmonic number $H(k) = \sum_{j=1}^k 1/j$ times the optimum, and that this factor is attained.

Timeline.

1974: Johnson proves the $H(k)$ bound for unweighted set cover with sets of size at most $k$ , together with a matching family of examples (this mission).
1975: Lovász proves the same bound for the fractional relaxation, giving an integrality-gap statement (Lovász 1975).
1979: Chvátal extends the bound to weighted set cover, with the greedy rule choosing the set of least cost per newly covered point (Chvátal 1979).
1998: Feige shows that no polynomial-time algorithm achieves $(1-\varepsilon)\ln n$ unless NP has slightly superpolynomial deterministic algorithms (Feige 1998), so the greedy guarantee is essentially the best possible.

Setting

An input $F$ of SET COVERING I is a finite family $\{S_1, \dots, S_p\}$ of finite sets. The set to be covered is $T = \bigcup_{S \in F} S$ . A subcover is a subfamily $F' \subseteq F$ with $\bigcup_{S \in F'} S = T$ , and its measure is $|F'|$ . The optimum $F^*$ is the minimum measure of a subcover; $F$ itself is a subcover, so the minimum exists. The subproblem SC(k) restricts the inputs to families no set of which has more than $k$ elements.

Algorithm C1 keeps a family SUB of chosen sets, the set UNCOV of uncovered points, and an array SET $[i]$ holding the still-uncovered part of $S_i$ . It starts with SUB $= \emptyset$ , UNCOV $= T$ , SET $[i] = S_i$ . While UNCOV is nonempty it chooses an index $j$ with $|\mathrm{SET}[j]|$ maximal, adds $S_j$ to SUB, and removes SET $[j]$ from UNCOV and from every SET $[i]$ . When UNCOV is empty it returns SUB. When several indices tie at Step 3 any of them may be chosen, so one input can have several choosable outputs. Following Section 2 of the paper, the algorithm's value $C1(F)$ is the worst choosable output, here the largest, and the ratio is $r(C1, F) = C1(F)/F^*$ .

For the proof the paper introduces configurations $K = \langle N_K, \mathrm{UNCOV}_K, \langle \mathrm{SET}_K[1], \dots, \mathrm{SET}_K[N_K]\rangle\rangle$ with $\bigcup_i \mathrm{SET}_K[i] = \mathrm{UNCOV}_K$ , runs from a configuration (sequences of admissible choices ending when UNCOV is empty), $\mathrm{Numbers}(R)$ , the set of indices chosen in a run $R$ , and calls a set $M$ selectable from $K$ if $M = \mathrm{Numbers}(R)$ for some run $R$ from $K$ . Write $n(K, i) = |\mathrm{SET}_K[i]|$ .

Formalization targets

Goal: Theorem 4

For every $k \ge 1$ :

\text{for every input } F \in SC(k) \text{ and every choosable } F_1:\quad |F_1| \le H(k)\cdot F^*,

\text{and some } F \in SC(k) \text{ with } F^* > 0 \text{ has a choosable } F_1 \text{ with } |F_1| = H(k)\cdot F^*.

The paper states this as $R[C1, SC(k)](n) \le \sum_{j=1}^k (1/j)$ for all $n > 0$ , with equality for all sufficiently large $n$ . The two-part form above is the size-free equivalent.

Milestones

Lemma 1. For a subcover $F_1$ with index set $M1 = \{i : S_i \in F_1\}$ and $K$ the configuration after Step 1: $F_1$ is choosable by C1 if and only if $M1$ is selectable from $K$ .
Lemma 2. For any configuration $K$ , any $M1$ selectable from $K$ and any $M0$ with $\bigcup_{i \in M0} \mathrm{SET}_K[i] = \mathrm{UNCOV}_K$ :

|M1| \le \sum_{i \in M0} \sum_{j=1}^{n(K,i)} \frac{1}{j}.

Fig. 1. For every $k \ge 1$ there is an explicit input of $SC(k)$ on $k \cdot k!$ points with $F^* = k!$ and a choosable output of $k!\,H(k)$ sets.

Significance

The result. Theorem 4 is the first proof that greedy set cover has a worst-case guarantee depending only on the largest set size, and it pins the guarantee down exactly: the constant $H(k)$ cannot be lowered for any $k$ . Since $H(k) \le 1 + \ln k$ , it also gives the well-known $1 + \ln n$ bound for general inputs. The $H(k)$ bound and its later refinements are the standard reference point for analyses of greedy covering, dual fitting and submodular covering.

Formalizing it. The theorem has been proved since 1974. As far as a search of the platform shows, no machine-checked proof of it exists: the platform holds a Kearns–Vazirani-style statement ComputationalLearning.greedy_set_cover (the $\mathrm{opt}\cdot\ln|U|$ form for a greedy sequence, still open) and a dual-fitting certificate lemma for weighted set cover, neither of which covers the $SC(k)$ bound, the tie-breaking semantics or the tightness construction. A complete development provides both halves of Theorem 4, the configuration and run machinery of Lemmas 1–2, and the explicit Fig. 1 family.

Difficulty

The obvious argument charges each chosen set to the points it newly covers and compares the charges with an optimal cover. A statement about the initial input alone, with the original sizes of the optimal sets, does not survive a single greedy step: after a step the optimal sets are only partly uncovered and the remaining run faces a different instance. This is why Lemma 2 is stated for an arbitrary configuration, in terms of the current sizes $n(K, i)$ , and for an arbitrary covering subfamily $M0$ . Because Step 3 breaks ties arbitrarily, the statement must hold for every admissible run, and a formalization that fixes one tie-breaking rule proves a weaker upper bound and cannot express the tightness example, which relies on adversarial ties at every stage.

For the tightness half, the difficulty is bookkeeping: showing that the $k!/j$ blocks of each segment are admissible choices at each stage and that no cover uses fewer than $k!$ sets.

Formalization scope

An input is an indexed family S : ι → Finset α over a finite index type ι and a ground type with decidable equality. The indices play the role of $1, \dots, N$ ; two indices may carry the same set, which only widens the input class. The family, subcovers and $F^*$ are taken over the set of sets family S, as on the page. $F^*$ is a Finset.inf' over the nonempty finite set of subcovers; if $T = \emptyset$ then $F^* = 0$ .
C1 is a nondeterministic step relation: a step is allowed for every index maximizing $|\mathrm{SET}[j]|$ . An output is choosable if a finite chain of steps from the initial state reaches a halting state with that SUB. No tie-breaking rule is fixed.
The paper's $R[A, P](n)$ is a maximum over inputs of size at most $n$ in an unspecified notation; it is replaced by the size-free two-part statement above, which is equivalent because $R$ is a maximum over finitely many inputs and nondecreasing in $n$ .
Ratios are stated multiplicatively in $\mathbb{Q}$ ( $|F_1| \le H(k)\cdot F^*$ ), never as a quotient, so an input with $F^* = 0$ does not make the bound vacuous, and the attainment part requires $F^* > 0$ . $H(k)$ is Mathlib's harmonic k.
Configurations carry the covering condition as a field; runs are an inductive predicate on the list of chosen indices; Selectable K M means $M$ is the set of indices of some run.
Lemma 1 assumes the family's sets are pairwise distinct (the paper's family is a set of sets); without that the index set $\{i : S_i \in F_1\}$ may contain a duplicate index C1 never chose.
Trivializing formalizations are ruled out: a deterministic tie-break, a ratio written as a division, the original set sizes in place of $n(K, i)$ in Lemma 2, or an attaining input with $F^* = 0$ would each change the theorem.

Contributions welcome: proofs of Lemma 2 (the core induction), of Lemma 1, of the Fig. 1 run, and of Theorem 4 from these; the configuration/run layer and the Fig. 1 family are reusable for other greedy covering analyses.

Selected references

David S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
Richard M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
László Lovász, On the ratio of optimal integral and fractional covers, Discrete Mathematics 13 (1975), 383–390. https://doi.org/10.1016/0012-365X(75)90058-8
Vašek Chvátal, A greedy heuristic for the set-covering problem, Mathematics of Operations Research 4 (1979), 233–235. https://doi.org/10.1287/moor.4.3.233
Uriel Feige, A threshold of ln n for approximating set cover, Journal of the ACM 45 (1998), 634–652. https://doi.org/10.1145/285055.285059

8 thms2 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems II: The Greedy Literal Algorithm B1 Has Worst-Case Ratio (k+1)/k on MS(k)Research Paper

Motivation

Maximum satisfiability asks for a truth assignment satisfying as many clauses of a propositional formula as possible. The paper notes that the restriction $MS(k)$ , in which every clause has at least $k$ literals, is polynomial complete for every $k \ge 1$ , so exact optimization is out of reach in general and one asks instead how close a fast algorithm is guaranteed to come. David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 256–278) set up a framework for exactly this question — optimization problems, nondeterministic approximation algorithms, and the worst-case ratio between the optimum and the algorithm's output — and applied it to subset-sum, maximum satisfiability, set covering, graph coloring and maximum clique. It is one of the founding papers of the theory of approximation algorithms.

Section 4 of the paper treats maximum satisfiability with two algorithms. This mission covers the first, a greedy literal-selection rule called B1, and its exact worst-case ratio (Theorem 2). A companion mission covers the weighted algorithm B2 (Theorem 3).

Timeline, for orientation:

1971–1972: Cook and Karp establish NP-completeness of satisfiability and of many combinatorial problems.
1974: Johnson proves that B1 has worst-case ratio exactly $(k+1)/k$ on $MS(k)$ and that the weighted algorithm B2 achieves $2^k/(2^k-1)$ (Theorems 2 and 3).
1990s: semidefinite and LP-based algorithms (Goemans–Williamson, SIAM J. Discrete Math. 1994) improve the constants for general MAX-SAT.

Setting

Let $L = \bigcup_{i>0}\{x_i, \bar x_i\}$ be the set of literals; the complement of $x_i$ is $\bar x_i$ and conversely. A clause is a finite set $C \subseteq L$ . A truth assignment is a set $T \subseteq L$ containing no complementary pair $\{x_i, \bar x_i\}$ ; it may leave variables unassigned. $T$ satisfies $C$ if $C \cap T \ne \emptyset$ .

An input is a finite set $S$ of clauses. Its feasible solutions are the subsets $S' \subseteq S$ satisfied by a single truth assignment, measured by $|S'|$ , and the optimum is

S^* = \max\{|S'| : S' \subseteq S,\ \text{some truth assignment satisfies every } C \in S'\}.

The subproblem $MS(k)$ admits only inputs whose clauses each contain at least $k$ distinct literals.

Algorithm B1 keeps four variables: SUB (clauses already satisfied), LEFT (clauses not yet satisfied), TRUE (literals made true) and LIT (literals still available). It starts with SUB $=$ TRUE $= \emptyset$ , LEFT $= S$ , LIT $= L$ . While some literal of LIT occurs in a clause of LEFT, it picks a literal $y \in$ LIT contained in the most clauses of LEFT, moves those clauses $YT$ from LEFT to SUB, adds $y$ to TRUE, and removes $y$ and $\bar y$ from LIT. When no literal of LIT occurs in LEFT it returns SUB.

The choice of $y$ is not determined when several literals tie. Following the paper's framework, every output reachable by some sequence of admissible choices is choosable, and the performance of B1 on $S$ is the smallest $|X|$ over choosable outputs $X$ . The worst-case ratio on inputs of size at most $n$ is

R[B1, MS(k)](n) = \max\{S^*/B1(S) : S \in MS(k),\ |S| \le n\}.

Formalization targets

Goal: Theorem 2 (p. 262)

For all $k \ge 1$ ,

R[B1, MS(k)](n) \le \frac{k+1}{k}\quad\text{for all } n > 0,

with equality for all sufficiently large $n$ . In the size-free form used here: every choosable output $X$ on every $S \in MS(k)$ satisfies $k\,S^* \le (k+1)\,|X|$ , and for every $k \ge 1$ some $S \in MS(k)$ has a choosable $X$ with $|X| > 0$ and $k\,S^* = (k+1)\,|X|$ .

Milestones (from the proof of Theorem 2, pp. 262–263)

In each iteration, the number of clauses saved (added to SUB) is at least the number of clauses remaining in LEFT that are wounded (lose a literal from LIT without being satisfied).
When B1 halts, every clause left in LEFT is dead: each of its literals has had its complement made true.
When B1 halts on an input of $MS(k)$ , $|\mathrm{SUB}| \ge k\,|\mathrm{LEFT}|$ , and SUB and LEFT partition $S$ .
On the four-clause input $\{\{x_1,x_2,x_3\},\{\bar x_1,x_4,x_5\},\{\bar x_2,x_6,x_7\},\{\bar x_3,x_8,x_9\}\}$ of $MS(3)$ , $S^* = 4$ while B1 may return three clauses.

Significance

The bound is stronger than a ratio: milestone 3 shows that B1 always satisfies at least $\tfrac{k}{k+1}|S|$ clauses, whatever the optimum. The tightness half shows that this simple greedy rule cannot be analysed any better, which is what motivated the weighted algorithm B2 of the same section, with ratio $2^k/(2^k-1)$ . The pair of theorems is an early instance of a now standard pattern: a potential-style counting argument for an upper bound, and an adversarial tie-breaking instance for the matching lower bound.

The result is proved in the paper; it has not, to our knowledge, been machine-checked. This mission produces a formal model of Johnson's framework for a maximization problem with a nondeterministic algorithm, a formal proof of the upper bound through the "saved versus wounded" accounting, and explicit tightness instances for every $k \ge 1$ . The paper spells out only $k = 3$ and states that "similar examples can be constructed for any other $k > 0$ "; the formal goal requires them for all $k$ .

Difficulty

The upper bound needs an invariant over entire runs, not over a single step: a clause wounded in one iteration may be saved in a later one, so wounds and saves must be tallied globally, and the count of wounds received by a clause that ends in LEFT must be matched with its number of literals. That matching relies on the facts that B1 never makes both a literal and its complement true and that a clause containing a true literal has already left LEFT. Clauses containing both $x_i$ and $\bar x_i$ are allowed and have to be handled.

The lower bound cannot be obtained from a fixed tie-breaking rule: the attaining run chooses negative literals whose count merely ties the maximum. For general $k$ the instance has to be built so that every literal occurs in few enough clauses that the adversarial choice is admissible at every step; at $k = 1$ the paper's pattern degenerates and needs adjusting.

Formalization scope

A literal is a pair (variable index in $\mathbb N$ , sign); a clause is a Finset of literals; an input is a Finset of clauses, so duplicate clauses are not allowed, as on the page. Tautological clauses are allowed.
A truth assignment is a Set of literals without a complementary pair (partial, as in the paper). $S^*$ is the maximum of $|S'|$ over the finite nonempty family of satisfiable subsets, taken with Finset.sup'.
B1 is a nondeterministic run relation: a state holds SUB, LEFT, TRUE and the set of decided variables (LIT is its complement, since $L$ is infinite); one step chooses any literal of LIT, of either sign, with maximum count; "choosable" is reachability of a halting state with the given SUB. No tie-break is fixed. A formalization that picks a variable and then its better sign, or that resolves ties deterministically, is a different algorithm and would make the tightness half false.
The ratio $R[B1, MS(k)](n)$ , whose problem size is left unspecified in the paper, is replaced by its size-free equivalent, and ratios are written multiplicatively in $\mathbb N$ : $k\,S^* \le (k+1)|X|$ . The tightness half requires $|X| > 0$ , so the empty input cannot witness it.
The running time $O(n \log n)$ is not stated.

Welcome contributions: proofs of the milestones, the invariants of reachable B1 states (SUB and LEFT partition $S$ ; TRUE is consistent and exactly covers the decided variables; no clause of LEFT meets TRUE), and the family of tightness instances for general $k$ . The run-relation encoding of choosable outputs is reusable for the other algorithms of the paper.

Selected references

D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
M. X. Goemans and D. P. Williamson, New 3/4-approximation algorithms for the maximum satisfiability problem, SIAM Journal on Discrete Mathematics 7 (1994), 656–666. https://doi.org/10.1137/S0895480192243516

8 thms2 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems I: The Subset-Sum Algorithms A_k Have Worst-Case Ratio (k+1)/kResearch Paper

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) is one of the founding papers of the theory of approximation algorithms. It asks, for optimization problems whose decision versions Karp had just shown to be polynomial complete, how close a fast heuristic can be guaranteed to come to the optimum in the worst case, and it measures this with a worst-case performance ratio that is still the standard yardstick.

Its first example is SUBSET-SUM, the simplest form of the knapsack problem: pack items of given sizes into a knapsack of capacity $b$ so as to fill it as much as possible. For this problem the paper gives a family of algorithms $A_k$ , one for each $k \ge 1$ , whose guaranteed ratio $(k+1)/k$ tends to $1$ . It is one of the first examples of what is now called a polynomial-time approximation scheme: for every $\epsilon > 0$ there is a polynomial-time algorithm within a factor $1 + \epsilon$ of optimal. Sahni (1975) extended the idea to the knapsack problem with utilities, and Ibarra and Kim (1975) later obtained fully polynomial schemes for knapsack and subset-sum.

This mission formalizes Theorem 1 of the paper, the performance guarantee of $A_k$ together with its tightness.

Setting

An input $\langle T, s, b\rangle$ of SUBSET-SUM is a finite set $T$ , a positive rational size $s(x)$ for every $x \in T$ , and a positive rational bound $b$ . An approximate solution is a subset $T' \subseteq T$ with $m(T') \le b$ , where the measure is $m(T') = \sum_{x \in T'} s(x)$ . The problem is a maximization problem with optimal measure

\langle T, s, b\rangle^* = \max\{\, m(T') : T' \subseteq T,\ m(T') \le b \,\}.

Fix $k \ge 1$ and call $x$ big if $s(x) > b/(k+1)$ and small otherwise. Algorithm $A_k$ keeps a set $\mathrm{SUB}$ , its measure $\mathrm{SUM}$ , and the remaining elements $\mathrm{LEFT}$ :

$\mathrm{SUB}$ is a subset of the big elements whose measure is as large as possible without exceeding $b$ ; $\mathrm{SUM} = m(\mathrm{SUB})$ and $\mathrm{LEFT} = T \setminus \mathrm{SUB}$ .
If $s(x) + \mathrm{SUM} > b$ for every $x \in \mathrm{LEFT}$ , return $\mathrm{SUB}$ .
Otherwise pick $y \in \mathrm{LEFT}$ with $s(y) + \mathrm{SUM}$ as large as possible without exceeding $b$ , move it from $\mathrm{LEFT}$ to $\mathrm{SUB}$ , add $s(y)$ to $\mathrm{SUM}$ , and return to step 2.

Steps 1 and 3 may have ties. Following the paper, a set $T_1$ is choosable by $A_k$ if some resolution of all ties produces it, and the performance $A_k(u)$ on input $u$ is the smallest measure of a choosable output. The ratio is $r(A_k, u) = u^*/A_k(u) \ge 1$ , and $R[A_k](n)$ is its maximum over inputs of size at most $n$ .

Formalization targets

Goal: Theorem 1 (p. 260)

For $k \ge 1$ and $n > 0$ ,

R[A_k](n) \le \frac{k+1}{k}, \qquad \lim_{n \to \infty} R[A_k](n) = \frac{k+1}{k}.

Formally, for every $k \ge 1$ : every choosable output $T_1$ of every input satisfies $k\,\langle T,s,b\rangle^* \le (k+1)\,m(T_1)$ ; and for every $\delta > 0$ some input has a choosable output $T_1$ with $m(T_1) > 0$ and $\langle T,s,b\rangle^* > \big(\tfrac{k+1}{k} - \delta\big)\,m(T_1)$ .

Milestones

For $T_1$ choosable and $T_0$ any approximate solution, $m(T_1^{\mathrm{BIG}}) \ge m(T_0^{\mathrm{BIG}})$ (p. 260).
If a small $x \in T$ is not in a choosable $T_1$ , then $s(x) + m(T_1) > b$ , hence $m(T_1) > kb/(k+1) \ge \tfrac{k}{k+1}\langle T,s,b\rangle^*$ (p. 261).
The stronger dichotomy: $m(T_1) = \langle T,s,b\rangle^*$ or $m(T_1) \ge \tfrac{k}{k+1}\,b$ (p. 260).
The lower-bound input $T = \{a_1,\dots,a_{k+2}\}$ , $s(a_1) = 1+\varepsilon$ , $s(a_i) = 1$ otherwise, $b = k+1$ : its optimum is $k+1$ , some output is choosable, and every choosable output has measure $k + \varepsilon$ (p. 261).

Significance

Theorem 1 shows that SUBSET-SUM admits polynomial-time algorithms with any worst-case ratio above $1$ , in contrast with the other problems of the paper (set covering, graph colouring, maximum clique), whose best known ratios grow with the input. The algorithms $A_k$ are an early instance of the partial-enumeration schemes later used for knapsack-type problems. The tightness half shows that the analysis of $A_k$ itself cannot be sharpened.

The theorem has a short published proof, but no machine-checked version is known; there is no subset-sum or knapsack approximation result on the platform. The mission produces a reusable model of SUBSET-SUM, a model of nondeterministic algorithms through a run relation that captures every tie-break, and a checked proof that the worst case is exactly $(k+1)/k$ . The same modelling pattern (choosable outputs, worst-case ratio taken over them) is used in the sibling missions of this series for MAX-SAT, set covering and exact covering.

Difficulty

The arithmetic of the upper bound is short; the difficulty is in reasoning about the algorithm as a nondeterministic process. The natural first attempt, implementing $A_k$ as a function with a fixed tie-breaking rule, proves a weaker statement: the guarantee must hold for every output the algorithm may return, including adversarial ties in step 1 (several maximum-measure sets of big elements) and step 3. Facts that are obvious for a single run, such as $\mathrm{SUM}$ always equalling $m(\mathrm{SUB})$ or which elements can enter $\mathrm{SUB}$ after step 1, have to be established for the run relation as a whole. The lower bound requires tracing the run on the explicit input for general $k$ : exactly $k-1$ unit elements are added after $a_1$ , and this must be shown for every choosable run, not only for one.

Formalization scope

Numbers. Sizes and the bound are rationals (ℚ), as in the paper; sizes are required to be positive on $T$ and $b > 0$ . The index $k$ is a natural number with $1 \le k$ as a hypothesis; $b/(k+1)$ is rational division, and "big" is the strict inequality $s(x) > b/(k+1)$ .
Optimum. opt u is Finset.sup' of the measure over the finite set of approximate solutions, which always contains $\emptyset$ ; it is $0$ when no element fits.
Run relation. Choosable k u T₁ states that some admissible step 1 choice, followed by a finite chain of admissible iterations (Relation.ReflTransGen), reaches a halting state returning $T_1$ . Every "closest to, without exceeding" is an existential choice among all maximizers.
Size-free restatement. The paper's input size $|u|$ ("in some standard notation") is never fixed, so the goal quantifies over all inputs instead of over sizes. The upper bound for all choosable outputs is equivalent to $R[A_k](n) \le (k+1)/k$ for all $n$ ; since $R[A_k]$ is nondecreasing, the limit claim is equivalent to the supremum of the ratio over all inputs being $(k+1)/k$ , which is the second part.
Multiplicative ratios. No ratio is written as a division, so an output of measure $0$ cannot satisfy a bound vacuously; the lower-bound part requires $m(T_1) > 0$ . The value $(k+1)/k$ is not claimed to be attained: the paper's family has ratio $(k+1)/(k+\varepsilon)$ .
Lower-bound input. A def on Fin (k + 2) exactly as on the page, with $0 < \varepsilon < 1$ (the page leaves the range implicit; $\varepsilon < 1$ keeps $a_1$ the only big element that fits when $k = 1$ ).
Ruled out. A formalization with a deterministic tie-break, with a bound of the form $\mathrm{opt}/m \le c$ in a field where $x/0 = 0$ , or with tightness for a single fixed $k$ would be trivial or weaker; none of these is the target.

Contributions welcome: proofs of the milestones and the goal, invariant lemmas for the run relation, and further sanity checks on small inputs. The running-time remark ( $O(n^k)$ for step 1) and Sahni's knapsack extension are not part of the mission.

Selected references

D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974) 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
S. Sahni, Approximate algorithms for the 0/1 knapsack problem, Journal of the ACM 22 (1975) 115–124. https://doi.org/10.1145/321864.321873
O. H. Ibarra, C. E. Kim, Fast approximation algorithms for the knapsack and sum of subset problems, Journal of the ACM 22 (1975) 463–468. https://doi.org/10.1145/321906.321909
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum (1972) 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9

8 thms2 active usersReviewed

Completed

Discrete Geometry Graph Theory·Captain: aarontcao

Lovasz Problem 11.8: triangle-free unit vector systems sum to Theta(n^(2/3))Research Paper

Let $u_1, \dots, u_n$ be unit vectors in a Euclidean space such that among any three of them some two are orthogonal. How large can $\|u_1 + \dots + u_n\|$ be?

The answer is $\Theta(n^{2/3})$ .

Attribution, which is commonly given wrong in both halves

Lovasz posed the question, as Problem 11.8 of Combinatorial Problems and Exercises (North Holland, 1979). Konyagin proved the $O(n^{2/3})$ upper bound in Systems of vectors in Euclidean space and an extremal problem for polynomials, Mat. Zametki 29 (1981) 63-74, doi:10.1007/BF01142512. Alon gave a matching lower bound in Explicit Ramsey graphs and orthonormal labelings, Electron. J. Combin. 1 (1994) R12, doi:10.37236/1192. The two together pin the exponent exactly.

Where the proof comes from

The hypothesis is a graph condition in disguise. Join $i$ to $j$ when $\langle u_i, u_j \rangle \ne 0$ ; then "among any three some two are orthogonal" says that graph is triangle-free.

The proof does not run through Ramsey counting, which is the natural first guess and does not reach the right exponent. It runs through the Lovasz theta function. Kashin and Konyagin bound $\theta = O(n^{1/3})$ for graphs of independence number less than 3, that is for complements of triangle-free graphs, and Cauchy-Schwarz turns that into the bound on the norm of the sum. The orthonormal labeling of a graph by unit vectors is not a coincidence of notation: it is the definition of $\theta$ that the argument uses.

What this mission will cost

State this honestly rather than discover it later. The Lovasz theta function, orthonormal graph labeling, and Shannon capacity are all absent from Mathlib. So the milestone chain that the upper bound needs cannot be written yet, and this proposal ships with exactly one milestone, which is Alon's lower bound.

google-deepmind/formal-conjectures contains an SDP-form definition of the theta function, with basic bounds such as lovaszThetaFunction_le_card since PR #6100 of 2026-09-18. The proof here needs the orthonormal-labeling form instead, so that file is a starting point rather than a foundation. Building the theta function, proving that the two forms agree, and getting the Kashin-Konyagin bound is the real content of this mission and is larger than the statement of the goal suggests.

The lower bound is the tractable half. It needs explicit Ramsey graphs and an orthonormal labeling of one, and it does not need $\theta$ at all.

Notes on the formalization

Both items are stated in Mathlib primitives alone, so the mission omits definition items. The triangle-free hypothesis is written as a condition on triples of indices rather than through SimpleGraph.CliqueFree 3, so that a reader auditing the statement does not have to unfold a graph construction to see what is assumed. Anyone proving it is free to build the graph and use the Mathlib predicate.

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Scheduling with Deadlines and Loss Functions: On One Processor, Decreasing Penalty-to-Length Order Is Optimal When No Task Finishes Before Its DeadlineResearch Paper

Motivation

A processor, a machine shop or a single server must work through a set of jobs one at a time, and each job is costly when it is late. Deciding the order is the single-machine sequencing problem, the simplest and most studied model of scheduling theory. Robert McNaughton's 1959 article Scheduling with Deadlines and Loss Functions (Management Science 6(1):1–12) treats it for a computer that must run several tasks, each with a deadline and a loss that grows linearly with the lateness. Its §2 gives the first sufficient condition under which a simple ratio rule is optimal in the presence of deadlines, and shows that interrupting and resuming tasks ("splitting", now called preemption) never helps on one processor.

Timeline.

1956: W. E. Smith, Various optimizers for single-stage production (Naval Research Logistics Quarterly 3), proves that sequencing jobs by non-increasing weight-to-processing-time ratio minimizes the total weighted completion time over non-preemptive sequences.
1959: McNaughton, §2 of the present paper, proves independently that the same ratio order is optimal against all schedules, split or not and with idle time (Theorem 2.3), and extends it to deadlines when no task finishes early in that order (Theorem 2.4). §3 of the same paper gives the "wrap-around" rule for preemptive makespan on identical processors, and §4 the non-preemptive optimality for weighted completion time on several processors.
1977: J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker show that minimizing total weighted tardiness on one machine, the general problem of §2, is strongly NP-hard (Annals of Discrete Mathematics 1); this is why §2 gives a sufficient condition and not an algorithm.

Setting

There are $m$ tasks $(1),\dots,(m)$ for a single processor, and the present is time $0$ . Task $(i)$ takes $a_i > 0$ units of processing time, has a deadline $d_i$ and a penalty rate $p_i \ge 0$ . If $(i)$ is finished at time $C_i \le d_i$ there is no loss; otherwise the loss on $(i)$ is $p_i x$ , where $x = C_i - d_i$ is the time from the deadline to the completion. Thus the loss on a task completed at time $t$ is

\ell_i(t) = p_i \max(0,\ t - d_i).

The ratio of task $(i)$ is $r_i = p_i / a_i$ .

A task may be split: part of it may run between times 4 and 6 and the remainder between times 8 and 11, and similarly in any finite number of parts. A schedule $S$ is therefore a finite list of pieces, each a task together with a start and a stop time. It is feasible when every piece lies in $[0,\infty)$ with start $\le$ stop, no two pieces overlap in time, and the pieces of each task $(i)$ have total length exactly $a_i$ . The completion time $C_i(S)$ is the latest stop time of a piece of $(i)$ , and the total loss is

c(S) = \sum_{i=1}^{m} \ell_i\bigl(C_i(S)\bigr).

For an order $\sigma$ of the tasks ( $\sigma(k)$ in position $k$ ), the sequenced schedule $S_\sigma$ runs the tasks without splits and without unused time: $\sigma(k)$ occupies $\bigl[\sum_{l<k} a_{\sigma(l)},\ \sum_{l\le k} a_{\sigma(l)}\bigr]$ . The order is in decreasing $r_i$ when $k \le l$ implies $r_{\sigma(l)} \le r_{\sigma(k)}$ . Finally $c^*(S)$ denotes the total loss of $S$ computed as if $d_1 = \dots = d_m = 0$ .

Formalization targets

Goal: Theorem 2.4 (p. 5)

If $\sigma$ is in decreasing $r_i$ and no task finishes before its deadline in $S_\sigma$ , i.e. $d_i \le C_i(S_\sigma)$ for every $i$ , then $S_\sigma$ is feasible and

c(S_\sigma) \le c(S') \qquad \text{for every feasible schedule } S'.

The competitors $S'$ may split tasks and leave the processor idle. The condition is sufficient but not necessary.

Milestones, in attack order

Theorem 2.1 (p. 4): if both $(i)$ and $(j)$ run in the $a_i + a_j$ consecutive units of time after a time $t$ past both deadlines and $r_i > r_j$ , their joint loss is strictly smaller when $(i)$ goes first:

\ell_i(t+a_i) + \ell_j(t+a_i+a_j) < \ell_j(t+a_j) + \ell_i(t+a_j+a_i).

The reduction in the proof of Theorem 2.2 (pp. 4–5): a feasible schedule with more than $m$ pieces can be replaced by a feasible one with fewer pieces and no greater loss.
Theorem 2.2 (p. 4): some optimal schedule, optimal among all feasible schedules, splits no task.
Theorem 2.3 (p. 5): if $d_1 = \dots = d_m = 0$ , the sequenced schedule in decreasing $r_i$ minimizes the total loss over all feasible schedules.
The display of the proof of Theorem 2.4 (p. 6): if no task finishes early in $S = S_\sigma$ , then for every feasible $S'$ ,

c(S') - c(S) \ge c^*(S') - c^*(S).

Significance

The result. Theorem 2.3 is the ratio rule for total weighted completion time, in its strongest single-machine form: it holds against preemptive schedules and schedules with idle time, not only against permutations. Theorem 2.4 carries the rule over to deadlines and linear tardiness penalties under a checkable condition on one schedule. Since weighted tardiness is strongly NP-hard in general, a condition of this kind is what one can hope for, and the paper's two-step heuristic for general deadlines (p. 6) is built on it. Theorem 2.2, as the paper remarks (p. 6), "does not depend on the linear loss function": it makes non-preemptive scheduling without loss of generality for single-machine objectives of this kind.

Formalizing it. All results of §2 are proved in the paper and are textbook material; none has a machine-checked proof on the platform. The platform's Scheduling Algorithms V mission formalizes the multi-processor results of §§3–4 (via Brucker's textbook), and nothing there states a single-processor ratio rule with deadlines. This mission supplies a single-processor schedule model with splitting, the interchange lemma, the non-preemption theorem and the ratio rule, each over all feasible schedules.

Difficulty

The interchange argument of Theorem 2.1 compares only two schedules that differ in the order of two adjacent tasks. Turning it into optimality against every feasible schedule requires two further steps, and each fails if done naively. First, a competitor may split tasks and leave gaps; the interchange argument does not apply to such schedules, so a separate argument must remove splits without raising any completion time. Second, with deadlines the loss $\max(0, t - d_i)$ is not linear in the completion time, so the ratio order is in general not optimal; the obvious attempt to repeat the interchange argument fails as soon as a task can finish before its deadline, since moving such a task later costs nothing. This is why Theorem 2.4 needs its hypothesis that no task finishes early, and why the paper leaves the general case to a heuristic.

Formalization scope

Tasks and positions are the zero-based indices of Fin m; times, lengths, deadlines and penalties are real numbers. A schedule is a List of pieces (task, start, stop), mirroring the public definition SchedulingAlgorithms_ParallelMachines with one processor. Feasibility requires $0 \le$ start $\le$ stop, pairwise disjoint pieces, and exact total length $a_i$ per task; zero-length pieces and unsorted lists are allowed. The completion time is the maximum stop time of the task's pieces ( $0$ for a task with no pieces, which feasibility excludes). "No split" means exactly one piece per task, so two abutting pieces count as a split. "Decreasing $r_i$ " is non-increasing, with ties in any order. "Minimal" and "optimal" are stated as $\le$ against every feasible schedule, never as an infimum.

Standing assumptions, stated in every item: $a_i > 0$ (tasks take time, and $r_i = p_i/a_i$ needs $a_i \ne 0$ ), and $p_i \ge 0$ for Theorems 2.2–2.4 and the proof steps (penalties are non-negative; with a negative penalty and idle time allowed the loss is unbounded below). Theorem 2.1 carries no sign condition. No condition is placed on the deadlines.

A formalization that restricts the competitors of Theorems 2.2–2.4 to unsplit schedules, or to sequenced schedules of other orders, states a weaker theorem and is ruled out: every statement quantifies over all feasible schedules.

A complete development needs: sums over sublists of pieces, rearrangements of pieces of a schedule and their effect on completion times, and optimality over permutations of a finite set of tasks. The schedule model and the non-preemption argument are reusable for any single-machine regular objective. Contributions of intermediate lemmas on these points are welcome.

Selected references

R. McNaughton, Scheduling with Deadlines and Loss Functions, Management Science 6(1):1–12, 1959. https://doi.org/10.1287/mnsc.6.1.1
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3(1–2):59–66, 1956. https://doi.org/10.1002/nav.3800030106
J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Annals of Discrete Mathematics 1:343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
P. Brucker, Scheduling Algorithms, 5th ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69516-5

7 thms2 active usersReviewed

Completed

Graph Theory Theoretical Computer Science·Captain: mikedeng1

Fast Algorithms for Finding Nearest Common Ancestors III: The Plies of the Compressed Tree Are SmallResearch Paper

Motivation

The nearest common ancestor problem asks, for a rooted tree and two of its vertices $v$ and $w$ , for the deepest vertex that is an ancestor of both, written $\operatorname{nca}(v,w)$ . It is a subroutine in string and graph algorithms.

Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) preprocess a static tree of $n$ vertices in linear time on a random-access machine so that each query takes constant time. For a complete binary tree the queries reduce to bit arithmetic on vertex numbers (§3). An arbitrary tree is first reduced, in §4, to a compressed tree $C$ whose sizes double along every edge, and $C$ is cut by rank into three plies. Lemma 9 bounds the size of each ply, and those bounds are what make the tables of the method fit in linear space. This mission formalizes the structural lemmas of §4 about $C$ and Lemma 9.

Timeline.

1976: Aho, Hopcroft and Ullman give an $O(\log\log n)$ -per-query random-access algorithm for static trees.
1979: Tarjan (Applications of path compression on balanced trees, J. ACM 26) uses the decomposition of a tree by the doubling rule on subtree sizes to compute functions on paths; Lemmas 5–7 of Harel–Tarjan are cited from there without proof.
1983: Sleator and Tarjan (A data structure for dynamic trees, J. Comput. System Sci. 26) use the same heavy/light split of edges for dynamic trees.
1984: Harel and Tarjan give the $O(n)$ -preprocessing, $O(1)$ -query algorithm, with the compressed tree and its plies (§4).

Setting

A rooted tree $T$ (Appendix, p. 354) consists of a finite vertex set $V$ with $n = |V|$ , a root $r \in V$ and a parent map $p_T$ , defined for $v \ne r$ , such that every vertex reaches $r$ by iterating $p_T$ . The edges of $T$ are the pairs $v \to p_T(v)$ for $v \ne r$ . If $p_T^i(v) = w$ for some $i \ge 0$ , then $v$ is a descendant of $w$ and $w$ an ancestor of $v$ . Every vertex is its own ancestor and descendant. The depth of $v$ is the number of edges from $v$ to $r$ . $\mathrm{size}_T(v)$ is the number of descendants of $v$ , including $v$ .

An edge $v \to p_T(v)$ is light if $2\cdot\mathrm{size}_T(v) \le \mathrm{size}_T(p_T(v))$ and heavy otherwise. At most one heavy edge enters each vertex, so the heavy edges partition $V$ into heavy paths. A vertex with no heavy edge entering or leaving it forms a heavy path by itself. The apex of a heavy path is its vertex of smallest depth, and $\mathrm{apex}(v)$ denotes the apex of the heavy path containing $v$ .

The compressed tree $C$ has the same vertices and root as $T$ , and its edges are

\{\, v \to \mathrm{apex}(p_T(v)) : v \ne r \,\}.

Write $p_C(v) = \mathrm{apex}(p_T(v))$ , and let $\mathrm{size}_C(v)$ be the number of descendants of $v$ in $C$ . The rank of $v$ is $\mathrm{rank}(v) = \lfloor \lg \mathrm{size}_C(v)\rfloor$ , where $\lg = \log_2$ . Let $\lg^{(i)}$ denote the $i$ -fold iterate of $\lg$ . Ply three is the set of vertices of rank at least $\lfloor\lg^{(2)} n\rfloor$ . Ply two is the set of vertices whose rank lies between $\lfloor\lg^{(3)} n\rfloor$ and $\lfloor\lg^{(2)} n\rfloor - 1$ , inclusive. Ply one is the set of vertices of rank below $\lfloor\lg^{(3)} n\rfloor$ .

Formalization targets

Goal: Lemma 9 in the explicit form of its proof

For every rooted tree on $n \ge 4$ vertices:

|\text{ply three}| \le \frac{4n}{\lg n}, \qquad |\text{ply two}| \le \frac{4n}{\lg^{(2)} n},

and for every vertex $v$ in ply one, every $C$ -descendant of $v$ lies in ply one and $\mathrm{size}_C(v) \le \lg^{(2)} n$ .

The paper states the first two bounds as $O(n/\log n)$ and $O(n/\log^{(2)} n)$ . The constants $4$ and $4$ are the ones its proof on p. 345 establishes. The third clause is the paper's "each connected component of ply one is a subtree of $C$ containing at most $\log^{(2)} n$ vertices", read vertex by vertex. Ply one is closed under $C$ -descendants, so the component of a ply-one vertex is the $C$ -subtree of its shallowest ply-one ancestor.

Milestones

Lemma 5 (p. 344): $\mathrm{size}_C(v) = \mathrm{size}_T(v)$ if $v$ is an apex, and $\mathrm{size}_C(v) = 1$ otherwise.
Lemma 6 (p. 344): $2\cdot\mathrm{size}_C(v) \le \mathrm{size}_C(p_C(v))$ for every $v \ne r$ .
Lemma 8 (p. 344): for every $i$ , at most $n/2^i$ vertices have rank $i$ .
Proof of Lemma 9, first sentence (p. 345): at most $n/2^{k-1}$ vertices have rank $k$ or greater.

A further item states Lemma 7 (p. 344): $C$ has depth at most $\lfloor\lg n\rfloor$ . The paper uses it to bound the tables of ply three, not in the proof of Lemma 9.

Significance

Lemma 9 is the counting step of the linear-time preprocessing. Ply three has $O(n/\log n)$ vertices, each with $O(\log n)$ ancestors in $C$ by Lemma 7, so storing every vertex's ply-three ancestors takes $O(n)$ space. Ply two has $O(n/\log^{(2)} n)$ vertices, each with $O(\log^{(2)} n)$ ply-two ancestors, which again gives $O(n)$ . Ply one splits into subtrees of at most $\lg^{(2)} n$ vertices, and these are small enough to be embedded in complete binary trees and answered by the bit arithmetic of §3.

Lemmas 5–8 and the proof of Lemma 9 are proved or cited in the paper, and none of them is open. As far as a search of the platform shows, none has a machine-checked proof, and Mathlib has no parent-map rooted trees, subtree sizes or heavy-path decompositions. The mission produces a reusable formal account of heavy paths and of the size-doubling compressed tree, with the paper's explicit constants.

Difficulty

The paper states Lemmas 5–7 without proof, citing Tarjan (1979). Lemma 5 requires identifying the $C$ -descendants of an apex with its $T$ -descendants. That identification needs a clean description of heavy paths: at most one heavy edge enters each vertex, a vertex's heavy path runs up to its apex, and the heavy paths do not overlap. Lemma 8 needs the observation that two vertices of equal rank are unrelated in $C$ , so that their descendant sets are disjoint and the sizes add up to at most $n$ . Lemma 9 turns floors of iterated real logarithms into bounds on powers of two. The step $2^{\lfloor \lg^{(2)} n\rfloor} > \tfrac12 \lg n$ loses a factor $2$ , and this is where the constant $4$ comes from; a proof that expects the constant $2$ fails at this step.

Formalization scope

Trees. A rooted tree is a structure over a Fintype vertex type $V$ with a root, a total parent map and the axiom that every vertex reaches the root. The paper's partial map is made total by $p_T(r) = r$ . Every statement about an edge $v \to p(v)$ assumes $v \ne r$ , since for $v = r$ Lemma 6 would read $2n \le n$ . The Appendix's printed " $p^0(v) = 0$ " is read as $p^0(v) = v$ .
Heavy edges and apex. A heavy edge is $v \ne r$ with $\mathrm{size}_T(p_T(v)) < 2\,\mathrm{size}_T(v)$ , the strict negation of light. $\mathrm{apex}(v)$ is computed by climbing heavy edges from $v$ until the first edge that is not heavy, which is the apex of the heavy path containing $v$ . The root is always an apex.
Compressed tree. $p_C(v) = \mathrm{apex}(p_T(v))$ for $v \ne r$ and $p_C(r) = r$ . Ancestors and sizes in $C$ are defined through iterates of $p_C$ .
Logarithms. The rank is Nat.log 2 of $\mathrm{size}_C$ , which is exactly $\lfloor\lg\mathrm{size}_C\rfloor$ . The ply thresholds are iterated Nat.log 2, which equal the real floors $\lfloor\lg^{(2)} n\rfloor$ and $\lfloor\lg^{(3)} n\rfloor$ for $n \ge 4$ . The bounds of the goal use Real.logb 2.
Added hypothesis $n \ge 4$ in the goal. It makes $\lg n \ge 2$ and $\lg^{(2)} n \ge 1$ , so the divisions are honest (Lean's $x/0 = 0$ ), and it makes $\lg^{(3)} n \ge 0$ . On the page it is hidden in the $O(\cdot)$ .
Division-free milestones. Lemma 8 is stated as $\#\{\mathrm{rank} = i\}\cdot 2^i \le n$ , and the rank- $\ge k$ count as $\#\{\mathrm{rank} \ge k\}\cdot 2^k \le 2n$ .
Ruled out. The goal is not an $\exists C$ statement. Replacing the paper's $4$ by an existential constant, or bounding ply three by $n$ , would discard the content of the lemma.
Welcome contributions. A library of facts about heavy paths is welcome: uniqueness of the entering heavy edge, apex characterizations, and the descendants of an apex in $C$ . So are proofs of Lemmas 5–8 and proofs that the iterated Nat.log thresholds agree with the real ones. It is reusable for heavy-light decompositions generally.

Selected references

D. Harel, R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2):338–355, 1984. https://doi.org/10.1137/0213024
R. E. Tarjan, Applications of path compression on balanced trees, J. ACM 26(4):690–715, 1979. https://doi.org/10.1145/322154.322161
A. V. Aho, J. E. Hopcroft, J. D. Ullman, On finding lowest common ancestors in trees, SIAM J. Comput. 5(1):115–132, 1976. https://doi.org/10.1137/0205011
D. D. Sleator, R. E. Tarjan, A data structure for dynamic trees, J. Comput. System Sci. 26(3):362–391, 1983. https://doi.org/10.1016/0022-0000(83)90006-5

9 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

Limits of Permutation Sequences I: Every Convergent Permutation Sequence Has a Limit Permutation, and Every Limit Permutation Is a LimitResearch Paper

Motivation

Large combinatorial structures are often best understood through their limits. For dense graphs, Lovász and Szegedy (2006) showed that every sequence of graphs whose subgraph densities converge has a limit object, a graphon, and that every graphon arises this way. Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) related this convergence to the cut distance. These results turned questions of extremal combinatorics and property testing into analysis on a compact space.

Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) carried this programme over to permutations. Their limit objects, called limit permutations here and now usually called permutons (as a probability measure on the square), underlie later work on quasirandom permutations, pattern densities, and property testing of permutations (Hoppen et al., 2011). This mission formalizes the paper's main result, Theorem 1.6: convergent permutation sequences have limits, and every limit is attained.

Timeline:

2006. Lovász and Szegedy prove that graphons are exactly the limits of convergent dense graph sequences.
2008. Borgs et al. characterize convergence by the cut distance.
2011–2013. Hoppen, Kohayakawa, Moreira, Ráth and Sampaio prove the permutation analogue (this paper), together with uniqueness of the limit and a characterization by a rectangular distance.

Setting

For $n \ge 1$ , $S_n$ is the set of permutations of $[n] = \{1,\dots,n\}$ , and $|\pi| = n$ for $\pi \in S_n$ . For $\tau \in S_k$ and $\pi \in S_n$ , the number of occurrences $\Lambda(\tau,\pi)$ counts the increasing $k$ -tuples $x_1 < \dots < x_k$ in $[n]$ with $\pi(x_i) < \pi(x_j) \iff \tau(i) < \tau(j)$ . The subpermutation density is $t(\tau,\pi) = \Lambda(\tau,\pi)/\binom nk$ for $k \le n$ and $0$ for $k > n$ . A permutation sequence $(\sigma_n)$ is convergent if $t(\tau,\sigma_n)$ converges for every fixed $\tau$ .

A function $F : [0,1]\to[0,1]$ is a cdf if it is non-decreasing and right-continuous with $F(0) \ge 0$ and $F(1) = 1$ . A limit permutation is a Lebesgue measurable $Z : [0,1]^2 \to [0,1]$ such that $Z(x,\cdot)$ is a cdf for every $x$ , and $\int_0^1 Z(x,y)\,dx = y$ for every $y$ . The set of limit permutations is $\mathcal Z$ .

With $Z$ one associates a random point $(X,Y)$ : $X \sim U[0,1]$ , and given $X$ , $Y$ has cdf $Z(X,\cdot)$ . Draw $k$ independent copies $(X_i,Y_i)$ . The $Z$ -random permutation $\sigma(k,Z)$ records the relative order of the $Y_i$ read in increasing order of the $X_i$ . The density of $\tau \in S_k$ in $Z$ is $t(\tau,Z) = \mathbf P(\sigma(k,Z) = \tau)$ . A sequence with $|\sigma_n| \to \infty$ converges to $Z$ , written $\sigma_n \to Z$ , if $t(\tau,\sigma_n) \to t(\tau,Z)$ for every $\tau$ .

For $\sigma \in S_n$ , the step limit permutation $Z_\sigma$ spreads the permutation matrix of $\sigma$ uniformly over its $n \times n$ grid cells. The rectangular distance $d_\square(Z_1,Z_2)$ is the largest difference, over axis-parallel rectangles, between the probabilities the two associated random points assign to the rectangle.

Formalization targets

Goal: Theorem 1.6

\text{(i)}\quad (\sigma_n)\ \text{convergent},\ |\sigma_n|\to\infty \ \Longrightarrow\ \exists Z\in\mathcal Z:\ \sigma_n\to Z;

\text{(ii)}\quad \forall Z\in\mathcal Z\ \ \exists (\sigma_n):\ \sigma_n\to Z.

The two parts together identify $\mathcal Z$ with the set of limits of permutation sequences.

Milestones

In the order the proof uses them:

Eq. (21): the joint distribution function of the random point associated with $Z$ is $F(x,y) = \int_0^x Z(t,y)\,dt$ .
Lemma 2.2: every law on $[0,1]^2$ with uniform marginals has a limit permutation as its conditional cdf, unique up to a null set of $x$ .
Lemma 2.1: for uniform marginals, weak convergence is equivalent to uniform convergence of the joint distribution functions.
Lemma 3.5: $|t(\tau,\sigma) - t(\tau,Z_\sigma)| \le \frac1n\binom k2$ .
Eq. (49): for $|\sigma_n| \to \infty$ , $\sigma_n \to Z \iff Z_{\sigma_n} \xrightarrow{t} Z$ .
Lemma 5.1: the densities $t(\tau,Z)$ determine the law of the associated random point.
Lemma 5.3: weak convergence, $d_\square$ -convergence and density convergence on $\mathcal Z$ are equivalent.
Lemma 4.2: for all large $k$ and every $Z$ , $\mathbf P\big(d_\square(Z,\sigma(k,Z)) \le 16k^{-1/4}\big) \ge 1 - \tfrac12 e^{-\sqrt k}$ .
Theorem 1.7 (corrected): if $\sigma_n \to Z_1$ , then $\sigma_n \to Z_2$ exactly when $Z_1(x,\cdot) = Z_2(x,\cdot)$ for almost every $x$ .

Significance

Theorem 1.6 makes $\mathcal Z$ , modulo null sets, the completion of the set of finite permutations under density convergence. Asymptotic statements about pattern densities, such as quasirandomness criteria, extremal pattern-density problems and the testability of permutation properties, can then be stated and proved on a compact space of measures rather than along sequences. Lemma 4.2 is the quantitative sampling statement behind testability, and Theorem 1.7 says that a limit, viewed as a measure on the square, is unique.

The results are proved in the paper and have been used for over a decade. To the best of current knowledge they are not formalized in any proof assistant. The mission produces a machine-checked account of the permuton correspondence: the definitions of subpermutation density, limit permutation and $Z$ -random permutation, and the equivalences between the three natural convergences on $\mathcal Z$ . Alternative proofs are welcome, for instance of (ii) through Lemma 4.2 and the Borel–Cantelli lemma rather than the paper's strong law for U-statistics.

Difficulty

The obvious route to (i) is compactness: the laws of the random points attached to $Z_{\sigma_n}$ have a weakly convergent subsequence. The weak limit is only a measure, however. Turning it into a function $Z$ that is a cdf in $y$ for every $x$ , with exact uniform integrals for every $y$ , requires a regular conditional distribution (Lemma 2.2). One then has to show that weak convergence carries the pattern densities along. That fails for general measures on the square, because the events defining $\sigma(k,Z)=\tau$ have boundaries on which ties occur. Uniform marginals are what rule the ties out. The limit must also be independent of the subsequence, which needs the uniqueness statement Lemma 5.1. For (ii), the natural random sequence converges only almost surely, so an almost-sure limit theorem or a quantitative concentration bound is unavoidable.

Formalization scope

$[0,1]$ is Mathlib's unitInterval with Lebesgue measure. A limit permutation is a curried real function Z : I → I → ℝ. Measurability is almost-everywhere measurability for the product measure, which is Lebesgue measurability. The cdf and integral conditions hold for every $x$ and every $y$ .
$S_n$ is Equiv.Perm (Fin n) (0-based), and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n). Patterns of every length, including the trivial length $0$ , are quantified over; the length- $0$ clause always holds.
The law of the associated random point is built by the inverse-cdf construction $(x,u) \mapsto (x, \inf\{y : u \le Z(x,y)\})$ applied to Lebesgue measure on the square. The density $t(\tau,Z)$ is the product measure of the event $A_\tau$ (strict orders, so ties are excluded).
$Z_\sigma$ is given in closed form; at $x = 0$ it uses the first row, a null-set choice that keeps every $Z_\sigma(x,\cdot)$ a cdf. $d_\square$ is the real supremum over rectangles, and is bounded on $\mathcal Z$ .
" $k$ sufficiently large" in Lemma 4.2 is $\exists k_0\,\forall k \ge k_0\,\forall Z$ , with the paper's constants $16$ , $k^{-1/4}$ , $\tfrac12 e^{-\sqrt k}$ . The probability is written as a sum of $t(\tau,Z)$ over the qualifying $\tau$ .
Theorem 1.7 is false as literally printed (its "if" direction fails); the corrected form assumes $\sigma_n \to Z_1$ .
A trivializing formalization is ruled out: $t(\tau,Z)$ is a genuine sampling probability under a probability measure whose joint distribution function is pinned down by Eq. (21), and $\sigma_n \to Z$ includes $|\sigma_n| \to \infty$ .

Needed infrastructure includes Prokhorov compactness of probability measures on a compact space, the Portmanteau theorem, conditional cdfs (ProbabilityTheory.condCDF), Hoeffding's inequality and Borel–Cantelli, all largely in Mathlib. The permutation-density and permuton layer is reusable for quasirandomness and testing results. Mission II of this series, on the rectangular-distance characterization, uses the same model.

Selected references

C. Hoppen, Y. Kohayakawa, C. G. Moreira, B. Ráth, R. M. Sampaio, Limits of permutation sequences, arXiv:1103.5844v2, 2012; J. Combin. Theory Ser. B 103 (2013). https://arxiv.org/abs/1103.5844v2
L. Lovász, B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96 (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002
C. Borgs, J. T. Chayes, L. Lovász, V. T. Sós, K. Vesztergombi, Convergent sequences of dense graphs I: Subgraph frequencies, metric properties and testing, Adv. Math. 219 (2008) 1801–1851. https://doi.org/10.1016/j.aim.2007.08.004
C. Hoppen, Y. Kohayakawa, C. G. Moreira, R. M. Sampaio, Testing permutation properties through subpermutations, Theoret. Comput. Sci. 412 (2011) 3555–3567. https://doi.org/10.1016/j.tcs.2010.10.041
P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962

17 thms2 active usersReviewed

Operations Research Probability·Captain: mikedeng1

The Erdős Matching Conjecture and Concentration Inequalities: The Conjecture in a Linear RangeResearch Paper

Motivation

In 1965 Erdős asked how large a family of $k$ -element subsets of an $n$ -element set can be if it contains no $s+1$ pairwise disjoint members. The question, now called the Erdős Matching Conjecture (EMC), contains the Erdős–Ko–Rado theorem (the case $s=1$ ) and is one of the central open problems of extremal set theory. Beyond combinatorics it is tied to tail bounds for sums of random variables (generalizations of Markov's inequality, see Alon, Frankl, Huang, Rödl, Ruciński and Sudakov, JCTA 2012, as cited on p. 2 of the paper) and to Dirac-type thresholds for perfect matchings in hypergraphs.

Timeline.

1965: Erdős proves the conjecture for $n\ge n_0(k,s)$ .
1959/1968: Erdős–Gallai settle $k=2$ ; Kleitman settles the case $n=k(s+1)$ implicitly.
1976: Bollobás, Daykin and Erdős prove it for $n\ge2k^3s$ .
2012: Huang, Loh and Sudakov prove it for $n\ge3k^2s$ .
2013: Frankl proves it for $n\ge(2s+1)k-s$ (JCTA 120).
2017: Frankl settles $k=3$ completely.
2018–2022: Frankl and Kupavskii prove it for $n\ge\frac53sk-\frac23s$ and all $s\ge s_0$ (arXiv:1806.08855), the result of this mission.

Setting

Write $[n]=\{1,\dots,n\}$ and $\binom{[n]}{k}$ for the set of its $k$ -element subsets. For a family $\mathcal F\subseteq\binom{[n]}k$ , a matching is a subfamily of pairwise disjoint members, and the matching number $\nu(\mathcal F)$ is the largest size of a matching. The Erdős matching function is

m(n,k,s)=\max\Big\{|\mathcal F| : \mathcal F\subseteq\tbinom{[n]}{k},\ \nu(\mathcal F)\le s\Big\}.

Two families show the conjectured value. The family of all $k$ -sets meeting $[s]$ has $\binom nk-\binom{n-s}k$ members; the family of all $k$ -subsets of $[k(s+1)-1]$ has $\binom{k(s+1)-1}k$ members. Both have $\nu\le s$ , and the EMC asserts $m(n,k,s)$ is the larger of the two numbers. For $n\ge(k+1)s$ the first is larger.

The proof uses the shifting order: for $A=\{a_1<\dots<a_k\}$ and $B=\{b_1<\dots<b_k\}$ , $A\prec B$ if $a_i\le b_i$ for all $i$ and $A\ne B$ . A family is initial if it is closed downward under $\prec$ . For $S\subseteq[s+1]$ , $\mathcal F(S)=\{F\setminus S: F\in\mathcal F,\ F\cap[s+1]=S\}$ , and $\partial$ denotes the shadow. Families $\mathcal F_1,\dots,\mathcal F_{s+1}$ are cross-dependent if no choice $F_i\in\mathcal F_i$ is pairwise disjoint, and nested if $\mathcal F_1\supseteq\dots\supseteq\mathcal F_{s+1}$ . A random $t$ -matching is a uniformly random ordered $t$ -tuple of pairwise disjoint $l$ -subsets of $[m]$ , and $\eta=|\mathcal G\cap\mathcal B|$ counts how many of its sets lie in a fixed family $\mathcal G$ of density $\alpha=|\mathcal G|/\binom ml$ .

Formalization targets

Goal: Theorem 1

There is an absolute constant $s_0$ such that for all $k\ge1$ , $s\ge s_0$ and

n\ge\tfrac53sk-\tfrac23s\qquad\text{we have}\qquad m(n,k,s)=\binom nk-\binom{n-s}k .

The constant $s_0$ is existential and uniform in $n$ and $k$ ; no value is fixed, so any improvement of the proof keeps the statement valid.

Stronger form: Theorem 14

For every $\varepsilon>0$ there is $s_0(\varepsilon)$ such that the same equality holds for all $s\ge s_0$ , $k\ge1$ and $n\ge s+(1.666+\varepsilon)s(k-1)$ . Theorem 1 follows by taking $\varepsilon<\frac53-1.666$ .

Milestones

Following the paper's proof: Lemma 3 (shifting), Proposition 4, Lemma 5, Proposition 6, Corollary 7 and Lemma 8 (structure of initial families and their shadows); Proposition 11, Theorem 12 and Proposition 13 (concentration of $\eta$ for random matchings); Lemma 18 and Lemma 15 (the weighted bound for cross-dependent nested families); Lemmas 16 and 17 (the induction step at $n=s+(1.666+\varepsilon)s(k-1)$ ); Theorem 14.

Significance

The theorem extends the range in which the EMC is known from $n\ge(2s+1)k-s$ to $n\ge\frac53sk-\frac23s$ for large $s$ , settling roughly a third of the remaining range. The paper uses it as a black box to derive a universal upper bound on $m(n,k,s)$ below that range (its Theorem 2) and consequences for Dirac thresholds. The concentration inequality of Theorem 12, a Gaussian tail for the number of members of a fixed family hit by a random matching, is a tool of independent use and has since been applied to rainbow versions of the problem (Kupavskii, arXiv:2104.08083).

The result is proved on paper; this mission formalizes it. No part of the argument has a machine-checked proof: Mathlib has shadows and the Erdős–Ko–Rado theorem, and the platform has Erdős–Ko–Rado for $s=1$ , but there is no formal theory of the matching number, shifted families, Kneser graph spectra, or martingale concentration for random matchings. A complete formalization would make the EMC in this range, and the concentration theorem, available for reuse.

Difficulty

Averaging over a random full partition of $[n]$ into $k$ -sets gives only $m(n,k,s)\le s\binom{n-1}{k-1}$ , far from the truth: the expected number of partition classes in $\mathcal F$ says nothing about how that number is distributed. The paper's step is to show the count is concentrated (Theorem 12) and to exploit the deterministic bound of Lemma 18, which penalizes matchings with many classes in $\mathcal F_{s+1}$ . Controlling the regime where the density $\alpha$ is small needs the separate comparison of Proposition 13.

The second difficulty is Lemma 17, whose proof in the appendix is a delicate estimate on sums and products of binomial coefficients over all $k\ge4$ , supported by numerical computations done in Mathematica. A formal proof needs certified numerics for these finite checks and a separate stability argument for $k>2\cdot10^4$ . The case $k=3$ is an external base case (Frankl 2017), so the induction on $k$ also needs that result or another route.

Formalization scope

Sets are finite sets of natural numbers; $[n]$ is Finset.Icc 1 n, so the paper's indices such as $[i(s+1)-1]$ and $s+1,2(s+1),\dots$ appear unshifted. $\nu$ is a maximum over subfamilies (members are distinct), and $m(n,k,s)$ is a finite maximum, always attained. Initial families are closed downward among $k$ -subsets of $[m]$ only. Random matchings are ordered tuples, and probabilities, expectations and covariances are uniform averages over the finite sample space. The constant $1.666$ is the exact decimal, not $5/3$ . The paper omits integer parts at $n=s+(c+\varepsilon)s(k-1)$ ; the formalization rounds $n$ up. Where the paper leaves hypotheses implicit, they are binders: $k\ge2$ in Corollary 7, Lemma 8 and Lemma 16, $k\ge4$ and the induction hypothesis in Lemma 17, $t\ge1$ in Theorem 12, and $q>0$ (the division $sx/q$ ) in Lemma 15.

The goal is the equality $m(n,k,s)=\binom nk-\binom{n-s}k$ ; exhibiting the family of $k$ -sets meeting $[s]$ proves only the lower bound and does not close it.

Useful infrastructure, reusable beyond this mission: shifting and the compression argument (Lemma 3), the shadow bounds of Section 2, the expander mixing lemma and the second eigenvalue of Kneser graphs, and the Azuma–Hoeffding inequality for the exposure martingale of a random matching. Contributions of any of these, and of alternative proofs of the milestones, are welcome.

Selected references

P. Frankl, A. Kupavskii, The Erdős Matching Conjecture and concentration inequalities, J. Combin. Theory Ser. B (2022); arXiv:1806.08855v3. https://arxiv.org/abs/1806.08855, https://doi.org/10.1016/j.jctb.2022.08.002
P. Erdős, A problem on independent r-tuples, Ann. Univ. Sci. Budapest. Eötvös Sect. Math. 8 (1965), 93–95.
P. Frankl, Improved bounds for Erdős' Matching Conjecture, J. Combin. Theory Ser. A 120 (2013), 1068–1072. https://doi.org/10.1016/j.jcta.2013.01.008
P. Frankl, On the maximum number of edges in a hypergraph with given matching number, Discrete Appl. Math. 216 (2017), 562–581.
H. Huang, P.-S. Loh, B. Sudakov, The size of a hypergraph and its matching number, Combin. Probab. Comput. 21 (2012), 442–450.
N. Alon, F. Chung, Explicit construction of linear sized tolerant networks, Discrete Math. 72 (1988), 15–19. https://doi.org/10.1016/0012-365X(88)90189-6
L. Lovász, On the Shannon capacity of a graph, IEEE Trans. Inform. Theory 25 (1979), 1–7. https://doi.org/10.1109/TIT.1979.1055985

23 thms2 active usersReviewed

Graph Theory Operations Research Optimization+1·Captain: mikedeng1

Linear-Time Approximation for Maximum Weight Matching: The Approximation Guarantee of the Scaling AlgorithmResearch Paper

Motivation

The maximum weight matching (MWM) problem asks, for a graph with edge weights, for a set of vertex-disjoint edges of largest total weight. It is a central problem of combinatorial optimization, with applications to transportation, assignment and scheduling, and as a subroutine for shortest paths, planar max cut, Chinese postman tours and metric TSP. Edmonds' blossom algorithm (1965) solves it on general graphs; the fastest implementation, due to Gabow, runs in $O(mn+n^2\log n)$ time, and the scaling algorithm of Gabow and Tarjan (1991) runs in $O(m\sqrt{n\log n}\,\log(nN))$ time on graphs with $n$ vertices, $m$ edges and integer weights of magnitude at most $N$ . Applications such as switch scheduling, graph clustering and sparse linear solvers accept a slightly suboptimal matching in exchange for speed. This motivates $(1-\epsilon)$ -approximate maximum weight matchings: matchings whose weight is at least a $1-\epsilon$ fraction of the optimum.

Timeline of linear and near-linear time approximation for general graphs (Section 1.3 and Table IV of the paper; the entries below are as the paper attributes them):

Folklore: the greedy algorithm, which repeatedly takes the heaviest remaining edge, gives a $\tfrac12$ -MWM in $O(m\log n)$ time.
Preis (STACS 1999): a $\tfrac12$ -MWM in linear time; Drake and Hougardy (2003) gave a simpler one.
Drake and Hougardy (2003; journal version Vinkemeier and Hougardy, ACM Trans. Algorithms 2005): a $(\tfrac23-\epsilon)$ -MWM in $O(m\epsilon^{-1})$ time; Pettie and Sanders (2004) improved this to $O(m\log\epsilon^{-1})$ .
Duan and Pettie (FOCS 2010) and Hanke and Hougardy (2010): a $(\tfrac34-\epsilon)$ -MWM in $O(m\log n\log\epsilon^{-1})$ time.
Duan and Pettie (2014): a $(1-\epsilon)$ -MWM in $O(m\epsilon^{-1}\log\epsilon^{-1})$ time, which is linear for every fixed $\epsilon$ .

Setting

Let $G=(V,E)$ be a finite simple graph with integer weights $w:E\to\{1,\dots,N\}$ , $N=2^L$ . A matching $M$ is a set of vertex-disjoint edges, with weight $w(M)=\sum_{e\in M}w(e)$ ; a vertex is free if no edge of $M$ touches it. $M$ is a $c$ -MWM if $c\cdot w(M')\le w(M)$ for every matching $M'$ .

A blossom is built recursively: a single vertex $\{v\}$ is a trivial blossom with $E_{\{v\}}=\emptyset$ ; an odd number $\ge3$ of disjoint blossoms $A_0,\dots,A_\ell$ joined in a cycle by edges $e_i\in A_i\times A_{i+1}$ form the blossom $B=\bigcup A_i$ with edge set $E_B=\bigcup E_{A_i}\cup\{e_0,\dots,e_\ell\}$ . It is full if $|M\cap E_B|=(|B|-1)/2$ . The algorithm keeps a laminar set $\Omega$ of full blossoms; a root blossom is a maximal one, and $G/\Omega$ contracts each root blossom to a single vertex.

Dual values $y:V\to\mathbb R$ and $z$ on odd vertex sets give each edge the value

yz(u,v)=y(u)+y(v)+\sum_{B\ \text{odd},\ u,v\in B} z(B).

The scaling algorithm (Figure 2 of the paper) has parameters $N$ and $\epsilon'=2^{-g}\le\tfrac14$ . It runs scales $i=0,\dots,L$ with granularity $\delta_i=\epsilon'N/2^i$ and truncated weights $w_i(e)=\delta_i\lfloor w(e)/\delta_i\rfloor$ . Each scale repeats four steps: augment along a maximal set of vertex-disjoint augmenting paths of the eligible graph $G_{\mathrm{elig}}$ , shrink a maximal set of new blossoms, adjust the duals by $\pm\delta_i/2$ , and dissolve root blossoms whose $z$ -value has reached zero. It stops when the free vertices' $y$ -values reach a scale-dependent value, which is $0$ at scale $L$ . Eligibility is given by Definition 3.2; the linear-time variant keeps the algorithm unchanged and uses Definition 3.10, which additionally ignores an edge $e$ in scales $i>\mathrm{scale}(e)+\log\epsilon'^{-1}$ unless it is a blossom edge.

Formalization targets

Goal: Theorem 3.12, approximation half

For every $\epsilon$ with $\epsilon'\le\epsilon/7$ , the algorithm of Figure 2 with Definition 3.10 eligibility has a terminating run, and every terminating run returns a matching $M$ with

w(M)\ \ge\ (1-\epsilon)\,w(M')\qquad\text{for every matching } M' \text{ of } G .

Milestones, in attack order

Lemma 2.3: approximate complementary slackness ( $yz(e)\ge(1-\epsilon_0)w(e)$ everywhere, $yz(e)\le(1+\epsilon_1)w(e)$ on matched and blossom edges, zero free duals) gives a $(1+\epsilon_1)^{-1}(1-\epsilon_0)$ -MWM.
Section 2 rescaling: rounding real weights to $\lfloor w/\gamma_r\rfloor$ , $\gamma_r=\epsilon w_{\max}/n$ , loses at most a factor $1-\epsilon/2$ .
Lemma 3.5: with Definition 3.2 the algorithm preserves Property 3.1, which consists of granularity, active blossoms, near domination $yz(e)\ge w_i(e)-\delta_i$ , near tightness $yz(e)\le w_i(e)+2(\delta_j-\delta_i)$ for type- $j$ edges, and equal free duals.
Lemma 3.6: eligible edges searched up to scale $i$ weigh at least $N/2^{i+1}+\delta_i$ , and matched edges satisfy $yz(e)\le(1+4\epsilon')w(e)$ .
Lemma 3.7: the output under Definition 3.2 is a $(1-5\epsilon')$ -MWM.
Theorem 3.8: the approximation half of Theorem 3.8, with $\epsilon'\le\epsilon/5$ .
Lemma 3.11: the invariants under Definition 3.10, including $yz(e)>(1-\epsilon')w_i(e)$ and $yz(e)<(1+6\epsilon')w_i(e)$ once $i>\mathrm{scale}(e)+\gamma$ .

Significance

The result. Theorem 3.12 gives the first algorithm for $(1-\epsilon)$ -approximate maximum weight matching on general graphs that runs in linear time for every fixed $\epsilon$ ; earlier linear-time algorithms achieved only $\tfrac12$ or $\tfrac23-\epsilon$ . Its analysis is a relaxation of Edmonds' complementary slackness conditions that grows weaker over the scales, but not uniformly, and Lemma 2.3 certifies an approximate matching by approximately feasible duals.

Formalizing it. The result is proved in the paper. Mathlib (at the pinned revision) has matchings, alternating walks and Tutte's theorem, but no blossoms, contracted graphs or weighted matching algorithms. A complete development gives a Lean model of blossoms, contraction and augmenting paths through blossoms, a verified primal–dual invariant for a scaling algorithm, and a checked approximate-slackness certificate for matchings. Each of these can be reused to formalize Edmonds' exact algorithm or the Gabow–Tarjan scaling algorithm.

Difficulty

The two halves of the argument pull against each other. Lemma 2.3 needs near domination and near tightness as multiplicative bounds. The algorithm maintains only additive bounds whose slack for an edge of type $j$ is $2(\delta_j-\delta_i)$ , and this slack does not shrink as the scales advance. Converting it into a factor $1+O(\epsilon')$ requires a lower bound on the weight of every edge that ever became eligible, which in turn depends on the free vertices' duals following an exact schedule across scales.

For Definition 3.10 the obvious argument breaks down: an edge that is ignored after scale $\mathrm{scale}(e)+\gamma$ may violate near domination and near tightness by an amount that grows with every later dual adjustment. The claim is that the accumulated violation stays within an $O(\epsilon')$ fraction of $w_i(e)$ , and establishing this requires tracking every adjustment that can reach an ignored edge.

On the combinatorial side, the Augmentation and Blossom Shrinking steps work in the contracted graph $G/\Omega$ . Their correctness uses the classical facts that augmenting paths lift through full blossoms and that blossoms stay full after augmentation (Lemma 2.1), which have to be formalized from scratch.

Formalization scope

Graphs are SimpleGraph V on a Fintype V with decidable equality; edges are Sym2 V; matchings are Finset (Sym2 V) with pairwise vertex-disjoint edges of $G$ ; weights are $w:\mathrm{Sym2}\,V\to\mathbb N$ with $1\le w(e)\le 2^L$ on edges. Duals, $\delta_i$ and $w_i$ are real numbers. $z$ is a function on all finite vertex sets and $yz$ sums it over the odd sets that contain the edge, as on the page. $N=2^L$ and $\epsilon'=2^{-g}$ , $g\ge2$ , are given through their exponents. $\mathrm{scale}(e)$ uses the convention $\mu_{-1}=+\infty$ . The paper's standing assumption $N\le n^2$ is used only for running time and is omitted.

The algorithm is a nondeterministic relation. A state holds $M$ , $\Omega$ with its blossom edge sets, $y$ , $z$ , a ghost record of the scale in which each edge last entered $M\cup\bigcup_{B\in\Omega}E_B$ , and the common free-vertex dual that drives the loop test. The maximal sets of augmenting paths and of new blossoms and the lifts of paths through blossoms are choices. Invariants are stated for states reachable by a run, and the goal asserts both that a terminating run exists and that every terminating run returns a $(1-\epsilon)$ -MWM.

The running times $O(m\epsilon^{-1}\log N)$ of Theorem 3.8 and $O(m\epsilon^{-1}\log\epsilon^{-1})$ of Theorem 3.12 are not formalized: the paper fixes no cost model, and its bounds rely on a modified depth-first search and on word-RAM table lookups. The explicit constants $\epsilon'\le\epsilon/5$ (Theorem 3.8) and $\epsilon'\le\epsilon/7$ (Theorem 3.12) are the ones the proofs supply.

The following trivializing formalizations are ruled out: a "matching" that may contain non-edges or repeated edges; a goal about a state only assumed to satisfy Property 3.1 rather than reached by the algorithm; a run relation with no terminating run, which the existence conjunct excludes; eligibility or blossoms chosen freely instead of by the page's rules; and comparison only against matchings of the contracted graph instead of all matchings of $G$ .

Welcome contributions include a Lean treatment of blossoms and their contraction (Lemma 2.1, which is not a milestone here), the lift of augmenting paths, Lemmas 3.3 and 3.4 as auxiliary results, and proofs of the milestones in the order listed.

Selected references

R. Duan and S. Pettie, Linear-Time Approximation for Maximum Weight Matching, Journal of the ACM 61(1), Article 1, 2014. https://doi.org/10.1145/2529989
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
H. N. Gabow and R. E. Tarjan, Faster scaling algorithms for general graph-matching problems, Journal of the ACM 38(4), 815–853, 1991. https://doi.org/10.1145/115234.115366
R. Preis, Linear time 1/2-approximation algorithm for maximum weighted matching in general graphs, STACS 1999, LNCS 1563, 259–269 (cited from the bibliography of Duan and Pettie 2014).
D. E. D. Vinkemeier and S. Hougardy, A linear-time approximation algorithm for weighted matchings in graphs, ACM Transactions on Algorithms 1(1), 107–122, 2005 (cited from the bibliography of Duan and Pettie 2014).
S. Pettie and P. Sanders, A simpler linear time 2/3 − ϵ approximation to maximum weight matching, Information Processing Letters 91(6), 271–276, 2004 (cited from the bibliography of Duan and Pettie 2014).

12 thms2 active usersReviewed

Completed

Graph Theory Operations Research Optimization·Captain: mikedeng1

Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems 1: The Augmentation Bound for Shortest Augmenting PathsResearch Paper

Why the number of augmentations matters

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 is a basic model in operations research, underlies bipartite matching, transportation and scheduling problems, and is a standard subroutine inside larger combinatorial algorithms.

The classical method for it is the labeling method of Ford and Fulkerson: starting from some flow, repeatedly find an augmenting path from source to sink along which flow can be increased, push as much as the path allows, and stop when no such path exists. When all capacities are integers, each augmentation raises the flow value by at least one, so the method terminates, but the number of augmentations can be as large as the final flow value, which is exponential in the size of the input. Edmonds and Karp give a four-node example in which the method alternates between two paths and needs $2M$ augmentations for capacities $M$ (Edmonds–Karp 1972, p. 250). With irrational capacities, Ford and Fulkerson showed that the method need not terminate at all and may converge to a non-maximum flow.

Timeline.

1956 — Ford and Fulkerson introduce the labeling method and the max-flow min-cut theorem (Ford–Fulkerson 1956).
1962 — Flows in Networks records the non-termination example for incommensurable capacities.
1970 — Dinic independently obtains a polynomial bound using layered (shortest-path) networks (Dinic 1970).
1972 — Edmonds and Karp prove that choosing each augmenting path with fewest arcs bounds the number of augmentations by $\tfrac14(n^3-n)$ , for arbitrary real capacities (Edmonds–Karp 1972, Theorem 1).

Setting

A network $N$ consists of a finite set of $n$ nodes, a source $s$ and a sink $t \ne s$ , and a set of arcs, which are ordered pairs $(u,v)$ with $u \ne v$ ; there is at most one arc from a node to another. One arc is the special return arc $(t,s)$ , and $A$ denotes the set of all other arcs. Each $(u,v) \in A$ has a real 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 with inflow equal to outflow at every node, the return arc included. The value $f(t,s)$ is the amount sent from $s$ to $t$ ; a maximum flow maximizes it.

Given a flow $f$ , the residual network $N^f$ has the same nodes, and $(u,v)$ is an arc of $N^f$ when $(u,v) \in A$ with $c(u,v) - f(u,v) > 0$ , or $(v,u) \in A$ with $f(v,u) > 0$ . An augmenting path is a sequence of distinct nodes $s = u_1, \dots, u_p = t$ whose consecutive pairs are arcs of $N^f$ . Each step carries a number $\varepsilon_i > 0$ (residual capacity forward, flow backward, or their sum when both $(u_i,u_{i+1})$ and $(u_{i+1},u_i)$ lie in $A$ ); $\varepsilon = \min_i \varepsilon_i$ , and a step with $\varepsilon_i = \varepsilon$ is a bottleneck arc. Augmenting raises $f(t,s)$ by $\varepsilon$ and shifts the flow on the path's arcs accordingly, using the paper's own rule for opposite arcs, which never exceeds a capacity.

A run with fewest-arc augmentations is a sequence $f^0, \dots, f^K$ where $f^0$ is a flow and each $f^{k+1}$ arises from $f^k$ by augmenting along a path $P^k$ with fewest arcs. The distance $\delta^k(u,v)$ is the least number of arcs of a directed path from $u$ to $v$ in $N^k = N^{f^k}$ , or $\infty$ .

Formalization targets

Goal — Theorem 1

For every network on $n$ nodes and every run of length $K$ with fewest-arc augmentations,

K \le \tfrac14\,(n^3 - n),

and if no augmenting path exists relative to $f^K$ , then $f^K$ is a maximum flow. The capacities are arbitrary positive reals, and the initial flow is arbitrary.

Milestones

§1.1: augmentation yields a flow with value $f(t,s) + \varepsilon$ , $\varepsilon > 0$ .
§1.1: a flow is maximum if and only if it admits no augmenting path.
Proposition 1: a bottleneck arc of $P^k$ is not an arc of $N^{k+1}$ .
Proposition 2: $(u,v) \in N^{k+1}$ implies $(u,v) \in N^k$ or $(v,u) \in P^k$ .
Lemma 1: if $(u,v)$ is a bottleneck arc at steps $k < m$ , then $(v,u) \in P^l$ for some $k < l < m$ .
Proposition 3: $\delta^k(s,u) \le \delta^{k+1}(s,u)$ and $\delta^k(u,t) \le \delta^{k+1}(u,t)$ .
Lemma 2: if $k < l$ , $(u,v) \in P^k$ and $(v,u) \in P^l$ , then $\delta^l(s,t) \ge \delta^k(s,t) + 2$ .
Proof of Theorem 1: each pair $\{u,v\}$ occurs as a bottleneck at most $\tfrac12(n+1)$ times.

Significance

The theorem shows that one simple rule for choosing augmenting paths, which a breadth-first labeling process implements, makes the number of augmentations depend on the number of nodes alone, independent of the capacities and of their arithmetic nature. It removes both pathologies of the unrestricted labeling method at once: exponential running time for integer capacities, and non-termination for irrational ones. Together with Dinic's work it is the starting point of the theory of strongly polynomial network-flow algorithms, and the distance-monotonicity argument (Proposition 3, Lemma 2) reappears in blocking-flow and push-relabel analyses.

The result is classical and fully proved in the paper. What this mission adds is a machine-checked version of the complete argument in the paper's own model: return arc, arbitrary real capacities, and the paper's augmentation rule for pairs of opposite arcs, which differs from Ford and Fulkerson's (footnote 1, p. 249). The platform has a max-flow min-cut theorem and an integer termination theorem for the Ford–Fulkerson method in the Bertsimas–Tsitsiklis model (Introduction to Linear Optimization, missions IX–X), but no bound on the number of augmentations. No machine-checked proof of Theorem 1 in Lean is known to exist.

Difficulty

The obvious argument, "each augmentation saturates a bottleneck arc, which then disappears", fails because a saturated arc can reappear after later augmentations push flow back along its reverse. Counting augmentations therefore requires control over how often the same pair of nodes can supply a bottleneck again, and no property of a single augmentation provides it; the bound has to come from an invariant of the whole run that holds for real capacities, where no integrality argument is available. A second trap is that the converse direction of milestone 2 (no augmenting path implies maximality) is a max-flow min-cut statement that the paper cites without proof; it must be proved in the paper's model with the return arc.

Formalization scope

Nodes form a finite type V with decidable equality and $n$ = Fintype.card V counts all nodes, $s$ and $t$ included. The arc set A is a Finset (V × V) with no loops and without $(t,s)$ ; capacities are real and positive on A. A flow is a function V → V → ℝ whose values off the arcs are ignored. A maximum flow is the predicate " $f(t,s) \ge g(t,s)$ for every flow $g$ ", never a real supremum. Paths are lists of distinct nodes with every consecutive pair a residual arc, so the return arc is never on a path. Distances take values in ℕ∞. A run is a pair of ℕ-indexed sequences constrained on indices up to $K$ . The explicit constants are stated as printed: $4K \le n^3 - n$ in ℕ (the truncated subtraction is harmless since $n \le n^3$ ) and $2\,b(u,v) \le n + 1$ for the per-pair count.

Case (b) of the paper's definition of augmenting paths is misprinted (its hypothesis repeats that of Case (c)); the formalization uses the reading $(u_i,u_{i+1}) \notin A$ , $(u_{i+1},u_i) \in A$ , which the paper's own description of $N^f$ on p. 251 confirms.

A trivializing formalization is ruled out: a run predicate that no sequence satisfies (for instance, one that requires paths through the return arc, or computes $\varepsilon = 0$ ) would make the bound vacuous; the step predicate here is satisfiable, and a concrete four-node run has been checked. Replacing the paper's augmentation rule by "increase the forward arc by $\varepsilon$ " would also change the theorem, because that rule can violate capacities.

A complete development needs basic facts on simple paths in finite digraphs, shortest paths and their subpaths, and a max-flow min-cut theorem in the paper's model. These are reusable well beyond this mission, as are the network, residual-network and augmentation definitions. Contributions proving any milestone independently are welcome.

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, Maximal Flow Through a Network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
E. A. Dinic, Algorithm for Solution of a Problem of Maximum Flow in a Network with Power Estimation, Soviet Mathematics Doklady 11:1277–1280, 1970. https://www.cs.bgu.ac.il/~dinitz/D70.pdf
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 7 (network flow problems; formalized on the platform in missions IX–X).

24 thms2 active usersReviewed

Graph Theory Theoretical Computer Science·Captain: mikedeng1

Sorting in c log n Parallel Steps: Sorting Networks of Logarithmic DepthResearch Paper

Motivation

A sorting network is a sorting procedure whose sequence of comparisons is fixed in advance, independently of the data. Its depth, the number of rounds of simultaneous comparisons on disjoint pairs, is the parallel running time. Sorting networks are used in parallel and hardware sorting, in switching networks, and in cryptography, where a data-independent (oblivious) sequence of operations is required. How small the depth can be as a function of the number of inputs $n$ is a basic question of parallel computation.

Timeline:

1968. Batcher's odd-even merge sort and bitonic sort give networks of depth $O((\log n)^2)$ and size $O(n(\log n)^2)$ (K. E. Batcher, Sorting networks and their applications, AFIPS Spring Joint Computer Conference, 1968). For $n$ a power of two they remain the best explicit networks in practice.
1973. Knuth's The Art of Computer Programming, Vol. 3, §5.3.4, surveys sorting networks. A simple counting argument gives the lower bound: every sorting network has depth at least $\log_2 n$ , since each output depends on at most $2^{\text{depth}}$ inputs.
1983. Ajtai, Komlós and Szemerédi construct networks of depth $O(\log n)$ and size $O(n\log n)$ (Combinatorica 3 (1983) 1–19, doi:10.1007/BF02579338), matching the lower bound up to a constant. The constant is not computed in the paper and is known to be very large.
1990. Paterson simplifies the construction and gives the first explicit, still very large, depth constant (M. S. Paterson, Improved sorting networks with O(log N) depth, Algorithmica 5 (1990) 75–92, doi:10.1007/BF01840378).
2014. Goodrich gives Zig-zag sort, a simpler deterministic data-oblivious sorting algorithm with $O(n\log n)$ comparisons that avoids the AKS machinery but is not of logarithmic depth (arXiv:1403.2777).

Setting

There are $n$ registers $R_1,\dots,R_n$ holding elements of a linearly ordered set. An elementary step (a comparator) $(i,j)$ with $i\neq j$ compares the contents of $R_i$ and $R_j$ and exchanges them if the content of $R_i$ is larger. Afterwards $R_i$ holds the minimum and $R_j$ the maximum of the two, and every other register is unchanged. A parallel step is a set of comparators in which no register occurs twice, so it has at most $n/2$ comparators. A comparator network $N$ is a finite sequence of parallel steps, fixed before the input is seen. Its depth $\operatorname{depth}(N)$ is the number of parallel steps and its size $\operatorname{size}(N)$ the total number of comparators. $N$ sorts if for every input $x=(x_1,\dots,x_n)$ the output $N(x)$ satisfies $N(x)_1\le\cdots\le N(x)_n$ .

The construction runs on the tree $T$ of finite $0$ - $1$ sequences, whose levels are ordered lexicographically. A chain on level $i$ assigns to every node of that level a set of registers, with the sets pairwise disjoint and of a common size $N(C)$ . A ⟨k, ε⟩ expander on ⟨A, B⟩, for disjoint register sets $A$ and $B$ , is a bipartite graph between $A$ and $B$ of maximum degree $k$ in which every nonempty $X\subseteq A$ has more than $(1-\varepsilon)\varepsilon^{-1}\min\{|X|,\varepsilon|B|\}$ neighbours, and symmetrically for $B$ . The Lean development uses the names ComparatorNetwork, compareExchange, IsChain, chainN, IsExpander, IsLowerSection for these objects.

Formalization targets

Goal: the AKS theorem (Abstract and §1, p. 1)

\exists\, c>0\ \ \forall n\ge 2\ \ \exists N:\quad N \text{ sorts},\qquad \operatorname{depth}(N)\le c\log_2 n,\qquad \operatorname{size}(N)\le c\,n\log_2 n .

The constant is absolute and is not fixed. Any explicit value would be invalidated by the next improvement, and the paper gives none.

Milestones (the paper's numbered lemmas that hold as stated)

Lemma 3 (p. 6): for $0<\varepsilon<1$ and $c\ge1$ there is $k(\varepsilon,c)$ such that every pair of disjoint sets with $1/c\le|A|/|B|\le c$ carries a $\langle k,\varepsilon\rangle$ expander.
Lemma 4 (p. 7): performing every comparator of such an expander once, in any order, from $A$ to $B$ leaves all but an $\varepsilon$ -fraction of any lower section $S$ with $|S|\le|A|$ in $A$ , and symmetrically for upper sections in $B$ :

|S\setminus\mathrm{Cont}(A)|\le\varepsilon|S| .

Lemma 1 (pp. 3–4): the splitting $V(C,k)$ of a chain, which moves one register of each leaf set up the tree, produces chains with properties (1.1)–(1.5).
Lemma 2 (p. 4): chains $W(C,k)$ with $a_k-1\le N(W(C,k))\le a_k$ exist under conditions (2a), (2.b).
Lemma 12(a) (p. 14): a violation of the order relation $R^\beta_G$ between two nodes of a level is witnessed by two consecutive nodes.

Significance

The result. The AKS theorem settles the asymptotic depth of sorting networks at $\Theta(\log n)$ and their size at $\Theta(n\log n)$ . It gives an $O(\log n)$ -time sorting algorithm with $n$ processors that performs only data-independent comparisons. It is the standard reference point for oblivious sorting in parallel algorithms, circuit complexity (sorting is in $\mathsf{NC}^1$ via comparators) and oblivious RAM constructions. Lemma 4, the ε-halver property of expander comparisons, is the component that later constructions (Paterson) reuse.

Formalizing it. The theorem has been proved since 1983. No Lean proof of the AKS theorem is known. Mathlib has no expander graphs in the ⟨k, ε⟩ sense and no sorting networks. The mission asks for a formal proof of the headline theorem by any route (the AKS construction or Paterson's variant), and for formal proofs of the paper's verified lemmas as reusable components. The expander lemma needs either an explicit family (Margulis; Gabber–Galil) or a probabilistic existence argument, both substantial on their own.

Difficulty

Every elementary argument stalls at depth $O((\log n)^2)$ : recursive merging needs $\log n$ merge rounds, and merging two sorted lists by a comparator network needs depth $\Omega(\log n)$ . A depth of $O(\log n)$ therefore cannot come from exact merging. It must come from constant-depth approximate operations (ε-halvers, which require bounded-degree expanders) combined with a mechanism that corrects the errors they leave. In the paper this mechanism is a movement of registers up and down a binary tree, controlled by a family of constants chosen in a fixed order (" $\varepsilon_1\ll q_2\ll1-g\ll q_1\ll 1/c_1\ll1$ ", p. 2). The accounting that shows the misplaced elements decay geometrically is the hard part. Several intermediate lemmas of the paper are false as printed, so the paper's text is not a checklist to transcribe.

Formalization scope

Conventions committed to in Lean:

Registers are Fin n, and contents lie in an arbitrary linearly ordered type. A network is a List of layers, each a List (Fin n × Fin n) of comparators with distinct endpoints, and no register occurs twice in a layer. A comparator $(i,j)$ puts the minimum into $i$ , and both directions $i<j$ and $i>j$ are allowed. Sorts means the output is monotone for every linearly ordered type and every input, not only for permutations.
$\log_2 n$ is Real.logb 2 n, and the goal is stated for $n\ge2$ . The constant $c$ is quantified before $n$ .
Tree levels are Fin (2^i), with numeric order equal to lexicographic order. A chain is a Fin (2^i) → Finset R.
Definition 2.2 of the paper, read literally, requires $|\Gamma_\emptyset|>0$ , which fails, so no graph would be an expander. The expansion inequalities are imposed on nonempty sets only, and the strict inequality is kept.

Trivializing formalizations are ruled out. The goal is not "for every $n$ there is a network of depth $O(\log n)$ " with the constant chosen after $n$ , which is true for trivial reasons. Layers without the disjointness condition would let a single layer contain a whole insertion sort. A bound on the number of comparisons alone, with unbounded depth, is a different and much older result; the goal states both the depth and the size bound.

The mission states the AKS theorem and the paper's lemmas that are correct as stated. It does not formalize the AKS algorithm itself ( $S^\alpha$ , $P^\alpha$ , the operations CH1–CH4, IMP) or its intermediate Lemmas 5–11 and 13–15. Those depend on unspecified constants constrained only by "sufficiently small" chains, and Lemmas 5, 10 and 12(b) are false as printed. A solver may of course define the algorithm, with pinned constants, as part of a proof.

Contributions welcome: a library of comparator networks (composition, the 0-1 principle, depth of Batcher's networks), existence of bounded-degree bipartite expanders, the ε-halver lemma, and any complete proof of the goal. The network and expander definitions are independent of this paper and reusable.

Selected references

M. Ajtai, J. Komlós, E. Szemerédi, Sorting in c log n parallel steps, Combinatorica 3(1) (1983) 1–19. doi:10.1007/BF02579338
K. E. Batcher, Sorting networks and their applications, Proc. AFIPS Spring Joint Computer Conference 32 (1968) 307–314. doi:10.1145/1468075.1468121
D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, Addison-Wesley, 1973, §5.3.4.
G. A. Margulis, Explicit constructions of concentrators, Problems of Information Transmission 9 (1973) 325–332.
O. Gabber, Z. Galil, Explicit constructions of linear-sized superconcentrators, J. Computer and System Sciences 22(3) (1981) 407–420. doi:10.1016/0022-0000(81)90040-4
M. S. Paterson, Improved sorting networks with O(log N) depth, Algorithmica 5 (1990) 75–92. doi:10.1007/BF01840378
M. T. Goodrich, Zig-zag sort: a simple deterministic data-oblivious sorting algorithm running in O(n log n) time, STOC 2014. arXiv:1403.2777

13 thms2 active usersReviewed

Completed

Graph Theory Operations Research Optimization+1·Captain: mikedeng1

An Analysis of Several Heuristics for the Traveling Salesman Problem II: Every Insertion Method Is Within ⌈lg n⌉ + 1 of the Optimal TourResearch Paper

Motivation

The traveling salesman problem asks for a shortest closed route visiting every node of a weighted complete graph exactly once. It is NP-hard, so practitioners use fast heuristics, and the basic question about a heuristic is how far from optimal its tour can be. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the simple constructive heuristics under the triangle inequality: nearest neighbor, the family of insertion methods, and several variants.

Insertion methods build a tour by growing it one node at a time. They are among the most widely used construction heuristics in practice and in textbooks, and they differ only in the rule that chooses which node to insert next: the nearest one, the cheapest one, the farthest one, a random one, or any other. This mission formalizes the paper's result that holds for the whole family at once, regardless of that rule: every insertion method produces a tour at most $\lceil \lg n\rceil + 1$ times longer than an optimal one (Theorem 3, p. 571).

Timeline. 1977: Rosenkrantz, Stearns and Lewis prove $\lceil\lg n\rceil+1$ for every insertion method (Theorem 3), $\tfrac12(\lceil\lg n\rceil+1)$ for nearest neighbor (Theorem 1), both from a shared counting lemma (Lemma 1), and the constant $2$ for nearest and cheapest insertion (Theorem 4). 1994: Bafna, Kalyanasundaram and Pruhs (Theoretical Computer Science 125, 1994) give instances on which some insertion methods reach ratio $\Omega(\log n/\log\log n)$ , so the logarithmic growth cannot be replaced by a constant for the family as a whole.

Setting

A traveling salesman graph with $n$ nodes consists of a finite node set $N$ with $|N|=n$ and a distance $d:N\times N\to\mathbb R$ with $d(i,j)=d(j,i)$ , $d(i,j)\ge 0$ and $d(i,j)+d(j,k)\ge d(i,k)$ for all nodes (the triangle inequality). A tour visits every node once and returns to its start; its length is the sum of its edge lengths, and OPTIMAL is the least length of a tour.

A subtour is a tour on a subset of the nodes; a single node is a tour without edges. Given a subtour $T$ and a node $k\notin T$ , TOUR $(T,k)$ is obtained by choosing an edge $(x,y)$ of $T$ minimizing

d(x,k)+d(k,y)-d(x,y)

and replacing it by the edges $(x,k)$ and $(k,y)$ ; if $T$ is a single node $i$ , TOUR $(T,k)$ is the two-node tour $(i,k),(k,i)$ . COST $(T,k)$ is the length of TOUR $(T,k)$ minus the length of $T$ .

An insertion method constructs subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ a single node and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some node $a_i\notin T_i$ , $1\le i<n$ . The final tour $T_n$ is the approximation, and INSERT denotes its length. No rule for choosing the $a_i$ is fixed, and ties between minimizing edges are broken arbitrarily.

Write $\lg$ for the logarithm to base 2 and $\lceil x\rceil$ for the least integer $\ge x$ .

Formalization targets

Goal: Theorem 3

For every traveling salesman graph with $n\ge 1$ nodes and every run of every insertion method,

\mathrm{INSERT}\ \le\ \bigl(\lceil\lg n\rceil+1\bigr)\cdot\mathrm{OPTIMAL}.

Milestones

(2.2), shortcutting: visiting a subset of the nodes in the order of a tour gives a tour of the subset that is no longer.
(2.1): if the numbers $l_1\ge\dots\ge l_n$ satisfy $d(p,q)\ge\min(l_p,l_q)$ for distinct $p,q$ , then $\mathrm{OPTIMAL}\ge 2\sum_{i=k+1}^{\min(2k,n)} l_i$ for $1\le k\le n$ .
Lemma 1: if $d(p,q)\ge\min(l_p,l_q)$ for distinct nodes and $l_p\le\frac12\mathrm{OPTIMAL}$ for all $p$ , then

\sum_p l_p\le\tfrac12\bigl(\lceil\lg n\rceil+1\bigr)\mathrm{OPTIMAL}.

Lemma 2: $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for every node $j$ of $T$ .
(3.7): $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$ .
(3.10): $\mathrm{COST}(T_i,a_i)\le 2\,d(a_i,a_j)$ whenever $j<i$ .
(3.12): $\mathrm{COST}(T_i,a_i)\le\mathrm{OPTIMAL}$ for $1\le i<n$ .

Significance

The result. Theorem 3 is a guarantee for an entire class of algorithms rather than for one. Any rule for choosing the next node, including rules designed for speed or for empirical quality, inherits a worst-case ratio of $\lceil\lg n\rceil+1$ from the insertion step alone. The rule matters only for improving on that: nearest and cheapest insertion achieve the constant $2(1-1/n)$ (Theorem 4 and its corollary, the subject of the third mission of this series), while the logarithmic bound remains the best general statement for other rules, such as farthest or arbitrary insertion. Lemma 1 is reusable on its own: it converts "every node carries a charge bounded by half the optimum and by its distance to other nodes" into a logarithmic bound, and the same lemma yields the nearest neighbor bound of Theorem 1.

Formalizing it. The theorem has been proved since 1977; the work here is a machine-checked proof of the known argument together with a reusable library for subtours, insertion and insertion costs. The companion nearest neighbor bound (Theorem 1) is already on the platform as SupplyChainTheory.nearest_neighbor_bound (proved), and nearest insertion with constant 2 as SupplyChainTheory.nearest_insertion_bound; neither covers arbitrary insertion methods or states Lemma 1 separately.

Difficulty

The per-step facts are local: each insertion is cheap relative to a node already present (Lemma 2) and relative to OPTIMAL (3.12). The obvious way to combine them, adding up $n-1$ costs each at most OPTIMAL, gives only the ratio $n-1$ . The logarithm comes from a global counting argument over all nodes simultaneously (Lemma 1), in which OPTIMAL is compared with tours on nested subsets of nodes of doubling size, and the per-node charges must be matched against the edges of those tours. Formally, the delicate parts are the bookkeeping of subtours as they grow (that every earlier node lies on the current subtour, and that the insertion cost equals the length increase), the shortcutting of a tour to an arbitrary subset, and the ceiling-of-logarithm arithmetic.

Formalization scope

Nodes are Fin n; a tour of all nodes is a permutation τ : Equiv.Perm (Fin n), and OPTIMAL is the minimum of the tour length over the finite, nonempty set of permutations. Subtours are duplicate-free lists of nodes, with closed length $d(x_0,x_1)+\dots+d(x_{m-1},x_0)$ . TOUR $(T,k)$ is encoded as inserting $k$ at a list position whose resulting length is minimal among all positions; inserting at a position removes exactly one edge of $T$ and raises the length by exactly $d(x,k)+d(k,y)-d(x,y)$ , so this is the paper's rule, with every tie-breaking allowed. COST is the minimum length increase over positions. The paper's 1-based subtour index is kept ( $T_1=[a_0]$ , $T_n$ final). $\lceil\lg n\rceil$ is Nat.clog 2 n. All quantities are real.

Conventions and deviations, each disclosed in the item statements:

The distance satisfies $d(i,i)=0$ , a normalization not in the paper; a loop never enters any length.
Ratios are multiplied out ( $\mathrm{INSERT}\le c\cdot\mathrm{OPTIMAL}$ ), so the paper's exclusion of the identically zero distance (1.1) is not needed.
Condition a) of Lemma 1 is required for distinct nodes only. The page says "for all nodes $p$ and $q$ ", which for $p=q$ would force every $l_p\le 0$ and make the lemma inapplicable in the proof of Theorem 3; the proof uses the condition only on edges of a tour.
(2.2) is stated for every subset of the nodes and every tour, which is what the shortcut argument shows; the paper applies it to one specific subset and an optimal tour.
(2.1) uses 0-based node labels, so its range $k+1,\dots,\min(2k,n)$ becomes $k,\dots,\min(2k,n)-1$ .

The goal quantifies over every run: any choice of the inserted nodes $a_i$ and any minimizing insertion position. Adding a selection rule (nearest, cheapest) or fixing a tie-breaking would state a weaker, different theorem; restricting to instances with OPTIMAL $=0$ or to a fixed small $n$ would trivialize it.

Reusable beyond this mission: the subtour and insertion library (closed length of a list, TOUR, COST, insertion runs) and Lemma 1, which also yields Theorem 1. Contributions welcome: proofs of the milestones, general lemmas about the closed length of List.insertIdx and of filtered lists, and a proof of Theorem 1 from this mission's Lemma 1.

Selected references

D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
V. Bafna, B. Kalyanasundaram, K. Pruhs, Not all insertion methods yield constant approximate tours in the Euclidean plane, Theoretical Computer Science 125(2):345–353, 1994.

10 thms2 active usersReviewed

Completed

Dynamic Programming Theoretical Computer Science·Captain: mikedeng1

A Faster Algorithm Computing String Edit Distances 1: for a finite alphabet and discrete costs, the block algorithm (Algorithms Y and Z) computes the edit distance from a finite tableResearch Paper

Motivation

The edit distance between two strings is the least total cost of a sequence of single-character insertions, deletions and replacements turning one string into the other. It is the basic similarity measure of spelling correction, file comparison and biological sequence alignment. Wagner and Fischer (JACM 1974) showed that it can be computed by filling a $(|A|+1) \times (|B|+1)$ matrix in $O(|A|\cdot|B|)$ time. Masek and Paterson (J. Comput. System Sci. 1980) gave the first asymptotic improvement: for a finite alphabet and edit costs that are integral multiples of a common constant, the edit distance can be computed in time $O(|A|\cdot|B|/\max(1, |B|/\log|A|))$ , that is $O(n^2/\log n)$ for two strings of length $n$ .

Timeline:

1970: Arlazarov, Dinic, Kronrod and Faradzev compute transitive closures by precomputing all small submatrices, the "four Russians" technique that Masek and Paterson adapt.
1974: Wagner and Fischer give the matrix-filling algorithm, with the first row and column of the matrix and the three-term recurrence for its interior (Theorems 1 and 2 of Masek–Paterson, cited from them).
1980: Masek and Paterson apply the four-Russians technique to the edit matrix, working with differences of adjacent entries, and show that the restriction to discrete costs cannot simply be dropped (their Section 4, the subject of the second mission of this series).
2015: Backurs and Indyk (arXiv:1412.0348) show that a strongly subquadratic algorithm would refute the Strong Exponential Time Hypothesis, so a logarithmic-factor speed-up of this kind is close to the best one can expect.

Setting

Let $\Sigma$ be an alphabet and $\lambda$ the null string. For a string $A$ , $|A|$ is its length, $A_n$ its $n$ -th character, $A^{i,j} = A_i \cdots A_j$ and $A^i = A^{1,i}$ , with $A^0 = \lambda$ .

An edit operation $a \to b$ is a pair $(a, b) \ne (\lambda, \lambda)$ of strings of length at most one: a replacement ( $a, b \ne \lambda$ , possibly $a = b$ ), a deletion ( $b = \lambda$ ) or an insertion ( $a = \lambda$ ). $B$ results from $A$ via $a \to b$ if $A = \sigma a \tau$ and $B = \sigma b \tau$ . An edit sequence $S = s_1, \dots, s_m$ takes $A$ to $B$ if there are strings $A = C_0, C_1, \dots, C_m = B$ with $C_{i-1} \to C_i$ via $s_i$ . A cost function $\gamma$ assigns a nonnegative real to every edit operation, $\gamma(S) = \sum_i \gamma(s_i)$ , and

\delta(\gamma, A, B) = \min\{\gamma(S) \mid S \text{ takes } A \text{ to } B\}.

Write $R_{a,b} = \gamma(a \to b)$ , $D_a = \gamma(a \to \lambda)$ , $I_a = \gamma(\lambda \to a)$ , and $\delta_{i,j} = \delta(\gamma, A^i, B^j)$ for the entries of the edit matrix. The cost function is normalized if $\gamma(a \to b) = \delta(\gamma, a, b)$ for every edit operation.

A step is a difference of two adjacent matrix entries, $\delta_{i,j} - \delta_{i-1,j}$ (vertical) or $\delta_{i,j} - \delta_{i,j-1}$ (horizontal). The cost set is $\Omega = \{D_a\} \cup \{I_a\} \cup \{R_{a,b}\}$ , and $\Omega$ is discrete if every element of $\Omega$ is an integral multiple of one constant $r > 0$ .

Algorithm Y takes two strings $C, D$ of length $m$ and two step vectors $R, S$ of length $m$ (the left column and top row of an $m \times m$ block) and fills a matrix $T$ of vertical steps and $U$ of horizontal steps by the recurrence of Corollary 1, returning the right column $R'$ and bottom row $S'$ . Algorithm Z cuts $A$ and $B$ into blocks of length $m$ , starts from the deletion costs of $A$ and the insertion costs of $B$ , obtains the steps of each block from Algorithm Y's output ("Fetch"), and returns the sum of the steps along the left column and the bottom row.

Formalization targets

Goal: correctness from a string-independent finite table

For a finite alphabet and a nonnegative, normalized cost function with discrete $\Omega$ , there is a finite set $T \subset \mathbb{R}$ such that for all $m \ge 1$ and all $A, B$ with $m \mid |A|$ , $m \mid |B|$ ,

\mathrm{cost}_{Z}(\gamma, m, A, B) = \delta(\gamma, A, B), \qquad \text{every entry of every } P(i,j), Q(i,j) \text{ lies in } T.

$T$ is fixed before $m$ , $A$ and $B$ . The second clause says that Algorithm Y's table need only range over $\Sigma^m \times \Sigma^m \times T^m \times T^m$ , whose size does not depend on the strings; this is what the running-time bound rests on.

Milestones

Theorem 1 [Wagner–Fischer]: $\delta_{0,0} = 0$ , $\delta_{i,0} = \sum_{r \le i} D_{A_r}$ , $\delta_{0,j} = \sum_{r \le j} I_{B_r}$ .
Theorem 2 [Wagner–Fischer]: $\delta_{i,j} = \min(\delta_{i-1,j-1} + R_{A_i,B_j}, \delta_{i-1,j} + D_{A_i}, \delta_{i,j-1} + I_{B_j})$ .
Corollary 1: the same recurrence written in terms of steps.
Algorithm Y returns the final step vectors of every $m \times m$ submatrix from its initial step vectors and strings (Section 2.1).
Lemma 3: $-I \le \delta_{i,j} - \delta_{i-1,j} \le D$ and $-D \le \delta_{i,j} - \delta_{i,j-1} \le I$ .
Lemma 4: if $\Omega$ is discrete, the set of possible steps is finite.

Significance

The result was the first algorithm for edit distance faster than quadratic, and its method (tabulate every possible small block of a dynamic program, described by differences rather than values) became the standard way of shaving a logarithmic factor from string dynamic programs. The discreteness hypothesis is where the method's power ends: Section 4 of the paper shows that with costs $1$ and $\pi$ the number of distinct steps grows without bound.

The results are proved in the paper; none of them is formalized. The Mathlib revision of this mission contains no edit-distance module. A formalization produces a definition of edit distance as a minimum over edit sequences, a machine-checked proof of the Wagner–Fischer recurrence for that definition under the normalization the paper assumes, and a checked proof that the four-Russians block assembly is correct and draws on a finite, string-independent table.

Difficulty

The hardest step is Theorem 2 for $\delta$ defined as a minimum over arbitrary edit sequences. An edit sequence may insert a character and later replace or delete it, or edit the same position many times, so the edit matrix's three-term recurrence does not follow by looking at the last operation. The upper bound is direct; the lower bound needs a normal form for edit sequences, and it fails without normalization: with $R_{a,c} = 10$ , $R_{a,b} = R_{b,c} = 1$ and all insertions and deletions costing $100$ , $\delta(\gamma, a, c) = 2$ while the recurrence gives $10$ .

The goal is then an induction over blocks that must keep track of which matrix entries each block's input and output vectors represent, with block boundaries at multiples of $m$ and the first row and column handled by Theorem 1.

Formalization scope

Strings are List α; characters are 1-based in all statements, as in the paper ( $A_i$ is A[i-1]). An edit operation is a structure with two Option α fields, not both none. $\delta$ is sInf of the set of costs of edit sequences taking $A$ to $B$ (nonempty, and bounded below for $\gamma \ge 0$ ). Costs are real-valued with an explicit nonnegativity hypothesis. Normalization is a hypothesis on Theorems 1, 2, Corollary 1, the Algorithm Y lemma and the goal; Lemmas 3 and 4 hold without it. The finite alphabet is [Fintype α] on Lemma 4 and the goal; Lemma 3 is stated for arbitrary upper bounds $I \ge I_a$ , $D \ge D_a$ , which implies the paper's version with maxima. The paper's standing assumption $|A| \ge |B|$ serves only the running time and is dropped. Step vectors are functions on Fin m.

Pinned statements. The paper states a running time $O(|A|\cdot|B|/\max(1,|B|/\log|A|))$ on a logarithmic-cost RAM; the goal formalizes the two facts that bound rests on, correctness and a finite table domain fixed before the strings. The RAM model, operation counts, the choice $m = \lfloor \log_k |A| \rfloor$ , the padding reduction for $m \nmid |A|$ , and the edit-path recovery of Section 2.3 are not formalized. Algorithm Y's result is a function (blockY); the Store/Fetch memory is not modelled.

The edit distance must stay the minimum over edit sequences: defining it by the Wagner–Fischer recurrence would make Theorems 1 and 2 true by definition and reduce the goal to a comparison of two recurrences. Algorithms Y and Z are transcribed from the pseudo-code and never refer to $\delta$ .

Useful beyond this mission: the §1.1 definitions and Theorems 1–2 are a general edit-distance library (the second mission of this series defines the same objects). Contributions of lemmas about normal forms of edit sequences, the triangle inequality for $\delta$ , and attainment of the minimum are welcome.

Selected references

W. J. Masek, M. S. Paterson, A Faster Algorithm Computing String Edit Distances, J. Comput. System Sci. 20 (1980), 18–31. https://doi.org/10.1016/0022-0000(80)90002-1
R. A. Wagner, M. J. Fischer, The String-to-String Correction Problem, J. ACM 21 (1974), 168–173. https://doi.org/10.1145/321796.321811
V. L. Arlazarov, E. A. Dinic, M. A. Kronrod, I. A. Faradzev, On Economical Construction of the Transitive Closure of an Oriented Graph, Soviet Math. Dokl. 11 (1970), 1209–1210.
A. Backurs, P. Indyk, Edit Distance Cannot Be Computed in Strongly Subquadratic Time (unless SETH is false), STOC 2015. https://arxiv.org/abs/1412.0348

10 thms2 active usersReviewed

Completed

Graph Theory Linear Optimization Operations Research·Captain: mikedeng1

On Certain Polytopes Associated with Graphs IV: Adjacent Stable Sets on the Stable Set PolytopeResearch Paper

Motivation

Many combinatorial optimization problems are linear programs over a polytope whose vertices are the zero–one incidence vectors of the feasible objects: matchings, stable sets, spanning trees. The edges of such a polytope (pairs of vertices joined by a one-dimensional face) govern the behaviour of the simplex method and of local-search procedures, which move from vertex to vertex along edges: a pivot of the simplex method on a nondegenerate basis replaces a vertex by one of its neighbours.

In December 1971 M. L. Balinski asked when two matchings $M_1, M_2$ of a graph are neighbours on the matching polyhedron determined by Edmonds (Edmonds 1965). V. Chvátal answered a more general question in §6 of On certain polytopes associated with graphs (Chvátal 1975): he characterized the neighbours on the stable set polytope of an arbitrary graph. Since matchings of $G$ are the stable sets of the line graph $L(G)$ , Balinski's question is the special case of line graphs (Corollary 6.3 of the paper).

Setting

Let $G=(V,E)$ be a finite undirected loopless graph. A stable set is a set of vertices no two of which are adjacent. $S(G)$ denotes the set of all zero–one vectors $x=(x_u : u\in V)$ such that $\{u : x_u=1\}$ is stable, and the stable set polytope is

P(G)=\operatorname{conv} S(G)\subseteq \mathbb R^V .

For $y\in S(G)$ the corresponding stable set is $Y=\{u : y_u=1\}$ .

For an integer-valued vector $c=(c_u : u\in V)$ write $cx=\sum_{u\in V}c_ux_u$ . Two vectors $y, z$ are neighbours in $P(G)$ if there is an integer-valued $c$ such that $y$ and $z$ are the only two vectors which maximize $cx$ over $S(G)$ ; in particular $y\neq z$ . This is the definition the paper states at the start of the proof of Theorem 6.2.

A bicoloration of a graph $T$ is a partition $V=B\cup R$ , $B\cap R=\emptyset$ , such that every edge joins $B$ to $R$ . Every tree has one.

In the Lean development these objects are stableVectors G ( $S(G)$ ), stablePolytope G ( $P(G)$ ), onesSet y ( $Y$ ), AreNeighbors G y z and IsBicoloration T B R, all in the namespace ChvatalPolytopes.Neighbors.

Formalization targets

Goal: Theorem 6.2 (p. 149)

For $y,z\in S(G)$ with corresponding stable sets $Y,Z$ ,

y \text{ and } z \text{ are neighbours in } P(G) \iff \text{the subgraph } H \text{ of } G \text{ induced by } (Y-Z)\cup(Z-Y) \text{ is connected.}

Milestone: Lemma 6.1 (p. 149)

For a tree $T=(V,E)$ with a bicoloration $V=B\cup R$ there are nonnegative integers $c_u$ ( $u\in V$ ) and $m$ with

\sum_{u\in V}c_ux_u\le m\quad\text{for all } x\in S(T),

with equality exactly when $x$ is the incidence vector of $B$ or of $R$ .

Milestone: the certificate of the "if" part (p. 149, proof of Theorem 6.2, (i))

If $H$ is connected with spanning tree $T$ , and $c_u$ ( $u\in (Y-Z)\cup(Z-Y)$ ), $m$ are as in Lemma 6.1 for $T$ , extend $c$ by $c_u=1$ on $Y\cap Z$ and $c_u=-1$ outside $Y\cup Z$ . Then

\sum_{u\in V}c_ux_u\le m+|Y\cap Z|\quad\text{for all } x\in S(G),

with equality if and only if $x=y$ or $x=z$ .

Significance

Theorem 6.2 describes the 1-skeleton of the stable set polytope of every graph by a condition that can be checked in linear time, although optimizing over $P(G)$ is NP-hard in general and no complete linear description of $P(G)$ is known for general graphs. Through line graphs it gives the adjacency criterion for the matching polytope (two matchings are neighbours if and only if their symmetric difference is a single path or cycle), which settled Balinski's question. Characterizations of this type underlie the analysis of simplex-type and pivoting algorithms on combinatorial polytopes and the study of their diameters.

The result has been proved since 1975. The mission asks for a machine-checked proof of the theorem as stated in the paper; no formal proof of Theorem 6.2 or of the matching-polytope corollary is known to exist on Prove2Me or in Mathlib. The two milestones isolate the constructive half (Lemma 6.1 and the weighting built from it), which is reusable for any statement that needs an explicit objective singling out two stable sets.

Difficulty

The "only if" direction and the equality analysis are elementary; the substance lies in the "if" direction. An objective that makes both $y$ and $z$ optimal is easy to write down, for example $c=y+z$ ; the difficulty is to make them the only optimal vectors. Any stable set that agrees with $Y$ on some connected pieces of $H$ and with $Z$ on others ties with $y$ and $z$ under naive weightings, so the weights on $(Y-Z)\cup(Z-Y)$ must be chosen so that every mixed choice loses strictly. The integrality requirement on $c$ and the need to control all of $S(G)$ , not only the stable sets contained in $Y\cup Z$ , rule out a direct perturbation argument.

Formalization scope

Graphs. $V$ is a finite type with decidable equality and $G$ is a SimpleGraph V; loops and multiple edges are excluded, as in the paper.
$S(G)$ and $P(G)$ . $S(G)$ is the set of incidence vectors in V → ℝ of stable finsets; $P(G)$ is convexHull ℝ (S G).
Neighbours. Defined exactly as on p. 149: $y\ne z$ and, for some $c : V\to\mathbb Z$ , the set of maximizers of $cx$ over $S(G)$ equals $\{y,z\}$ . The face-lattice notion of an edge of $P(G)$ is not used; its equivalence with this definition is not part of the paper.
Induced subgraph and connectedness. $H$ is G.induce of the set $(Y\setminus Z)\cup(Z\setminus Y)$ , and "connected" is Mathlib's SimpleGraph.Connected, which requires at least one vertex. For $y=z$ both sides of the goal are therefore false.
Trees. SimpleGraph.IsTree, which includes connectedness; a spanning tree of $H$ is a graph $T$ on the vertex set of $H$ with $T\le H$ and T.IsTree. In Lemma 6.1 the integers $c_u$ and $m$ are natural numbers.

A trivializing formalization — defining neighbours through the symmetric-difference condition or through Lemma 6.1's certificate, or omitting $y\neq z$ from the definition — is excluded: neighbours are defined only through unique maximizers of integer objectives over $S(G)$ .

A complete development needs only finite graphs, induced subgraphs, spanning trees of connected graphs (available in Mathlib) and finite sums. Contributions welcome beyond the milestones: the equivalence of this notion of neighbours with the one-dimensional faces of $P(G)$ , and Corollary 6.3 for the matching polytope via line graphs.

Selected references

V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory, Series B 18 (1975), 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
M. W. Padberg, On the facial structure of set packing polyhedra, Mathematical Programming 5 (1973), 199–215. https://doi.org/10.1007/BF01580121

6 thms2 active usersReviewed

Missions

An Analysis of Several Heuristics for the Traveling Salesman Problem III: Nearest and Cheapest Insertion Are Within a Factor of TwoResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary to Theorem 4, eq. (4.12)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Limits of Permutation Sequences II: Convergence Is Equivalent to Being Cauchy in the Rectangular DistanceResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.8, under ∣σn∣→∞|\sigma_n|\to\infty∣σn​∣→∞

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Faster Algorithm Computing String Edit Distances 2: Discrete Edit Costs Are NecessaryResearch Paper

Motivation

Setting

Formalization targets

Goal (Theorem 5, as its proof establishes it)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Maximizing Non-Monotone Submodular Functions III: Guarantees of Deterministic Local SearchResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.4 (p. 1141)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

On Certain Polytopes Associated with Graphs III: The Stable Set Polytope after Substituting a Graph for a VertexResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Local Search Heuristics for k-Median and Facility Location Problems II: p-Swap Local Search for k-Median Has Locality Gap 3 + 2/pResearch Paper

Motivation

Setting

Formalization targets

Goal: locality gap at most 3+2/p3 + 2/p3+2/p

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities I: The Growth Function DichotomyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 267)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Santa Claus Schedules Jobs on Unrelated Machines: The Configuration LP Has Integrality Gap at Most 33/17Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1

Milestones

Significance

Difficulty

Goal: Theorem 1.8, under $|\sigma_n|\to\infty$

Goal: locality gap at most $3 + 2/p$