Operations Research

Motivation

Chapter 8 established an exact correspondence between lift-and-project cuts and simple disjunctive cuts, but its practical payoff is what this chapter develops: the cut-generating LP (CGLP)_k never needs to be formulated or solved on its own. Every pivot of (CGLP)_k can instead be mimicked directly on the much smaller simplex tableau of the original LP relaxation — replacing a large auxiliary linear program with bookkeeping on a tableau the solver already has. This chapter works out that correspondence at the level of individual pivots: which tableau pivot improves the resulting cut, and by how much, answered entirely in terms of ordinary tableau coefficients and two closed-form evaluation functions.

Setting

S:={1,…,m+p} and N:={m+p+1,…,m+p+n} index the surplus and structural variables of (LP) respectively — giving a direct correspondence between (LP)'s own variables and the surplus variables of Ãx≥b̃. For a basic solution with nonbasic set J (row set M1∪M2 from Chapter 8), Â:=Ã_J is the resulting nonsingular submatrix, and row k of the tableau reads x_k+ Σ_{j∈J}ā_{kj}s_j=ā_{k0}. Adding γ times row i to row k gives the composite row (9.10), x_k+γx_i+Σ_{j∈J}(ā_{kj}+γā_{ij})s_j=ā_{k0}+γā_{i0}, from which a new simple disjunctive cut can be read off whenever 0<ā_{k0}+γā_{i0}<1.

Formalization targets

Theorem 9.3 (goal) — the most-improving pivot column

The pivot column in row i most improving the cut from row k is indexed by l*∈J minimizing f⁺(γ_l) (if ā_{kl}ā_{il}<0) or f⁻(γ_l) (if ā_{kl}ā_{il}>0), over all l∈J with -ā_{k0}/ā_{i0}<γ_l<(1-ā_{k0})/ā_{i0}, γ_l:=-ā_{kl}/ā_{il}.

The chain of results building toward it

Lemma 9.1 (the tableau coefficients' closed form, eq. (9.4)-(9.5)) and Theorem 9.2 (the reduced costs of the CGLP columns u_i,v_i in terms of tableau coefficients, eq. (9.6)) are the two milestones the goal's own machinery is built from. Proposition 9.4, a bridge to Chapters 10-11's general split disjunctions, is included as a genuine milestone despite its payoff lying mostly outside this chapter.

Significance

The results themselves. This chapter is what makes lift-and-project cuts practical: instead of solving an (m+p+n)-row auxiliary LP from scratch for every candidate cut, a single pivot on the (LP)'s own tableau — guided by reduced costs that are themselves closed-form functions of tableau entries — identifies whether an improving cut exists and which one it is. Theorem 9.3's evaluation functions f⁺,f⁻ are exactly the tool a cutting-plane implementation would compute at every candidate pivot.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 08-cut-correspondence's (CGLP)_k apparatus locally, per the series convention and BRIEF.md's explicit instruction, and extends it with this chapter's own generalization to an arbitrary tableau row (needed since Lemma 9.1/Theorem 9.2 concern every basic variable's row, not only the disjunction row k).

Difficulty

Lemma 9.1's book proof is a four-case block-matrix verification (structural/surplus, basic/nonbasic); this mission instead states its content as the identity it is actually for — that the closed-form coefficients express every row's slack as an affine function of the nonbasic rows' slacks, for every point x — which follows tautologically from x=Â⁻¹b̂+Â⁻¹s_J's own definition once stated this way, without needing to reconstruct the block-matrix case analysis. Theorem 9.2's difficulty is that "reduced cost" is not already available as a formalized LP concept in this mission's apparatus; rather than build a generic LP reduced-cost theory, this mission follows the book's own derivation directly — explicitly constructing the pivoted-out extension of a basic solution (eq. (9.7)-(9.9)) and asserting that its objective value decomposes with r_{u_i},r_{v_i} as coefficients, which is genuine, non-circular content matching the proof's own final step ("we can then read the reduced costs... as the coefficients").

Formalization scope

This chapter makes the row/variable identification of Chapters 6-8 fully explicit (N directly indexes the structural variables), but no theorem's own displayed formula in this chunk needs that correspondence beyond what SurplusM's row-general treatment (this chunk's own generalization of 08-cut-correspondence's Surplus) already provides — see MODERATION_NOTES.md for why the S/N/B/R/P/Q block structure is proof machinery, not part of the stated content, throughout.

Theorem 9.3's range condition on γ_l, truncated in BRIEF.md's own excerpt, was completed by reading the PDF directly (confirmed identical to the range derived earlier in the same section): -ā_{k0}/ā_{i0}<γ_l<(1-ā_{k0})/ā_{i0}.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 9.
• E. Balas, M. Perregaard, A precise correspondence between lift-and-project cuts, simple disjunctive cuts, and mixed integer Gomory cuts for 0-1 programming, Mathematical Programming B 94 (2003), 221–245 (cited in the text as [33], the origin of the tableau-pivoting procedure this chapter derives Lemma 9.1 and Theorem 9.2 from).

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

Convexity is what makes optimization tractable: a linear program's feasible region is convex, and this single fact underwrites the simplex method, LP duality, and everything built on top of them. Integer and disjunctive programs have no such luck — their feasible regions are unions of polyhedra, and a union of convex sets is generally not convex. If the convex hull of such a union could always be described compactly, integer programming would reduce to linear programming: optimize the same linear objective over the hull instead of the union, and any optimal vertex of the hull is automatically integral. The obstacle has always been that the convex hull of a union of polyhedra in $\mathbb{R}^n$, described directly by its facets in $\mathbb{R}^n$, typically needs exponentially many inequalities.

Balas's Theorem 2.1, proved in the 1970s and presented here as Chapter 2 of Disjunctive Programming (Balas, Springer 2018), breaks this exponential barrier by changing where the description lives. Rather than writing down the hull's facets in $\mathbb{R}^n$, Theorem 2.1 lifts the problem to a higher-dimensional space — one auxiliary copy of $\mathbb{R}^n$ per polyhedron in the union — where the hull becomes the projection of a single, explicitly given polyhedron whose size grows only linearly with the number of polyhedra. This "extended formulation" technique, born here, became one of the central tools of modern integer programming and combinatorial optimization: representing a hard polytope as the projection of an easy one in higher dimension underlies, for instance, the polynomial-size extended formulations known for many combinatorial polytopes.

Setting

Fix a finite index set $Q$. For $h \in Q$, let $A_h$ be a real matrix and $b_h$ a vector of matching row dimension, and set $P_h := \{x \in \mathbb{R}^n : A_h x \ge b_h\}$. The union $F := \bigcup_{h \in Q} P_h$ is the disjunctive set. Write $Q^* := \{h \in Q : P_h \ne \emptyset\}$ for the feasible disjuncts.

The recession cone of a nonempty polyhedron $P_h$ is $C_h := \{y : A_h y \ge 0\}$: the set of directions along which one can travel indefinitely from any point of $P_h$ while remaining in $P_h$. For a subset $M \subseteq Q$ and sets $S_h$ ($h \in M$), the (finite) Minkowski sum $\sum_{h \in M} S_h$ is $\{x : x = \sum_{h \in M} y^h \text{ for some } y^h \in S_h\}$. The maximal indices $Q^{**} \subseteq Q^*$ are the feasible disjuncts whose polyhedron is not contained in any other feasible disjunct's polyhedron.

Given a set $S \subseteq \mathbb{R}^n \times \beta$, its projection onto $x$ is $\mathrm{Proj}_x(S) := \{x : \exists\, y \in \beta,\ (x,y) \in S\}$.

