Combinatorics

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

1. The index is at most $2^r$ (p. 265): $\Delta^S(x_1, \dots, x_r) \le 2^r$.
2. 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$.
3. The polynomial bound (p. 266): $\Phi(n, r) \le r^n + 1$ for $n > 0$, $r \ge 0$.
4. 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$.
5. 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

Motivation

This mission is the sixteenth and last of the Disjunctive Programming series, and its goal theorem is the book's own closing result. The chapter's arc closes a loop opened at the very start of the book: Theorem 2.1 (02a-convex-hull) gave the convex hull of a union of polyhedra in the same space via lifting; this chapter's Theorem 13.13 (not drafted in this mission — see below) gives the dominant of a union of polytopes in different spaces, and the chapter's final result specializes that machinery to the case where the two polytopes are polymatroids — obtaining a fully explicit, closed-form convex hull in the original variable space, with no lifting at all. Polymatroids are among the most heavily studied objects in combinatorial optimization, from Edmonds's foundational greedy-algorithm characterization onward (J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87), and a disjunction of two polymatroids — "satisfy one covering system or the other" — arises naturally whenever two competing combinatorial resource constraints interact.

Setting

Fix a ground set $N = \{1,\dots,n\}$. A set function $r : 2^N \to \mathbb{R}$ is a polymatroid rank function if $r(\emptyset)=0$, $r$ is nondecreasing, and $r$ is submodular: $r(A)+r(B) \ge r(A\cup B)+r(A\cap B)$ for all $A,B\subseteq N$. (A related but distinct condition, used earlier in the chapter for "Application 1," additionally requires $r(A)\le|A|$ on every proper subset — matroid rank functions satisfy both.) The associated polymatroid is

$$P(r) := \Big\{x \in \mathbb{R}^n_+ : \textstyle\sum_{j\in A} x_j \le r(A) \text{ for all } A \subseteq N\Big\}.$$

For two ground sets $M,N$ and set functions $r_1,r_2$, the disjoint-space union is $Z(r_1,r_2) := \{(x,y)\in[0,1]^m\times[0,1]^n : x\in P(r_1) \text{ or } y\in P(r_2)\}$. For polymatroid rank functions $r_1,r_2$ on the same ground set $N$, $\Pi := \{\pi \ge 0 : \pi x \le 1 \text{ for } x \in P(r_1)\cup P(r_2)\}$ and $U := \{u \ge 0 : \sum_A u_A r_i(A) \le 1,\ i=1,2\}$ (indexed by all subsets $A \subseteq N$) are the auxiliary polytopes the final proof reduces to.

Formalization targets

Proposition 13.16. For set functions $r_1,r_2$ satisfying the Application-1 conditions,

$$\mathrm{conv}(Z(r_1,r_2)) = \Big\{(x,y) : \frac{|A|-x(A)}{|A|-r_1(A)} + \frac{|B|-y(B)}{|B|-r_2(B)} \ge 1 \ \forall A\subseteq M, B\subseteq N \text{ with } r_1(A)<|A|,\ r_2(B)<|B|\Big\}.$$

Corollary 13.21. The same-space specialization: $\mathrm{conv}(P(r_1)\cup P(r_2)) = \{w\in[0,1]^n : w=x+y, \text{[the same displayed inequality, } A,B\subseteq N\text{]}\}$.

Proposition 13.22. $\Pi$ is exactly the projection, onto $\pi$, of $\{\pi_j \le \sum_{A\ni j} u_A\ (j\in N),\ \sum_A u_A r_i(A)\le1\ (i=1,2),\ \pi,u\ge0\}$.

Proposition 13.23. Every extreme point of $\Pi$ arises from an extreme point of $U$ via $\pi_j = \sum_{A\ni j} u_A$.

Theorem 13.24 (goal, the book's closing theorem). For polymatroid rank functions $r_1,r_2$,

$$\mathrm{conv}(P(r_1)\cup P(r_2)) = \Big\{x\ge0 : x(A)\le\max\{r_1(A),r_2(A)\}\ \forall A\subseteq N;\ \ \frac{r_2(B)-r_1(B)}{r_1(A)r_2(B)-r_1(B)r_2(A)}x(A) + \frac{r_1(A)-r_2(A)}{r_1(A)r_2(B)-r_1(B)r_2(A)}x(B) \le 1$$ $$\ \forall A,B\subseteq N \text{ with } (r_1(A)-r_2(A))(r_1(B)-r_2(B))<0\Big\}.$$

The targets trace the book's own tower: the disjoint-space specialization (13.16) and its same-space corollary (13.21) establish the lifted description; Propositions 13.22-13.23 build the blocker/projection machinery; Theorem 13.24 collapses everything into the unlifted, original-variable-space closed form that is the book's final word.

Significance

Theorem 13.24 is a genuinely rare achievement in polyhedral combinatorics: a complete, explicit, non-lifted facet description for the union of two polymatroids — objects whose individual facet structure is already exponential and only tractable via the greedy algorithm and submodular minimization. That the union of two such objects still admits a closed form, stated purely in terms of the two rank functions evaluated at pairs of subsets, is the payoff the entire chapter's machinery (dominants, blockers, upper monotonicity, disjoint-space unions) was built toward. The result strictly generalizes an earlier theorem restricted to matroid polyhedra, obtained there by different techniques specific to matroids; this proof works because polymatroid optimization (Edmonds's greedy algorithm) survives in the more general submodular, non-0/1-truncated setting.

Both directions are proved in the source (Balas's own chapter, building on Edmonds's polymatroid theory and the disjoint-union machinery developed earlier in the same chapter) but have no counterpart on this platform: nothing existing treats polymatroids, polymatroid rank functions, or a closed-form union of two polymatroids. Mathlib's Combinatorics/Matroid/* covers matroids and their rank functions but not this strictly more general polymatroid object (an integer- or real-valued submodular monotone set function, not a matroid's 0/1-truncated rank). This mission produces the first Lean statements of all five targets.

Difficulty

The obvious shortcut for Theorem 13.24 is to state only the "single active subset" family of inequalities ($x(A)\le\max\{r_1(A),r_2(A)\}$) and treat the two-subset family as a minor addendum — but the two-subset inequalities are not optional refinements, they are half of the facet system, arising from the genuinely two-dimensional case of the underlying linear program (a basic feasible solution of $U$ with two nonzero components). Dropping them, or stating them only for a special case of $A,B$, would produce a strictly weaker (and generally invalid, since it would omit real facets) description.