Formalization targets

Theorem 2.1 (goal) — the convex hull of a disjunctive set

$$\mathrm{cl}\,\mathrm{conv}(F) = \mathrm{Proj}_x(P), \qquad P := \Big\{(x, \{y^h\}_{h \in Q^*}, \{y^h_0\}_{h \in Q^*}) : x = \!\!\sum_{h \in Q^*}\!\! y^h,\ A_h y^h - b_h y^h_0 \ge 0,\ y^h_0 \ge 0,\ \!\!\sum_{h \in Q^*}\!\! y^h_0 = 1 \Big\}.$$

This is the weakest correct statement: it claims only that the closed convex hull equals the projection of this specific lifted polyhedron $P$, not any stronger uniqueness or minimality claim about lifted representations in general (that refinement is Theorem 2.1's own follow-up discussion, not part of the theorem itself).

Corollary 2.2 — the extreme-point correspondence

Extreme points of $\mathrm{cl}\,\mathrm{conv}(F)$ correspond bijectively to the extreme points of $P$ that place all of their mass on a single disjunct's coordinates.

Theorem 2.3 — tightness of the lifted representation

$$P_Q = P \iff C_k \subseteq \sum_{h \in Q^*} C_h \quad \forall\, k \in Q \setminus Q^*,$$

where $P_Q$ is the variant of $P$ indexed by all of $Q$ rather than only $Q^*$.

Theorem 2.4 — from the convex hull to the union itself

Under two recession-cone conditions on $Q^{**}$, restricting $P_Q$'s $y^h_0$ variables to $\{0,1\}$ makes its $x$-projection recover $F$ itself, not merely $\mathrm{cl}\,\mathrm{conv}(F)$.

Significance

The result itself. Theorem 2.1 is the founding extended-formulation result of integer programming: it shows that every union of finitely many polyhedra — hence every mixed-integer program's feasible region, once expressed in disjunctive normal form — has a lifted description of size linear in the number of disjuncts, in stark contrast to the union's own facet description, which is generally exponential. Corollary 2.2 shows this lifting is not merely an upper bound with extraneous points: its extreme points correspond exactly, one-to-one, with the extreme points of the object it represents. Theorems 2.3 and 2.4 sharpen the picture: 2.3 tells you exactly when you can avoid knowing in advance which disjuncts are nonempty, and 2.4 tells you exactly when the same family of lifted systems, restricted to integral $y^h_0$, describes the union $F$ exactly rather than only its convex hull — this is Jeroslow and Lowe's characterization of when a disjunctive set is representable as the feasible region of an integer program at all.

Formalizing it. No object in this mission — the disjunctive set $F$, its lifted polyhedron $P$, recession cones of a union's components, or the extreme-point correspondence between a polytope and its lift — exists on the platform prior to this mission or anywhere in Mathlib (substrate.md records zero LP/polyhedron modules in Mathlib as of this writing). This mission is a from-scratch formalization of the book's central construction, restating (rather than importing) the disjunctive-set vocabulary introduced by the companion IntroDuality mission, per the series' convention that a draft mission cannot import another draft mission's definitions.

Difficulty

The natural first attempt at Theorem 2.1 tries to prove the two inclusions $\mathrm{cl}\,\mathrm{conv}(F) \subseteq \mathrm{Proj}_x(P)$ and $\mathrm{Proj}_x(P) \subseteq \mathrm{cl}\,\mathrm{conv}(F)$ by a direct facet-by-facet or vertex-by-vertex argument in $\mathbb{R}^n$ — exactly the exponential-size approach the theorem exists to avoid. The book's own first proof instead works entirely with convex combinations: an arbitrary point of $\mathrm{cl}\,\mathrm{conv}(F)$ is a combination of at most $|Q^*|$ points, one from each polyhedron in the union (Carathéodory-style), which converts directly into a point of $P$ by splitting the combination's weight across the lifted coordinates — and conversely, a point of $P$ decomposes, disjunct by disjunct, into a convex combination of that disjunct's own vertices and extreme rays. Neither direction ever needs to enumerate facets of $\mathrm{cl}\,\mathrm{conv}(F)$ in $\mathbb{R}^n$. The second proof (via projection and the polar cone $W$ of the lifted system) shows the projected inequalities coincide with exactly the valid-inequality characterization of Theorem 1.2 (disjunctive Farkas), which is a different, complementary way of seeing why no facet of $\mathrm{cl}\,\mathrm{conv}(F)$ is missed.

Formalization scope

All theorems are stated over a finite index set Q : Type* with [Fintype Q], matrices Matrix (Fin (m h)) (Fin n) ℝ with m : Q → ℕ allowed to depend on h, and vectors in Fin n → ℝ. DisjunctiveSet, FeasibleIndices, MaximalIndices, RecessionCone, and MinkowskiSumOver fix the chapter's vocabulary; ProjX, LiftedPolyhedron, and IntegerRestricted fix the lifted system and its variants. cl conv F is Mathlib's closure (convexHull ℝ ·); extreme points use Mathlib's Set.extremePoints.

LiftedPolyhedron ranges its auxiliary vectors $\{y^h\}$, $\{y^h_0\}$ over all of $Q$ rather than only the index subset Qidx the book restricts to, forcing the components outside Qidx to zero. This is an equivalent, Finset/decidability-free encoding — appending zero terms changes neither the defining sums nor the constraints — documented as a convention, not a weakening, in MODERATION_NOTES.md; the same definition instantiates both the $(2.1)$ system (Qidx = Q^*) and the $(2.1)_Q$ variant (Qidx = Q) that Theorem 2.3 compares.

A trivializing formalization is ruled out explicitly: taking $|Q^*| = 1$ collapses the lifted system to $x = y^1$, $y^1_0 = 1$, a vacuous restatement of $x \in P_1$ that proves nothing about unions. Every theorem here is stated for a generic finite Q, never specialized to a fixed small size. Contributions beyond this mission's statements would need genuine polyhedral machinery (vertex/extreme-ray decomposition of a polyhedron, Carathéodory's theorem for cones) that is itself absent from Mathlib and would be welcome as a separate, reusable definitions layer.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 2, §2.1.
• E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (reprint of a 1974 MSRR, cited in the text as [6], the origin of Theorem 2.1).
• M. Conforti, M. Di Summa, Y. Faenza, On the size of extended formulations for polytopes associated with unions of polyhedra, SIAM Journal on Discrete Mathematics, cited in the text as [59] — establishes the tightness (minimum additional-variable count) of Theorem 2.1's lifted representation.
• R. G. Jeroslow, J. K. Lowe, Modelling with integer variables, Mathematical Programming Study 22 (1984), 167–184 (cited in the text as [86]; the characterization behind Theorem 2.4's significance).

Motivation

Linear programming duality is one of the load-bearing facts of optimization: every feasible linear program has a dual whose value matches the primal's, and this correspondence drives the simplex method's stopping criterion, sensitivity analysis, and most complexity results for polyhedral problems. Integer and mixed-integer programs have no such duality theorem in general — the feasible region of a mixed-integer program is not convex, and the entire apparatus of linear programming duality is built on convexity.

Disjunctive programming, introduced by Egon Balas in the early 1970s, closes part of this gap. A disjunctive set is a union of finitely many polyhedra rather than a single polyhedron — the natural convex-analytic shadow of the "either/or" logical structure that integer variables encode (an integer variable's feasible region is a finite union of half-open pieces, hence a disjunction of the linear constraints that pin it to each value). Balas's insight was that disjunctive programs — linear programs whose feasible region is such a union — admit a strong duality theorem of their own, generalizing the linear-programming case rather than replacing it. This mission formalizes that theorem (Theorem 1.5 of Balas, Disjunctive Programming, Springer 2018) together with the two results the same chapter builds around it: the founding construction of the field, the intersection cut (Theorem 1.1, circa 1970), and the disjunctive generalization of Farkas' Lemma (Theorem 1.2), which characterizes every valid inequality — hence every cutting plane — for a disjunctive set.

Setting

Fix a finite index set $Q$. For each $h \in Q$, let $A_h$ be a real $m_h \times n$ matrix and $b_h \in \mathbb{R}^{m_h}$, and set $P_h := \{x \in \mathbb{R}^n : A_h x \ge b_h\}$. The union $F := \bigcup_{h \in Q} P_h$ is a disjunctive set: any (linear) system of inequalities combined with the logical connectives "and", "or", "not" reduces, via its disjunctive normal form, to a set of exactly this shape. Because a union of convex sets need not be convex, $F$ is generally nonconvex even though each $P_h$ is a polyhedron.

A disjunctive program minimizes a linear objective over such a union:

$$(DP)\qquad z_0 = \min\Big\{ c x : x \in \textstyle\bigcup_{h \in Q} X_h \Big\}, \qquad X_h := \{x : A_h x \ge b_h,\ x \ge 0\}.$$

Its dual $(DD)$ pairs a scalar $w$ with one dual multiplier vector $u_h$ per disjunct, requiring $w \le u_h b_h$ and $u_h A_h \le c$, $u_h \ge 0$, simultaneously for every $h \in Q$, and maximizes $w$. Write $Q^* := \{h \in Q : X_h \ne \emptyset\}$ for the disjuncts whose primal system is feasible, and $Q^{**} := \{h \in Q : U_h \ne \emptyset\}$ (with $U_h := \{u_h \ge 0 : u_h A_h \le c\}$) for those whose dual system is feasible.

The theorems below also use two objects from the origin of the subject (§1.2): given a basic solution $\bar x$ of a linear program's optimal simplex tableau, with basic index set $I$ and nonbasic index set $J$, the tableau's coefficients $\bar a_{ij}$ ($i \in I$, $j \in J$) determine, for each nonbasic $j$, an extreme ray direction $r^j$ of the associated LP cone. A convex set $S$ is $P_I$-free at $\bar x$ if $\bar x$ lies in the interior of $S$ and that interior contains no point of the mixed-integer feasible set $P_I$.

Formalization targets

Theorem 1.1 — the intersection cut

$$\lambda^*_j := \max\{\lambda_j \ge 0 : \bar x + \lambda_j r^j \in S\}, \qquad \sum_{j \in J} \frac{1}{\lambda^*_j}\, x_j \ge 1.$$

The displayed inequality cuts off $\bar x$ but excludes no point of $P_I$, for any $P_I$-free convex set $S$ containing $\bar x$ in its interior.

Theorem 1.2 — Farkas' Lemma for Disjunctive Sets

$$\big(\forall x \in F,\ \alpha x \ge \alpha_0\big) \iff \big(\forall h \in Q^*,\ \exists\, u_h \ge 0,\ u_h A_h = \alpha,\ \alpha_0 \le u_h b_h\big).$$

Theorem 1.5 (goal) — duality for disjunctive programs

Under the Regularity Condition — $(Q^* \ne \emptyset$ and $Q \setminus Q^{**} \ne \emptyset) \Rightarrow Q^* \setminus Q^{**} \ne \emptyset$ — exactly one of:

1. both $(DP)$ and $(DD)$ are feasible, each attains an optimum, and $z_0 = w_0$; or
2. one of the two is infeasible, and the other is infeasible or has no finite optimum.

This is the weakest faithful statement of the theorem: it asserts only the shape of the dichotomy established by Balas, not any strengthened or specialized form of it.

Corollary 1.6 — necessity of the Regularity Condition

If the Regularity Condition fails, $(DP)$ is feasible, and $(DD)$ is infeasible, then $(DP)$ still has a finite minimum — exhibiting the duality gap that opens up once the condition is dropped.

Significance

The results themselves. Theorem 1.5 is the mission-critical fact that makes disjunctive programming a genuine extension of linear programming rather than an unrelated combinatorial device: every LP-duality-based algorithmic tool (bounding, sensitivity, complementary-slackness optimality certificates) has a disjunctive-programming counterpart because of this theorem. Theorem 1.1's intersection cut is the historical seed of an entire branch of integer-programming algorithms — lift-and-project cuts, mixed-integer Gomory cuts, and the split closure (later missions of this series) all specialize or generalize it. Theorem 1.2 is the structural fact that makes cutting-plane generation for disjunctive sets tractable at all: every valid inequality decomposes into per-disjunct Farkas certificates.

Formalizing it. None of these results, nor the union-of-polyhedra machinery they are stated over, exist on the platform prior to this mission: the platform's existing Farkas' Lemma and linear-programming strong duality theorems (SmaleNinth.farkas_lemma, SmaleNinth.lp_strong_duality) are the ordinary single-polyhedron statements, which is exactly the special case $|Q|=1$ of the theorems formalized here — genuinely different statements, not restatements. This mission is a from-scratch formalization of the disjunctive generalization, including the vocabulary (disjunctive sets, the paired primal/dual index sets $Q^*, Q^{**}$, the Regularity Condition) that the rest of the fifteen-mission Balas series builds on.

Difficulty

The obvious first attempt collapses the disjunctive dual $(DD)$ to $|Q|$ separate ordinary LP duals, one per disjunct, and tries to combine their individual strong-duality statements. This fails: $(DD)$ couples all disjuncts through the single shared scalar $w$, which must simultaneously satisfy $w \le u_h b_h$ for every $h \in Q$ at once, not disjunct-by-disjunct. The Regularity Condition exists precisely because this coupling can break down — Balas's own example (a two-term disjunctive program with an infeasible dual but a feasible, bounded primal) shows that without the condition, situation (2) of the dichotomy can fail: the primal can have a finite optimum with no matching dual optimum. Any formalization that omits the Regularity Condition, or weakens it to an informal restriction like "nondegenerate", either proves a false statement or proves nothing (a vacuous hypothesis), which Corollary 1.6 exists specifically to rule out.

Formalization scope

All three theorems are stated over a finite index set Q : Type* with [Fintype Q], real matrices Matrix (Fin (m h)) (Fin n) ℝ with row-dimension m : Q → ℕ allowed to depend on h (the book never assumes a common row count across disjuncts), and vectors in Fin n → ℝ. Poly, PolyNonneg, and DualPoly are the plain, nonnegative-orthant, and dual polyhedral systems respectively; FeasibleIndices and RegularityCondition pin $Q^*$/$Q^{**}$ and the Regularity Condition exactly as stated on p. 13. "No finite optimum" is formalized via UnboundedBelowOn / UnboundedAboveOn: nonempty (feasible) together with no finite bound on the objective, matching Balas's case (2), which explicitly distinguishes infeasibility from unboundedness.

A trivializing formalization is ruled out explicitly: fixing $|Q| = 1$ collapses Theorem 1.5 to ordinary LP duality (already on the platform) and Theorem 1.2 to ordinary Farkas' Lemma, so both theorems are stated for a generic finite Q, never specialized. Theorem 1.5's "exactly one of" dichotomy is formalized as a logical Xor of the two situations, not a weaker Or, since the book asserts mutual exclusivity, not merely that one holds.

The intersection-cut theorem (1.1) is formalized over a generic finite index type ι standing for the full set of structural and surplus variables, with I J : Finset ι the basic/nonbasic partition; a complete development would additionally need the simplex-tableau apparatus connecting ι, I, J, and abar to an actual linear program, which lies outside this mission and belongs instead to the tableau-focused later missions of the series (SimplexTableau, RayCGLP). The extremeRay and PIFree definitions introduced here are local to this mission and are restated, not imported, by later missions that need related vocabulary — per the series' convention that a draft mission cannot import another draft mission's definitions.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 1.
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Operations Research 19 (1971), 19–39. (Theorem 1.1's origin, cited in the text as [4].)
• E. Balas, Disjunctive programming, Annals of Discrete Mathematics 5 (1979), 3–51. (Cited in the text as [9], the origin of Theorem 1.5.)

Motivation

A 0–1 integer program asks for the best 0–1 vector satisfying a system of linear inequalities. Its linear relaxation is easy to optimize over, but the relaxation is usually much larger than the convex hull of the 0–1 solutions. Lift-and-project methods close this gap systematically: they lift the relaxation to a higher-dimensional space, add constraints that every 0–1 point satisfies there, and project back, obtaining a tighter relaxation that still contains every 0–1 solution.

L. Lovász and A. Schrijver introduced one of the two standard lift-and-project hierarchies in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim., 1991). Their operators $N$ and $N_+$ represent a 0–1 point $x$ by the matrix $xx^{\mathsf T}$, impose linear (and for $N_+$ semidefinite) constraints on such matrices, and project back to $\mathbb R^{n+1}$. The same paper applies the operators to the stable set polytope, where one round already produces the odd hole, odd wheel, clique and odd antihole constraints. The Lovász–Schrijver hierarchy, the Sherali–Adams hierarchy (1990) and Lasserre's semidefinite hierarchy (2001) are the three reference lift-and-project methods; their rank lower bounds are a standard tool for proving that a relaxation cannot solve a combinatorial problem in few rounds.

This mission formalizes the first structural fact about the operator $N$: iterating it $n$ times on any relaxation in $n$ variables yields exactly the 0–1 hull (Theorem 1.4 of the paper).

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$; the space $\mathbb R^n$ of the original problem is the hyperplane $x_0 = 1$, and polytopes are replaced by the convex cones they generate.

• A convex cone is a nonempty set closed under addition and nonnegative scaling. For a set $S$, $\operatorname{cone}(S)$ is the set of nonnegative combinations of finitely many vectors of $S$.
• The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \text{ for all } x \in K\}$.
• A 0–1 vector has every coordinate, $x_0$ included, equal to $0$ or $1$. The cube cone $Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$; it is the cone over the unit cube.
• For a convex cone $K$, $K^\circ$ is the cone spanned by the 0–1 vectors in $K$. For $K \subseteq Q$ this is the cone over the convex hull of the 0–1 points of the relaxation.

For convex cones $K_1, K_2 \subseteq Q$, the matrix cone $M(K_1, K_2)$ consists of the $(n+1)\times(n+1)$ real matrices $Y = (y_{ij})$ such that

1. $Y$ is symmetric;
2. $y_{ii} = y_{0i}$ for $1 \le i \le n$ (the diagonal equals the 0th column);
3. $u^{\mathsf T} Y v \ge 0$ for every $u \in K_1^*$ and $v \in K_2^*$.

$M_+(K_1, K_2)$ adds the condition that $Y$ is positive semidefinite. The projections are $N(K_1, K_2) = \{Ye_0 : Y \in M(K_1, K_2)\}$ and $N_+(K_1, K_2) = \{Ye_0 : Y \in M_+(K_1, K_2)\}$, where $e_0$ is the 0th unit vector. The cut operator is $N(K) = N(K, Q)$, and its iterates are $N^0(K) = K$, $N^t(K) = N(N^{t-1}(K))$.

Two families of hyperplanes appear in the proofs: $H_i = \{x : x_i = 0\}$ and $G_i = \{x : x_i = x_0\}$, the hyperplanes through the two opposite facets of $Q$ in direction $i$.

Formalization targets

Goal: Theorem 1.4

For every closed convex cone $K \subseteq Q$,

$$N^n(K) = K^\circ .$$

The statement is uniform in $n$ and in $K$: no polyhedrality, no bound on the number of constraints, and no assumption that $K$ contains a 0–1 point.

Milestones

1. Condition (iii″). For a closed convex cone $K \subseteq Q$ and a symmetric $Y$ with $y_{ii} = y_{0i}$: $Y \in M(K, Q)$ if and only if every column of $Y$ is in $K$ and the difference of the first column and any other column is in $K$.
2. Lemma 1.1. For closed convex cones $K_1, K_2 \subseteq Q$,

$$(K_1 \cap K_2)^\circ \subseteq N_+(K_1, K_2) \subseteq N(K_1, K_2) \subseteq K_1 \cap K_2 .$$

3. Lemma 1.3. For a closed convex cone $K \subseteq Q$ and every $1 \le i \le n$,

$$N(K) \subseteq (K \cap H_i) + (K \cap G_i).$$

4. Claim (4) in the proof of Theorem 1.4. For every set $T$ of $t \ge 1$ coordinates, with $\bar F$ the union of the faces of the unit cube that fix the coordinates in $T$ to $0$ or $1$,

$$N^t(K) \subseteq \operatorname{cone}(K \cap \bar F).$$

5. The remark after Lemma 1.1. $N(K_1 \cap K_2, K_1 \cap K_2) \subseteq N(K_1, K_2) \subseteq N(K_1 \cap K_2, Q)$.

Significance

Theorem 1.4 is what makes $N$ a hierarchy rather than a single cut: the relaxations $K \supseteq N(K) \supseteq N^2(K) \supseteq \dots$ reach the 0–1 hull after at most $n$ rounds, so the $N$-rank of a valid inequality (the least $t$ with the inequality valid for $N^t(K)$) is a well-defined number between $0$ and $n$. The rest of the paper measures combinatorial constraints by this rank: odd hole constraints have rank one on the stable set polytope, and the rank of a stable set inequality is bounded by its defect. Rank lower bounds for lift-and-project hierarchies, in the literature that followed, all presuppose this finite convergence.

The theorem is proved in the paper; to the best of available knowledge none of the Lovász–Schrijver operators has been formalized in a proof assistant. A formalization provides machine-checked definitions of the matrix cones and the cut operators that later missions in this series (odd holes, the defect bound, the $N_+$ constraints) state their results against, and a checked proof of the column characterization (iii″) that all of those proofs use.

Difficulty

The inclusion $K^\circ \subseteq N^n(K)$ follows from Lemma 1.1 once each $N^t(K)$ is known to be a convex cone. The reverse inclusion is the content. A first attempt shows that one round of $N$ forces one coordinate to be integral, and then iterates; but $N(K)$ is not contained in the union of $K \cap H_i$ and $K \cap G_i$, only in their Minkowski sum (Lemma 1.3), so a point of $N(K)$ is not itself integral in any coordinate. The induction must carry a statement about cones spanned by intersections with unions of cube faces, and it needs each iterate $N^t(K)$ to again be a closed convex cone inside $Q$ so that Lemma 1.3 can be reapplied. Closedness of the projection $N(K)$ is not automatic: a linear image of a closed cone need not be closed.

Formalization scope

• Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι for a finite type ι; none is $x_0$ and some i is $x_i$, and $n$ is the cardinality of ι, which may be $0$.
• $\operatorname{cone}(S)$ is Mathlib's PointedCone.hull ℝ S; $Q$ and $K^\circ$ are defined as spans of 0–1 vectors, as on the page, not by the inequality description $0 \le x_i \le x_0$.
• $M(K_1, K_2)$ is defined by condition (iii) through the polar cones; the column form (iii″) is a milestone, not the definition.
• The operators $N$, $N_+$ and the iterates are defined on arbitrary sets; the hypotheses (convex cone, contained in $Q$, closed) are carried by the theorems.
• Closedness. The paper tacitly takes its cones closed (they are polyhedral in all its applications), and the rewriting (iii′) on p. 169 needs it. Every statement here assumes the cones closed. Without this the goal is false: for $K = \{x : 0 < x_1 < x_0\} \cup \{0\}$ in $\mathbb R^2$, $K^\circ = \{0\}$ while $N(K) = Q$.
• In the proof of Theorem 1.4 the page places the cube $Q'$ in the hyperplane "$x_0 = 0$"; this is a misprint for $x_0 = 1$, and claim (4) is formalized with $x_0 = 1$.
• Not formalized in this mission: Lemma 1.2 (the dual description of $N(K)^*$), Lemma 1.5 (the $N_+$ analogue of Lemma 1.3, part of a later mission), and the algorithmic results of Section 1.c.

Contributions welcome: proofs that $N(K)$ is a closed convex cone contained in $Q$ whenever $K$ is, a proof of $Q^* = \operatorname{cone}\{e_i, e_0 - e_i\}$, and lemmas on cones spanned by the intersection of a generating set with a supporting hyperplane; these are reusable by the other missions of the series.

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
• H. D. Sherali and W. P. Adams, A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems, SIAM Journal on Discrete Mathematics 3(3) (1990) 411–430. https://doi.org/10.1137/0403036
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization 11(3) (2001) 796–817. https://doi.org/10.1137/S1052623400366802
• 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

Motivation

Manufacturing cells, communication protocols, traffic systems and database transaction managers are naturally described not by differential equations but by sequences of discrete events: a machine starts, a part arrives, a message is lost. Ramadge and Wonham's 1987 paper (SIAM J. Control Optim. 25(1)) set up a control theory for such systems in which the plant is an automaton, the controller is another automaton that may disable some events, and specifications are formal languages. The framework, now called supervisory control theory or the Ramadge–Wonham framework, is the standard model for the logical control of discrete event systems and underlies the textbook treatment in Cassandras and Lafortune (Introduction to Discrete Event Systems, 2008) and Wonham and Cai (Supervisory Control of Discrete-Event Systems, 2019).

The question the paper answers is the basic synthesis question of the theory: given a plant, a set of legal behaviours and a set of minimally acceptable behaviours, when does a controller exist that keeps the plant legal, achieves at least the acceptable behaviour, and never deadlocks, and what is the least restrictive such controller?

Setting

A generator is $\mathcal G = (Q, \Sigma, \delta, q_0, Q_m)$ with a state set $Q$, a finite alphabet $\Sigma$ of events, a partial transition function $\delta : \Sigma \times Q \to Q$, an initial state $q_0$ and marker states $Q_m \subseteq Q$. Extending $\delta$ to strings, the generated language $L(\mathcal G)$ is the set of strings $w$ for which $\delta(w, q_0)$ is defined, and the marked language $L_m(\mathcal G)$ is the subset of those that end in $Q_m$. The closure $\bar K$ of a language $K$ is its set of prefixes; $K$ is closed if $K = \bar K$. Throughout, $\mathcal G$ is assumed trim in the sense $L(\mathcal G) = \bar L_m(\mathcal G)$: every generated string can be completed to a marked one.

The alphabet is split into controllable events $\Sigma_c$ and uncontrollable events $\Sigma_u = \Sigma - \Sigma_c$. A supervisor $\mathcal S = (S, \phi)$ consists of a deterministic, accessible automaton $S = (X, \Sigma, \xi, x_0, X_m)$, whose state set $X$ may be infinite, and a map $\phi$ assigning to each state $x$ the set of controllable events it enables; uncontrollable events are always enabled. The closed loop $\mathcal S/\mathcal G$ runs $S$ and $\mathcal G$ in lockstep: an event occurs when the plant can execute it, the supervisor enables it, and the supervisor's automaton can follow it. This defines the languages $L(\mathcal S/\mathcal G)$, $L_m(\mathcal S/\mathcal G)$ and the controlled language $L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G) \cap L_m(\mathcal G)$.

$\mathcal S$ is complete if its automaton never refuses an event that the plant can execute and $\phi$ enables; it is proper if it is complete and

$$\bar L_m(\mathcal S/\mathcal G) = \bar L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G),$$

that is, every closed-loop string can be completed to a marked task. A language $K$ is controllable if $K \subseteq L(\mathcal G)$ and $\bar K \Sigma_u \cap L(\mathcal G) \subseteq \bar K$. For $L \subseteq L(\mathcal G)$, $\mathbf C_{\mathcal G}(L)$ is the class of controllable sublanguages of $L$ and $\mathbf F_{\mathcal G}(L)$ the class of sublanguages $K$ of $L$ with $K = \bar K \cap L_m(\mathcal G)$.

Given $\emptyset \neq L_a \subseteq L_g \subseteq L_m(\mathcal G)$, the Supervisory Marking Problem (SMP) asks for a proper $\mathcal S$ with $L_a \subseteq L_m(\mathcal S/\mathcal G) \subseteq L_g$, and the Supervisory Control Problem (SCP) for a proper $\mathcal S$ with $L_a \subseteq L_c(\mathcal S/\mathcal G) \subseteq L_g$.

Formalization targets

Goal: Theorem 7.1 (pp. 218–219)

$$\text{SMP solvable} \iff \sup \mathbf C_{\mathcal G}(L_g) \supseteq L_a, \qquad \text{SCP solvable} \iff \sup\{\mathbf C_{\mathcal G}(L_g) \cap \mathbf F_{\mathcal G}(L_g)\} \supseteq L_a,$$