The condition $(r_1(A)-r_2(A))(r_1(B)-r_2(B))<0$ is easy to state but not to motivate without the underlying linear algebra: it is exactly the condition under which the $2\times2$ system $u_Ar_1(A)+u_Br_1(B)=1$, $u_Ar_2(A)+u_Br_2(B)=1$ has a solution with both $u_A,u_B>0$ — a fact the book verifies by direct computation (Cramer's rule) rather than a structural argument, which is why this mission states the condition exactly as derived rather than paraphrasing it into a more "intuitive" but unfaithful form.

Formalization scope

The ambient space is Fin n → ℝ throughout (or Fin m → ℝ / Fin n → ℝ separately for Proposition 13.16's disjoint spaces), matching the series default; subsets $A,B\subseteq N$ are Finset (Fin n), and the auxiliary variable $u$ of Propositions 13.22-13.23 is indexed by Finset (Fin n) itself (a genuine Fintype for fixed n), matching "$u_A$ for all $A\subseteq N$" directly. IsApp1SetFunction and IsPolymatroidRankFunction are kept as two distinct predicates — the goal theorem uses the latter, Proposition 13.16/Corollary 13.21 the former — matching BRIEF.md's explicit warning to locate and preserve the book's own exact numbered conditions rather than infer a single merged notion. A trivializing formalization to rule out explicitly: stating Theorem 13.24 with only the single-subset inequality family, which would omit the two-subset facets that are half of the theorem's actual content.

This mission depends on no other chunk's Lean definitions; it restates 13a-dominants's dominant/blocker/upper-monotone vocabulary only informally (the underlying object, not any specific Lean declaration), per the series convention, since no chunk in this series can import another's draft module. Theorem 13.13 (the general dominant of a disjoint-space union) and Theorem 13.18 (the general same-space reduction) — the two results whose specializations Proposition 13.16 and Corollary 13.21 respectively are — were not drafted this pass; see HARD.md. As the last mission of the whole book, this chunk's items.yaml closes the series begun in 01-intro-duality: sixteen missions, one book, spanning from the founding disjunctive Farkas lemma to this closed-form union of two polymatroids.

Selected references

• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87 (reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, Springer, 2003, 11–26, https://doi.org/10.1007/3-540-36478-1_2).
• E. Balas, A. Bockmayr, N. Pisaruk, and L. Wolsey, On unions and dominants of polytopes, Mathematical Programming A 99 (2004), 223–239. https://doi.org/10.1007/s10107-003-0432-4
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 13, §13.2.1–13.8 (the book's final chapter). https://doi.org/10.1007/978-3-030-00148-3

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:

1. Step 1. Compute $|B|$ and obtain $w$, the exponent for which $2^{2w}$ is the highest power of 2 dividing $|B|$.
2. Step 2. Compute $\operatorname{adj}(B)$.
3. 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

1. 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$.
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$.
3. 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.
4. 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|$.
5. Lemma 3: under the same hypothesis, $(v_i, v_j) \in M$ iff $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.
6. 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

Motivation

Many polytopes that arise from combinatorial optimization problems have no small facet description in their natural variable space, yet become describable by a compact linear system once lifted to a higher-dimensional space of auxiliary variables and projected back down — Chapter 2's own extended formulation of the convex hull of a disjunctive set is one instance of this phenomenon. This chapter turns the idea around: rather than using projection to build a compact formulation, it uses projection to prove integrality of a formulation that is already compact but whose integrality is not obvious from any standard sufficient condition (total unimodularity, balancedness, etc.). The technique is illustrated on three closely related combinatorial polytopes built from perfectly matchable, assignable, and path-decomposable vertex subsets of a graph or digraph — each proved integral by lifting to an edge- or arc-variable space where total unimodularity is easy to check, then projecting.

Setting

For a finite vertex set $V$, the incidence vector of $W \subseteq V$ is $1$ on $W$, $0$ elsewhere, and $x(S) := \sum_{i \in S} x_i$. A graph $G(W)$ has a perfect matching if there is a fixed-point-free involution on $W$ respecting adjacency. The PMS (Perfectly Matchable Subgraph) polytope of $G$ is $\mathrm{conv}(X)$ where $X$ is the set of incidence vectors of such $W$; $N(S) := \{j \notin S : (i,j) \in E \text{ for some } i \in S\}$.

For a digraph $(V,A)$: $G(W)$ is assignable if it admits a cycle decomposition (a permutation of $W$ respecting arcs), giving the Assignable Subgraph Polytope. For an acyclic digraph with distinguished nodes $s,t$: $G(W \cup \{s,t\})$ admits an $s$-$t$ path decomposition if a collection of interior-node-disjoint $s$-$t$ paths covers it, giving the $s$-$t$ Path Decomposable Subgraph Polytope over $W \subseteq V \setminus \{s,t\}$. $\Gamma(S)$ and $\Gamma^*(S)$ are the corresponding out-neighborhood operators. For an arbitrary graph, $c(S)$ counts the connected components of the induced subgraph $G(S)$.

Formalization targets

Theorem 5.1 (goal) — the PMS polytope of a bipartite graph

$$0 \le x_i \le 1\ (i \in V), \qquad x(V_1) - x(V_2) = 0, \qquad x(S) - x(N(S)) \le 0\ \ (S \subseteq V_1).$$

Theorem 5.2 — the Assignable Subgraph Polytope

$$0 \le x_i \le 1\ (i \in V), \qquad x(S \setminus \Gamma(S)) - x(\Gamma(S) \setminus S) \le 0 \quad (S \subseteq V).$$

Theorem 5.3 — the $s$-$t$ Path Decomposable Subgraph Polytope

$$0 \le x_i \le 1\ (i \in V), \qquad x(S \setminus \Gamma^*(S)) - x(\Gamma^*(S) \setminus S) \le 0 \quad (S \subseteq V \setminus \{s,t\}).$$

Theorem 5.4 — the PMS polytope of an arbitrary graph

$$0 \le x_i \le 1\ (i \in V), \qquad x(S) - x(N(S)) \le |S| - c(S)$$

for every $S$ all of whose components are single nodes or nonbipartite with odd order — the weakest faithful statement, since dropping the side condition would assert the inequality for subsets it does not hold for.

Significance

The results themselves. Each theorem gives an explicit, checkable linear system defining a polytope that arises naturally from a combinatorial covering/decomposition property, turning "does $G(W)$ have property $X$" into a linear-programming feasibility question. Theorem 5.1 is the one the book proves in full and the template for the other three: bipartite matching, digraph assignment, and acyclic-digraph path decomposition are structurally parallel problems (all reduce to checking a König–Hall-type combinatorial condition), and the same lift-and-project technique handles all three uniformly. Theorem 5.4 extends the idea to arbitrary (non-bipartite) graphs at the cost of a sharper right-hand side and a component-based side condition, connecting to Edmonds' classical matching-polytope theory while remaining a genuinely different object (a polytope of coverable vertex sets, not of matchings themselves).

Formalizing it. No object in this mission — the PMS, Assignable, or Path Decomposable Subgraph polytopes, or their defining neighbor operators — exists on the platform prior to this mission. The closest platform result, MetricTSP.pm_polytope_decomposition (Edmonds' perfect matching polytope theorem, in edge-variable space over a fixed vertex set requiring every vertex matched), is a genuinely different object from Theorem 5.4's PMS polytope (vertex-variable space, vertices may be left unmatched by design) and is not reused as a kind: reference item; it is noted here as related, not equivalent.

Difficulty

The natural first attempt tries to verify each polytope's integrality directly, by checking a known sufficient condition (total unimodularity, balancedness) on the displayed vertex-space system itself. This fails: the book states explicitly that (5.5)'s coefficient matrix is not totally unimodular, which is exactly why the lift-to-edge-variables step is necessary at all. The real content of each theorem is the two-part argument: (1) the lifted system in edge/arc variables is totally unimodular (checkable directly), so its polyhedron is integral; and (2) the vertex- space system is exactly the projection of the lifted one — a nontrivial fact requiring Chapter 2's projection machinery, not merely an unfolding of definitions. Theorem 5.4's extra difficulty, flagged explicitly in the text, is that its projection cone is not pointed, so the proof must work with a finite generating set rather than extreme rays, and it suffices to find a subset of generators producing every facet rather than a complete generating set — a genuinely harder argument the book itself outsources to a citation.

Formalization scope

Undirected graphs use Mathlib's SimpleGraph; digraphs use a bare relation A : V → V → Prop (not required symmetric or irreflexive, matching the book's unrestricted notion). Bipartition is recorded via part : V → Bool (decidable by construction) rather than two Set V halves, keeping the sums x(V_1), x(V_2) computable over Finsets throughout. IsAssignable uses Equiv.Perm on the vertex-set subtype, since a cycle decomposition is exactly a permutation. IsComponentOf and IsBipartiteOn (Theorem 5.4) are built directly from reachability and 2-colorability rather than Mathlib's induced-subgraph/ConnectedComponent API, matching the "maximal connected subset" reading of "component" the book's own prose intends.

IsPathDecomposable (Theorem 5.3) encodes "admits an $s$-$t$ path decomposition" via a degree-constrained arc set (every interior node has exactly one incoming and one outgoing chosen arc, none entering $s$ or leaving $t$, at least one leaving $s$) rather than an explicit list of vertex-disjoint paths — provably equivalent by the standard fact that an acyclic arc set with this degree pattern always decomposes into such a path family, and considerably lighter to state and reason about than constructing Path objects directly.

A trivializing formalization is ruled out explicitly: every theorem keeps the fractional box constraint $0 \le x_i \le 1$ rather than the integral $x_i \in \{0,1\}$ (per BRIEF.md's own warning, dropping the relaxation collapses the claim to a restatement of the combinatorial definition), and Theorem 5.1 is stated only for bipartite graphs — never generalized to subsume Theorem 5.4's genuinely different inequality system and side condition.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 5, §5.2.
• M. O. Ball, U. Derigs, An analysis of alternate strategies for implementing matching algorithms, Networks 13 (1983) (cited in the text as [13], the origin of Theorems 5.2 and 5.3).
• W. R. Pulleyblank, J. Edmonds, Facets of 1-matching polyhedra, in Hypergraph Seminar, Springer Lecture Notes in Mathematics 411 (1974) — the origin of the perfectly matchable subgraph polytope literature (cited in the text as [34], the origin of Theorem 5.1).
• L. Lovász, M. D. Plummer, Matching Theory, Elsevier, 1986 (cited in the text as [35], the origin of Theorem 5.4).

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

1. 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)$.
2. 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)$.
3. 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)$.
4. 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

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

1. 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$.
2. 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}.$$

3. 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

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)

1. 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).
2. When B1 halts, every clause left in LEFT is dead: each of its literals has had its complement made true.
3. When B1 halts on an input of $MS(k)$, $|\mathrm{SUB}| \ge k\,|\mathrm{LEFT}|$, and SUB and LEFT partition $S$.
4. 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