and in each case the solving supervisor can be taken minimally restrictive: its marked (respectively controlled) language equals the supremal element and contains that of every proper supervisor whose language lies in $L_g$.

Milestones

1. Proposition 4.1 (i), (ii): marking is independent of control; every $K \subseteq L_m(\mathcal G)$, or $K \subseteq L \cap L_m(\mathcal G)$ for an achievable closed $L$, is the marked language of a complete supervisor.
2. Proposition 5.1: a complete supervisor realizes $(L_m, L_c, L) = (K_1, K_2, K_3)$ iff $K_1 \subseteq K_2$, $K_2 = K_3 \cap L_m(\mathcal G)$ and $K_3$ is closed and controllable.
3. Theorem 6.1 (i), (ii): a proper supervisor with $L_m(\mathcal S/\mathcal G) = K$ exists iff $K$ is controllable; one with $L_c(\mathcal S/\mathcal G) = K$ exists iff $K$ is controllable and $L_m(\mathcal G)$-closed.
4. Proposition 7.1: $\mathbf C_{\mathcal G}(L)$ and $\mathbf F_{\mathcal G}(L)$ contain $\emptyset$ and are closed under arbitrary unions.
5. The supremal elements (p. 218): $\sup \mathbf C_{\mathcal G}(L)$, $\sup \mathbf F_{\mathcal G}(L)$ and $\sup\{\mathbf C_{\mathcal G}(L) \cap \mathbf F_{\mathcal G}(L)\}$ belong to their classes.

Significance

Theorem 7.1 reduces the existence of a correct, non-blocking controller to a single language inclusion, and identifies the supremal controllable sublanguage as the behaviour of the least restrictive solution. That object is the backbone of the later theory: modular and decentralized control, control under partial observation, and the computational results that $\sup \mathbf C_{\mathcal G}(L)$ is regular and computable when $\mathcal G$ is finite and $L$ regular all start from it.

The result is proved in the paper and has been taught for decades; it is not open. Mathlib has no model of generators with partial transitions, supervisors or controllability (its DFA has a total transition function and a single accepted language), and no formalization of this theory exists on the platform. This mission provides one: a reusable Lean model of generators with partial transitions, supervisors with possibly infinite state, closed loops and controllability, together with the paper's existence theorems stated against it. A second mission on the same paper (quotients of supervisors, Theorem 10.1) builds on the same objects.

Difficulty

The combinatorial core of Proposition 7.1 is a short prefix-closure computation. The work lies in the constructions: to show existence, a supervisor must be built for an arbitrary controllable language, which in general is not regular, so the supervisor needs an infinite state set (for example strings of the target language) together with a proof that the closed loop generates exactly the intended language, is complete, and is proper. The converse directions require relating the closed-loop run to separate runs of the plant and of the supervisor's automaton. The naive shortcut of reading the "sup" as an arbitrary member of $\mathbf C_{\mathcal G}(L_g)$ containing $L_a$ skips the content of the supremal-element milestone; the goal is stated with the actual union.

Formalization scope

• The alphabet is a type α with [Fintype α]; strings are List α, the empty string is [], and $s\sigma$ is s ++ [σ]. Languages are Set (List α); the closure is pre K = {s | ∃ t, s ++ t ∈ K}.
• A generator is a structure with a state type Q : Type, a partial transition δ : α → Q → Option Q, an initial state and a marker set. No finiteness is assumed on states, of the plant or of the supervisor. Supervisors and generators live in Type 1.
• $\phi$ maps states to Ec → Bool; an event outside $\Sigma_c$ is enabled by definition, so uncontrollable events cannot be disabled.
• The closed loop is the product run from $(x_0, q_0)$; the accessible part in the paper's display (2.1) changes no language and is not built.
• Standing assumptions carried by every theorem: $\Sigma$ finite, $L(\mathcal G) = \bar L_m(\mathcal G)$, supervisor automata accessible (as a hypothesis on every input supervisor and a conjunct of every "there exists a supervisor").
• $\sup$ is sSup in the complete lattice Set (List α).
• A formalization in which the closed loop ignores $\phi$ or the plant, in which completeness is dropped from properness, or in which the supervisor is restricted to finitely many states, is not the paper's theorem and is ruled out by the definitions above.

Welcome contributions: the basic run lemmas (closed-loop runs project to plant and supervisor runs), the string-state supervisor construction, and proofs of the milestones in the given order.

Selected references

• P. J. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1):206–230, 1987. https://doi.org/10.1137/0325013
• W. M. Wonham and P. J. Ramadge, On the Supremal Controllable Sublanguage of a Given Language, SIAM J. Control Optim. 25(3):637–659, 1987. https://doi.org/10.1137/0325036
• C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed., Springer, 2008. https://doi.org/10.1007/978-0-387-68612-7
• W. M. Wonham and K. Cai, Supervisory Control of Discrete-Event Systems, Springer, 2019. https://doi.org/10.1007/978-3-319-77452-7

Motivation

Clique-width is a graph parameter introduced by Courcelle and Olariu (Discrete Appl. Math. 101 (2000)) that measures how far a graph is from being built by a few labelled operations. Every problem expressible in monadic second-order logic with quantification over vertices and vertex sets (MSO$_1$) can be solved in linear time on graphs given together with a decomposition of bounded clique-width (Courcelle, Makowsky and Rotics, Theory Comput. Syst. 33 (2000)). Bounded clique-width is more general than bounded tree-width: complete graphs have unbounded tree-width but clique-width $2$.

For fixed $k$ there was, before this paper, no polynomial-time algorithm that either decides that a graph has clique-width at least $k+1$ or outputs a decomposition of clique-width bounded by a function of $k$; the best known algorithm, by Johansson (2001), gave width $2k\log n$. Oum and Seymour (J. Combin. Theory Ser. B 96 (2006)) closed this gap with approximation $2^{3k+2}-1$, through rank-width and a factor-3 approximation for the branch-width of symmetric submodular functions.

Timeline:

• 1991: Robertson and Seymour introduce branch-width of graphs and hypergraphs (J. Combin. Theory Ser. B 52).
• 2000: Courcelle and Olariu define clique-width; Courcelle, Makowsky and Rotics solve MSO$_1$ problems on graphs given with a $k$-expression.
• 2001: Johansson gives a $2k\log n$ approximation.
• 2006: Oum and Seymour define rank-width, prove $\mathrm{rwd}(G) \le \mathrm{cwd}(G) \le 2^{\mathrm{rwd}(G)+1}-1$, and give an $O(n^9 \log n)$ algorithm that outputs a $(2^{3k+2}-1)$-expression or certifies clique-width above $k$.

Setting

All graphs are finite and simple. For a finite set $V$, a function $f : 2^V \to \mathbb{Z}$ is submodular if $f(X)+f(Y) \ge f(X\cap Y)+f(X\cup Y)$ and symmetric if $f(X) = f(V\setminus X)$.

A branch-decomposition of $f$ is a pair $(T, L)$ where $T$ is a tree with at least two vertices and all degrees at most $3$, and $L$ is a bijection from $V$ onto the leaves of $T$. Removing an edge $e$ of $T$ splits the leaves in two; the width of $e$ is $f$ of the set of elements of $V$ on one side. The width of $(T, L)$ is the largest edge width, and the branch-width $\mathrm{bw}(f)$ is the least width of a branch-decomposition, with $\mathrm{bw}(f) = f(\emptyset)$ when $|V| \le 1$.

A set $W \subseteq V$ is well-linked with respect to $f$ if for every partition $(X, Y)$ of $W$ and every $Z$ with $X \subseteq Z \subseteq V\setminus Y$, $f(Z) \ge \min(|X|, |Y|)$.

Let $A(G)$ be the adjacency matrix of $G$ over $\mathrm{GF}(2)$. For disjoint $X, Y \subseteq V(G)$, $\mathrm{cutrk}^*_G(X, Y)$ is the rank of the submatrix of $A(G)$ with rows $X$ and columns $Y$, and the cut-rank function is $\mathrm{cutrk}_G(X) = \mathrm{cutrk}^*_G(X, V(G)\setminus X)$. The rank-width $\mathrm{rwd}(G)$ is $\mathrm{bw}(\mathrm{cutrk}_G)$.

A $k$-expression is a term built from constants $\cdot_i$ (a vertex with label $i \in \{1,\dots,k\}$), the operators $\eta_{i,j}$ ($i \ne j$; add all edges between labels $i$ and $j$), $\rho_{i\to j}$ (relabel $i$ into $j$) and disjoint union $\oplus$. Its value is the labelled graph it produces; $G$ has clique-width $\mathrm{cwd}(G) \le k$ if some $k$-expression has value isomorphic to $G$.

An interpolation of $f$ is a function $f^*$ on disjoint pairs $(X, Y)$ that agrees with $f$ on $(X, V\setminus X)$, is monotone, submodular in the sense $f^*(A,B)+f^*(C,D) \ge f^*(A\cap C, B\cup D) + f^*(A\cup C, B\cap D)$, and has $f^*(\emptyset,\emptyset)=f(\emptyset)$.

Formalization targets

Goal: Theorem 1.1, certificate form

For a graph $G$ with at least one vertex and an integer $k \ge 1$:

$$\exists\, W,\ |W| = 3k+1,\ W \text{ well-linked for } \mathrm{cutrk}_G \;\Longrightarrow\; \mathrm{cwd}(G) \ge k+1,$$ $$\nexists\, W,\ |W| = 3k+1,\ W \text{ well-linked for } \mathrm{cutrk}_G \;\Longrightarrow\; \mathrm{cwd}(G) \le 2^{3k+2}-1.$$

The same explicit condition decides which side of the approximation holds; this is what the paper's algorithm certifies.

Milestones

1. Proposition 4.1: properties of an interpolation, including that $X \mapsto f^*(X, B) - f(\emptyset)$ is a matroid rank function on $V\setminus B$ when $f(\{v\}) - f(\emptyset) \le 1$.
2. Proposition 4.2: $f_{\min}(X,Y) = \min_{X\subseteq Z\subseteq V\setminus Y} f(Z)$ is an interpolation.
3. Theorem 5.1: a well-linked set of size $k$ forces $\mathrm{bw}(f) \ge k/3$ (for $k \ne 1$).
4. Theorem 5.2: no well-linked set of size $k$ implies $\mathrm{bw}(f) \le k$, when $f(\{v\}) \le 1$.
5. Proposition 6.1: $\mathrm{rk}\,M[X_1,Y_1] + \mathrm{rk}\,M[X_2,Y_2] \ge \mathrm{rk}\,M[X_1\cup X_2, Y_1\cap Y_2] + \mathrm{rk}\,M[X_1\cap X_2, Y_1\cup Y_2]$.
6. Corollary 6.2: submodularity of $\mathrm{cutrk}^*_G$ and $\mathrm{cutrk}_G$.
7. Section 6 claim: $\mathrm{cutrk}_G$ is symmetric submodular and $\mathrm{cutrk}^*_G$ interpolates it.
8. Proposition 6.3: $\mathrm{rwd}(G) \le \mathrm{cwd}(G) \le 2^{\mathrm{rwd}(G)+1}-1$.

Significance

The dichotomy turns clique-width, for which no exact polynomial algorithm is known even for fixed $k$, into a parameter that can be approximated with an explicit witness in each direction. Downstream, every algorithm for graphs of bounded clique-width that needs a $k$-expression as input becomes applicable to graphs given without one, at the cost of an exponential blow-up of the width.

The result is proved in the literature; this mission formalizes it. To our knowledge none of the objects involved — branch-width of set functions, rank-width, cut-rank, $k$-expressions, clique-width — has been formalized in Mathlib, and the submodularity of submatrix rank (Proposition 6.1) is absent from Mathlib's Matrix.rank API. The formal development would give reusable definitions of branch-decompositions of arbitrary integer set functions, of cut-rank, and of clique-width, and a machine-checked link between the combinatorial and the linear-algebraic width parameters.

Difficulty

The upper bound in Theorem 5.2 is the core. The natural approach, growing a branch-decomposition one leaf split at a time while keeping the width at most $k$, gets stuck at a leaf carrying a set $B$ with $f(B) = k$: a split of $B$ into two parts of $f$-value below $k$ has to be found, and it must be found from the failure of well-linkedness of a set that is not obviously related to $B$. The paper's device is the interpolation $f^*$, which attaches a matroid to $B$ whose base has exactly $f(B)$ elements. Formalizing this requires handling partial branch-decompositions, their extensions, and a maximality argument over trees, none of which exists in Mathlib.

Proposition 6.3's upper bound is a second, independent difficulty: a rank-decomposition must be converted into a $k$-expression by an induction over a rooted binary tree, with a relabelling argument bounding the number of labels by the number of distinct nonzero rows of a $\mathrm{GF}(2)$ matrix of rank $k$. Its lower bound needs the tree structure of a $k$-expression to be read as a branch-decomposition.

Formalization scope

The ground set is a Fintype V with DecidableEq V; subsets are Finset V; set functions are Finset V → ℤ, as in the paper. A branch-decomposition is a tree T : SimpleGraph (Fin n) with $n \ge 2$, all neighbour sets of size at most $3$, and an injective map $L$ from $V$ onto the vertices of degree $1$; the side of an edge $uw$ is found by reachability from $u$ after deleting $uw$. Branch-width, rank-width and clique-width are never computed as minima: "$\mathrm{bw}(f) \le k$" is the predicate "$|V| \le 1$ and $f(\emptyset) \le k$, or a branch-decomposition of width at most $k$ exists", lower bounds say that every branch-decomposition has a wide edge, and "$\mathrm{cwd}(G) \le k$" is "$G$ has a $k$-expression". Labels $\{1,\dots,k\}$ are Fin k. The value of a $k$-expression has as vertex type the occurrences of constants (a nested sum type), and $\eta_{i,j}$ requires $i \ne j$. Cut-rank uses Matrix.rank over ZMod 2 of submatrices of SimpleGraph.adjMatrix. An interpolation is a function on all pairs of subsets whose axioms are imposed on disjoint pairs only.

Running time is not formalized. The paper's Theorem 1.1 asserts an $O(n^9\log n)$ algorithm; there is no cost model on the page, and the goal states the certificate the algorithm returns instead. Without the running time, "$\mathrm{cwd}(G) \ge k+1$ or $\mathrm{cwd}(G) \le 2^{3k+2}-1$" holds for every graph, so that reading is ruled out as a formalization of the goal; so are well-linkedness with respect to anything other than $\mathrm{cutrk}_G$, widths defined by an unguarded infimum (which is $0$ on an empty family), $k$-expressions whose value is not the graph up to isomorphism or whose $\eta$ may join equal labels, and Theorem 5.1 stated for $k = 1$.

Correction of Theorem 5.1. As printed, Theorem 5.1 fails for $k = 1$: a singleton is always well-linked, but the edgeless graph on two vertices has cut-rank identically $0$ and branch-width $0 < 1/3$. The milestone carries the hypothesis $k \ne 1$; the goal uses the theorem only at size $3k+1 \ge 4$.

The graph with no vertex is excluded from the goal and from the upper bound of Proposition 6.3, since it has no $k$-expression for any $k$. Contributions welcome: proofs of the milestones, lemmas on branch-decompositions (suppressing degree-2 vertices, extending partial decompositions), and submatrix-rank submodularity, which is reusable beyond this mission.

Selected references

• S. Oum and P. Seymour, Approximating clique-width and branch-width, J. Combin. Theory Ser. B 96 (2006) 514–528. https://doi.org/10.1016/j.jctb.2005.10.006
• B. Courcelle and S. Olariu, Upper bounds to the clique width of graphs, Discrete Appl. Math. 101 (2000) 77–114. https://doi.org/10.1016/S0166-218X(99)00184-5
• B. Courcelle, J. A. Makowsky and U. Rotics, Linear time solvable optimization problems on graphs of bounded clique-width, Theory Comput. Syst. 33 (2000) 125–150. https://doi.org/10.1007/s002249910009
• N. Robertson and P. D. Seymour, Graph minors. X. Obstructions to tree-decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-N

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) was one of the first systematic worst-case analyses of polynomial-time heuristics for NP-complete optimization problems. Its Section 5 proves the harmonic bound $\sum_{j=1}^k 1/j$ for the greedy algorithm on minimum-cardinality set cover, a result that still underlies the standard $\ln n$ approximation guarantee.

Section 6, the subject of this mission, asks what happens when the cost of a cover is its total size rather than its number of sets. This problem, SET COVERING II (EC), is the optimization version of the EXACT COVER recognition problem of Karp's list (Karp 1972): a family has a disjoint subcover exactly when the optimum equals the number of covered points. Johnson shows that the change of measure breaks the cardinality greedy but that a greedy rule based on an overlap ratio recovers essentially the same guarantee. The same accounting (paying for each newly covered point) later became the standard analysis of greedy weighted set cover (Chvátal 1979).

Setting

An input is a finite family $F = \{S_1, \dots, S_p\}$ of finite sets. Its covered set 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

$$m_{EC}(F') = \sum_{S \in F'} |S|.$$

The optimum $F^*$ is the least measure of a subcover; since every subcover has measure at least $|T|$, an optimal subcover is one with the least possible overlapping. The subproblem EC$(k)$ admits only families in which every set has at most $k$ points.

Algorithm C2 keeps a subfamily SUB (initially empty), the unused sets LEFT (initially $F$) and the uncovered points UNCOV (initially $T$). While UNCOV is nonempty it chooses $S' \in$ LEFT minimizing

$$\mathrm{Ratio}(S) = \frac{|S - \mathrm{UNCOV}|}{|S \cap \mathrm{UNCOV}|},$$

the number of already-covered points of $S$ per newly covered point, and moves $S'$ from LEFT to SUB, removing its points from UNCOV. When several sets tie, any of them may be chosen; a subcover is choosable by C2 if some sequence of admissible choices returns it.

The overlap of a chosen set is $|S' - \mathrm{UNCOV}|$ at the moment it is chosen, and the cumulative overlap $\mathrm{OV}(F_1)$ of a run returning $F_1$ is the sum of these overlaps.

Formalization targets

Goal: Theorem 6 (p. 271)

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

$$R[C2, EC(k)](n) \le 1 + \ln(k) \le \sum_{j=1}^k \frac1j + \frac12,$$

and for all sufficiently large $n$, $R[C2, EC(k)](n) \ge \sum_{j=1}^k (1/j)$. In the size-free form used here, for every $k \ge 1$:

1. every subcover $M$ choosable by C2 on an input of EC$(k)$ satisfies $m_{EC}(M) \le (1 + \ln k)\,F^*$;
2. $1 + \ln k \le \sum_{j=1}^k 1/j + 1/2$;
3. some input of EC$(k)$ with $F^* > 0$ has a choosable subcover with $m_{EC}(M) \ge \big(\sum_{j=1}^k 1/j\big) F^*$.

Milestones (proof of Theorem 6, pp. 271–272)

• the measure of the output is $|T| + \mathrm{OV}(F_1)$;
• if C2 may choose a set with $\mathrm{Ratio}(S') \ge y$, then $(y+1)\,|\mathrm{UNCOV}| \le F^*$;
• with $a = F^*/|T|$ and $x = |T - \mathrm{UNCOV}|/|T|$, the next chosen set has $\mathrm{Ratio}(S') \le a/(1-x) - 1$;
• on EC$(k)$, $\mathrm{OV}(F_1) \le |T|\,(a[\ln(k) + 1] - 1)$;
• the analytic inequality $1 + \ln(k) \le \sum_{j=1}^k 1/j + 1/2$;
• the lower-bound input (Fig. 1 of the paper with every set of $F_1$ filled out to exactly $k$ points) on which C2 may pay $\sum_{j=1}^k 1/j$ times the optimum.

Significance

The result. The measure $\sum|S|$ penalizes overlap, and the paper notes (without proof, p. 270) that an algorithm returning an optimal cover for the cardinality measure can be a factor $k$ from optimal for this one. Theorem 6 shows that the ratio rule C2 is within $1 + \ln k$ of the least-overlap cover, and the lower bound shows that no analysis of C2 can beat $\sum_{j=1}^k 1/j$. The two bounds differ by less than $1/2$ for every $k$. The theorem was an early instance of a logarithmic guarantee for a weighted covering problem, where each set's cost is its size.

Formalizing it. The theorem has been proved since 1974; no machine-checked proof is known to exist. The mission produces a formal model of the EC problem and of C2 as a nondeterministic process, the overlap identity, and the discrete form of the paper's area-under-a-curve estimate. The last is the part the paper argues informally, through a step function and an integral.

Difficulty

The cardinality argument for C1 counts the sets chosen; here the sets have different sizes, so it does not apply. The overlap C2 pays per newly covered point is not bounded by a constant: early choices can be free and late ones cost up to $k-1$ per point, and the bound on the cumulative overlap must hold against the whole run, for every sequence of tie-breaks.

In a formal proof the integral must be replaced by a sum. Covered points arrive in blocks (one block per chosen set), the charge is constant on a block but the bound depends on the covered fraction at the start of the block, and the sum has to be compared with a logarithm. The terms $a\ln a$ and $a/k$ that the paper drops using $1 \le a \le k$ must be controlled as well, and the relation $1 \le a \le k$ must itself be proved from optimality. The lower bound needs an explicit run of C2 through ties on an input with $k \cdot k!$ points, checking at every stage that the intended set is a ratio minimizer.

Formalization scope

• Inputs. A family is p : ℕ with S : Fin p → Finset α (0-based, repetitions allowed; a repeated set counts twice in the measure if both copies are chosen, which C2 never does). Subcovers and SUB, LEFT are index sets. $F^*$ is a minimum over the finite, nonempty set of subcovers (Finset.inf'), never a junk value.
• Algorithm. C2 is a step relation on states (SUB, LEFT, UNCOV). The choice at Step 3 is existential over all minimizers, so every result quantifies over every choosable output (the paper's WORST). $\mathrm{Ratio}(S)$ is $+\infty$ when $S \cap \mathrm{UNCOV} = \emptyset$; the formal rule requires the chosen set to meet UNCOV and compares ratios by cross-multiplication, with no division.
• Overlap. The cumulative overlap depends on the run, not on the output alone, so it is carried by an inductive run relation RunOV.
• No problem size. The paper's $R[A, P](n)$ maximizes over inputs of size at most $n$ in an unspecified encoding. Upper bounds are stated for every input and every choosable output; the lower bound exhibits one input and one choosable output. Given monotonicity of $R$ in $n$, these are equivalent to the paper's claims. Ratios are stated multiplicatively, so $F^* = 0$ does not create a vacuous bound.
• Numbers. Measures are natural numbers cast to $\mathbb R$; $\ln$ is Real.log; $\sum_{j=1}^k 1/j$ is Mathlib's harmonic k.
• Ruled out. A deterministic tie-break would prove a weaker upper bound and could not realize the lower-bound run, and a ratio with $x/0 = 0$ would make disjoint-from-UNCOV sets the most attractive choice. The formalization uses neither.

The overlap identity and the discrete integral comparison are reusable for any greedy covering analysis that charges cost per newly covered point. Contributions welcome include proofs of the milestones, the invariants of the C2 run relation (SUB and LEFT partition the indices; UNCOV $= T - \bigcup$ SUB), and the explicit lower-bound run.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 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
• V. Chvátal, A greedy heuristic for the set-covering problem, Math. Oper. Res. 4 (1979), 233–235. https://doi.org/10.1287/moor.4.3.233