Linear Optimization

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Understanding and Using Linear Programming VII: LP Rounding Schedules Unrelated Machines Within Twice the Optimal MakespanTextbook

Motivation

Scheduling indivisible jobs on parallel machines to finish all of them as early as possible is a basic problem in operations research and in the theory of algorithms. In the unrelated machines model each job may take a different time on each machine, with no relation between the rows of the time table, as when machines of different types (black-and-white, duplex, colour copiers in the book's example) handle jobs of different kinds. Minimizing the makespan in this model is NP-hard, so the question is how close to the optimum a polynomial-time algorithm can get.

1990. Lenstra, Shmoys and Tardos (Math. Programming 46, 259–271) give a polynomial-time algorithm that rounds a basic optimal solution of a linear programming relaxation and returns a schedule of makespan at most $2\,t_{\mathrm{opt}}$ . The same paper shows that approximating the optimum makespan within a factor less than $3/2$ is NP-hard.
2007. Matoušek and Gärtner present the algorithm in §8.3 of Understanding and Using Linear Programming in a simplified, somewhat less efficient form: minimize $t^*(T) + T$ over the thresholds $T$ rather than binary-searching for the smallest $T$ with $t^*(T) \le T$ . This mission follows the book's presentation.

The gap between $3/2$ and $2$ for the general unrelated-machines problem has remained open since 1990; it is the standard example of LP rounding driven by the sparsity of basic solutions.

Setting

There are $m$ machines $M$ and $n$ jobs $J$ ; $d_{ij} > 0$ is the running time of job $j$ on machine $i$ . A schedule is a map $\sigma : J \to M$ assigning each job to one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i} d_{ij}$ , the makespan of $\sigma$ is the largest load, and $t_{\mathrm{opt}}$ is the makespan of an optimal schedule, one whose makespan is at most that of every schedule.

For a real threshold $T$ , the linear program $\mathrm{LPR}(T)$ in the variables $t$ and $x_{ij}$ is

\begin{aligned} \text{minimize } \ & t \\ \text{subject to } \ & \textstyle\sum_{i \in M} x_{ij} = 1 \ \ (j \in J), \qquad \textstyle\sum_{j \in J} d_{ij} x_{ij} \le t \ \ (i \in M),\\ & x_{ij} \ge 0, \qquad x_{ij} = 0 \ \text{ whenever } d_{ij} > T . \end{aligned}

Its optimal value is $t^*(T)$ , with $t^*(T) = \infty$ when $\mathrm{LPR}(T)$ is infeasible. The constraint matrix $A$ has one row per machine, one per job and one per pair with $d_{ij} > T$ ; the column of $x_{ij}$ carries $d_{ij}$ in the row of machine $i$ , $1$ in the row of job $j$ , and $1$ in the row of the constraint $x_{ij} = 0$ if present. Assumption 8.3.1 on a solution $x^*$ is that the columns of $A$ belonging to its nonzero variables are linearly independent; basic feasible solutions satisfy it. The support graph of $x^*$ is the bipartite graph $G = (M \cup J, E)$ with $E = \{\{i,j\} : x^*_{ij} > 0\}$ .

Formalization targets

Goal: Theorem 8.3.4

Let $T^*$ minimize $t^*(T) + T$ over all real $T$ and let $(t^*, x^*)$ be an optimal solution of $\mathrm{LPR}(T^*)$ satisfying Assumption 8.3.1. Then there is a schedule $\sigma$ with $x^*_{\sigma(j) j} > 0$ for every job $j$ and

\max_{i \in M} \sum_{j : \sigma(j) = i} d_{ij} \;\le\; 2\, t_{\mathrm{opt}} .

Milestones

Lemma 8.3.2. Every subgraph of the support graph $G$ has at most as many edges as vertices: $|E'| \le |M'| + |J'|$ .
Lemma 8.3.3. For $T \ge 0$ and an optimal solution $(t^*, x^*)$ of $\mathrm{LPR}(T)$ satisfying Assumption 8.3.1, some schedule along the edges of $G$ has makespan at most $t^* + T$ .
Proof of Theorem 8.3.4, first step. $\mathrm{LPR}(t_{\mathrm{opt}})$ is feasible and $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$ .
Proof of Theorem 8.3.4, second step. $t^*(T^*) + T^* \le 2\,t_{\mathrm{opt}}$ .

Significance

The theorem gives a polynomial-time 2-approximation for an NP-hard problem, and its proof isolates a reusable principle: a basic solution of an assignment-type LP has a support graph in which every subgraph has at most as many edges as vertices (a pseudoforest), so all but a matching's worth of the fractional assignment is already integral. The same sparsity argument underlies rounding results for the generalized assignment problem and for many later scheduling and allocation relaxations.

The result has been proved since 1990 and is textbook material. It is not formalized on Prove2Me or, to the maintainers' knowledge, in Mathlib. This mission produces a machine-checked version of the rounding theorem together with the counting lemma on basic solutions, the relaxation inequality $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$ , and the bound on the chosen threshold, each stated on shared definitions of the scheduling LP.

Difficulty

The obvious approach, rounding every job to the machine carrying the largest fraction of it, can overload a machine by many jobs at once and gives no constant factor. The bound $t^* + T$ needs two facts that are not visible from the LP value alone: that the support of a basic solution is sparse in the precise sense of Lemma 8.3.2, which has to be read off the linear independence of columns of the constraint matrix after deleting rows; and that the jobs left fractional can be matched injectively to machines, which requires a Hall-type condition derived from that sparsity. Relating linear independence of real column vectors to an edge count in a bipartite graph, and then producing a matching, is where the formal work lies.

A second subtlety is the threshold $T$ : the bound $t^* + T \le 2 t_{\mathrm{opt}}$ holds only because $T^*$ is chosen by minimizing over thresholds, and the relaxation at $T = t_{\mathrm{opt}}$ must be compared with the one at $T^*$ through optimal solutions of different linear programs.

Formalization scope

Machines are Fin m, jobs are Fin n (0-based; the book's machines $1,\dots,m$ and jobs $m+1,\dots,m+n$ are disjoint index sets), running times form d : Matrix (Fin m) (Fin n) ℝ, and the standing hypothesis $d_{ij} > 0$ of §8.3 appears in every theorem. A schedule is a function Fin n → Fin m; the makespan is the supremum of the loads over the finite type Fin m, which is the maximum for $m \ge 1$ . The optimum $t_{\mathrm{opt}}$ is the makespan of a schedule assumed optimal, never an infimum.

Optimal values of $\mathrm{LPR}(T)$ are never written as sInf: statements quantify over optimal solutions, i.e. feasible $(t, x)$ with $t \le t'$ for every feasible $(t', x')$ . The book's convention $t^*(T) = \infty$ for infeasible $\mathrm{LPR}(T)$ is encoded by letting thresholds without an optimal solution impose no condition in the minimality hypothesis on $T^*$ , which reads $t^* + T^* \le t + T$ for every real $T$ and every optimal solution $(t, x)$ of $\mathrm{LPR}(T)$ . The constraint matrix used in Assumption 8.3.1 has rows indexed by Fin m ⊕ Fin n ⊕ {(i, j) // T < d i j} and excludes the column of $t$ , as on p. 151.

"Efficiently construct" in Lemma 8.3.3 and "computes" in Theorem 8.3.4 are formalized by the property of the constructed schedule, not by its running time: every job goes to a machine $i$ with $x^*_{ij} > 0$ . This constraint is what rules out the trivializing formalization — "some schedule has makespan at most $2 t_{\mathrm{opt}}$ " is true of the optimal schedule itself and says nothing about the rounding.

A complete development needs: finite linear algebra (a linearly independent family of vectors supported on $k$ coordinates has at most $k$ members), Hall's marriage theorem (available in Mathlib as Finset.all_card_le_biUnion_card_iff_exists_injective), and the existence of an optimal solution of a feasible, bounded linear program (used to apply the minimality of $T^*$ at $T = t_{\mathrm{opt}}$ ). The counting lemma for basic solutions and the definitions of $\mathrm{LPR}(T)$ are reusable for other assignment relaxations. Proofs of any milestone, and alternative proofs of Lemma 8.3.3 by the direct pseudoforest argument of p. 153–154, are welcome.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.3, pp. 148–156. https://doi.org/10.1007/978-3-540-30717-4
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990), 259–271. https://doi.org/10.1007/BF01585745

7 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Understanding and Using Linear Programming VI: The Minimax Theorem for Zero-Sum GamesTextbook

Why zero-sum games belong in a linear programming course

A two-player zero-sum game models any situation in which one party's gain is exactly the other party's loss: a military allocation in the spirit of Colonel Blotto, a sealed-bid contest, rock–paper–scissors. The central question is what each player should do when the opponent is also reasoning about them. John von Neumann answered it in 1928 with the minimax theorem (von Neumann 1928): each player has a strategy guaranteeing the same number, the value of the game, whatever the opponent does. The theorem underlies modern game theory, robust decision making, and the analysis of online learning algorithms, where regret bounds are routinely derived from it.

Section 8.1 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) presents the theorem as an application of linear programming duality. This mission is the sixth of a series formalizing the capstone results of the book.

Setting

Alice has $m \ge 1$ pure strategies and Bob has $n \ge 1$ . A real $m \times n$ payoff matrix $M = (m_{ij})$ records Alice's gain, and Bob's loss, when Alice plays her $i$ th and Bob his $j$ th pure strategy. A mixed strategy of Alice is a probability vector $\mathbf x \in \mathbb R^m$ , $\sum_i x_i = 1$ , $\mathbf x \ge \mathbf 0$ ; a mixed strategy of Bob is a probability vector $\mathbf y \in \mathbb R^n$ . When the players randomize independently, Alice's expected payoff is

\mathbf x^T M \mathbf y = \sum_{i,j} m_{ij} x_i y_j .

The worst-case payoffs are

\beta(\mathbf x) = \min_{\mathbf y} \mathbf x^T M \mathbf y, \qquad \alpha(\mathbf y) = \max_{\mathbf x} \mathbf x^T M \mathbf y,

over mixed strategies. A mixed strategy of Bob is a best response against $\mathbf x$ if it minimizes $\mathbf x^T M\mathbf y$ ; a mixed strategy of Alice is a best response against $\mathbf y$ if it maximizes it. A pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium (Definition 8.1.1) if each is a best response against the other. Alice's $\tilde{\mathbf x}$ is worst-case optimal if $\beta(\tilde{\mathbf x}) = \max_{\mathbf x} \beta(\mathbf x)$ ; Bob's $\tilde{\mathbf y}$ is worst-case optimal if $\alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$ .

The proof in the book passes through three linear programs: the dual of (8.1), which for a fixed $\mathbf x$ maximizes $x_0$ subject to $M^T \mathbf x - \mathbf 1 x_0 \ge \mathbf 0$ ; program (8.2), the same with $\mathbf x$ as variables subject to $\sum_i x_i = 1$ , $\mathbf x \ge \mathbf 0$ ; and program (8.4), which minimizes $y_0$ subject to $M \mathbf y - \mathbf 1 y_0 \le \mathbf 0$ , $\sum_j y_j = 1$ , $\mathbf y \ge \mathbf 0$ .

Formalization targets

Goal: Theorem 8.1.3 (minimax theorem for zero-sum games)

For every $m \times n$ payoff matrix with $m, n \ge 1$ : worst-case optimal mixed strategies exist for both players; for any worst-case optimal $\tilde{\mathbf x}$ of Alice and $\tilde{\mathbf y}$ of Bob, the pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium; and there is a single number $v$ , the value of the game, with

\beta(\tilde{\mathbf x}) = \tilde{\mathbf x}^T M \tilde{\mathbf y} = \alpha(\tilde{\mathbf y}) = v

for every such pair. The third clause is what distinguishes the theorem from the existence of some saddle point.

Milestones

$\beta$ and $\alpha$ are attained minima and maxima (p. 135).
Lemma 8.1.2(i): $\beta(\mathbf x) \le \mathbf x^T M \mathbf y \le \alpha(\mathbf y)$ for all mixed $\mathbf x, \mathbf y$ , hence $\max_{\mathbf x}\beta \le \min_{\mathbf y}\alpha$ .
Lemma 8.1.2(ii): both strategies of a mixed Nash equilibrium are worst-case optimal.
Lemma 8.1.2(iii): $\beta(\tilde{\mathbf x}) = \alpha(\tilde{\mathbf y})$ implies that $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium.
The dual of (8.1) has optimal value $\beta(\mathbf x)$ (p. 137).
Eq. (8.3): an optimal solution $(\tilde x_0, \tilde{\mathbf x})$ of (8.2) satisfies $\tilde x_0 = \beta(\tilde{\mathbf x}) = \max_{\mathbf x}\beta(\mathbf x)$ .
Eq. (8.5): an optimal solution $(\tilde y_0, \tilde{\mathbf y})$ of (8.4) satisfies $\tilde y_0 = \alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$ .
Programs (8.2) and (8.4) both have optimal solutions, and their optimum values coincide (p. 138).
The minimax equality (p. 137):

\max_{\mathbf x}\min_{\mathbf y}\mathbf x^T M \mathbf y = \min_{\mathbf y}\max_{\mathbf x}\mathbf x^T M \mathbf y .

Significance

The theorem gives a complete prescription for zero-sum play: a worst-case optimal strategy secures at least the value against any opponent, and a worst-case optimal opponent holds the player to at most the value, so both players can announce their strategies in advance without loss. With Lemma 8.1.2(ii) it yields a characterization: a pair of mixed strategies is a Nash equilibrium if and only if both are worst-case optimal. The minimax equality is used downstream in online learning (regret-to-value arguments), in robust optimization, and in Yao's principle for randomized algorithms.

The mathematics is classical and proved; what this mission adds is a machine-checked version in the book's own formulation. The platform already has AGT.zero_sum_minimax (Algorithmic Game Theory I), which proves the existence of a saddle point, and the general FamousTheorems.sion_minimax_theorem. Neither states that every pair of worst-case optimal strategies is an equilibrium with a common value, and neither exhibits the LP route: the dual of (8.1), the programs (8.2) and (8.4), and their duality. The mission records that route statement by statement, so that it can be reused as a worked instance of LP duality.

Difficulty

Lemma 8.1.2 is routine; the entire content is the reverse inequality $\max_{\mathbf x}\beta(\mathbf x) \ge \min_{\mathbf y}\alpha(\mathbf y)$ . The obvious attack, maximizing $\beta$ directly, fails because $\beta$ is a minimum of linear functions and hence not linear, so its maximization is not a linear program as written. The obstacle is removed only by an appeal to LP duality in the proof, together with the facts that the simplices are nonempty and compact, and that the relevant programs are feasible and bounded so that optima exist. None of this is supplied by the pure-strategy structure of the game: pure Nash equilibria need not exist (rock–paper–scissors has none).

Formalization scope

Pure strategies are indexed by Fin m and Fin n, with the book's standing assumption $m, n \ge 1$ carried as hypotheses 1 ≤ m, 1 ≤ n by every theorem; the book's indices $1,\dots,m$ become $0,\dots,m-1$ . Mixed strategies are Mathlib's stdSimplex ℝ (Fin m), the payoff is x ⬝ᵥ (M *ᵥ y). $\beta(\mathbf x)$ is the real sInf and $\alpha(\mathbf y)$ the real sSup of the payoffs over the opponent's simplex; milestone 1 states that these are attained. A mixed Nash equilibrium is defined in the verbal form of Definition 8.1.1 (mutual best responses). Worst-case optimality is defined against all mixed strategies, never as a saddle-point condition, so the goal is not circular with Lemma 8.1.2(iii). LP optimality is stated as "feasible and at least as good as every feasible point", so no supremum over a possibly empty or unbounded feasible set is used.

The book's clause that worst-case optimal strategies "can be efficiently computed by linear programming" is algorithmic and is not part of the formal statement; there is no complexity model. A goal asserting only the existence of worst-case optimal strategies, or only the existence of some equilibrium, would drop the theorem's third clause and is ruled out: the common value $v$ is quantified before all pairs of worst-case optimal strategies.

A complete development needs compactness of the standard simplex, continuity of the bilinear payoff, and a strong duality theorem for linear programs in the form of the programs (8.2)/(8.4); the latter is reusable across the whole series. Proofs by other routes (Sion's theorem, a separating hyperplane argument, fixed points) are welcome for the goal; the LP milestones stand on their own as statements about the programs.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.1, pp. 131–142. https://doi.org/10.1007/978-3-540-30717-4
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
M. Sion, "On general minimax theorems", Pacific Journal of Mathematics 8 (1958), 171–176. https://doi.org/10.2140/pjm.1958.8.171

12 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Understanding and Using Linear Programming II: Optimal Basic Feasible Solutions and Vertices in Equational FormTextbook

Motivation

Every finite algorithm for linear programming rests on one structural fact: if a linear program has an optimum at all, it has one at a point singled out by finitely many linear conditions. The simplex method walks between such points, and exact complexity analyses, sensitivity analysis and integrality arguments all start from them. Chapter 4 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), establishes this fact for linear programs in equational form, in the definitions that the rest of the book (the simplex method of Chapter 5, duality in Chapter 6, the applications in Chapter 8) uses.

This mission is the second of a series formalizing that book. It fixes the book's notion of a basic feasible solution and of a vertex, and targets the theorem that optimal solutions exist whenever the program is feasible and bounded, and can then be chosen basic.

Setting

A linear program in equational form is

\text{maximize } c^{T}x \quad\text{subject to}\quad Ax=b,\ x\ge 0,

where $A$ is a real $m\times n$ matrix, $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ , and $x\ge 0$ means every coordinate of $x$ is nonnegative. A feasible solution is an $x\in\mathbb{R}^n$ satisfying both constraints; the set of them is $P$ . An optimal solution is a feasible $x$ with $c^{T}y\le c^{T}x$ for every feasible $y$ . The objective is bounded from above if some real $M$ satisfies $c^{T}x\le M$ for all feasible $x$ .

Throughout Section 4.2 the book assumes that $A$ has $n\ge m$ columns and rank $m$ (its rows are linearly independent). For $S\subseteq\{1,\dots,n\}$ , $A_S$ denotes the matrix formed by the columns of $A$ with indices in $S$ . A basis is an $m$ -element set $B$ for which $A_B$ is nonsingular, i.e. its columns are linearly independent. A basic feasible solution is a feasible $x$ for which some basis $B$ has $x_j=0$ for every $j\notin B$ .

A point $v$ is a vertex of $P$ if $v\in P$ and some nonzero $c\in\mathbb{R}^n$ satisfies $c^{T}v>c^{T}y$ for every $y\in P\setminus\{v\}$ : $v$ is the unique maximizer over $P$ of a nonzero linear function.

Formalization targets

Goal: Theorem 4.2.3 (p. 46)

For $A$ of rank $m$ with $n\ge m$ ,

\Bigl(P\neq\emptyset\ \wedge\ \exists M\ \forall x\in P,\ c^{T}x\le M\Bigr)\ \Longrightarrow\ \exists\,x^{*}\ \text{optimal},

\exists\,x^{*}\ \text{optimal}\ \Longrightarrow\ \exists\,\tilde x\ \text{optimal and basic feasible}.

Both parts are one theorem, as in the book. Part (i) says optimal solutions fail to exist only for the two obvious reasons, infeasibility and unboundedness; part (ii) says an optimum can always be found among basic feasible solutions.

Milestones

Lemma 4.2.1 (p. 45): a feasible $x$ is basic if and only if the columns of $A_K$ are linearly independent, where $K=\{j : x_j>0\}$ .
Proposition 4.2.2 (p. 45): for a basis $B$ there is at most one feasible solution vanishing outside $B$ .
The statement proved inside the proof of Theorem 4.2.3 (p. 47): if the objective is bounded above, every feasible $x_0$ is dominated by a basic feasible $\tilde x$ , $c^{T}\tilde x\ge c^{T}x_0$ .
Theorem 4.4.1 (p. 54): a point of $P$ is a vertex of $P$ if and only if it is a basic feasible solution.

Significance

Theorem 4.2.3 gives a finite, if impractical, algorithm for linear programming: enumerate the at most $\binom{n}{m}$ sets $B$ , solve $A_Bx_B=b$ , and keep the best nonnegative solution. It is the correctness backbone of the simplex method, which visits basic feasible solutions in a smarter order, and it is the source of the book's claim that a feasible and bounded linear program has an optimal solution. Theorem 4.4.1 identifies this algebraic notion with the geometric corners of the feasible polyhedron, which is what makes statements such as "the LP relaxation has an integral vertex" in later chapters meaningful.

All of these results are classical and fully proved in the book. The value of formalizing them here is the definition layer: later missions of this series (Bland's rule, the central path, the scheduling application) state their results about bases and basic feasible solutions in exactly these definitions, and a proved Theorem 4.2.3 in this form lets them import the existence of an optimal basic solution instead of re-deriving it. Related facts are already machine-checked on Prove2Me in the formulation of Bertsimas and Tsitsiklis (Introduction to Linear Optimization I and II: minimization over polyhedra $\{x : a_i^{T}x\ge b_i\}$ , extreme points, basic solutions as $n$ active linearly independent constraints). Those statements concern a different presentation of the program and a different notion of basic solution; connecting them to the equational-form statements here is itself a welcome contribution.

Difficulty

The obvious argument for part (i), "a continuous function on a closed set bounded above attains its supremum", fails: the feasible set is usually unbounded, and a linear function bounded above on an unbounded closed convex set need not obviously attain its supremum without using the polyhedral structure. The existence of an optimum is exactly the nontrivial content of part (i); compactness is not available.

For milestone 1, the delicate direction is the converse: a set of linearly independent columns indexed by $K$ must be completed to an $m$ -element basis, which requires the rank- $m$ assumption. For Theorem 4.4.1, the direction from vertex to basic feasible solution is not local: a vertex is defined by an optimization property, while basicness is a statement about the support of the point.

Formalization scope

All items live in the namespace MatousekLP.BFS and share one definition module, MatousekLP.BFS.EquationalForm. Conventions:

vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ are 0, …, n-1;
$Ax=b$ is A *ᵥ x = b, $x\ge 0$ is 0 ≤ x (pointwise), $c^{T}x$ is c ⬝ᵥ x;
a subset $B$ of indices is a Finset (Fin n); " $A_B$ nonsingular" is linear independence over $\mathbb{R}$ of the family of columns of $A$ indexed by the elements of $B$ , together with B.card = m;
the standing assumption of §4.2 is the pair of hypotheses m ≤ n and A.rank = m on every theorem;
"optimal" and "bounded from above" are stated against every feasible point. No real supremum over the feasible set appears anywhere, so an empty or unbounded feasible set cannot make a statement hold through a default value;
"vertex" is the book's unique-maximizer definition of p. 53, not Mathlib's Set.extremePoints; the book's remark on p. 55 that the two coincide is not used as a definition;
Theorem 4.4.1 carries the extra hypothesis $n\ge 1$ : for $n=0$ there is no nonzero vector in $\mathbb{R}^0$ , the single feasible point $0$ is basic but not a vertex, and the book's equivalence fails.

A formalization in which "optimal" were defined through sSup of the objective over the feasible set would make part (ii) trivially true or false on unbounded programs; the definitions here rule that out. Dropping the rank hypothesis would make part (ii) false (no basis exists when the rows are dependent), so it is not optional.

Reusable infrastructure: the column-restriction and basis vocabulary, the support set $K$ , and the extension of a linearly independent set of columns to a basis of the column space are needed again in the simplex chapter. Proofs of any milestone, and bridges to Mathlib's Set.extremePoints or to the Bertsimas–Tsitsiklis statements on the platform, are welcome.

Selected references

J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Universitext, Springer, 2007, Chapter 4, pp. 41–56. https://doi.org/10.1007/978-3-540-30717-4
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 2.
G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1

6 thms2 active usersReviewed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Understanding and Using Linear Programming I: Integral Bipartite Matchings, Total Unimodularity and König's TheoremTextbook

Motivation

Many combinatorial optimization problems are integer programs: linear objectives and linear constraints, with the extra requirement that the variables be integers. Dropping that requirement gives the LP relaxation, which is solvable efficiently but in general only bounds the integer optimum. For a small but important class of problems the relaxation loses nothing: its optimum is attained at an integral point, so linear programming solves the combinatorial problem exactly. Bipartite matching is the standard example, and the job-assignment problem that opens Chapter 3 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) is a maximum-weight perfect matching problem in a bipartite graph.

The same phenomenon, combined with linear programming duality, produces combinatorial min–max theorems. The oldest of them is König's theorem (1931) on matchings and vertex covers in bipartite graphs; Hall's marriage theorem (1935) follows from it. This mission formalizes the book's treatment of both strands: the integrality of the bipartite matching LP (Section 3.2), total unimodularity and König's theorem (Section 8.2), and, on the same objects for general graphs, the LP-rounding 2-approximation for vertex cover (Section 3.3).

Setting

Let $G = (V, E)$ be a finite simple graph. A bipartition of $G$ is a pair of disjoint sets $X, Y$ with $X \cup Y = V$ such that every edge joins a vertex of $X$ to a vertex of $Y$ ; $G$ is bipartite if it has one. A matching is a set $M \subseteq E$ in which each vertex is incident to at most one edge; a vertex cover is a set $C \subseteq V$ containing at least one end-vertex of every edge. A matching is maximum if no matching has more edges; a vertex cover is minimum if no vertex cover has fewer vertices.

The incidence matrix of $G$ has a row for each vertex and a column for each edge, with entry $1$ when the vertex lies on the edge and $0$ otherwise. A real matrix is totally unimodular if every square submatrix, obtained by deleting some rows and some columns, has determinant $0$ , $1$ or $-1$ .

Given real edge weights $w_e$ , the integer program (3.1) maximizes $\sum_{e} w_e x_e$ subject to $\sum_{e \ni v} x_e = 1$ for every vertex $v$ and $x_e \in \{0,1\}$ ; its 0/1 solutions are the perfect matchings. Its LP relaxation replaces $x_e \in \{0,1\}$ by $0 \le x_e \le 1$ . The vertex-cover relaxation (3.3) minimizes $\sum_v x_v$ subject to $x_u + x_v \ge 1$ for every edge $\{u,v\}$ and $0 \le x_v \le 1$ .

Formalization targets

Goal: König's theorem (Theorem 8.2.2)

For every finite bipartite graph $G$ ,

\max\{|M| : M \text{ a matching of } G\} \;=\; \min\{|C| : C \text{ a vertex cover of } G\}.

Total unimodularity (Lemmas 8.2.3–8.2.5)

A \text{ TU} \;\Rightarrow\; (A \mid e_i) \text{ TU}; \qquad A \text{ TU},\ b \in \mathbb{Z}^m,\ \max\{c^Tx : Ax \le b,\ x \ge 0\} \text{ attained} \;\Rightarrow\; \text{attained at some } x^* \in \mathbb{Z}^n;

and the incidence matrix of a bipartite graph is totally unimodular.

Integrality of the perfect-matching relaxation (Theorem 3.2.1)

If the LP relaxation of (3.1) for a bipartite graph with real weights is feasible, it has an optimal solution with all $x_e \in \{0,1\}$ , which is also optimal for (3.1).

Consequences on the same objects

Hall's theorem (Theorem 8.2.1): if $|N(T)| \ge |T|$ for every $T \subseteq X$ , where $N(T) \subseteq Y$ is the set of neighbours of $T$ , then some matching covers every vertex of $X$ . And for an arbitrary graph, with $x^*$ optimal for (3.3), $S_{LP} = \{v : x^*_v \ge \tfrac12\}$ and $S_{OPT}$ a minimum vertex cover (§3.3, p. 38):

S_{LP} \text{ is a vertex cover and } |S_{LP}| \le 2\,|S_{OPT}| .

Significance

König's theorem says that for bipartite graphs the two natural certificates, a matching (a lower bound on any vertex cover) and a vertex cover (an upper bound on any matching), always meet. It makes maximum matchings and minimum vertex covers computable by linear programming, whereas minimum vertex cover in general graphs is NP-hard; Section 3.3's rounding bound quantifies what the LP still gives in that general case. Lemma 8.2.4 is the general tool behind this and behind the max-flow min-cut theorem that the book mentions on p. 148: any integer program with a totally unimodular constraint matrix and integral right-hand side can be solved as a linear program.

All results here are classical and proved. The formalization work is to connect them: Mathlib already has the definition of total unimodularity (Matrix.IsTotallyUnimodular), closure under appending unit-like rows, and Hall's theorem in the form of Finset.all_card_le_biUnion_card_iff_exists_injective. To the best of the drafting survey, neither König's theorem nor the total unimodularity of bipartite incidence matrices nor the integrality lemma 8.2.4 is in Mathlib, and no König statement was found among the platform's missions. The mission produces these in a form that later chapters on network flows and combinatorial duality can import.

Difficulty

The inequality "maximum matching $\le$ minimum vertex cover" is immediate, since each edge of a matching needs its own cover vertex. The difficulty is the reverse inequality, and it is exactly where bipartiteness is needed: the triangle has maximum matching $1$ and minimum vertex cover $2$ . Along the book's route, the obstacle is that LP duality equates the optima of the two relaxations, which are real numbers; one must show that both relaxations already have integral optimal solutions, which is the content of total unimodularity and Lemma 8.2.4. Theorem 3.2.1 is a separate integrality statement with equality constraints and weights of arbitrary sign; it is not a consequence of the Birkhoff–von Neumann theorem unless the graph is complete bipartite with equal sides.

Formalization scope

Graphs are SimpleGraph V on a Fintype vertex type with decidable equality; edges are elements of Sym2 V, and a matching is a Finset (Sym2 V) of edges. Bipartiteness is the existence of finite sets $X, Y$ forming a bipartition; the empty graph and the empty vertex type are allowed and the statements remain the book's there. Vertex covers are Mathlib's SimpleGraph.IsVertexCover. Matrices are real; LP vectors are Fin n → ℝ (0-based indices) or indexed by the edge set or the vertices. An "optimal solution" is always a feasible point that is at least as good as every feasible point: no supremum or infimum over a possibly empty or unbounded set is used, and König's theorem asserts that both a maximum matching and a minimum vertex cover exist and have equal size. Lemma 8.2.4 takes $b \in \mathbb{Z}^m$ and allows real $c$ ; its conclusion is an integral optimal solution, not merely an integral feasible one. Theorem 3.2.1 is the perfect-matching version with equality constraints, not the " $\le 1$ " matching version discussed in the book's remarks.

A formalization in which König's theorem compares a supremum and an infimum of possibly empty sets, or in which "optimal" is not tied to feasibility, would be trivializing and is ruled out by these conventions.

Useful infrastructure, reusable beyond this mission: Laplace expansion arguments for totally unimodular matrices, the equivalence of the inequality form with the equational form, existence of optimal basic feasible solutions, and LP duality in inequality form (the platform's LinearOptimization.lp_strong_duality states duality for a general-form LP). Combinatorial proofs of König and Hall are equally welcome; only the statements are fixed.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §3.2–3.3 and §8.2. https://doi.org/10.1007/978-3-540-30717-4
D. Kőnig, "Gráfok és mátrixok", Matematikai és Fizikai Lapok 38 (1931), 116–119.
P. Hall, "On representatives of subsets", Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
A. J. Hoffman, J. B. Kruskal, "Integral boundary points of convex polyhedra", in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton, 1956, 223–246. https://doi.org/10.1515/9781400881987-014
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, Chapter 19.

12 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Operations Research+1·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design VII: Crémer–McLean Full Surplus Extraction with Correlated TypesTextbook

Motivation

Bayesian mechanism design asks which collective decisions and payments a designer can implement when every agent holds private information, the type, drawn from a commonly known prior. Most of the classical theory (Myerson's optimal auction, the Myerson–Satterthwaite impossibility, the public goods results) assumes that types are independent. Once types are correlated, as they are when bidders' values share a common component, the theory changes in a way that is best read as a paradox: Crémer and McLean (Econometrica 1988) showed that a designer can then extract the entire surplus, leaving agents no information rents. This mission formalizes Chapter 6 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press 2015), which sets up Bayesian mechanism design in general, treats independent types, and proves the Crémer–McLean theorem, together with the one numbered result of Chapter 9, the impossibility theorem of Jehiel and Moldovanu for interdependent values.

Timeline of the results formalized here:

Rochet (1987) characterized implementable decision rules by cyclical monotonicity; Proposition 6.1 is its interim version for independent types.
Crémer and McLean (1988): under their condition on the prior, every direct mechanism can be made Bayesian incentive-compatible without changing its decision rule or interim payments (Proposition 6.4).
Krishna and Maenner (2001): revenue equivalence for convex type sets and convex utilities (Proposition 6.2).
Jehiel and Moldovanu (2001): with interdependent values, efficient decisions are generically not Bayesian implementable (Proposition 9.1).
Kosenok and Severinov (2008): an identifiability condition added to Crémer–McLean gives ex post budget balance as well (Proposition 6.6).

Setting

There are finitely many agents $i \in I$ and a set $A$ of alternatives. Agent $i$ has a type $\theta_i \in \Theta_i$ and utility $u_i(a,\theta_i) - t_i$ from alternative $a$ and payment $t_i$ . Types $\theta = (\theta_1,\dots,\theta_N) \in \Theta = \prod_i \Theta_i$ are drawn from a common prior $\mu$ ; $\mu(\cdot\mid\theta_i)$ is the conditional distribution of the others' types $\theta_{-i}$ given $\theta_i$ . Types are independent if $\mu(\cdot\mid\theta_i)$ does not depend on $\theta_i$ .

A direct mechanism $(q, t_1,\dots,t_N)$ is a decision rule $q:\Theta\to A$ and payment rules $t_i:\Theta\to\mathbb R$ . It is Bayesian incentive-compatible (BIC) if for every $i$ and all $\theta_i,\theta_i'$ ,

\int_{\Theta_{-i}} u_i(q(\theta_i,\theta_{-i}),\theta_i) - t_i(\theta_i,\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i) \ \ge\ \int_{\Theta_{-i}} u_i(q(\theta_i',\theta_{-i}),\theta_i) - t_i(\theta_i',\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i).

The interim decision rule $Q_i(\theta_i)$ is the distribution of $q(\theta_i,\theta_{-i})$ given $\theta_i$ , and the interim expected payment is $T_i(\theta_i) = \int t_i(\theta_i,\theta_{-i})\,d\mu(\theta_{-i}\mid\theta_i)$ . A mechanism is ex post budget balanced if $\sum_i t_i(\theta) = 0$ for every $\theta$ , and ex ante budget balanced if $\int_\Theta \sum_i t_i\,d\mu = 0$ .

In §6.4 every $\Theta_i$ is finite and $\mu(\theta) > 0$ for every $\theta$ . The prior satisfies the Crémer–McLean condition if for no agent $i$ and type $\theta_i$ there are weights $\lambda \ge 0$ on $\Theta_i\setminus\{\theta_i\}$ with

\mu(\theta_{-i}\mid\theta_i) = \sum_{\theta_i'\ne\theta_i}\lambda(\theta_i')\,\mu(\theta_{-i}\mid\theta_i')\quad\text{for all }\theta_{-i}.

Identifiability requires that for every full-support distribution $\nu\ne\mu$ some agent's type $\theta_i$ has a belief $\nu(\cdot\mid\theta_i)$ that is not a nonnegative combination of the beliefs $\mu(\cdot\mid\theta_i')$ .

Formalization targets

Goal: Crémer–McLean (Proposition 6.4)

If $\mu$ satisfies the Crémer–McLean condition, then for every direct mechanism $(q,t)$ there is a BIC direct mechanism $(q,t')$ with

\sum_{\theta_{-i}} t_i(\theta_i,\theta_{-i})\,\mu(\theta_{-i}\mid\theta_i) = \sum_{\theta_{-i}} t_i'(\theta_i,\theta_{-i})\,\mu(\theta_{-i}\mid\theta_i)\quad\text{for all } i,\theta_i.

Milestones

Proposition 6.1 (independent types): $q$ is part of a BIC mechanism iff it is interim cyclically monotone, $\sum_{\kappa=1}^{k-1}\big(\int_A u_i(a,\theta_i^{\kappa+1})\,dQ_i(\theta_i^\kappa) - \int_A u_i(a,\theta_i^\kappa)\,dQ_i(\theta_i^\kappa)\big)\le 0$ for every cycle $\theta_i^k = \theta_i^1$ .
Proposition 6.2 (independent types, convex type sets, convex utilities): two BIC mechanisms with $Q_i' = Q_i$ have $T_i' = T_i + \tau_i$ .
Proposition 6.3 (independent types): every ex ante budget balanced mechanism has an equivalent ex post budget balanced one.
Proposition 6.5 (Farkas's alternative), already proved on the platform as Polyhedral.farkas_lemma.
Proposition 6.6 (Kosenok–Severinov): under Crémer–McLean and identifiability, every ex ante budget balanced mechanism has an equivalent BIC and ex post budget balanced one.
Proposition 9.1 (Jehiel–Moldovanu): in the linear interdependent-values model, under a regularity condition on first best rules and the weight condition $\alpha^i_{ai}/\alpha^i_{bi}\ne\sum_j\alpha^i_{aj}/\sum_j\alpha^i_{bj}$ for some $i,a,b$ , no first best direct mechanism is BIC. It uses its own model (§9.3) and is not on the goal's proof path.

Significance

The Crémer–McLean theorem says that, with correlated finite types, incentive compatibility imposes essentially no constraint: every decision rule and every interim payment rule can be implemented. In a single-unit auction this gives full surplus extraction. The result is the benchmark against which the literature on risk aversion, limited liability, collusion and the genericity of priors (Robert 1991, Laffont–Martimort 2000, Heifetz–Neeman 2006) measures its departures, and Proposition 6.6 extends it to budget-balanced mechanisms, which is what bilateral trade and public goods applications need. Propositions 6.1–6.3 are the independent-types counterpart that the correlated case breaks: they show why revenue equivalence and the ex ante/ex post budget-balance equivalence hold there and fail here. Proposition 9.1 shows the opposite failure, for interdependent values, where efficient decisions cannot be implemented even without participation or budget constraints.

All results are proved in the literature (Kosenok–Severinov's proof is omitted in the book). Apart from Farkas's alternative (Proposition 6.5), which is proved on the platform, none of them is formalized in Mathlib or on the platform; the platform's other mechanism design results (dominant-strategy results in a valuation model, revenue equivalence for symmetric independent auctions) do not cover correlated types.

Difficulty

For the goal the difficulty is the uniformity of the construction: a single payment adjustment must make truth-telling optimal against every possible deviation of every type of every agent, while leaving each type's expected payment unchanged. The obvious scoring-rule adjustment, charging $-\ln\mu(\theta_{-i}\mid\theta_i')$ , changes interim payments, and removing that change is where the Crémer–McLean condition enters. For Proposition 6.2 the envelope argument must handle convex type sets that are not open and utilities that are only convex, not differentiable. For Proposition 9.1 the obvious argument differentiates interim utility twice; the proposition does not assume that interim utility is twice differentiable, so that regularity has to be derived from the hypotheses on the interim probabilities.

Formalization scope

Three definition files carry the three models. Independent types (§6.2–6.3): type sets are arbitrary measurable spaces, the prior is the product of probability measures $\rho_i$ , and interim quantities are integrals against it. Finite correlated types (§6.4): finite type sets, a prior $\mu:\Theta\to\mathbb R$ with $\mu(\theta)>0$ and $\sum_\theta\mu(\theta)=1$ , and conditional beliefs $\mu(\theta_{-i}\mid\theta_i) = \mu(\theta)/\mu(\theta_i)$ ; the alternative set $A$ is arbitrary. Interdependent values (§9.3): finite $A$ , signals in $[0,1]^A$ with positive densities, independent across agents, linear utilities with nonzero weights $\alpha^j_{ai}$ .

Committed conventions and explicit formulas:

The Crémer–McLean condition uses nonnegative weights without a sum-to-one constraint, as Definition 6.7 prints it.
"Equivalent" in Propositions 6.4 and 6.6 means the same decision rule and the same interim expected payments at truthful reports, as Proposition 6.4 states; in Proposition 6.3 it is the report-by-report notion, which under independence is equality of the interim payment rules $T_i$ .
Proposition 6.2 adds continuity of $u_i(a,\cdot)$ on $\Theta_i$ , and Proposition 6.3 adds at least two agents; without them the printed statements are false.
Measurability, which the book omits throughout, is made explicit: decision rules are measurable, and the payment sections and utilities are integrable against the relevant interim distributions.
In Proposition 9.1 the partial derivatives are derivatives within the closed cube $[0,1]^K$ , and the weight condition is the displayed ratio inequality.

A trivializing formalization of the goal, one that proves it only for mechanisms that are already incentive compatible, or with a payment rule that is not a function of the reported type profile, or with "equivalent" weakened to "some BIC mechanism exists", is ruled out: the statement quantifies over every direct mechanism and fixes both the decision rule and every interim payment.

Reusable infrastructure: finite conditional expectations under a full-support prior, the Crémer–McLean and identifiability conditions, and the interim model with product priors. Proofs of any milestone and of the goal, including via the Farkas reference, are welcome.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
J. Crémer and R. P. McLean, "Full extraction of the surplus in Bayesian and dominant strategy auctions", Econometrica 56(6), 1988. https://doi.org/10.2307/1913096
G. Kosenok and S. Severinov, "Individually rational, budget-balanced mechanisms and allocation of surplus", Journal of Economic Theory 140(1), 2008.
P. Jehiel and B. Moldovanu, "Efficient design with interdependent valuations", Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00237
V. Krishna and E. Maenner, "Convex potentials with an application to mechanism design", Econometrica 69(4), 2001. https://doi.org/10.1111/1468-0262.00225
J.-C. Rochet, "A necessary and sufficient condition for rationalizability in a quasi-linear context", Journal of Mathematical Economics 16(2), 1987. https://doi.org/10.1016/0304-4068(87)90007-3

10 thms2 active usersReviewed

Numerical Analysis Theoretical Computer Science·Captain: Lucas

Extended Smale's 9th Problem I: no algorithm computes K digits of LP minimisersResearch Paper

Motivation

Linear programming is usually described as "solvable in polynomial time", but that statement is about rational inputs given exactly. In Smale's list of problems for the 21st century (Smale 1998), Problem 9 asks for a polynomial-time algorithm over the reals deciding the feasibility of $Ax \ge y$ , and Smale explicitly calls for "models which process approximate inputs and which permit round-off computations". Real data such as $\sqrt 2$ , entries of a discrete cosine transform, or even $1/3$ in floating point can only be accessed approximately.

Bastounis, Hansen and Vlačić pose the extended Smale's 9th problem: in a model where the algorithm can only query approximations of the input to any requested accuracy, can one compute minimisers of linear programming, basis pursuit and Lasso to $K$ correct digits? Their Main Theorem I (Theorem 3.4) shows that the answer depends on $K$ in a sharp way: for a suitable class of well-conditioned, bounded inputs, no algorithm at all (not only no efficient one) produces $K$ correct digits, while $K-1$ digits are computable (but not in bounded time) and $K-2$ digits are computable in polynomial time.

This mission targets the first, impossibility, half of Theorem 3.4(i) for linear programming.

Setting

Linear program. For $A \in \mathbb R^{m\times N}$ , $y\in\mathbb R^m$ and $c = \mathbf 1_N=(1,\dots,1)$ , the solution set is

\Xi(y,A) = \operatorname*{argmin}_{x\in\mathbb R^N}\ \langle x, c\rangle \quad\text{subject to}\quad Ax = y,\ x\ge 0 .

It is a subset of $M_N = \mathbb R^N$ with the $\ell^p$ norm, $p\in[1,\infty]$ . An input is a pair $\iota = (y,A)$ , and the evaluations of $\iota$ are its coordinates $y_i$ and entries $A_{ij}$ .

Extended model ( $\Delta_1$ -information). Let $D_n = \{k2^{-n} : k\in\mathbb Z\}$ . An oracle representation of $\iota$ is a family $\tilde\iota = (\tilde\iota_{j,n})$ , indexed by evaluations $j$ and accuracies $n = 1,2,\dots$ , with $\tilde\iota_{j,n}\in D_n + iD_n$ and $|\tilde\iota_{j,n} - f_j(\iota)|\le 2^{-n}$ . An algorithm must succeed on every oracle representation of every input.

General algorithm. To make impossibility results independent of the machine model, the paper uses general algorithms (Definition 9.3): a map $\Gamma$ from inputs to $M\cup\{\mathrm{NH}\}$ ( $\mathrm{NH}$ = no output) together with a nonempty set $\Lambda_\Gamma(\iota)$ of evaluations read on $\iota$ . This set is finite whenever $\Gamma$ halts. The output is determined by the values read, and any input that agrees on those values reads the same set. Turing machines and BSS machines with an oracle are special cases; general algorithms can even solve the halting problem.

Error and breakdown epsilon. The error is $\operatorname{dist}(\Gamma(\iota),\Xi(\iota)) = \inf_{\xi\in\Xi(\iota)} d(\Gamma(\iota),\xi)$ , with distance $\infty$ from $\mathrm{NH}$ . The strong breakdown epsilon $\varepsilon_B^s$ is the supremum of all $\varepsilon\ge 0$ such that every general algorithm has error $>\varepsilon$ on some input (Definition 9.17).

Formalization targets

Goal: Theorem 3.4(i), deterministic part, for LP

For every integer $K\ge1$ , all dimensions $4\le m<N$ and every $p\in[1,\infty]$ there is a nonempty class $\Omega_{m,N}$ of inputs $(y,A)$ with nonempty solution sets, $\|y\|_\infty\le 2$ and $\|A\|_{\max}=1$ , such that

\neg\,\exists\,\Gamma\ \text{general algorithm on oracle representations}:\quad \forall\,\tilde\iota,\ \ \operatorname{dist}_{\ell^p}\big(\Gamma(\tilde\iota),\,\Xi(\iota)\big)\le 10^{-K}.

Milestones

Lemma 11.1: the explicit solution sets of the LP inputs $(y_1e_1, A(\alpha,\beta,m,N))$ .
Proposition 10.5 (ii), deterministic part: two input sequences that converge in evaluation to a common input and whose solutions stay $\kappa$ apart force $\varepsilon_B^s\ge\kappa/2$ for a suitable choice of $\Delta_1$ -information.
§9.6, (i) ⇒ (ii): a lower bound on $\varepsilon_B^s$ for one specific $\Delta_1$ -information transfers to the problem with all oracle representations.
Proposition 9.32 (i) (deterministic consequence via Proposition 10.1): $\varepsilon_B^s>10^{-K}$ for LP on a suitable $\Omega_{m,N}$ .

Significance

The theorem shows that for LP with inexact input, being non-computable in Turing's sense does not rule out a finer complexity theory. The paper builds a " $K$ / $K-1$ / $K-2$ digits" classification on this. It also explains why established solvers can return wrong answers with a success flag on small, well-conditioned LPs (§4 of the paper), and it bears on computer-assisted proofs that rely on inexact LP, such as the Flyspeck proof of the Kepler conjecture.

The result is proved on paper. As far as the proposer knows, it has not been machine-checked. This mission formalizes the deterministic impossibility part for LP and puts in place reusable infrastructure: general algorithms, breakdown epsilons and $\Delta_1$ -information. That infrastructure is the base for later missions on the randomised parts of Theorem 3.4(i)–(ii), the weak breakdown epsilon (iii), the exit-flag theorem (Theorem 5.1), and basis pursuit and Lasso.

Difficulty

The obvious objection is that LP is in P for rational inputs, so some rounding scheme ought to work. It fails because an algorithm must halt after reading finitely many approximations. Two inputs that agree to that accuracy but have minimisers far apart then receive the same output. Setting this up needs a notion of algorithm strong enough to cover every computational model, a precise $\Delta_1$ -information model in which the adversary controls the approximations, and explicit LP geometry in which an arbitrarily small perturbation of $A$ moves the minimiser by a fixed amount.

Formalization scope

Inputs are $(y,A)\in(\mathrm{Fin}\,m\to\mathbb R)\times\mathrm{Matrix}(\mathrm{Fin}\,m)(\mathrm{Fin}\,N)\,\mathbb R$ . Evaluations are complex-valued, as in Definition 9.2. Outputs lie in PiLp p (Fin N → ℝ).
A general algorithm is a structure with an output run : Ω → Option M (none = NH) and a read set queried, satisfying the axioms (i)–(iii) of Definition 9.3.
Errors take values in $[0,\infty]$ (ℝ≥0∞), and the error of NH is $\infty$ . The infimum over an empty solution set is $\infty$ . The goal also requires nonempty solution sets, so no junk value enters.
Oracle accuracies are indexed by $n\in\{1,2,\dots\}$ (ℕ+). An oracle input is stored as a pair (input, oracle family), and algorithms can read only the oracle family.
Out of scope: randomised algorithms, the positive statements (iii)–(iv), runtime, and the condition-number bounds $\mathrm{Cond}(AA^*)\le3.2$ , $C_{FP}\le4$ , $\mathrm{Cond}(\Xi)\le179$ .

Selected references

A. Bastounis, A. C. Hansen, V. Vlačić, The extended Smale's 9th problem — On computational barriers and paradoxes in estimation, regularisation, computer-assisted proofs, and learning, preprint (2021).
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20 (1998). https://doi.org/10.1007/BF03025291

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Odd Minimum Cut-Sets and b-Matchings 2: A Capacitated b-Matching Blossom Inequality Is Violated iff G(x, d) Has an Odd Cut of Capacity Less Than OneResearch Paper

Motivation

A b-matching with upper bounds in a graph $G=(V,E)$ assigns a nonnegative integer $x_e\le d_e$ to every edge so that the edges at each node $i$ carry at most $b_i$ in total. Maximizing a linear objective over such assignments is an integer program that contains ordinary matching ( $b\equiv 1$ , $d\equiv 1$ ) and appears in assignment, transportation and scheduling models with capacities on both nodes and arcs. Edmonds and Johnson showed that the integer hull of this system is described by adding the blossom (matching) inequalities to the linear relaxation (Edmonds–Johnson 1970; cited in the paper as [8], [13]). There are exponentially many blossom inequalities, so a cutting-plane method needs a separation procedure: given a fractional point $\bar x$ , find a violated blossom inequality or certify that none exists.

M. W. Padberg and M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7 (1982), gave this procedure. Section 1 of the paper computes a minimum-capacity cut with an odd number of odd-labelled nodes in polynomial time; Sections 2 and 3 reduce blossom separation to that computation. This mission formalizes Section 3, the case with upper bounds $d$ . The companion mission Odd Minimum Cut-Sets and b-Matchings 1 formalizes Section 1.

Timeline: Edmonds (1965) describes the perfect matching polytope; Edmonds and Johnson (1970) extend the description to capacitated $b$ -matching; Gomory and Hu (1961) give the cut-tree that Section 1 of Padberg–Rao relies on; Padberg and Rao (1982) reduce separation to odd minimum cuts. Later work (Letchford, Reinelt and Theis, 2008) shortened the resulting algorithms; the reduction itself is the one stated here.

Setting

Let $G=(V,E)$ be a finite simple undirected graph, $b\in\mathbb Z_{>0}^V$ and $d\in\mathbb Z_{>0}^E$ . The system is

Ax\le b,\qquad x\le d,\qquad x\ge 0, \tag{3.1}

with $A$ the node–edge incidence matrix. For $W\subseteq V$ write $E(W)$ for the edges with both ends in $W$ and $(W:V-W)$ for the cut-set of $W$ , the edges with exactly one end in $W$ . For $T\subseteq (W:V-W)$ with $b(W)+d(T)=\sum_{i\in W}b_i+\sum_{e\in T}d_e$ odd, the blossom inequality is

x(W)+x(T)=\sum_{e\in E(W)}x_e+\sum_{e\in T}x_e\le \tfrac12\bigl(b(W)+d(T)-1\bigr). \tag{3.3}

Let $\bar x$ be a real point feasible for (3.1) and $\bar s=b-A\bar x$ its node slacks. Let $E(\bar x)$ be the edges with $\bar x_e>0$ . The labelled weighted graph $G(\bar x,d)$ has nodes $V$ , a special node $S$ , and one new node $i_e$ for each $e\in E(\bar x)$ . For each such edge $e=[i,j]$ , where $i$ is the end the construction scans first, it has an edge $[i,i_e]$ of weight $d_e-\bar x_e$ and an edge $[i_e,j]$ of weight $\bar x_e$ . Each $i\in V$ is joined to $S$ with weight $\bar s_i$ . There are no other edges. A node $i_e$ is odd iff $d_e$ is odd; $S$ is odd iff $b(V)$ is odd; a node $i\in V$ is odd iff $b_i$ plus the $d_e$ of the subdivided edges scanned from $i$ is odd. A node set $U$ is odd when it contains an odd number of odd nodes, and $\bar y(U:\tilde V-U)$ denotes the total weight of the edges leaving $U$ (its cut capacity).

Formalization targets

Goal: Theorem 3.1

For every feasible $\bar x$ and every scan order,

\exists\,W\subseteq V,\ T\subseteq (W:V-W):\ b(W)+d(T)\text{ odd},\ \bar x(W)+\bar x(T)>\tfrac12\bigl(b(W)+d(T)-1\bigr)

\Longleftrightarrow\quad \exists\,U\subseteq \tilde V \text{ odd}:\ \bar y(U:\tilde V-U)<1 .

The paper's closing sentence, that $W$ and $T$ can be obtained constructively from the proof of Lemma 3.2, describes the proof and is not part of the formal statement.

Milestones

Eq. (3.6): $2x(W)+x(W:V-W)+x(T)+s(W)+t(T)=b(W)+d(T)$ for $T\subseteq(W:V-W)$ , with $t=d-x$ .
Eq. (3.7): $\bar x$ violates (3.3) for $(W,T)$ iff $\bar x(W:V-W)+d(T)-2\bar x(T)+\bar s(W)<1$ .
Lemma 3.1: if $T\subseteq (W:V-W)\cap E(\bar x)$ and $b(W)+d(T)$ is odd, some odd $U$ with $S\notin U$ has $\bar y(U:\tilde V-U)$ equal to the left side of (3.7) (Eq. (3.8)).
Lemma 3.2: every odd $U$ with $S\notin U$ and capacity $<1$ arises this way from some $(W,T)$ with $b(W)+d(T)$ odd.

Significance

Theorem 3.1 is what makes the blossom inequalities of capacitated $b$ -matching usable in a linear-programming based cutting-plane method: combined with the odd minimum cut algorithm of Section 1, it separates them in polynomial time. By the equivalence of separation and optimization, it also yields a polynomial-time algorithm for capacitated $b$ -matching through the ellipsoid method. The paper notes the further consequence that every odd cut-set of capacity less than one, not only a minimum one, gives a violated inequality.

The results are proved in the 1982 paper; none of them has a machine-checked proof that this mission is aware of. What the mission adds is a formal statement of the graph $G(\bar x,d)$ and of the reduction, and a checked proof of it. The definitions of the capacitated $b$ -matching system, its blossom inequalities and the subdivided graph are reusable for later work on matching polytopes and on the uncapacitated case of Section 2.

Difficulty

The identities (3.6) and (3.7) are bookkeeping over incidences. The substance is the correspondence between node sets $W$ with complemented edge sets $T$ and odd node sets $U$ of $G(\bar x,d)$ . In one direction the right $U$ must pick, for every cut edge, the side of $i_e$ that makes the edge contribute $\bar x_e$ or $d_e-\bar x_e$ as (3.7) requires, and its parity must be computed through the orientation-dependent labels. In the other direction an arbitrary odd cut of capacity below one must be shown to have this shape; this uses $d_e\ge 1$ to exclude every other position of a new node $i_e$ , and it uses the evenness of the total label to pass from an odd set containing $S$ to its complement. A point $\bar x$ whose blossom violation uses an edge $e\in T$ with $\bar x_e=0$ has no new node for $e$ . Such a $T$ has to be ruled out, and the argument uses the capacity bound. It is not an assumption of the theorem.

Formalization scope

The graph is a Mathlib SimpleGraph V on a finite type with decidable adjacency; edges are elements of G.edgeFinset : Finset (Sym2 V). The data are b : V → ℕ and d : Sym2 V → ℕ, positive on nodes and on edges, and a real point x : Sym2 V → ℝ. Feasibility means the linear relaxation of (3.1); integrality of $\bar x$ is not assumed. All halves and differences are computed in ℝ. When $W=V$ the cut-set is empty, so the paper's convention " $T$ is empty" holds automatically.

$G(\bar x,d)$ is fixed by definitions from $(G,b,d,\bar x)$ and an orientation tail choosing the end of each edge scanned first; every theorem quantifies over the orientation. The node type is Option V ⊕ {e // e ∈ E(x̄)}, with none the special node $S$ . Weights are a symmetric function on nodes with $0$ meaning "no edge". The labels are given in closed form. The paper assigns them by a sequential scan that flips the parity of the scanned end by $d_e$ , and addition mod 2 does not depend on the order of the scan. "The cut capacity of an odd minimum cut-set is less than one" is stated as "some odd cut has capacity less than one"; the two agree, and the formulation avoids a minimum over a possibly empty family.

Two trivializing formalizations are ruled out: $G(\bar x,d)$ is constructed, not an arbitrary labelled graph assumed to satisfy (3.8); and no infimum over odd cuts is taken, since a real sInf of an empty family is $0$ and would make the right side true when no odd cut exists.

Contributions welcome: proofs of the milestones, lemmas on cut capacities of symmetric weight functions on finite types, and parity bookkeeping for labelled node sets.

Selected references

M. W. Padberg, M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7(1), 67–80, 1982. https://doi.org/10.1287/moor.7.1.67
J. Edmonds, E. L. Johnson, Matching: a well-solved class of integer linear programs, in Combinatorial Structures and Their Applications, Gordon and Breach, 89–92, 1970; reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, 27–30, 2003. https://doi.org/10.1007/3-540-36478-1_3
R. E. Gomory, T. C. Hu, Multi-terminal network flows, Journal of the SIAM 9(4), 551–570, 1961. https://doi.org/10.1137/0109047
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
A. N. Letchford, G. Reinelt, D. O. Theis, Odd minimum cut sets and b-matchings revisited, SIAM Journal on Discrete Mathematics 22(4), 1480–1487, 2008. https://doi.org/10.1137/060664793

7 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Selected Topics in Column Generation II: A Strictly Redundant Column Is Never Optimal for the Ratio Pricing ProblemResearch Paper

Motivation

Column generation solves linear programs with far more columns than can be written down: a restricted master problem holds a few columns, its dual multipliers are passed to a pricing problem, and the pricing problem returns a column to add. It is the standard engine behind branch-and-price for vehicle routing, crew scheduling and cutting stock, where the master problem is very often a set-partitioning problem (Lübbecke and Desrosiers 2005; Desrosiers and Lübbecke 2005).

Which column the pricing problem returns matters. The classical Dantzig rule picks the column of most negative reduced cost, but in set-partitioning masters with identical subproblems this rule tends to produce columns that are "weak" in the dual: their dual constraint is implied by the constraints of smaller columns. Sol (1994, PhD thesis, Eindhoven) called such columns redundant and studied pricing rules that avoid them. In their survey, Lübbecke and Desrosiers state the key fact as Proposition 2 (Operations Research 53(6), p. 1016): under ratio pricing, a strictly redundant column is never the optimal choice.

Setting

Let the rows of a set-partitioning master problem be $\{1,\dots,m\}$ . A column is a subset $s$ of the rows, with incidence vector $\mathbf a_s \in \{0,1\}^m$ ( $(\mathbf a_s)_i = 1$ iff $i \in s$ ). Let $\mathcal A$ be a finite collection of nonempty columns with costs $c_s$ . The master problem is

\min \sum_{s \in \mathcal A} c_s \lambda_s \quad\text{s.t.}\quad \sum_{s \in \mathcal A} \mathbf a_s \lambda_s = \mathbf 1,\ \lambda \ge 0,

with $\lambda$ integer in the integer program. Its dual has one free multiplier $u_i$ per row and one constraint $\mathbf u^{\mathsf T}\mathbf a_s \le c_s$ per column.

A column $s$ is redundant, eq. (30), p. 1015, if

\mathbf a_s = \sum_{r \subset s} \mathbf a_r \lambda_r \qquad\text{and}\qquad c_s \ge \sum_{r \subset s} c_r \lambda_r ,

with $\lambda_r \ge 0$ and $r$ ranging over the columns of $\mathcal A$ that are proper subsets of $s$ ; then its dual constraint is implied by those of its subcolumns. It is strictly redundant if the cost inequality is strict. The pair $(\mathcal A, \mathbf c)$ has the subcolumn property if $c_r < c_s$ for all $r, s \in \mathcal A$ with $r \subsetneq s$ . Given dual multipliers $\bar{\mathbf u} \in \mathbb R^m$ , the ratio pricing problem (31) is

\min\left\{ \frac{c(\mathbf a) - \bar{\mathbf u}^{\mathsf T}\mathbf a}{\mathbf 1^{\mathsf T}\mathbf a} \;\middle|\; \mathbf a \in \mathcal A \right\},

the reduced cost per covered row. In Lean these objects are incidence, IsRedundant, IsStrictlyRedundant, SubcolumnProperty and pricingRatio in the namespace Lubbecke2005.SubcolumnPricing.

Formalization targets

Goal: Proposition 2 (p. 1016)

Let $(\mathcal A, \mathbf c)$ satisfy the subcolumn property, $\emptyset \notin \mathcal A$ , and let $\bar{\mathbf u} \in \mathbb R^m$ be arbitrary. If $s \in \mathcal A$ is strictly redundant, then

\neg\Bigl(\forall \mathbf a \in \mathcal A:\ \frac{c_s - \bar{\mathbf u}^{\mathsf T}\mathbf a_s}{\mathbf 1^{\mathsf T}\mathbf a_s} \le \frac{c(\mathbf a) - \bar{\mathbf u}^{\mathsf T}\mathbf a}{\mathbf 1^{\mathsf T}\mathbf a}\Bigr),

that is, $\mathbf a_s$ is not an optimal solution of (31). The paper states the proposition and refers to Sol (1994) for the concept; it gives no proof.

Milestone: the cost shift (§5.1, p. 1016)

If only $c_r \le c_s$ holds for $r \subsetneq s$ in $\mathcal A$ , the shifted costs $c'_s = c_s + |s|$ satisfy the subcolumn property, and on every $\lambda$ with $\sum_s \mathbf a_s \lambda_s = \mathbf 1$ ,

\sum_{s} c'_s \lambda_s = \sum_s c_s \lambda_s + m .

This is the paper's remark that the shift "adds to $z^\star$ a constant term equal to the number of rows and does not change the problem".

Significance

Proposition 2 is the paper's argument for alternative pricing rules (§5.2): it shows that dividing the reduced cost by the number of covered rows filters out a whole class of columns that contribute nothing to the dual polyhedron, whatever the current dual multipliers are. Steepest-edge pricing, Devex and the lambda pricing rule are motivated along the same lines. The cost-shift remark extends the proposition to cost structures that are only weakly monotone under inclusion, which covers the frequent case of costs that do not decrease when rows are added to a column.

The result is published and elementary once stated precisely, but the paper leaves the definition of redundancy informal (no sign on $\lambda$ , no index set of the sum), and those choices decide whether the proposition is true. A formal statement pins them down. To our knowledge neither the proposition nor the vocabulary of redundant columns and ratio pricing has a machine-checked formalization; the definitions here are reusable for other statements about pricing rules in set-partitioning column generation.

Difficulty

The mathematical difficulty is modest; the difficulty is in the reading. With multipliers $\lambda_r$ of arbitrary sign in (30), the proposition is false: on rows $\{1,2,3\}$ take $s = \{1,2,3\}$ , $r_1 = \{1,2\}$ , $r_2 = \{2,3\}$ , $r_3 = \{2\}$ with costs $2.2$ , $2$ , $2$ , $1.9$ and $\bar{\mathbf u} = 0$ ; then $\mathbf a_s = \mathbf a_{r_1} + \mathbf a_{r_2} - \mathbf a_{r_3}$ , $2.2 > 2.1$ , the subcolumn property holds, and $s$ has the unique smallest ratio. The empty column is a second trap: its denominator $\mathbf 1^{\mathsf T}\mathbf a$ is zero. The formal statement has to exclude both, and has to keep the minimum in (31) over $\mathcal A$ only.

Formalization scope

Conventions committed to in Lean:

Rows are Fin m (indexed from $0$ ); a column is a Finset (Fin m), and its incidence vector is the real 0/1 vector incidence s : Fin m → ℝ. The collection $\mathcal A$ is a Finset (Finset (Fin m)); costs are a function Finset (Fin m) → ℝ, of which only the values on $\mathcal A$ matter.
Reading of (30): the multipliers are nonnegative ( $\lambda_r \ge 0$ ), the Farkas form of "the corresponding constraint is redundant for the dual problem". The paper leaves the sign implicit; with signed multipliers the proposition fails (example above).
Reading of $r \subset s$ : proper inclusion, over columns $r \in \mathcal A$ only. With $r \subseteq s$ every column would be redundant via $\lambda_s = 1$ .
Strictly redundant: (30) with strict cost inequality; the equality part is unchanged.
Reading of (31)'s denominator: $\emptyset \notin \mathcal A$ is a hypothesis of the goal ("a set-partitioning column covers at least one row"); it is named here as an addition to the literal text. The denominator is 1 ⬝ᵥ incidence a, which equals $|a|$ .
Dual multipliers: $\bar{\mathbf u} \in \mathbb R^m$ is arbitrary; no sign, no optimality for the restricted master.
"Cannot be an optimal solution" is stated literally as the negation of "the ratio of $\mathbf a_s$ is at most the ratio of every column of $\mathcal A$ "; this is equivalent to the existence of a column with strictly smaller ratio. No infimum over real sets is used.
The subcolumn property is kept as a hypothesis because the paper states it, although the conclusion may hold without it.
Cost shift: stated for real multipliers; the optimal value $z^\star$ is not formalized, and "does not change the problem" is rendered as the pointwise identity on the feasible set.

A trivializing formalization — a redundancy witness not tied to the proper subcolumns of $s$ in $\mathcal A$ , signed multipliers, or an empty column with ratio $0$ — is ruled out by the definitions above.

Needed infrastructure is only finite sums of vectors in $\mathbb R^m$ and the identity $\mathbf 1^{\mathsf T}\mathbf a_s = |s|$ . Contributions welcome: proofs of the goal and the milestone, and further statements from §5 (for example the redundancy characterisation of Sol 1994) built on the same definitions.

Selected references

M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
M. Sol, Column Generation Techniques for Pickup and Delivery Problems, PhD thesis, Eindhoven University of Technology, 1994 (cited in the paper as Sol 1994).
J. Desrosiers and M. E. Lübbecke, A Primer in Column Generation, in Column Generation, Springer, 2005. https://doi.org/10.1007/0-387-25486-2_1
F. Vanderbeck, Decomposition and Column Generation for Integer Programs, PhD thesis, Université catholique de Louvain, 1994.

3 thms2 active usersReviewed

Combinatorics Operations Research Optimization·Captain: mikedeng1

An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem I: ALGORITHM 1, Linear Grouping with LP Rounding, Is an Asymptotic Approximation SchemeResearch Paper

Motivation

One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in $(0,1)$ . It is the model behind cutting stock (cutting rolls of paper or steel to ordered widths), memory and file allocation, and batch scheduling on identical machines, and it is NP-hard. Its algorithmic study is therefore about approximation: how close to the optimum a polynomial-time algorithm can guarantee to come.

1961–1963: Gilmore and Gomory introduce the configuration linear program for cutting stock and solve it by column generation (Gilmore–Gomory 1961).
1974: Johnson, Demers, Ullman, Garey and Graham analyse First Fit and related heuristics, with asymptotic ratio $17/10$ and $11/9$ (Johnson et al. 1974).
1981: Fernandez de la Vega and Lueker give the first asymptotic approximation scheme, packing within $(1+\varepsilon)\,OPT(I) + 1$ bins in time linear in $n$ for fixed $\varepsilon$ , using elimination of small pieces and linear grouping (Fernandez de la Vega–Lueker 1981).
1982: Karmarkar and Karp replace the enumeration of configurations by an approximate solution of the configuration LP and a rounding step, obtaining an additive term polynomial in $1/\varepsilon$ (this mission), and, with geometric grouping, $OPT(I) + O(\log^2 OPT(I))$ (Karmarkar–Karp 1982).
2013–2017: Rothvoß and then Hoberg–Rothvoß improve the additive term to $O(\log OPT \cdot \log\log OPT)$ and $O(\log OPT)$ (Hoberg–Rothvoß 2017).

Setting

An instance $I$ is a finite multiset of piece sizes, each in the open interval $(0,1)$ . Write $n(I)$ for the number of pieces, $m(I)$ for the number of distinct sizes, and $SIZE(I)$ for the sum of all sizes. A packing of $I$ is a finite multiset of bins, each a multiset of sizes, whose union is exactly $I$ and in which every bin has total size at most $1$ . Its cost is the number of bins, and $OPT(I)$ is the minimum cost.

A configuration of $I$ is a nonempty multiset of sizes occurring in $I$ with total at most $1$ . With $b_t$ the number of pieces of size $t$ and $a_{tc}$ the number of occurrences of $t$ in configuration $c$ , the fractional bin-packing problem is the linear program

\min\ \mathbf 1\cdot x\quad\text{s.t.}\quad x\ge 0,\qquad \sum_c a_{tc}x_c \ge b_t\ \ \text{for every size } t,

whose optimal value is $LIN(I)$ . A basic feasible solution is an extreme point of its feasible region.

For instances $I,J$ , write $I\le J$ if there is a one-to-one map $f$ from the pieces of $I$ into the pieces of $J$ with $x\le f(x)$ . Linear grouping with parameter $k$ sorts $I$ non-increasingly, cuts it into groups $G_1,\dots,G_q$ of $k$ consecutive pieces (the last possibly shorter), rounds every piece of $G_i$ up to the largest size of $G_i$ to get $G_i'$ , and outputs $J = \bigcup_{i\ge 2} G_i'$ and $J' = G_1$ .

ALGORITHM 1 takes $I$ and $\varepsilon>0$ : (1) discard the pieces of size $\le \max(1/n(I), \varepsilon/2)$ , leaving $J$ ; (2) apply linear grouping to $J$ with $k = \lceil n(J)\varepsilon^2\rceil$ , giving $K$ and $K'$ ; (3) put each piece of $K'$ in its own bin; (4) obtain from a Fractional Bin-Packing subroutine a basic feasible solution $x$ of the LP of $K$ with $\mathbf 1\cdot x\le LIN(K)+1$ ; (5) round $x$ to a packing of $K$ with at most $\mathbf 1\cdot x + (m(K)+1)/2$ bins; (6) shrink the pieces back to obtain a packing of $J$ ; (7) insert the discarded pieces, opening a new bin only when a piece fits nowhere. $A(I)$ is the cost of the resulting packing.

Formalization targets

Goal: Theorem 3, as its proof establishes it

A(I) \le (1+2\varepsilon)\,OPT(I) + \frac{1}{2\varepsilon^2} + 3 \qquad\text{for every } \varepsilon>0,\ \text{every instance } I,\ \text{every run of ALGORITHM 1.}

The additive term depends on $\varepsilon$ only, so ALGORITHM 1 is an asymptotic approximation scheme. The paper prints the factor $1+\varepsilon$ , which fails for ALGORITHM 1 as printed (see Formalization scope); running the algorithm with $\varepsilon/2$ gives the paper's main result (4), $A(I)\le(1+\varepsilon)OPT(I)+O(\varepsilon^{-2})$ , stated as a separate corollary with the explicit term $2/\varepsilon^2+3$ .

Milestones

Lemma 1: $OPT(I)\le 2\,SIZE(I)+1$ .
Lemma 2: $SIZE(I)\le LIN(I)\le OPT(I)\le LIN(I)+\frac{m(I)+1}{2}$ .
Corollary 1: every basic feasible solution $x$ can be rounded to a packing of cost $\le \mathbf 1\cdot x + \frac{m(I)+1}{2}$ .
Lemma 3: inserting pieces of size $\le g/2$ last, with new bins only when necessary, costs at most $\max(A, (1+g)\,OPT(I)+1)$ .
Monotonicity: $I\le J$ implies $OPT$ , $LIN$ and $SIZE$ do not decrease.
Lemma 4: linear grouping loses at most $k$ in $OPT$ , $LIN$ and $SIZE$ .
Proof steps (ii)–(iii) (corrected): $k\le 2\varepsilon\,OPT(I)+1$ .
Proof step (iv): $m(K)\le 1/\varepsilon^2$ .
Proof step (vii): $\mathbf 1\cdot x\le OPT(I)+1$ .
Proof step (viii) (corrected): the packing of Step 6 has at most $(1+2\varepsilon)OPT(I)+\frac{1}{2\varepsilon^2}+\frac52$ bins.

Significance

The result showed that the configuration LP, of exponential size in general, can be used for a guaranteed approximation: its value is within $(m+1)/2$ of the integer optimum, and grouping reduces $m$ at small cost. The same template (eliminate small items, group, solve the configuration LP, round a basic solution, reinsert) underlies later schemes for bin packing, cutting stock, bin packing with cardinality constraints and scheduling, and the LP-based analysis is the starting point of the Rothvoß and Hoberg–Rothvoß improvements.

The theorems are proved in the literature; none of them has a machine-checked proof on the platform or, to our knowledge, in Mathlib. This mission produces a checked analysis of the algorithm, including a correction: the printed approximation factor is not valid for the algorithm as printed, and the checked statement records the factor its proof yields. The definitions (instances, packings, the configuration LP, basic solutions, the order $I\le J$ , any-fit insertion) are reusable for the second mission of the series and for other bin-packing results.

Difficulty

The Lean statements are short, but several proofs need linear-programming structure that is not in Mathlib in this form. Lemma 2 and Corollary 1 use that an extreme point of $\{x\ge0,\ Ax\ge b\}$ has at most as many nonzero coordinates as there are rows of $A$ ; the configuration LP is indexed by a finite but implicitly described set of multisets. Monotonicity of $LIN$ under $I\le J$ ("clearly" in the paper) requires transporting a fractional solution across a piece-to-piece matching whose images are types, not pieces. The existence of a run requires an optimal basic feasible solution of the configuration LP. Lemma 3 concerns an insertion process with unrestricted order and bin choice, so its bound has to hold for every execution, not for one greedy rule.

Formalization scope

Sizes are real numbers in the open interval $(0,1)$ ; the paper says "a rational number between 0 and 1". Real sizes generalize rational ones; the open interval is what the paper's arguments use.
Instances are Multiset ℝ; packings are Multiset (Multiset ℝ) with join equal to the instance, bin loads at most $1$ , empty bins allowed and counted. $OPT$ is a natural-number infimum over a set that is always nonempty.
LP solutions are Multiset ℝ →₀ ℝ supported on configurations. $LIN$ is a real infimum over a set that is nonempty (singleton configurations) and bounded below by $0$ . "Basic" is the extreme-point property; the bound on the number of nonzero coordinates is a consequence, not the definition.
The Fractional Bin-Packing subroutine is modelled by its contract only (§5, p. 315): any basic feasible solution of cost at most $LIN(K)+1$ . The ellipsoid method of §6 is not modelled.
ALGORITHM 1 is a relation Alg1Run ε I P: $P$ is a possible output. Every open choice is quantified: the subroutine's output, the packing of Step 5 (any packing within the stated bound), the size reduction of Step 6 (bin by bin), and the insertion of Step 7 (any order, any fitting bin). The goal holds for every run, and a separate item states that a run exists, so the goal is not vacuous.
The paper's $O(\cdot)$ in result (4) is replaced by the explicit $2/\varepsilon^2+3$ .
Corrected statements. The printed Theorem 3 bound $(1+\varepsilon)OPT(I)+\frac{1}{2\varepsilon^2}+3$ fails: for $\varepsilon=1/10$ and $19\,000$ pieces of size $0.051$ , some run uses $1180$ bins while the bound is $1153$ . The failing step is (ii), $SIZE(J)\ge\varepsilon\,n(J)$ , since Step 1 discards only pieces $\le\varepsilon/2$ . Steps (ii)–(iii) and (viii) are stated with $2\varepsilon$ ; step (iv) is stated as $m(K)\le 1/\varepsilon^2$ because its first link $m(K)\le n(K)/k$ fails when the last group is short.
Running time (Theorem 3's first half, Corollary 1's time bound, the function $T$ ) is out of scope.
Trivializations are ruled out: "some packing has at most the bound" is not the goal; the goal constrains every output of the algorithm, and the packing property of that output is part of its conclusion.

Proofs of any item are welcome; Lemma 2, Corollary 1 and the monotonicity display are the most reusable.

Selected references

N. Karmarkar, R. M. Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd FOCS (SFCS 1982), IEEE, pp. 312–320. https://doi.org/10.1109/sfcs.1982.61
W. Fernandez de la Vega, G. S. Lueker, Bin packing can be solved within 1+ε in linear time, Combinatorica 1 (1981) 349–355. https://doi.org/10.1007/BF02579456
P. C. Gilmore, R. E. Gomory, A Linear Programming Approach to the Cutting-Stock Problem, Operations Research 9 (1961) 849–859. https://doi.org/10.1287/opre.9.6.849
D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM J. Comput. 3 (1974) 299–325. https://doi.org/10.1137/0203025
R. Hoberg, T. Rothvoß, A Logarithmic Additive Integrality Gap for Bin Packing, Proc. SODA 2017, 2616–2625. https://doi.org/10.1137/1.9781611974782.172

16 thms2 active usersReviewed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems I: Optimal Competitiveness of Randomized Block Snoopy CachingResearch Paper

Motivation

In a shared-memory multiprocessor, each processor keeps copies of memory blocks in its own cache, and all caches listen ("snoop") on a common bus. Every bus cycle spent keeping these copies consistent is a cycle not available for useful work, so the protocol that decides when a block is shared by several caches and when it is private to one cache directly controls bus traffic. The decision has to be made on-line, without knowing which processor will touch the block next.

Karlin, Manasse, Rudolph and Sleator (Algorithmica 1988) introduced competitive analysis for this problem and gave a deterministic algorithm with competitive ratio $2$ , which is optimal among deterministic algorithms. Karlin, Manasse, McGeoch and Owicki (Algorithmica 1994) showed that randomization helps: against an oblivious adversary the optimal ratio for block snoopy caching is $e_p/(e_p-1)$ , where $p$ is the cost of transferring a block. The same paper develops a general method for "nonuniform" problems, in which some state transitions are much more expensive than others, and the snoopy-caching result is its first application.

Setting

Fix $n$ processors and one memory block $B$ holding $p-1$ variables; transferring $B$ over the bus costs $p$ bus cycles. The block is in one of $n+1$ states: shared between all caches, or private to the cache of processor $i$ .

A request is a read $\mathrm{R}_i$ or a write $\mathrm{W}_i$ by processor $i$ . Moving from a private state to any other state costs $p$ ; moving from the shared state is free. A read $\mathrm{R}_i$ costs $0$ if $B$ is shared or private to $i$ and $+\infty$ otherwise. A write $\mathrm{W}_i$ costs $0$ if $B$ is private to $i$ , $1$ if $B$ is shared (one bus cycle broadcasts the new value), and $+\infty$ otherwise.

Before request $j$ the system is in state $s_{j-1}$ . A read is a look-ahead-one request: the algorithm may change state at the moment of the request, after seeing it. A write is a look-ahead-zero request: it is served in whatever state the system is in. After either kind, the algorithm may move again. The cost of a request is the cost of the move to the serving state, plus the task cost there, plus the cost of the move afterwards. Every write is preceded by a read to the same block, so in an admissible sequence each write $\mathrm{W}_i$ directly follows $\mathrm{R}_i$ or $\mathrm{W}_i$ .

The off-line optimum $C_{opt}(s_0,\sigma)$ is the least total cost of serving $\sigma$ from the initial state $s_0$ with full knowledge of $\sigma$ . A randomized on-line algorithm $A$ is a probability distribution over deterministic on-line algorithms; its expected cost on $\sigma$ is $\mathbf{E}C_A(\sigma)$ . $A$ is $c$ -competitive against an oblivious adversary from $s_0$ if there is a constant $a$ with

\mathbf{E}C_A(\sigma)\le c\cdot C_{opt}(s_0,\sigma)+a

for every admissible $\sigma$ . Put

e_p=\left(1+\frac1p\right)^p .

Formalization targets

Goal: Theorem 4

For $n\ge 2$ , $p\ge 1$ and every initial state $s_0$ :

\Big(\forall A\ \forall c:\ A \text{ is } c\text{-competitive from } s_0 \Rightarrow c\ge \tfrac{e_p}{e_p-1}\Big)\ \wedge\ \exists A:\ A \text{ is } \tfrac{e_p}{e_p-1}\text{-competitive from } s_0 .

The two conjuncts are milestones of their own: the lower bound (Theorem 4, first claim) and attainment (Theorem 4, second claim).

The phase linear program (§3.2, pp. 552–554)

For $p\ge1$ , real $\pi_1,\dots,\pi_{p+1}$ with $\pi_{p+1}=1$ , and real $\alpha$ with

\pi_{k+1}p+\sum_{i=1}^{k}(1-\pi_i)\le\alpha k\qquad(k=0,\dots,p),

one has $\alpha\ge e_p/(e_p-1)$ . Conversely, at $\alpha=e_p/(e_p-1)$ the choice $\pi_k=(\alpha-1)\big(((p+1)/p)^{k-1}-1\big)$ satisfies $\pi_{p+1}=1$ , $0\le\pi_1\le\dots\le\pi_{p+1}$ , and makes every constraint an equality.

Significance

The theorem settles the randomized competitive ratio of block snoopy caching exactly: $2$ at $p=1$ , $9/5$ at $p=2$ , decreasing to $e/(e-1)\approx1.582$ as $p\to\infty$ , against the deterministic optimum $2$ . The same ratio $e/(e-1)$ is the randomized optimum for the continuous ski-rental and spin-block problems treated later in the paper, and the snoopy-caching case is its discrete counterpart with ratio $e_p/(e_p-1)$ . The phase-LP method used here recurs in the paper's two-server results.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of the snoopy-caching task system with look-ahead-zero requests, of randomized algorithms against an oblivious adversary with infinite task costs allowed, and of the off-line optimum, together with the exact optimal ratio. The platform's fractional ski-rental result (PrimalDualOnline.SkiRental.fractional_competitive) proves an $e_B/(e_B-1)$ bound for a different model: one deterministic fractional algorithm, with no lower bound over randomized algorithms. It is related work, not a special case.

Difficulty

The linear program is elementary. The gap is between the LP and the algorithms. The paper's lower bound reduces arbitrary randomized algorithms to phase-based ones, whose state distribution at the end of each phase agrees with the optimal algorithm's known state, and whose behaviour inside a phase depends only on the number of writes so far. This reduction (Theorems 1 and 3 of the paper, pp. 545–549) is where the argument is not routine. An algorithm may keep the block private to a processor that is not the active one, may randomize over histories rather than over phase lengths, and the off-line optimum is not a sum of per-phase costs at the ends of the sequence. The obvious approach, bounding a single adversarial phase, does not suffice, because an algorithm may pay more in one phase and recover it in the next; the additive constant $a$ and the infinite horizon have to be handled. For attainment, the mixture of threshold algorithms must be written as a genuine distribution over on-line algorithms, with the initial phase from a private state absorbed into the additive constant.

Formalization scope

Everything lives in the namespace NonuniformCompetitive.Snoopy. States are Option (Fin n) (none = shared). Costs are in ℝ≥0∞; $+\infty$ is a genuine outcome, so an algorithm that ever pays $+\infty$ with positive probability on an admissible sequence is not competitive. A deterministic on-line algorithm is a pair of functions of the request prefix (the state at the moment of the last request, and the state after it), with the look-ahead-zero rule as a field. Moves "immediately before" a request are made without knowledge of it and are recorded as moves after the previous request. A randomized algorithm is a probability space with a measurable cost on every sequence, and its expected cost is a lower Lebesgue integral. The off-line optimum is an infimum in ℝ≥0∞ over schedules starting in $s_0$ ; it is finite on admissible sequences.

Conventions added to the printed statement, all from the paper's setting: (i) $n\ge2$ , since with one processor the block can stay private for free; (ii) one block, since the proof of Theorem 4 splits a multi-block system into independent blocks (p. 551); (iii) admissibility in the form "each write of $i$ directly follows a read or write of $i$ ", the reading of "every write is preceded by a read to the same block" that the proof uses; without it every algorithm is defeated by a write from a processor whose block copy was invalidated; (iv) $p\in\mathbb{N}$ , $p\ge1$ ; (v) both claims from every initial state, with an additive constant depending on $n$ , $p$ , $s_0$ .

The lower bound is over all randomized algorithms, not over phase-based or deterministic ones; a statement restricted to phase-based algorithms, or the LP alone in place of the goal, would not be Theorem 4. The LP variables are free, as in the paper.

Welcome contributions: a formal version of the phase reduction (Theorems 1 and 3 of the paper) for this task system, which is reusable for the paper's other nonuniform problems; the threshold algorithms and their mixture; and a proof that the off-line optimum decomposes by write runs up to a bounded error.

Selected references

A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), 542–571. https://doi.org/10.1007/BF01189993
A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3 (1988), 79–119. https://doi.org/10.1007/BF01762111
A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Revenue Management Under the Markov Chain Choice Model IV: Dimension Reduction Recovers a Choice-Based Solution with at Most n+1 Nested Offer SetsResearch Paper

Motivation

In network revenue management a firm sells $n$ products that consume $m$ capacitated resources over $T$ periods, and in each period it chooses which offer set of products to make available. When customers choose among the offered products according to a choice model, the standard planning tool is the choice-based linear program, which assigns a frequency $u_S\ge 0$ to every offer set $S\subseteq N$ (Liu and van Ryzin 2008). It has $2^n$ variables. Its optimal solution is what the firm actually implements: a randomization over offer sets.

For the Markov chain choice model of Blanchet, Gallego and Goyal (2016), Feldman and Topaloglu (2017) show that the choice-based program is equivalent to a reduced linear program with only $2n$ variables. The reduced program can be solved directly, but its solution is a pair of vectors $(\hat x,\hat z)$ , not a randomization over offer sets. This mission formalizes the paper's Section 7, which converts the reduced solution back into a randomization over offer sets: the Dimension Reduction algorithm, and Theorem 9, which says that the algorithm produces at most $n+1$ offer sets and that these sets are nested.

Setting

Products are indexed by $N=\{1,\dots,n\}$ . A customer arrives wanting product $j$ with probability $\lambda_j$ . If the product she visits is offered, she buys it. Otherwise she moves to product $i$ with probability $\rho_{j,i}$ , and leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$ . Throughout, $\lambda_j>0$ , $\rho_{j,i}\ge0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j,i$ .

For an offer set $S\subseteq N$ , the (Balance) equations

P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S

have a unique solution. $P_{j,S}$ is the probability that product $j$ is purchased, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. Write $P_S=(P_{j,S})_j$ and $R_S=(R_{j,S})_j$ .

The set $\mathcal H$ consists of all pairs $(x,z)\in\mathbb R^n\times\mathbb R^n$ with $x,z\ge0$ and $x_j+z_j=\lambda_j+\sum_{i}\rho_{i,j}z_i$ for all $j$ . The (Reduced) linear program maximizes $\sum_j T r_j x_j$ over $(x,z)\in\mathcal H$ subject to the capacity rows $\sum_j T a_{q,j}x_j\le c_q$ for each resource $q$ .

The Dimension Reduction algorithm starts from the optimal solution $(\hat x,\hat z)$ of (Reduced) and sets $(x^1,z^1)=(\hat x,\hat z)$ . At iteration $k$ it forms $S^k=\{j: x^k_j>0\}$ . It stops with $\alpha^k=1$ if $S^k=\emptyset$ . Otherwise it sets $\alpha^k=\min\{x^k_j/P_{j,S^k}: j\in S^k\}$ , stops if $\alpha^k=1$ , and if not updates

x^{k+1}_j=\frac{x^k_j-\alpha^kP_{j,S^k}}{1-\alpha^k},\qquad z^{k+1}_j=\frac{z^k_j-\alpha^kR_{j,S^k}}{1-\alpha^k}.

The weights are $\gamma^k=(1-\alpha^1)\cdots(1-\alpha^{k-1})\alpha^k$ .

Formalization targets

Goal: Theorem 9

Let $(\hat x,\hat z)$ be optimal for (Reduced). The algorithm stops at some first iteration $K$ with $1\le K\le n+1$ . At that $K$ ,

\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},\qquad \sum_{k=1}^K\gamma^k=1,\qquad S^1\supseteq S^2\supseteq\cdots\supseteq S^K .

Milestones

In the order the proof uses them:

(Balance) has a unique, nonnegative solution for every $S$ (p. 1325).
$P_{j,S}>0$ for $j\in S$ (p. 1325).
For $(\hat x,\hat z)\in\mathcal H$ : $\hat z_j\ge R_{j,S_{\hat x}}$ . This is Lemma 11 of the online appendix, as quoted on p. 1332.
For $(\hat x,\hat z)\in\mathcal H$ with nonempty support: $\alpha_{\hat x}\le1$ (p. 1332).
The two stopping configurations are (Balance) solutions: $S_{\hat x}=\emptyset$ gives $(P_\emptyset,R_\emptyset)$ , and $\alpha_{\hat x}=1$ gives $(P_{S_{\hat x}},R_{S_{\hat x}})$ (p. 1332).
Lemma 8: one step of the algorithm maps $\mathcal H$ into $\mathcal H$ and removes a minimizing index from the support (p. 1333).
The iterates stay in $\mathcal H$ , and $S^{k+1}\subseteq S^k\setminus\{j^k\}$ (pp. 1333–1334).

Significance

Theorem 9 makes the reduced program usable. Together with the equivalence of (Reduced) and the choice-based program, it produces an optimal choice-based solution that offers at most $n+1$ sets. By a basic-solution count the choice-based program has an optimal solution with at most $m+1$ nonzero offer sets. Theorem 9 bounds the number by the number of products instead, and adds a structural property: the offered sets form a chain. Each set is contained in the previous one, so the implemented policy offers a single nested sequence of assortments. The algorithm needs at most $n+1$ solutions of linear systems of size $n$ . It never enumerates offer sets.

The result is proved in the paper. As far as a search of the platform and of Mathlib shows, it has not been formalized. Mathlib's Carathéodory theorem (Analysis/Convex/Caratheodory) bounds the number of points in a convex combination. It does not construct this decomposition, and it does not give nestedness. Formalizing Theorem 9 therefore requires the paper's argument: a verified, terminating peeling procedure on the polyhedron $\mathcal H$ whose output is a convex combination of (Balance) solutions indexed by a chain of sets.

Difficulty

The algorithm divides twice. Step 2 divides by $P_{j,S^k}$ , which must be positive on $S^k$ . Step 3 divides by $1-\alpha^k$ , which must be nonzero whenever the algorithm continues. Both rest on nontrivial facts: the positivity of purchase probabilities, and the bound $\alpha\le1$ on $\mathcal H$ . That bound in turn requires the comparison $\hat z\ge R_{S_{\hat x}}$ . The paper proves this comparison only in its online appendix; it is a monotonicity property of the inverse of $I-\rho^\top$ restricted to the unoffered products. The update of Step 3 can make coordinates of $z$ negative unless this comparison holds, so the naive observation that " $(x^k,z^k)$ is a combination of points of $\mathcal H$ " does not by itself keep the iterates in $\mathcal H$ .

Termination is not a consequence of $\alpha^k<1$ alone. It needs the strict decrease of the support, which comes from choosing a minimizing index. The weights $\gamma^k$ are defined by products of the $(1-\alpha^l)$ . Their sum telescopes to $1$ only because the last step has $\alpha^K=1$ .

Formalization scope

Everything lives in the namespace MarkovChainChoice.DimReduction. Products are Fin n and offer sets are Finset (Fin n). The model is a structure carrying $\lambda_j>0$ , $\sum_i\rho_{j,i}<1$ and, as a disclosed implicit hypothesis, $\rho_{j,i}\ge0$ . The pair $(P_S,R_S)$ is chosen by Classical.epsilon among the solutions of (Balance); milestone 1 is what identifies it with the paper's unique solution. Revenues, capacities and consumptions carry no sign conditions. "Optimal for (Reduced)" means feasible and at least as good as every feasible point.

The iterates are indexed from $k=1$ as in the paper. The value at index $0$ is an unused copy of the input. "The algorithm stops at iteration $K$ " is the first $K\ge1$ with $S^K=\emptyset$ or $\alpha^K=1$ . Iterates after the first stop involve a division by zero, which Lean evaluates to $0$ , and no statement refers to them. The termination bound $K\le n+1$ is a conclusion of the goal, not a hypothesis. The goal is about the algorithm's actual iterates, not about an arbitrary sequence that satisfies the invariants. The paper's $\subset$ and $\supset$ denote non-strict inclusion and are rendered as $\subseteq$ and $\supseteq$ .

Two milestones are stated more generally than the page. The paper states the iteration invariants for the (Reduced) optimum; the Lean requires only $(\hat x,\hat z)\in\mathcal H$ , which every feasible (Reduced) solution satisfies. Lemma 8's $\arg\min$ may be a set; the statement holds for every minimizer. The page contains printed slips: on p. 1332, $\hat v_j$ has numerator $\hat x_j-\alpha R_{j,S}$ , and the paper writes $R_{\hat x}$ for $R_{S_{\hat x}}$ . The Lean uses the correct forms, as in Lemma 8 and Step 3. None of these slips appears in a milestone quotation.

A complete development needs a small theory of M-matrices, in the form of nonnegativity of $(I-Q)^{-1}$ for substochastic $Q$ , together with finite induction on supports. The comparison lemma (milestone 3) and the (Balance) existence and uniqueness result (milestone 1) are reusable across the other missions on this paper. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0169

14 thms2 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Single Machine Scheduling with Release Dates I: The Preemptive Time-Indexed and Mean Busy Time LP Relaxations Have the Same Optimal ValueResearch Paper

Motivation

Minimizing the total weighted completion time $\sum_j w_j C_j$ of jobs with release dates on a single machine, written $1\,|\,r_j\,|\,\sum w_j C_j$ in scheduling notation, is strongly NP-hard. Most constant-factor approximation algorithms for it, and for many related scheduling problems, follow one pattern: solve a linear programming relaxation, which gives a lower bound on the optimum, and round its solution into a schedule whose cost is compared with that bound. The quality of the algorithm is therefore limited by the quality of the relaxation, and the question of which relaxations are equivalent is a basic one for the method.

Two relaxations of $1\,|\,r_j\,|\,\sum w_j C_j$ are central. The time-indexed relaxation of Dyer and Wolsey (doi:10.1016/0166-218X(90)90104-K) has one variable per job and unit time slot, a pseudopolynomial number of variables. The mean busy time relaxation has one variable per job but one constraint per subset of jobs, the shifted parallel inequalities studied by Queyranne and others. Goemans, Queyranne, Schulz, Skutella and Wang (doi:10.1137/S089548019936223X, Section 2) show that both have the same optimal value, and that both are solved by one simple preemptive schedule. This mission formalizes that result, Corollary 2.6, together with the lemmas and theorems its proof uses.

Timeline:

1990: Dyer and Wolsey formulate several time-indexed relaxations of $1\,|\,r_j\,|\,\sum w_j C_j$ , among them the formulation (D) used here.
1993: Queyranne (doi:10.1007/BF01581271) describes the polyhedron of completion-time vectors on one machine without release dates by the parallel inequalities.
1994–1995: Queyranne and Schulz use shifted parallel inequalities in polyhedral approaches to machine scheduling with release dates.
1996: Goemans (IPCO, LNCS 1084) gives a supermodular relaxation for scheduling with release dates, the source of the canonical decompositions used for (R).
2002: Goemans, Queyranne, Schulz, Skutella and Wang prove that (D) and the mean busy time relaxation (R) have equal value, attained by the preemptive "LP schedule", and use this common bound for randomized approximation algorithms with ratios $1.7451$ and $1.6853$ .

Setting

There are $n$ jobs $N = \{1, \dots, n\}$ . Job $j$ has an integral processing time $p_j > 0$ , an integral release date $r_j \ge 0$ and a weight $w_j \ge 0$ . For a nonempty set $S$ of jobs, $p(S) = \sum_{j\in S} p_j$ and $r_{\min}(S) = \min_{j \in S} r_j$ .

A preemptive schedule gives each job a bounded measurable set $A_j \subseteq [r_j, \infty)$ of processing times of Lebesgue measure $p_j$ , the sets pairwise disjoint. The mean busy time of $j$ is $M_j = \frac{1}{p_j}\int_{A_j} t\,dt$ .

The LP schedule processes, at every moment, the available (released, unfinished) job of largest ratio $w_j/p_j$ , ties broken by index. With the jobs indexed so that $w_1/p_1 \ge \cdots \ge w_n/p_n$ , this is the available job of smallest index. As the data are integral, it runs one job or none in each unit slot $[\tau, \tau+1)$ ; $y^{LP}_{j\tau} \in \{0,1\}$ records whether it runs $j$ there, and $M^{LP}_j$ is its mean busy time of $j$ .

The preemptive time-indexed relaxation (D) with horizon $T$ has real variables $y_{j\tau} \ge 0$ for $\tau = r_j, \dots, T-1$ and reads

Z_D = \min \sum_j w_j C_j \quad\text{s.t.}\quad \sum_{j : r_j \le \tau} y_{j\tau} \le 1\ (\tau < T), \qquad \sum_{\tau=r_j}^{T-1} y_{j\tau} = p_j, \qquad C_j = \tfrac12 p_j + \tfrac{1}{p_j}\sum_{\tau=r_j}^{T-1}\big(\tau + \tfrac12\big) y_{j\tau}.

The mean busy time relaxation (R) reads

Z_R = \min \sum_j w_j\big(M_j + \tfrac12 p_j\big) \quad\text{s.t.}\quad \sum_{j\in S} p_j M_j \ge p(S)\big(r_{\min}(S) + \tfrac12 p(S)\big) \quad (\emptyset \ne S \subseteq N).

The horizon $T$ is required to bound the makespan of some feasible nonpreemptive schedule, for instance $T = \max_j r_j + \sum_j p_j$ .

Formalization targets

Goal: Corollary 2.6

For every instance, every weight vector $w \ge 0$ and every admissible horizon $T$ ,

Z_D = Z_R .

No ordering of the jobs and no reference to the LP schedule appear in the goal.

Milestones

Lemma 2.1. (D) has an optimal solution with $y_{j\tau} \in \{0,1\}$ .
Theorem 2.2. With the jobs sorted by $w_j/p_j$ , $y^{LP}$ is an optimal solution to (D).
Lemma 2.4. For every preemptive schedule and nonempty $S$ , $\sum_{j\in S} p_j M_j \ge p(S)\big(r_{\min}(S)+\tfrac12 p(S)\big)$ , with equality if and only if $S$ occupies $[r_{\min}(S), r_{\min}(S)+p(S))$ without interruption.
Theorem 2.5. With the jobs sorted by $w_j/p_j$ , $M^{LP}$ is an optimal solution to (R).
Eq. (2.6). $M^{LP}_j = \frac{1}{p_j}\sum_{\tau=r_j}^{T-1} y^{LP}_{j\tau}\big(\tau + \frac12\big)$ .

Significance

The equality $Z_D = Z_R$ lets one choose, for each purpose, the more convenient of the two relaxations. (D) is intuitive and a transportation problem, but has pseudopolynomially many variables; (R) has $n$ variables and a supermodular right-hand side, which the paper uses to describe its polyhedron. Theorems 2.2 and 2.5 show that the common optimum is attained by the LP schedule, which is computable greedily; the approximation guarantees of Section 3 of the paper, and of later work on $\alpha$ -point scheduling, are all measured against this value.

A formal development adds three things. First, a machine-checked model of preemptive single-machine schedules with release dates, of mean busy times, and of the LP schedule as a concrete recursive object, reusable by any formalization of $\alpha$ -point methods (two companion missions of this series use the same objects). Second, a formal statement of the two relaxations with honest optimal values. Third, verified proofs of results that are proved in the paper by short interchange and averaging arguments, whose measure-theoretic details (integrals over processing sets, null sets in the equality case) the paper leaves implicit. The results are proved in the literature; to our knowledge none of them has been machine-checked.

Difficulty

The paper's arguments are short, and each rests on a step that is informal on the page. Lemma 2.1 cites the integrality of transportation problems, a statement about the vertices of a polytope rather than a one-line fact. Theorem 2.2 ends with the claim that a 0/1 solution admitting no improving exchange "must correspond to the LP schedule", which is a property of the greedy rule that has to be derived from its definition. Theorem 2.5 depends on how the LP schedule arranges the jobs of each prefix $\{1, \dots, i\}$ of the sorted order in time; this is the only place sortedness enters, and it is again a property of the concrete schedule. Lemma 2.4 is an extremal statement about integrals over sets of prescribed measure, and its equality case holds only up to null sets. Finally, the goal concerns arbitrary, unsorted weights, while the two theorems it combines are about sorted indices, so the goal is not a direct conjunction of the milestones.

Formalization scope

Jobs are Fin n, numbered from $0$ ; $p_j$ , $r_j$ and the horizon $T$ are natural numbers and weights are real. A preemptive schedule is a family of processing sets $A_j \subseteq \mathbb R$ , not indicator functions. The LP schedule is defined by recursion on unit slots with the smallest-index rule; the sortedness of $w_j/p_j$ is a hypothesis of Theorems 2.2 and 2.5, not part of the definition. Variables of (D) are functions $y : \text{jobs} \times \mathbb N \to \mathbb R$ required to vanish outside $r_j \le \tau < T$ . $Z_D$ and $Z_R$ are infima of the objective over the feasible sets; under the stated hypotheses the feasible sets are nonempty and the objectives bounded below, so these are the LP values. Optimality in the milestones is stated as attaining the minimum, not through these infima.

The horizon hypothesis rules out the trivializing case in which (D) is infeasible and its infimum takes the junk value $0$ ; (D) is kept a linear program over real $y$ , since restricting to $\{0,1\}$ would make Lemma 2.1 vacuous. The running-time claim of Corollary 2.6 ( $O(n\log n)$ ) is not formalized.

A complete development needs: integrals of the identity over finite unions of intervals; a rearrangement lemma for sets of given measure; basic properties of the LP schedule (it is a preemptive schedule, it is work-conserving and finishes by any admissible $T$ , its blocks are canonical); and a relabelling argument. The schedule model and the LP-schedule lemmas are reusable for the companion missions on $\alpha$ -point scheduling. Contributions of any of these lemmas as separate theorems are welcome.

Selected references

M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single machine scheduling with release dates, SIAM Journal on Discrete Mathematics 15(2):165–192, 2002. doi:10.1137/S089548019936223X
M. E. Dyer, L. A. Wolsey, Formulating the single machine sequencing problem with release dates as a mixed integer program, Discrete Applied Mathematics 26(2–3):255–270, 1990. doi:10.1016/0166-218X(90)90104-K
M. Queyranne, Structure of a simple scheduling polyhedron, Mathematical Programming 58:263–285, 1993. doi:10.1007/BF01581271
M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proceedings of the 8th ACM-SIAM Symposium on Discrete Algorithms (SODA), 591–598, 1997.

10 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Revenue Management Under the Markov Chain Choice Model III: The Reduced Linear Program Is Equivalent to the Choice-Based Linear ProgramResearch Paper

Motivation

Network revenue management decides which products to make available to arriving customers when products share scarce resources: an airline sells itineraries (products) that consume seats on flight legs (resources), and each itinerary has a fare. When customers choose among the offered products, rather than asking for one fixed product, the standard planning tool is a deterministic linear program that replaces random choices by their expected values. Gallego, Iyengar, Phillips and Dubey (2004, Columbia CORC technical report TR-2004-01) and Liu and van Ryzin (2008) formulated this choice-based linear program; its solution drives bid-price and offer-set policies used in practice.

The difficulty is size. The choice-based program has one variable for each subset of products, $2^n$ in all, and is solved by column generation, whose pricing subproblem is itself an assortment problem. Feldman and Topaloglu (Oper. Res. 65(5), 2017) show that when customers choose under the Markov chain choice model of Blanchet, Gallego and Goyal (2016), the choice-based program is equivalent to a linear program with only $2n$ variables and $m+n$ constraints. This mission formalizes that equivalence, Theorem 7 of the paper.

Setting

There are $n$ products, $N=\{1,\dots,n\}$ . Under the Markov chain choice model a customer first visits product $j$ with probability $\lambda_j$ . If the product she visits is offered, she buys it. Otherwise she moves from product $j$ to product $i$ with probability $\rho_{j,i}$ , or leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$ . The paper assumes throughout that

\lambda_j>0\quad\text{and}\quad\sum_{i\in N}\rho_{j,i}<1\qquad\text{for all } j\in N.

For an offer set $S\subseteq N$ , $P_{j,S}$ is the expected number of visits to product $j$ while it is offered, which is its purchase probability, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. The pair $(P_S,R_S)$ is the solution of the (Balance) equations

P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S .

Dropping the constraints tied to $S$ gives the polyhedron

\mathcal H=\Big\{(x,z)\in\mathbb R^{2n}_+ : x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \ \forall j\in N\Big\}.

The network has $m$ resources, $M=\{1,\dots,m\}$ , with capacities $c_q$ ; the selling horizon has $T$ periods; product $j$ earns $r_j$ and consumes $a_{q,j}$ units of resource $q$ . With $u_S$ the probability of offering $S$ in a period, the (Choice Based) linear program is

\max_{u\in\mathbb R^{2^n}_+}\Big\{\sum_{S\subseteq N}\sum_{j\in N}T r_jP_{j,S}u_S:\ \sum_{S\subseteq N}\sum_{j\in N}Ta_{q,j}P_{j,S}u_S\le c_q\ \forall q\in M,\ \sum_{S\subseteq N}u_S=1\Big\},

and the (Reduced) linear program is

\max_{(x,z)\in\mathbb R^{2n}_+}\Big\{\sum_{j\in N}T r_jx_j:\ \sum_{j\in N}Ta_{q,j}x_j\le c_q\ \forall q\in M,\ x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \forall j\in N\Big\}.

In (Reduced), $x_j$ is the expected number of visits to product $j$ while it is available and $z_j$ the expected number of visits while it is not.

Formalization targets

Goal: Theorem 7

Let $(\hat x,\hat z)$ be an optimal solution of (Reduced). Then there are subsets $S^1,\dots,S^K\subseteq N$ and positive scalars $\gamma^1,\dots,\gamma^K$ with $\sum_k\gamma^k=1$ such that

\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},

and for any such subsets and scalars the vector $\hat u$ with $\hat u_{S^k}=\gamma^k$ and $\hat u_S=0$ for $S\notin\{S^1,\dots,S^K\}$ is optimal for (Choice Based), with objective value equal to that of $(\hat x,\hat z)$ in (Reduced). In particular the two programs have the same optimal value.

Milestones

(Balance) has a unique and nonnegative solution for every offer set (§2, p. 1325).
Lemma 1: an extreme point $(\hat x,\hat z)$ of $\mathcal H$ equals $(P_{S},R_{S})$ for $S=\{j:\hat x_j>0\}$ (p. 1326).
Lemma 10: $\mathcal H$ is bounded (quoted on p. 1331; proved in the online appendix).
Every point of $\mathcal H$ is a positive convex combination of finitely many extreme points of $\mathcal H$ (proof of Theorem 7, p. 1331).
Every feasible $u$ of (Choice Based) yields the feasible point $\tilde x_j=\sum_S P_{j,S}u_S$ , $\tilde z_j=\sum_S R_{j,S}u_S$ of (Reduced), with the same objective value (proof of Theorem 7, p. 1332).

Significance

The result. Theorem 7 replaces a program with $2^n$ columns by one with $2n$ variables and $m+n$ constraints, solvable directly by any LP solver, and it returns an optimal solution of the original program, not only its value. The optimal value is the standard upper bound on the optimal expected revenue of a network revenue management policy, and the dual variables of the capacity constraints are the bid prices used to control sales. The decomposition of part 1 is what turns the small program's solution back into offer-set frequencies that a policy can implement; Section 7 of the paper makes that decomposition algorithmic (a separate mission of this series).

Formalizing it. The theorem is proved in the paper; to the best of available knowledge no machine-checked version exists. A formal proof checks the link between polyhedral geometry (extreme points of $\mathcal H$ and the solutions of (Balance)) and linear-programming optimality, and records exactly which properties of the Markov chain choice model are used: the standing assumptions enter through uniqueness and nonnegativity of $(P_S,R_S)$ and through boundedness of $\mathcal H$ .

Difficulty

The inequality "(Reduced) $\ge$ (Choice Based)" is a direct computation: averaging the (Balance) equations with weights $u_S$ lands in $\mathcal H$ . The reverse direction is where the obvious argument fails. A point of $\mathcal H$ has no offer set attached to it, and a general polyhedron need not be the convex hull of its extreme points: it can contain lines or rays. The argument requires that $\mathcal H$ is bounded, which depends on the substochasticity $\sum_i\rho_{j,i}<1$ , and that each extreme point is exactly some $(P_S,R_S)$ , which uses the structure of the balance equations and the uniqueness of their solution. Neither follows from general linear-programming facts. In Lean, the finite vertex representation of a bounded polyhedron is also not a one-line consequence of Mathlib's Krein–Milman theorem, which gives only the closure of the convex hull.

Formalization scope

Products are Fin n, offer sets Finset (Fin n), resources Fin m. The model is a structure Model n holding $\lambda$ , $\rho$ (rho j i $=\rho_{j,i}$ , the transition from $j$ to $i$ ) and the standing assumptions $\lambda_j>0$ and $\sum_i\rho_{j,i}<1$ ; the nonnegativity $\rho_{j,i}\ge0$ , implicit in the paper because the $\rho_{j,i}$ are probabilities, is an added field. $(P_S,R_S)$ is a solution of (Balance) chosen by Classical.epsilon, and milestone 1 is what identifies it with the paper's unique solution. $\mathcal H$ is a subset of (Fin n → ℝ) × (Fin n → ℝ), extreme points are Mathlib's Set.extremePoints ℝ, and boundedness is Bornology.IsBounded. $T$ is a natural number entering as a real factor exactly where the paper writes it; $c$ , $a$ , $r$ carry no sign conditions, as in the paper. "Optimal solution" means feasible and at least as good as every feasible point; no supremum is used.

Two conventions are disclosed. The paper defines $\hat u$ by $\hat u_{S^k}=\gamma^k$ ; the formalization sets $\hat u_S=\sum_{k:S^k=S}\gamma^k$ , which agrees when the $S^k$ are distinct and is the only consistent reading otherwise. Milestone 5 is stated for every feasible $u$ of (Choice Based), while the paper applies it to an optimal one; its argument uses only feasibility. No printed statement needed correction.

The goal is not only the decomposition of part 1, which is milestones 2 and 4 combined: it also asserts optimality of $\hat u$ and equality of the optimal values, and a formalization that drops part 2 does not state Theorem 7. Part 2 is required for every decomposition, and part 1 guarantees one exists, so part 2 is not vacuous.

A complete development needs the vertex representation of polytopes (reusable beyond this mission; LinearOptimization.polyhedron_resolution on the platform proves the resolution theorem in another encoding), the theory of substochastic matrices behind (Balance) (invertibility of $I-\bar Q$ with a nonnegative inverse), and finite-sum manipulations over Finset (Fin n). Contributions to any milestone, and bridges to existing polyhedral results, are welcome.

Selected references

J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0172
G. Gallego, G. Iyengar, R. Phillips, A. Dubey, Managing Flexible Products on a Network, Computational Optimization Research Center Technical Report TR-2004-01, Columbia University, 2004 (technical report; no DOI).
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Revenue Management Under the Markov Chain Choice Model I: The Dual Linear Program Yields an Optimal AssortmentResearch Paper

Motivation

A retailer or an airline decides which products to make available, and customers choose among what is offered. When a preferred product is missing, many customers substitute to another product instead of leaving. Assortment optimization asks which subset of products to offer so that the expected revenue from a customer is as large as possible, and its answer depends entirely on the choice model used to describe substitution.

The Markov chain choice model was introduced by Blanchet, Gallego and Goyal (EC 2013; Oper. Res. 64(4), 2016), who showed that it contains the multinomial logit model as a special case and proposed it as an approximation of general random-utility choice models. Feldman and Topaloglu (Oper. Res. 65(5), 2017) study revenue management under this model. Their first result, the subject of this mission, is that the assortment problem, a search over all $2^n$ offer sets, is solved by one linear program with $n$ variables. The same paper uses this result for its dynamic single-resource and network results, which are the subjects of the companion missions II–IV of this series.

Timeline:

2013/2016: Blanchet, Gallego and Goyal introduce the model and give a polynomial-time assortment algorithm.
2017: Feldman and Topaloglu show that the optimal assortment is read off an optimal solution of a dual linear program (their Theorem 2), and derive structural and capacity-control consequences.

Setting

There are $n$ products $N=\{1,\dots,n\}$ . A customer arrives to purchase product $j$ with probability $\lambda_j$ . If the product she visits is offered, she buys it. Otherwise she transitions to product $i$ with probability $\rho_{j,i}$ and checks whether $i$ is offered, or leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$ . Throughout, $\lambda_j>0$ , $\rho_{j,i}\ge0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j$ .

For an offer set $S\subseteq N$ , let $P_{j,S}$ be the expected number of visits to product $j$ while it is offered (the probability that $j$ is purchased) and $R_{j,S}$ the expected number of visits to $j$ while it is not offered. The pair $(P_S,R_S)$ is the unique solution of the (Balance) equations

P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S .

With revenue $r_j\in\mathbb R$ for product $j$ , the (Assortment) problem is $\max_{S\subseteq N}\sum_{j\in N}P_{j,S}r_j$ . Two linear programs enter: the maximization of $\sum_j r_jx_j$ over the polyhedron

\mathcal H=\Big\{(x,z)\in\mathbb R^{2n}_+:\ x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \ \forall j\in N\Big\},

and its dual

\min_{v\in\mathbb R^n}\Big\{\sum_{j\in N}\lambda_jv_j:\ v_j\ge r_j\ \ \forall j\in N,\ \ v_j\ge\sum_{i\in N}\rho_{j,i}v_i\ \ \forall j\in N\Big\}.\qquad\text{(Dual)}

Formalization targets

Goal: Theorem 2 (p. 1326)

For every optimal solution $\hat v$ of (Dual), the set $\hat S=\{j\in N:\hat v_j=r_j\}$ is an optimal assortment:

\sum_{j\in N}P_{j,S}\,r_j\ \le\ \sum_{j\in N}P_{j,\hat S}\,r_j\qquad\text{for all } S\subseteq N .

Milestones, in the order the paper uses them

(p. 1325) The (Balance) equations have a unique nonnegative solution for every $S$ .
Lemma 1 (p. 1326): for an extreme point $(\hat x,\hat z)$ of $\mathcal H$ and $S_{\hat x}=\{j:\hat x_j>0\}$ , $P_{j,S_{\hat x}}=\hat x_j$ and $R_{j,S_{\hat x}}=\hat z_j$ for all $j$ .
(p. 1326) The linear program over $\mathcal H$ has an optimal solution, and its optimal value equals the optimal value of (Assortment).
(p. 1326) (Dual) has an optimal solution, and its optimal value equals that of the linear program over $\mathcal H$ .
(p. 1326, proof of Theorem 2) An optimal $\hat v$ satisfies $\hat v_j=r_j$ or $\hat v_j=\sum_i\rho_{j,i}\hat v_i$ for each $j$ .

Significance

Theorem 2 reduces a combinatorial problem over $2^n$ offer sets to a linear program, so the assortment problem under the Markov chain choice model is solvable in polynomial time. The same structure drives the rest of the paper: the dual variables $\hat v_j$ are used to show that optimal offer sets shrink when all revenues fall by a common amount, to show that the optimal offer sets of the single-resource dynamic program are nested in the remaining capacity and time, and to reduce the choice-based network linear program to a compact one.

The result is proved in the paper. This mission produces a machine-checked version of it and of its supporting lemmas; to the knowledge of the mission author no formalization of the Markov chain choice model exists. The definition layer (the model, the (Balance) solution, $\mathcal H$ and (Dual)) is the first formal encoding of this choice model and is shared, with the same encoding, by missions II–IV.

Difficulty

The obvious route, comparing $\sum_jP_{j,S}r_j$ across offer sets directly, fails because $P_{j,S}$ is defined only implicitly through a linear system whose coefficient matrix changes with $S$ ; there is no closed-form expression that can be compared across offer sets, and enumerating the $2^n$ sets is exponential. The connection to linear programming needs an exact correspondence between the vertices of $\mathcal H$ and the (Balance) solutions, which is a statement about polyhedra, not about Markov chains. Even well-posedness is not free: existence, uniqueness and nonnegativity of $(P_S,R_S)$ depend on the row sums $\sum_i\rho_{j,i}$ being strictly below one. Mathlib has extreme points of convex sets but no ready-made theory of vertices of polyhedra or of linear programming duality in this form.

Formalization scope

Products are Fin n (0-based), offer sets are Finset (Fin n) (the paper's $S\subset N$ is non-strict inclusion, so every subset including $\emptyset$ and $N$ is an offer set), and rho j i is $\rho_{j,i}$ , the transition from $j$ to $i$ . The model structure carries the paper's standing assumptions $\lambda_j>0$ and $\sum_i\rho_{j,i}<1$ (p. 1325) and the implicit nonnegativity $\rho_{j,i}\ge0$ . Revenues are arbitrary reals with no sign assumption. $\mathbb R^{2n}$ is (Fin n → ℝ) × (Fin n → ℝ), and extreme points are Mathlib's Set.extremePoints ℝ.

The pair $(P_S,R_S)$ is a solution of (Balance) chosen by Classical.epsilon; milestone 1 states that it satisfies (Balance), is nonnegative and equals every solution, so all statements are about the paper's $(P_S,R_S)$ and not about a junk value. Every optimum (of (Assortment), of the linear program over $\mathcal H$ , of (Dual)) is stated as "feasible and at least as good as every feasible point", never through sSup or sInf. The goal is stated for every optimal $\hat v$ of (Dual), which is what the proof uses; uniqueness of $\hat v$ is neither assumed nor claimed. Replacing the hypothesis " $\hat v$ optimal for (Dual)" by " $\hat v$ feasible for (Dual)" would make the statement false, and an existential over $\hat v$ would weaken it; neither is the target.

No hypothesis beyond the paper's is added. Two printed index slips on pp. 1325–1326 (a garbled sum in the discussion after (Balance), and $\sum_i\rho_{i,j}\hat z_j$ for $\sum_i\rho_{i,j}\hat z_i$ in the proof of Lemma 1) are not part of any statement here.

Welcome contributions: the existence and uniqueness of (Balance) solutions via Neumann series for substochastic matrices, a characterization of vertices of polyhedra given by equality constraints and nonnegativity, and a strong duality statement usable for this primal–dual pair. These are reusable well beyond this mission.

Selected references

J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

8 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis II: Local Optimality for Integrally Convex FunctionsTextbook

Motivation

For a convex function on $\mathbb R^n$ , a point is a global minimizer as soon as it is a local minimizer — this is one of the earliest and most consequential facts of convex analysis, and it underlies why local-search and gradient methods can certify global optimality in convex programs. The discrete analogue is not automatic: a function on the integer lattice $\mathbb Z^n$ can be "locally optimal" with respect to any fixed finite neighborhood system and still fail to be a global minimizer, unless the function's discrete structure is compatible with that neighborhood in the right way. Identifying exactly which classes of lattice functions admit a local-to-global optimality principle, and with respect to which neighborhood, is one of the organizing questions of discrete convex analysis.

Integrally convex functions, introduced by Favati and Tardella (1990) and developed systematically by Murota, are the most general class of $\mathbb Z^n$ -valued functions for which such a principle holds. They are defined purely in terms of the classical convex closure of a real relaxation, which lets one import theorems from ordinary convex analysis, but the resulting notion of local optimality — checking only the $3^n - 1$ neighbors obtained by independently nudging each coordinate by $-1$ , $0$ , or $+1$ (excluding the trivial no-change case) — is a genuinely discrete, dimension-independent statement about functions whose domain can be arbitrarily large. Almost every discrete convex function class studied later in the book, including M-convex and L-convex functions, is a special case of integral convexity, and this mission's goal theorem is the direct ancestor of the optimality criteria (Theorems 6.26 and 7.14) that drive the algorithms in the rest of the book.

Setting

Let $f : \mathbb Z^n \to \mathbb R \cup \{+\infty\}$ be a function with nonempty effective domain $\operatorname{dom}_{\mathbb Z} f = \{x \in \mathbb Z^n : f(x) \ne +\infty\}$ . The convex closure of $f$ is

\bar f(x) = \sup_{p \in \mathbb R^n,\, \alpha \in \mathbb R} \{\langle p,x\rangle + \alpha : \langle p,y\rangle + \alpha \le f(y)\ \forall y \in \mathbb Z^n\} \qquad (x \in \mathbb R^n),

the pointwise supremum of every affine function minorizing $f$ on all of $\mathbb Z^n$ . If $\bar f$ agrees with $f$ on integer points, $f$ is convex extensible. The integral neighborhood of $x \in \mathbb R^n$ is

N(x) = \{y \in \mathbb Z^n : \lfloor x_i \rfloor \le y_i \le \lceil x_i \rceil,\ 1 \le i \le n\},

and the local convex extension $\tilde f$ relaxes $\bar f$ 's definition by requiring the affine minorant condition only on $N(x)$ rather than on all of $\mathbb Z^n$ . Always $\tilde f \ge \bar f$ pointwise, and the two agree on $\mathbb Z^n$ . A function $f$ is integrally convex if $\tilde f = \bar f$ everywhere on $\mathbb R^n$ — equivalently, if $\tilde f$ is a convex function on all of $\mathbb R^n$ (it is automatically convex on every unit cube $[z, z+1]^n$ with $z \in \mathbb Z^n$ , but need not be convex globally without this extra condition).

A discrete set $S \subseteq \mathbb Z^n$ is hole free if $S$ equals the set of integer points in its own real convex hull, and $\arg\min f[-p]$ denotes the minimizer set, over $\mathbb Z^n$ , of the linearly perturbed function $f[-p](x) = f(x) - \langle p,x\rangle$ .

Formalization targets

Goal: Theorem 3.21 (local optimality characterizes global optimality)

For integrally convex $f$ and $x \in \operatorname{dom}_{\mathbb Z} f$ :

f(x) \le f(y)\ (\forall y \in \mathbb Z^n) \iff f(x) \le f(x + \chi_Y - \chi_Z)\ (\forall\, Y, Z \subseteq \{1,\dots,n\}),

where $\chi_Y \in \{0,1\}^n$ is the indicator vector of $Y$ . The right-hand side is a check over at most $3^n - 1$ points (each coordinate independently unchanged, incremented, or decremented), regardless of how large $\operatorname{dom}_{\mathbb Z} f$ is; this uniform, dimension-only bound is the entire content of the theorem, and is the weakest correct formulation — restricting to a single $(Y,Z)$ or letting the right-hand side range over all of $\mathbb Z^n$ would trivialize or falsify the equivalence.

Milestones: Propositions 3.18 and 3.19

Proposition 3.18: $f$ convex extensible $\implies$ $\arg\min f[-p]$ hole free for every $p$ (and conversely, when $\operatorname{dom}_{\mathbb Z} f$ is bounded). Proposition 3.19: $f$ is integrally convex if and only if every restriction $f_{[a,b]}$ to a finite integer interval is integrally convex — integral convexity is detectable by looking at bounded pieces of $f$ one at a time.

Significance

The result itself. Theorem 3.21 is what makes integrally convex functions tractable: without it, verifying global optimality on an infinite or exponentially large integer domain would require checking every point. The theorem reduces this to a check whose size depends only on the dimension $n$ , not on the size of the domain, and it does so for the widest class of lattice functions for which such a reduction is possible — the class is defined precisely so that this property holds and no wider natural class enjoys it. Every specialized local-optimality theorem later in the book (for M-convex, M $^\natural$ -convex, L-convex, and L $^\natural$ -convex functions) restricts this same neighborhood-checking principle to a class where the local check can be made even smaller (a single-element exchange rather than a full sign pattern) precisely because those classes are integrally convex plus more.

Formalizing it. No matching item exists on the platform: a direct search for "integrally convex" returns no results, and the theorem's own proof leans on results (Theorem 1.1's local-to-global principle for ordinary convex functions on $\mathbb R^n$ , and an LP-duality-based alternate formula for $\tilde f$ ) that are either classical convex analysis or belong to a different chapter of this same book. The remaining work is therefore to give a complete, correct account of the definitional chain — convex closure, local convex extension, integral convexity — in a form a solver can build a proof from directly, and to state the finite local-check equivalence itself exactly at the strength the book proves it, not a plausible-looking weakening of it.

Difficulty

The natural first attempt is to try to prove the " $\Leftarrow$ " direction of Theorem 3.21 by a direct induction on the $\ell^1$ -distance to a global minimizer, moving one coordinate at a time. This fails in general lattice functions (a function that is only "coordinatewise convex" can have strict local minima that are not global), and the theorem's actual proof instead routes through the real relaxation: it shows the neighborhood-check hypothesis forces $x$ to be a local minimizer of the local convex extension $\tilde f$ restricted to the unit ball around $x$ , then invokes ordinary convex analysis (local minimality implies global minimality for a convex function on $\mathbb R^n$ ) to conclude $x$ globally minimizes $\bar f$ , and finally uses integral convexity ( $\tilde f = \bar f$ ) to transfer this back to $f$ on $\mathbb Z^n$ . The identification of $f$ 's local behavior with $\tilde f$ 's convexity on a single unit cube — rather than any coordinatewise or separable argument — is the step that makes the class of integrally convex functions exactly the right one for this theorem, and is where a naive combinatorial argument breaks down.

Formalization scope

The ground set is $\mathbb Z^n$ , represented as Fin n → ℤ; $f$ 's codomain is WithTop ℝ (exactly $\mathbb R \cup \{+\infty\}$ ), while the convex closure $\bar f$ and local convex extension $\tilde f$ take values in EReal (exactly $\mathbb R \cup \{\pm\infty\}$ , a complete lattice, so their defining suprema are total functions with no side conditions). A trivializing formalization of the goal would quantify the right-hand side over a single fixed $(Y,Z)$ pair, or over all of $\mathbb Z^n$ instead of the sign-pattern neighbors; both are excluded by keeping $Y, Z$ universally quantified Finset (Fin n) ranging over the full $3^n$ sign-pattern space (minus the trivial case, which the equivalence still holds through vacuously).

Checked against the platform (GET /theorems?q=integrally convex, 0 hits) and against Mathlib's Analysis/Convex/ for the classical facts this chapter's proof would eventually need (ordinary convex-function local-to-global optimality, LP duality): these are broadly available in Mathlib's convex-analysis library in some form, but none of them is imported here, since none appears in the statement of any item this mission drafts — they belong to a proof this pass does not attempt. Contributions to a shared DiscreteConvex.IntegralConvexity definitions layer are welcome from chunks 06–09, which specialize integral convexity to M-convex and L-convex functions and will need the same convex-closure/local-extension vocabulary.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
P. Favati, F. Tardella, "Convexity in nonlinear integer programming," Ricerca Operativa, 53, 1990, pp. 3–44.

14 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

Formalization targets

Goal: Theorem 5.1

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

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

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

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

6 thms2 active usersReviewed

Convex Optimization Discrete Geometry Operations Research+1·Captain: mikedeng1

On Polyhedral Approximations of the Second-Order Cone II: A Lower Bound on the Size of Polyhedral ApproximationsResearch Paper

Motivation

A conic quadratic program minimizes a linear objective subject to constraints of the form $\|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell$ . Interior-point methods solve such programs in polynomial time, but around 2000 the available solvers handled far smaller instances than linear programming codes did. Ben-Tal and Nemirovski (Math. Oper. Res. 26(2), 2001) asked whether a conic quadratic program can be replaced by a linear program of comparable size, and answered it by approximating each second-order cone by a projection of a polyhedral cone. Their Theorem 1.1 builds such an approximation with accuracy $\varepsilon$ using $O(k\ln(2/\varepsilon))$ variables and inequalities. The present mission is their Proposition 3.1: this size is optimal in order, because every polyhedral $\varepsilon$ -approximation needs $\Omega(k\ln(1/\varepsilon))$ inequalities.

The question of how many linear inequalities are needed to represent or approximate a convex set as a projection (its extension complexity) has since become a subject of its own, and the lower bound of Proposition 3.1 is one of its early explicit instances for a non-polyhedral cone.

Setting

For $y\in\mathbb R^k$ write $\|y\|_2=\sqrt{y_1^2+\dots+y_k^2}$ . The Lorentz cone is

L^k=\{(y,t)\in\mathbb R^k\times\mathbb R\mid t\ge\|y\|_2\}.

Let $\varepsilon>0$ . A polyhedral $\varepsilon$ -approximation of $L^k$ is a linear map $\Pi:\mathbb R^k\times\mathbb R\times\mathbb R^p\to\mathbb R^q$ such that

if $(y,t)\in L^k$ , then $\Pi(y,t,u)\ge0$ for some $u\in\mathbb R^p$ ;
if $\Pi(y,t,u)\ge0$ for some $u$ , then $\|y\|_2\le(1+\varepsilon)t$ .

Here $\ge0$ is componentwise, $p$ is the number of auxiliary variables and $q$ the number of homogeneous linear inequalities. Equivalently, the polyhedral cone $K=\{(y,t,u)\mid\Pi(y,t,u)\ge0\}$ projects onto a cone $\widehat L^k$ of the $(y,t)$ -space with $L^k\subseteq\widehat L^k\subseteq\{(y,t)\mid\|y\|_2\le(1+\varepsilon)t\}$ . The slice of $\widehat L^k$ at height one is $G=\{y\mid(y,1)\in\widehat L^k\}$ , and $B=\{y\mid\|y\|_2\le1\}$ denotes the closed unit ball.

Formalization targets

Goal: Proposition 3.1, Eq. (13)

\exists\,c>0\ \ \forall k\ge2,\ \forall\varepsilon\in(0,\tfrac12],\ \forall p,q,\ \forall\Pi\ \text{polyhedral }\varepsilon\text{-approximation of }L^k:\qquad q\ \ge\ c\,k\ln\tfrac1\varepsilon .

The constant is absolute, as in the paper, and no value is fixed; the goal asserts only the order of growth.

Milestones (claims of the proof, in order)

Reduction. For $\varepsilon>0$ one may replace $\Pi$ by an approximation with the same $q$ , at most $p$ auxiliary variables and the same projection, whose cone $K$ contains no line.
Extreme rays. A line-free cone $\{z\mid Az\ge0\}$ defined by $q$ inequalities is the conic hull of at most $2^q$ extreme rays.
Sandwich. $B\subseteq G\subseteq(1+\varepsilon)B$ .
Vertices. If $K$ has no line, $G$ is the convex hull of $N\le2^q$ points.
Covering. If $\operatorname{conv}\{y_1,\dots,y_N\}\supseteq B$ and all $\|y_i\|_2\le1+\varepsilon$ , the closed balls of radius $\sqrt{2\varepsilon(1+\varepsilon)}$ about the $y_i$ cover the sphere $\{\|y\|_2=1+\varepsilon\}$ .
Counting. For $k\ge2$ and $\varepsilon\le\tfrac12$ such a covering needs $N\ge\exp\{c\,k\ln(1/\varepsilon)\}$ balls.

Significance

The result. Proposition 3.1 shows that the construction of Theorem 1.1 is optimal up to an absolute factor in the number of inequalities: approximating a conic quadratic constraint in dimension $k$ to relative accuracy $\varepsilon$ by linear inequalities costs $\Theta(k\ln(1/\varepsilon))$ inequalities, no more and no less. It separates what lifting (auxiliary variables) buys, a logarithmic dependence on $1/\varepsilon$ , from what it cannot buy, a sub-linear dependence on $k$ or on $\ln(1/\varepsilon)$ . Without auxiliary variables a polytope approximating the ball needs $\varepsilon^{-\Omega(k)}$ facets; the proposition says the logarithm of that count is the true cost even when lifting is allowed.

Formalizing it. The result is proved in the paper, in about fifteen lines that appeal to "elementary geometry" and to an unstated covering estimate. No machine-checked proof is known to exist. The mission produces a checked proof of the lower bound together with reusable facts: the finiteness bound on extreme rays of a pointed polyhedral cone and a lower bound on the number of balls needed to cover a Euclidean sphere, which Mathlib does not contain in this form. A companion mission of this series formalizes the matching upper bound (Theorem 1.1).

Difficulty

The obvious argument counts vertices of $G$ : at most $2^q$ of them, and a polytope between $B$ and $(1+\varepsilon)B$ needs many vertices. The difficulty is in making "many" quantitative with the right exponent. A direct volume comparison of $G$ with $B$ gives nothing, since $G$ may have the volume of $(1+\varepsilon)B$ . The argument needs the transfer from "the convex hull of the points contains $B$ " to "the points are $\sqrt{2\varepsilon(1+\varepsilon)}$ -dense on the outer sphere", and then a lower bound on the size of a covering of a sphere by balls whose centres need not lie on the sphere, uniform down to $k=2$ and up to $\varepsilon=\tfrac12$ , where $\ln(1/\varepsilon)$ is only $\ln2$ and the radius $\sqrt{2\varepsilon(1+\varepsilon)}$ is comparable to the sphere's radius. A second, easily overlooked step is the passage to a line-free cone: $K$ itself may contain lines in the $u$ -directions, in which case it has no extreme rays at all.

Formalization scope

Vectors of $\mathbb R^k$ are Fin k → ℝ, and the Euclidean norm is written out as eucNorm y = √(∑ i, y i ^ 2); the norm Mathlib puts on Fin k → ℝ is the sup norm, under which $L^k$ is polyhedral and the goal is false. A polyhedral approximation is an $\mathbb R$ -linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ), and $p$ , $q$ are the dimensions of its types; with arbitrary (nonlinear) maps, $\Pi(y,t)=t-\|y\|_2$ would give $q=1$ , so linearity is what makes the statement non-trivial. "Extreme ray" means a ray $\{sr\mid s\ge0\}$ , $r\ne0$ , that is an extreme subset (Mathlib IsExtreme) of the cone, counted once per ray.

Corrections of the printed statement. Proposition 3.1 is printed for every positive integer $k$ . It is false for $k=1$ : $L^1=\{|y|\le t\}$ is polyhedral, and $\Pi(y,t)=(t-y,t+y)$ is a polyhedral $\varepsilon$ -approximation with $q=2$ for every $\varepsilon$ , so $q\ge c\ln(1/\varepsilon)$ fails for small $\varepsilon$ . The goal and the counting milestone are therefore stated for $k\ge2$ , which is the case the proof covers. The phrase "polyhedral $\alpha$ approximation" in the proof is read as $\varepsilon$ . The paper's $O(1)$ constants are existential and quantified before every variable they are uniform over; no numerical value is asserted.

A complete development needs the Minkowski–Weyl representation of pointed polyhedral cones by extreme rays, basic convex-hull and separation arguments in Euclidean space, and a lower bound for covering numbers of spheres (for instance by a cap-measure or volume argument). The extreme-ray and covering lemmas are independent of the Lorentz cone and are welcome as stand-alone contributions.

Selected references

A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

10 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Generalization Bounds in the Predict-then-Optimize Framework IV: Distance to Degeneracy and the Strength Property for PolytopesResearch Paper

Motivation

Many decision problems in operations research are solved in two stages: a model predicts the unknown cost vector of a linear optimization problem from features, and the predicted costs are then passed to a solver. The smart predict-then-optimize (SPO) loss of Elmachtoub and Grigas measures the quality of a prediction by the excess true cost of the decision it induces, rather than by the prediction error itself. El Balghiti, Elmachtoub, Grigas and Tewari study how well the empirical SPO loss generalizes. Their margin-based bounds (Theorems 4 and 5 of the paper) require a geometric condition on the feasible region, the strength property, and a way to compute the distance to degeneracy that enters the margin loss.

Section 5 of the paper verifies this condition in the two cases that matter in practice. For strongly convex regions it is Theorem 7 (mission III of this series). This mission covers the other case, §5.2: feasible regions that are polytopes given by a list of points, which includes the unit simplex of multiclass classification and the feasible regions of shortest-path, assignment and other combinatorial problems written as convex hulls.

Setting

Let $E$ be a finite-dimensional real vector space (the paper's $\mathbb R^d$ ) with a norm $\|\cdot\|$ . A cost vector $\hat c$ is a linear functional on $E$ ; its value at $w$ is written $\hat c^\top w$ , and its dual norm is $\|\hat c\|_*=\max_{\|w\|\le1}\hat c^\top w$ .

The feasible region is a polytope with a known convex hull representation: pairwise distinct points $v_1,\dots,v_K\in E$ and

S=\mathrm{conv}\{v_1,\dots,v_K\}.

Redundant points (points that are convex combinations of the others) are allowed. For a cost vector $\hat c$ , $P(\hat c)$ is the problem $\min_{w\in S}\hat c^\top w$ , and an optimization oracle $w^*$ is any map with $w^*(\hat c)\in\arg\min_{w\in S}\hat c^\top w$ for every $\hat c$ .

The degenerate set $\mathcal C^\circ$ is the set of cost vectors $\hat c$ for which $P(\hat c)$ has more than one optimal solution.
The distance to degeneracy is $\nu_S(\hat c)=\inf_{c\in\mathcal C^\circ}\|c-\hat c\|_*$ .
$S$ has the strength property with parameter $\mu>0$ if

\hat c^\top\big(w-w^*(\hat c)\big)\ \ge\ \frac{\mu\,\nu_S(\hat c)}{2}\,\|w-w^*(\hat c)\|^2\qquad\text{for all } w\in S\text{ and all }\hat c.

The negative normal cone at $v_j$ is $\mathcal K_j=-N_S(v_j)=\{\hat c:\hat c^\top(w-v_j)\ge0\ \text{for all } w\in S\}$ , the cost vectors for which $v_j$ is optimal.
The diameter is $\Delta(S)=\sup_{w_1,w_2\in S}\|w_1-w_2\|$ .

Formalization targets

Goal: Theorem 8, strength claim (p. 25)

If $S=\mathrm{conv}\{v_1,\dots,v_K\}$ is not a singleton, then for every oracle $w^*$ , $S$ has the strength property with parameter

\mu=\frac{2}{\Delta(S)}>0 .

Milestones, in attack order

Eq. (9) (p. 24): each cone is described by finitely many inequalities,

\mathcal K_j=\{\hat c:\hat c^\top(v_i-v_j)\ge0\ \text{for all } i=1,\dots,K\}.

Proposition 2 (p. 25): $P(\hat c)$ has a unique optimal solution if and only if $\hat c\in\mathrm{int}(\mathcal K_j)$ for some $j$ ; hence

\mathcal C^\circ=\mathbb R^d\setminus\bigcup_{j=1}^K\mathrm{int}(\mathcal K_j).

Diameter (p. 25, the sentence before Theorem 8): $\Delta(S)=\max_{i,j}\|v_i-v_j\|$ .
Theorem 8, eq. (10) (p. 25): for every oracle and every $\hat c$ ,

\nu_S(\hat c)=\min_{j:\,v_j\ne w^*(\hat c)}\frac{\hat c^\top(v_j-w^*(\hat c))}{\|v_j-w^*(\hat c)\|}.

Significance

The result. Formula (10) turns the distance to degeneracy, defined as an infimum over an infinite non-convex set, into a minimum of $K$ explicit ratios that needs one oracle call. This makes the margin SPO loss of the paper computable for polytopes. The strength claim, combined with the paper's Theorems 4 and 5, yields margin-based generalization bounds for the SPO loss over any polytope with a known vertex list, with a dependence on the hypothesis class through its multivariate Rademacher complexity rather than through a Natarajan dimension. For the unit simplex it recovers known margin bounds for multiclass classification (Example 8).

Formalizing it. The results are proved in the paper; to our knowledge none of them is machine-checked. A formalization produces, beyond the four statements, a Lean account of the normal fan of a polytope presented by a point list, its interplay with uniqueness of linear-optimization solutions, and distances to its boundary measured in a dual norm. These are standard facts of polyhedral theory that Mathlib does not yet state in this form.

Difficulty

The obstacle is that $\nu_S$ is a distance to the degenerate set, and that set is neither convex nor given by inequalities: it is a union of lower-dimensional pieces of the normal fan, so no projection formula applies, and its description depends on which points of the representation are redundant. Relating a dual-norm ball around $\hat c$ to the finitely many inequalities of eq. (9) is where the argument needs care. A Euclidean shortcut is not available: the norm is arbitrary, and the numerator of (10) and the distance $\nu_S$ are measured in different norms. A second trap is the oracle: at a degenerate $\hat c$ it may return a point that is not among the $v_j$ , and (10) must still hold.

Formalization scope

$E$ is a finite-dimensional real normed space; cost vectors are elements of StrongDual ℝ E, whose operator norm is the dual norm. Interiors and distances in the cost space use that norm.
The polytope is v : Fin K → E, injective, with $S$ = convexHull ℝ (Set.range v). Nonemptiness, compactness and convexity of $S$ (the paper's §2 standing assumptions) follow from this representation; Proposition 2 and the diameter identity add $K\ge1$ , which is that nonemptiness.
"Not a singleton" is S.Nontrivial. Without it $\mathcal C^\circ=\emptyset$ , $\nu_S\equiv0$ and the strength property holds for free; with it, $0\in\mathcal C^\circ$ and $\nu_S$ is a genuine distance. The goal's parameter $2/\Delta(S)$ is stated to be positive, so the Lean conventions $\mathrm{diam}=0$ on unbounded or one-point sets and $2/0=0$ cannot trivialize it.
The oracle is arbitrary: every theorem quantifies over all maps $w$ with $w(\hat c)\in\arg\min_S\hat c$ , never a fixed selection.
$\nu_S$ is Metric.infDist to $\mathcal C^\circ$ ; $\Delta(S)$ is Metric.diam, correct here because $S$ is bounded. Minima and maxima over finite index sets are stated with IsLeast/IsGreatest, so no junk value of min' or sInf enters.
Reusable infrastructure: the negative normal cones and normal fan of a point-list polytope, the characterization of unique optima of linear optimization over a polytope, and the dual-norm distance to the boundary of a polyhedral cone. Contributions of any of these as standalone lemmas are welcome.

Selected references

O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, arXiv:1905.11488v3, 2022 (Mathematics of Operations Research, 2023). https://arxiv.org/abs/1905.11488
A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 2009. https://doi.org/10.1007/978-3-642-02431-3

7 thms2 active usersReviewed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

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

Motivation

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

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

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 4.1

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

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

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

Milestones

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

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

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

Significance

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

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

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

The milestones are stated with the corresponding hypotheses.

Difficulty

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

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

Formalization scope

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

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

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

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

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

Useful contributions include:

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

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

Selected references

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

13 thms2 active usersReviewed

Completed

Discrete Geometry Operations Research Optimization·Captain: mikedeng1

Maximal Lattice-Free Convex Sets in Linear Subspaces II: Minimal Valid Inequalities Come from Maximal Lattice-Free Convex SetsResearch Paper

Cutting planes from lattice-free convex sets

Cutting planes for mixed-integer linear programs are often derived from a few rows of an optimal simplex tableau. Keeping $q$ rows for basic integer variables $x_1,\dots,x_q$ , dropping the nonnegativity of $x$ (Gomory's corner polyhedron, Gomory 1969) and then the integrality of the nonbasic variables leaves the set of $s\ge0$ with $f+\sum_j r^js_j\in\mathbb Z^q$ . Balas observed in 1971 that convex sets with no integral point in their interior give valid inequalities for such sets (Balas 1971). Andersen, Louveaux, Weismantel and Wolsey (2007) for two rows, and Borozan and Cornuéjols (2009) for any number of rows, showed that for rational data the irredundant valid inequalities correspond to maximal lattice-free convex sets. Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543; Math. Oper. Res. 35(3), 2010) removed the rationality assumption. This mission formalizes that result, Theorem 3 of their paper.

Setting

Fix $q\ge0$ , a point $f\in\mathbb R^q$ and a linear subspace $W\subseteq\mathbb R^q$ , and assume that the affine space $f+W$ contains an integral point. Products such as $ry$ are standard inner products.

$\mathcal W$ is the space of real functions $s=(s_r)_{r\in W}$ with finite support. The semi-infinite relaxation is

R_f(W)=\Big\{s\in\mathcal W \ \Big|\ f+\sum_{r\in W}rs_r\in\mathbb Z^q,\ s_r\ge0\ (r\in W)\Big\}.

A linear inequality is a pair $(\psi,\alpha)$ with $\psi:W\to\mathbb R$ an arbitrary function and $\alpha\in\mathbb R$ , read as $\Psi(s)=\sum_{r\in W}\psi(r)s_r\ge\alpha$ . It is valid if every $s\in R_f(W)$ satisfies it.
$V$ is the affine hull of $(f+W)\cap\mathbb Z^q$ , and $\mathcal V=\{s\in\mathcal W\mid f+\sum_r rs_r\in V\}$ . A linear inequality is trivial if every $s\in\mathcal V$ with $s\ge0$ satisfies it. When $W$ is irrational (not spanned by the integral points it contains, up to translation), $V$ is a proper affine subspace of $f+W$ .
$\sum\psi(r)s_r\ge\alpha$ dominates $\sum\psi'(r)s_r\ge\alpha$ if $\psi\le\psi'$ pointwise. A valid inequality is minimal if no valid inequality with the same $\alpha$ and a different $\psi'\le\psi$ exists.
Choose $C\in\mathbb R^{\ell\times q}$ and $d\in\mathbb R^\ell$ with $V=\{x\in f+W\mid Cx=d\}$ . Two valid inequalities are equivalent if $\psi(r)=\rho\psi'(r)+\lambda^TCr$ for all $r\in W$ and $\alpha=\rho\alpha'+\lambda^T(d-Cf)$ , for some $\rho>0$ , $\lambda\in\mathbb R^\ell$ .
A maximal lattice-free convex set in $f+W$ is a convex $B\subseteq f+W$ with no integral point in its interior relative to $f+W$ , inclusionwise maximal with these properties.
For $K\subseteq W$ closed, convex, with $0$ in its interior relative to $W$ : the polar $K^*=\{y\in W\mid ry\le1\ \forall r\in K\}$ , $\hat K=\{y\in K^*\mid\exists x\in K,\ xy=1\}$ , and $\rho_K(r)=\sup_{y\in\hat K}ry$ . For such a $B$ with $f$ in its interior, $\psi_B=\rho_{B-f}$ ; for a polyhedral $B=\{x\in f+W\mid a_i(x-f)\le1\}$ with tight rows this is $\psi_B(r)=\max_ia_ir$ .

A function $\sigma:W\to\mathbb R$ is sublinear if $\sigma(\lambda r)=\lambda\sigma(r)$ for $\lambda\ge0$ and $\sigma(r+r')\le\sigma(r)+\sigma(r')$ .

Formalization targets

Goal: Theorem 3 (p. 6)

Every nontrivial valid linear inequality for $R_f(W)$ is dominated by a nontrivial minimal valid linear inequality for $R_f(W)$ .
Every nontrivial minimal valid linear inequality for $R_f(W)$ is equivalent to one of the form

\sum_{r\in W}\psi_B(r)s_r\ \ge\ 1

with $\psi_B\ge0$ on $W$ and $B$ a maximal lattice-free convex set in $f+W$ with $f$ in its interior.

The goal is stated as one conjunction. It fixes no constants and makes no rationality assumption on $f$ or $W$ .

Milestones

In the order in which the proof on pp. 15–21 uses them:

Lemma 23 (a sublinear valid inequality below any valid one)
Lemma 26 (invariance under equivalence)
Claims 1 and 2 in the proof of Theorem 3
Theorem 28 (Basu–Cornuéjols–Zambelli: $\rho_K$ is the smallest sublinear function with $1$ -sublevel set $K$ )
Remark 30 and Claim 4 (the inequality $\sum\rho_K(r)s_r\ge1$ )
Remark 29 ( $\rho_K=\max_ia_ir$ for tight rows)
Claim 6 (a shift by $\lambda^TC$ making $\psi$ nonnegative)
Claim 7 ( $\psi_B$ below a nonnegative sublinear $\psi''$ )
Lemma 31 (maximal lattice-free sets give minimal inequalities)

Significance

Theorem 3 says that the minimal valid inequalities of $R_f(W)$ are exactly those produced by maximal lattice-free convex sets, up to the equivalence forced by the affine hull $\mathcal V$ . It also says that for irrational $W$ , where valid inequalities can have negative coefficients, some equivalent form always has nonnegative coefficients. The paper derives two further results from it: a description of the closure of $\operatorname{conv}(R_f(W))$ in a suitable norm (Theorem 4), and a reduction of extreme inequalities of the infinite model to finite ones (Theorem 5). Both results remain unproved without it.

The result has a complete proof in the paper, which relies on the cited Theorem 28 from Basu, Cornuéjols, Zambelli. To our knowledge none of it is machine-checked. A formalization would provide a definitional layer for corner relaxations, lattice-free sets and valid inequalities, which is currently absent from Mathlib. It would also expose where the page is imprecise; see the scope section.

Difficulty

For rational data every valid inequality can be written with right-hand side $1$ and nonnegative coefficients, and $\psi$ is then the gauge of $B_\psi$ . For irrational $W$ this fails. Since $R_f(W)\subseteq\mathcal V$ , adding $\lambda^TCr$ to $\psi$ changes nothing on $R_f(W)$ , so coefficients can be negative, and $B_\psi=\{x\in f+W\mid\psi(x-f)\le\alpha\}$ may have a full-dimensional recession cone. A maximal lattice-free set containing $B_\psi$ then yields a $\psi_B$ that need not lie below $\psi$ (the example on pp. 21–22 shows this). One must first pass to an equivalent inequality whose set has no full-dimensional recession cone within $V$ . This step combines the structure theorem for maximal lattice-free sets in irrational subspaces (Theorem 9 of the paper) with a duality argument. A second obstacle is that $\psi$ is an arbitrary function: validity alone gives no convexity or continuity, and Lemma 23 is needed to recover them.

Formalization scope

Ambient space. $\mathbb R^q$ is EuclideanSpace ℝ (Fin q), $W$ is a Submodule, and $\mathcal W$ is W →₀ ℝ. The printed phrase "the set $\{r\mid s_r>0\}$ has finite cardinality" is read as ordinary finite support.
Standing hypothesis. Every statement assumes that $f+W$ contains an integral point. Without it $R_f(W)=\emptyset$ and every inequality is valid, so this hypothesis rules out the trivializing formalization. The equivalence predicate carries the hypothesis $V=\{x\in f+W\mid Cx=d\}$ together with validity of both inequalities. With $C,d$ unconstrained, equivalence would be rescaling only, and part 2 of the goal would be false for irrational $W$ .
Interiors. All interiors are relative: to $f+W$ for $B$ and $B_\psi$ , to $W$ for $K$ .
$\psi_B$ . It is defined as $\rho_{B-f}$ , independent of any description of $B$ .

The paper is imprecise in three places, and the formalization departs from the page in each:

Remark 29 is false without tight rows: for $K=(-\infty,1]\subseteq\mathbb R$ written with $a_1=1$ , $a_2=1/2$ , $\rho_K(r)=r\ne\max(r,r/2)$ for $r<0$ . It is stated with the tightness the paper arranges before using it.
The identity $\operatorname{int}(B_\psi)=\{x\mid\psi(x-f)<\alpha\}$ on p. 17 fails at $\alpha=0$ , for example for $\psi\equiv0$ . Claims 1 and 2 use the strict sublevel set, and Claim 2 is false for the topological interior.
Claims 5 and 7 invoke Corollary 20 in $f+W$ , although it is proved only for a lattice of a linear space. Corollary 20 and Claim 5 are therefore not milestones.

Two kinds of contributions are especially welcome: reusable infrastructure for polars of convex sets relative to a subspace and for sublinear functions on submodules, and a proof of Theorem 28.

Selected references

A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543v1
A. Basu, G. Cornuéjols, G. Zambelli, Convex sets and minimal sublinear functions, J. Convex Anal. 18(2), 2011 (reference [9]).
V. Borozan, G. Cornuéjols, Minimal valid inequalities for integer constraints, Math. Oper. Res. 34(3), 2009. https://doi.org/10.1287/moor.1090.0400
K. Andersen, Q. Louveaux, R. Weismantel, L. Wolsey, Inequalities from two rows of a simplex tableau, IPCO 2007. https://doi.org/10.1007/978-3-540-72792-7_1
E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2, 1969. https://doi.org/10.1016/0024-3795(69)90017-2

16 thms2 active usersReviewed

Discrete Geometry Number Theory Operations Research+1·Captain: mikedeng1

Maximal Lattice-Free Convex Sets in Linear Subspaces I: Characterization of Maximal Lattice-Free Convex Sets in a SubspaceResearch Paper

Motivation

Cutting planes for mixed-integer linear programs are often derived from convex sets that contain no integer point in their interior. Balas observed in 1971 that every such lattice-free convex set containing the current fractional LP solution in its interior yields a valid inequality, the intersection cut (Balas, Intersection cuts, Oper. Res. 19, 1971). The strongest cuts come from sets that are inclusionwise maximal, so the shape of maximal lattice-free convex sets matters to multi-row cut generation.

The case where the set lives in a subspace arises in practice. Taking $q$ rows of an optimal simplex tableau restricts the integer points to an affine subspace $f+W$ of $\mathbb R^q$ spanned by the tableau columns. When $W$ is irrational, its integer points span only a proper subspace $V\subsetneq W$ . The classical theory does not cover this case, and it is the case that the second mission of this series (minimal valid inequalities of the relaxation $R_f(W)$ ) needs.

Timeline.

Lovász (Geometry of numbers and integer programming, 1989) stated the characterization for rational subspaces (Proposition 3.1) and gave only a sketch of the proof. The irrational-hyperplane case is not visible in that sketch.
Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543v1; Math. Oper. Res. 35(3), 2010, doi:10.1287/moor.1100.0461) gave a complete proof of Lovász's theorem for an arbitrary lattice of a linear space (Theorem 10). They also extended it to a space $W$ strictly larger than the span $V$ of the lattice (Theorem 9, equivalently Theorem 1 for $\mathbb Z^n$ ).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product and the open balls $B_\varepsilon(x)$ . For $X\subseteq\mathbb R^n$ , $\langle X\rangle$ denotes its linear span.

A lattice of a linear space $V$ is an additive group $\Lambda=\{\lambda_1a_1+\dots+\lambda_ma_m\mid\lambda_i\in\mathbb Z\}$ generated by linearly independent vectors $a_1,\dots,a_m$ with $\langle a_1,\dots,a_m\rangle=V$ (Definition 6, IsLatticeOf Λ V). A linear subspace $L\subseteq V$ is a $\Lambda$ -subspace if it has a basis contained in $\Lambda$ (Definition 7, IsLambdaSubspace Λ V L). For $\mathbb Z^2$ , the line $x_2=2x_1$ is a $\Lambda$ -subspace and the line $x_2=\sqrt2x_1$ is not.

For sets $W,S$ the interior relative to $W$ is $\mathbf{int}_W(S)=\{x\in S\mid B_\varepsilon(x)\cap W\subseteq S\text{ for some }\varepsilon>0\}$ (intW W S). The relative interior is $\mathbf{relint}(S)=\mathbf{int}_{\operatorname{aff}(S)}(S)$ .

Let $W\supseteq V$ be a linear space. A set $S$ is a $\Lambda$ -free convex set of $W$ if $S\subseteq W$ , $S$ is convex and $\Lambda\cap\mathbf{int}_W(S)=\emptyset$ . It is maximal if no other $\Lambda$ -free convex set of $W$ properly contains it (Definition 8, IsLambdaFree, IsMaxLambdaFree).

The statements also use a polyhedron in $W$ ( $W$ intersected with finitely many closed half-spaces), a polytope (convex hull of a finite set), the dimension $\dim(S)$ of the affine hull with $\dim\emptyset=-1$ (affDim), and a facet: a nonempty face $S\cap\{\langle a,x\rangle=b\}$ of a valid inequality with $\dim F=\dim S-1$ . The recession cone is $\operatorname{rec}(S)=\{r\mid x+tr\in S\ \forall x\in S,\ t\ge0\}$ and the lineality space is $\operatorname{rec}(S)\cap-\operatorname{rec}(S)$ .

Formalization targets

Goal: Theorem 9 (p. 8)

For a lattice $\Lambda$ of $V$ and a linear space $W\supseteq V$ with $\dim W\ge1$ , a set $S$ is a maximal $\Lambda$ -free convex set of $W$ if and only if

\text{(i) } S \text{ is a full-dimensional polyhedron in } W,\ S\cap V \text{ is maximal } \Lambda\text{-free in } V,\ F\mapsto F\cap V \text{ is a bijection of facets};

\text{(ii) } S=v+L \text{ is a hyperplane of } W \text{ with } L\cap V \text{ a hyperplane of } V \text{ that is not a } \Lambda\text{-subspace};

\text{(iii) } S \text{ is a half-space of } W \text{ containing } V \text{ on its boundary.}

Main milestone: Theorem 10 (p. 8)

For $\dim V\ge1$ , $S$ is a maximal $\Lambda$ -free convex set of $V$ if and only if either $S=P+L$ is a polyhedron with $P$ a polytope, $L$ a $\Lambda$ -subspace and $\dim S=\dim P+\dim L=\dim V$ , with no lattice point in $\mathbf{int}_V(S)$ and a lattice point in the relative interior of every facet; or $S=v+L$ is an affine hyperplane of $V$ whose direction $L$ is not a $\Lambda$ -subspace.

Supporting milestones

Lemma 13 (bounded full-dimensional case), Lemma 15 (lattice points near half-lines), Lemma 16 ( $S+\langle\operatorname{rec}S\rangle$ stays $\Lambda$ -free), Lemma 17 (projection along a $\Lambda$ -subspace is a lattice), Lemma 18 (lattice points near non-lattice subspaces), Lemma 19 (maximal hyperplanes), Claims 1 and 2 in the proof of Theorem 10, and identity (6), $\mathbf{int}_W(S)\cap V=\mathbf{int}_V(S\cap V)$ .

Significance

Theorem 10 says that maximal lattice-free sets are cylinders over polytopes with a lattice point on every facet, apart from the irrational hyperplanes. This is the structural fact behind the finiteness of facet counts (at most $2^{\dim P}$ ) and behind every classification of maximal lattice-free sets in low dimension, such as the triangles and quadrilaterals of the two-row relaxation. Theorem 9 extends it to irrational subspaces. There the new cases are the half-spaces of (iii), which have $V$ on their boundary, and the hyperplanes of (ii), whose trace on $V$ is a hyperplane of $V$ that is not a $\Lambda$ -subspace. Theorem 9 is the geometric input to the paper's Theorem 3: every minimal valid inequality of $R_f(W)$ is the gauge of a maximal lattice-free convex set of $f+W$ .

These results are proved on paper. No machine-checked version of Lovász's theorem, of Theorem 9, or of the lattice-approximation Lemmas 15 and 18 is known to exist. The mission produces the definitions of lattices of subspaces, relative interiors and lattice-free sets on which the second mission of the series builds.

Difficulty

The obvious argument separates each lattice point from $S$ by a half-space and intersects the half-spaces. It gives a polyhedron only when finitely many lattice points matter, that is, when $S$ is bounded. For unbounded $S$ , the recession directions must be shown to be lineality directions and to be spanned by lattice vectors. Both steps rest on simultaneous Diophantine approximation (Dirichlet's theorem) applied in irrational directions, and on a density argument for the projected lattice when the lineality space is not a $\Lambda$ -subspace. In the subspace setting of Theorem 9, one must also track the interiors relative to $W$ and to $V$ separately. Identity (6) holds only when $\mathbf{int}_W(S)$ meets $V$ , and the half-space case (iii) is exactly the case where it does not.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), linear spaces are Submodule ℝ, and $\Lambda$ is an AddSubgroup. All declarations live in the namespace MaxLatticeFree.Geometry. Every interior is relative (intW, relint). With the ambient topological interior, every subset of a proper subspace would be trivially lattice-free, and the classification would collapse. A lattice must have a linearly independent generating family; a dense finitely generated subgroup such as $\mathbb Z+\sqrt2\mathbb Z$ is excluded. Dimensions are integers with $\dim\emptyset=-1$ , and facets are nonempty, so no dimension equation holds through truncated subtraction.

Two readings of the page are fixed.

Theorem 9 assumes $\dim W\ge1$ and Theorem 10 assumes $\dim V\ge1$ . For $W=V=\{0\}$ the only maximal set is $\emptyset$ , which satisfies none of the listed cases, so the printed statements are false there.
Identity (6) is stated under the three hypotheses its proof uses, not inside the case analysis of Theorem 9.

The paper's Theorem 1 (the same result for $\mathbb Z^n$ and affine $W$ ) is not included, and neither are the cited results of Barvinok and Dirichlet (Theorems 11, 14, Corollary 12). They are welcome as supporting lemmas. Infrastructure that is useful beyond this mission includes Dirichlet's simultaneous approximation theorem in $\mathbb R^m$ , discreteness of lattices of subspaces, and the relation between intW/relint and Mathlib's intrinsicInterior.

Selected references

A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543
L. Lovász, Geometry of numbers and integer programming, in: Mathematical Programming: Recent Developments and Applications, 1989, pp. 177–210.
E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
A. Barvinok, A Course in Convexity, Graduate Studies in Mathematics 54, AMS, 2002. https://doi.org/10.1090/gsm/054

18 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming XVI: Unions of Upper Monotone Polytopes and PolymatroidsTextbook

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

6 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming XIV: Disjunctive Cuts from the V-Polyhedral RepresentationTextbook

Motivation

The lift-and-project cut-generating LP (CGLP) is the workhorse of the book's cutting-plane machinery, but its number of variables grows with $q$ , the number of terms in the disjunction — a real computational cost for disjunctions with many terms. An alternative representation of the same disjunctive hull, built from vertices and extreme rays rather than from a dual LP, trades this away: its number of variables is fixed at $n$ regardless of $q$ , at the price of a constraint set that is generally exponential in size (T. H. Kim, V-polyhedral disjunctive cuts, PhD thesis and papers with E. Balas; the underlying representation traces to the classical Minkowski–Weyl theorem for polyhedra). This mission formalizes the chapter's capstone: the V-polyhedral, lift-and-project, and generalized-intersection-cut families — three representations that look structurally different — coincide exactly.

Setting

A disjunctive set in V-polyhedral (vertex-ray) form is $F := \bigcup_{h\in Q} P^h$ , $P^h := \mathrm{conv}\,V^h + \mathrm{cone}\,R^h$ , where $V^h$ / $R^h$ are the (finite) sets of vertices and extreme rays of the $h$ -th disjunct. The conic hull of a set $S$ is the set of all finite nonnegative combinations of its elements. For a reference point $x_F \in F$ , the disjunctive cone $C_{x_F}$ is the homogenization, at $x_F$ , of the translated disjunctive system: $(x',x_0') \in \mathbb{R}^n \times \mathbb{R}_+$ with $Ax' + (Ax_F-b)x_0' \ge 0$ and $\bigvee_h(D^hx' + (D^hx_F-d^h_0)x_0' \ge 0)$ .

For a relaxation $\tilde P^h$ of each disjunct with $P^h \subseteq \tilde P^h \subseteq C(x^h)$ (the LP cone at the disjunct's own optimum $x^h$ ), write $\tilde V^h$ , $\tilde R^h$ for its vertices and rays, and $C := \mathrm{conv}(\bigcup_h \tilde V^h) + \mathrm{cone}(\bigcup_h \tilde R^h)$ for the single combined polyhedron they generate. The associated L&P cut-generating LP is

\alpha = u^h \tilde D^h, \qquad \beta \le u^h \tilde d^h_0 \quad (h\in Q), \qquad \textstyle\sum_{h\in Q} u^h e = 1, \qquad u^h \ge 0.

Formalization targets

Proposition 12.1. $\alpha x \ge \beta$ is valid for $F$ if and only if $\alpha p \ge \beta$ for every $p \in V^h$ and $\alpha r \ge 0$ for every $r \in R^h$ , over every $h \in Q$ .

Proposition 12.3. For a cut $\alpha x \ge \beta$ tight at $x_F$ ( $\alpha x_F = \beta$ ) and $x \in F$ : $\alpha x < \beta$ if and only if $\alpha(x - x_F) < 0$ for the corresponding point $(x - x_F, 1)$ of $C_{x_F}$ .

Theorem 12.4. If $(\alpha,\beta)$ satisfies $\alpha p \ge \beta$ for every $p \in \tilde V^h$ and $\alpha r \ge 0$ for every $r \in \tilde R^h$ (over every $h$ ), and the mixed-integer feasible set $P_I$ lies in the combined polyhedron $C$ , then $\alpha x \ge \beta$ is valid for $P_I$ .

Theorem 12.5 (goal). $(\alpha,\beta)$ is valid for the combined vertex-ray system if and only if there exists a multiplier $u = \{u^h\}_{h\in Q}$ making it simultaneously a feasible solution of the CGLP above and a generalized intersection cut from

S := \{x \in \mathbb{R}^n : u^h \tilde D^h x \le u^h \tilde d^h_0,\ h \in Q\}.

The targets move from the elementary generator-validity fact (12.1) and its algorithmic companion (12.3, which the iterative cut-generation procedure of §12.1 uses to search only adjacent extreme points) through the same validity criterion generalized to a relaxed system (12.4) to the three-way unification (12.5) that is the entire point of introducing the V-polyhedral representation in the first place.

Significance

Theorem 12.5 explains why the V-polyhedral approach is worth having at all: it produces exactly the same cuts as the lift-and-project CGLP, so nothing is lost by switching representations, while the computational cost profile is reversed (the book's own estimate, not part of this mission's targets, shows the V-polyhedral approach at least $q^3$ times cheaper for a $q$ -term disjunction using $\tilde P^h = C(x^h)$ ). This matters directly for disjunctions with many terms — split disjunctions used one or two at a time throughout most of the earlier chapters — which the CGLP approach makes increasingly expensive as $q$ grows, but which the V-polyhedral approach handles without a growing variable count.

Both directions are proved in the source (this book's own §12, citing the underlying V-polyhedral cut idea to Balas's joint work with T. H. Kim, and the GIC-to-L&P equivalence to §11.4's own Theorem 11.5) but have no formalized counterpart on this platform: nothing existing treats V-polyhedral representations, disjunctive cones, or a three-way cut-family equivalence. This mission produces the first Lean statements of all four targets.

Difficulty

The obvious shortcut for Theorem 12.5 is to state only "the V-polyhedral cuts and the L&P cuts coincide" and treat the GIC leg as a footnote, since the book's own two-line proof dispatches the GIC equivalence by citing an earlier theorem rather than re-deriving it. But the theorem's actual claim is a three-way equivalence with a specific, described $S$ built from the very multipliers that solve the CGLP — dropping the GIC leg, or defining $S$ independently of those multipliers, would understate what is being asserted (the book's own remark following the theorem stresses that the GIC-defining points and the V-polyhedral vertices are typically different points that nonetheless yield equivalent cuts, which is exactly the content a two-way statement would erase).

For Theorem 12.4, the subtlety is that $C$ (the combined polyhedron) is not the union $\bigcup_h \tilde P^h$ but its convex hull — a strictly larger set in general — so validity for $C$ 's generators is a priori a stronger requirement than validity for each $\tilde P^h$ separately; the theorem's force is that this stronger validity is still exactly what is needed (and obtained) to conclude validity for $P_I$ .

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default, with the disjunction index Q left as a general type for Propositions 12.1/12.3 (so the same Ph/DisjSet definitions serve any finite disjunction) and specialized to [Fintype Q] where a finite sum over disjuncts is needed (Theorem 12.4's combined polyhedron, the CGLP of Theorem 12.5). V^h/R^h (Proposition 12.1) and Ṽ^h/R̃^h (Theorem 12.4) are formalized with the same underlying definitions (Ph, IsVPolyhedralValid) applied to different vertex/ray data, per BRIEF.md's explicit warning that these are distinct objects — not by duplicating the definitions under two names. "Is a generalized intersection cut from $S$ " (IsGICFromS) is formalized via the exact characterization Theorem 11.4's own remark in 11a-intersection-cuts gives for the GIC family (valid outside $S$ 's interior, and a genuine cut), rather than by re-deriving the underlying extreme-ray construction — a trivializing formalization this mission rules out would instead drop this leg's dependence on the same multiplier u that witnesses the CGLP leg, decoupling S from the solution it is supposed to come from.

This mission depends on no other chunk's Lean definitions; it restates 02a-convex-hull's vertex/extreme-point vocabulary, 11a-intersection-cuts's cut apparatus, and 11b-monoidal-strengthening's disjunctive-cut conventions only informally, per the series convention. Theorem 12.2 (the extreme-ray/edge correspondence underlying the "adjacent vertices only" search strategy) was not drafted this pass — see HARD.md — since a faithful, non-circular formalization of "edge of a polytope incident with a point" needs face-lattice machinery beyond what any earlier chunk in this series has built. The ConicHull/DisjunctiveCone/CombinedC definitions are reusable by any later mission touching V-polyhedral cut generation.

Selected references

E. Balas and T. H. Kim, Cutting planes from extended LP formulations, Mathematical Programming 156 (2016), 587–606. https://doi.org/10.1007/s10107-015-0885-2
E. Balas and M. Perregaard, Generalized intersection cuts and a new cut generating paradigm, Mathematical Programming A 137 (2013), 19–35. https://doi.org/10.1007/s10107-011-0483-x
A. Kazachkov, Non-Recursive Cut Generation, PhD dissertation, Carnegie Mellon University, 2018 (cited by Balas for the relaxation-based V-polyhedral cut generator of §12.2).
E. Balas, Disjunctive Programming, Springer, 2018, Chapter 12. https://doi.org/10.1007/978-3-030-00148-3

5 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming XII: Intersection Cuts, Generalized Intersection Cuts, and Lift-and-Project CutsTextbook

Motivation

Intersection cuts (Balas, 1971) are the founding construction of cutting-plane theory for mixed 0-1 and mixed-integer programs: given a fractional LP solution $\bar x$ and a convex region $S$ around it known to contain no feasible integer point, the hyperplane through the points where $S$ 's boundary meets the extreme rays of the LP cone at $\bar x$ cuts off $\bar x$ without cutting off any feasible solution. What makes intersection cuts foundational rather than merely one technique among many is a completeness question: do intersection cuts, iterated over every choice of cutting region, exhaust the strongest possible cuts — the facets of the integer hull itself — or only some weaker subclass? Balas answered this affirmatively for standard intersection cuts (those derived from convex sets free of feasible integer points, as originally defined), while a narrower, more recently popular variant restricted to lattice-free sets provably falls short of this completeness (E. Balas, Intersection Cuts — A New Type of Cutting Planes for Integer Programming, Operations Research 19 (1971), 19–39, https://doi.org/10.1287/opre.19.1.19). This mission formalizes that completeness theorem, together with a companion pair of results (Balas and Kis, 2016) pinning down exactly when a lift-and-project cut — a strictly more general cutting-plane construction from an arbitrary disjunction — coincides with a standard intersection cut, and what happens when it provably does not (E. Balas and T. Kis, On the relationship between standard intersection cuts, lift-and-project cuts, and generalized intersection cuts, Mathematical Programming A 160 (2016), 85–114, https://doi.org/10.1007/s10107-015-0975-1).

Setting

Fix a finite index set $\iota$ (structural and surplus variables of an LP relaxation together), a basic index set $I \subseteq \iota$ and a nonbasic (cobasis) set $J$ , with optimal simplex-tableau coefficients $\bar a_{ij}$ for $i \in I$ , $j \in J$ . The extreme ray of the LP cone $C(J)$ at a basic solution $\bar x$ associated with $j \in J$ has direction $r^j$ with $r^j_i = -\bar a_{ij}$ for $i \in I$ , $r^j_j = 1$ , and $r^j_i = 0$ otherwise; $C(J)$ itself is the cone with apex $\bar x$ generated by these $n = |J|$ rays. A convex set $S$ is $P_I$ -free at $\bar x$ if $\bar x$ lies in $\mathrm{int}\, S$ and $\mathrm{int}\, S$ contains no point of the mixed-integer feasible set $P_I$ . The standard intersection cut (SIC) derived from such an $S$ is $\sum_{j\in J} \tfrac{1}{\lambda_j} x_j \ge 1$ , where $\lambda_j$ is the largest $t \ge 0$ with $\bar x - t r^j \in S$ .

The corner polyhedron $\mathrm{corner}(J)$ is the convex hull of the integer points contained in $C(J)$ ; it satisfies $C(J) \supset \mathrm{corner}(J) \supset \mathrm{conv}(P_I)$ . A set $F$ is a facet of a polyhedron $Q$ if it is a proper extreme subset of $Q$ of affine dimension exactly $\dim(Q) - 1$ .

For a lift-and-project cut, fix $P := \{x : \tilde A x \ge \tilde b\}$ and a family of inequalities $d^t x \ge d^t_0$ , $t \in T$ , presenting a $P_I$ -free polyhedron $S := \{x : d^t x \le d^t_0,\ t\in T\}$ . The associated cut-generating LP (CGLP) constraint set (11.6) is

\alpha - u^t \tilde A - u^t_0 d^t = 0, \qquad -\beta + u^t \tilde b + u^t_0 d^t_0 = 0 \ (t\in T), \qquad \textstyle\sum_{t\in T}(u^t e + u^t_0) = 1, \qquad u^t, u^t_0 \ge 0,

whose feasible solutions $(\alpha,\beta,\{u^t,u^t_0\})$ correspond to valid lift-and-project (L&P) cuts $\alpha x \ge \beta$ for the disjunction built from $P$ and the terms $d^t x \ge d^t_0$ . An inequality $\gamma^1 x \ge \gamma^1_0$ dominates $\gamma^2 x \ge \gamma^2_0$ on $P$ if every $x \in P$ satisfying the first also satisfies the second.

Formalization targets

Theorem 11.2 (goal). Every facet $F$ of $\mathrm{conv}(P_I)$ , defined by $\varphi x \ge \varphi_0$ and cutting off some vertex $v$ of $P$ (i.e. $\varphi v < \varphi_0$ ), is realized exactly by the standard intersection cut derived at $v$ from $T := \{x : \varphi x \le \varphi_0\}$ :

T \text{ is } P_I\text{-free at } v, \qquad \Big\{x : 1 \le \textstyle\sum_{j\in J} \tfrac{1}{\lambda_j} x_j\Big\} = \{x : \varphi_0 \le \varphi x\}.

Corollary 11.3. Every vertex of a corner polyhedron not already in $\mathrm{conv}(P_I)$ is cut off by some standard intersection cut — the same completeness claim restated at the level of individual excluded vertices rather than facets.

Theorem 11.9. A sufficient condition for an L&P cut to reduce to a standard intersection cut: if a basic feasible CGLP solution's multipliers $u^t$ are all supported on a single common nonsingular cobasis $\iota$ , then

\{x : \beta \le \alpha x\} = \{x : 1 \le \textstyle\sum_j \pi_j\, s_j(x)\}

for the intersection cut with coefficients $\pi_j := \max_{t} \pi^t_j$ , $\pi^t_j := d^t(-\bar a_j)/(d^t_0 - d^t \bar a_0)$ , expressed via the surplus values $s_j$ at $\iota$ 's rows.

Theorem 11.11. When Theorem 11.9's condition fails — even after every positive rescaling of the solution — no intersection cut from $S$ is equivalent to the L&P cut; and when the solution additionally uniquely minimizes the CGLP objective, the L&P cut is strictly better than, and dominated by none of, every intersection cut from $S$ .

The targets move from the completeness statement itself (11.2, its vertex-level restatement 11.3) to the mechanism explaining why completeness holds in general: a sufficient condition for literal coincidence (11.9), and a proof that failure of that condition is never fatal to completeness because the L&P cut remains at least as strong, in a precise domination sense (11.11).

Significance

Theorem 11.2 is the theoretical justification for standard intersection cuts as a complete cutting plane paradigm: no facet of the integer hull is out of reach of some choice of $P_I$ -free cutting region, in sharp contrast to the restricted (lattice-free) variant that dominates the modern multi-row cut literature but is provably incomplete in this sense. Theorems 11.9 and 11.11 locate lift-and-project cuts precisely relative to this complete family: L&P cuts specialize exactly to intersection cuts under an explicit, checkable structural condition on the CGLP solution, and strictly dominate the intersection-cut family whenever that condition cannot be met — which is what makes lift-and-project the strictly more general (and, on general non-split disjunctions, strictly more powerful) construction.

Both directions are proved in the source (Balas 1971 for Theorem 11.2; Balas and Kis 2016 for Theorems 11.9 and 11.11) but have no counterpart on this platform: nothing existing treats intersection cuts, corner polyhedra, cut-generating LPs, or the correspondence between these two cutting-plane families. This mission produces the first Lean statements of all four.

Difficulty

The obvious shortcut for Theorem 11.2 is to treat "cuts off a vertex" and "is $P_I$ -free" as producing merely some valid cut, and stop there — Theorem 1.1 already guarantees that much. The actual content is the equality: the specific intersection cut constructed from the halfspace $T$ does not just happen to be valid, it reconstructs $\varphi$ itself, coefficient for coefficient, because $T$ is a single hyperplane so every one of the LP cone's $n$ extreme rays exits it through the same boundary. Losing sight of this collapses the theorem into a restatement of Theorem 1.1 with no new content.

For Theorem 11.11, the difficulty is that "no intersection cut from $S$ is equivalent" must survive scaling: a naive argument might rule out one specific $(\alpha,\beta)$ -representative satisfying Theorem 11.9's condition while missing that a positive rescaling of the same cut could still satisfy it under a different multiplier vector. The theorem's hypothesis is deliberately built to close this gap by quantifying over every positive scalar and every feasible solution realizing the rescaled pair, not just the given one.

Formalization scope

The ambient space is a generic finite index type ι for Theorem 11.2/Corollary 11.3 (structural and surplus variables together, matching 01-intro-duality's own convention for the intersection- cut apparatus), and Fin n → ℝ for the CGLP-based Theorems 11.9/11.11, matching the series' default. P_I is left as an abstract parameter throughout (never expanded into an explicit integrality predicate on a specific coordinate subset for Theorem 11.2, matching 01-intro- duality's own treatment), except in the corner-polyhedron definitions, where it is made concrete via a coordinate set Nprime since the corollary's statement depends on it directly. "Facet" and "extreme ray" are restated from 02b-polarity's conventions (affine dimension via Module.finrank of vectorSpan; IsExtreme) rather than reinvented, since Chapter 2 already pins these down precisely for this series. "Basic feasible solution" to the CGLP in Theorem 11.9 is captured entirely by the theorem's own submatrix-support condition, not through a separate, independently-derived basicness predicate — the book's own proof uses no other property of basicness, so adding one would be unused decoration, not additional fidelity. Cut equivalence throughout is formalized as exact set equality of the two halfspaces, matching the series' established convention (e.g. 10-split-closure's Theorem 10.1) for what "equivalent cuts" means.

This mission depends on no other chunk's Lean definitions: the intersection-cut apparatus (extremeRay, PIFree) is restated from 01-intro-duality, the facet apparatus (PolyDim, IsFacet) from 02b-polarity, and the tableau apparatus (Ahat, Bhat, Abar, Abar0, SurplusM) from 08-cut-correspondence/09-simplex-tableau/10-split-closure, per the series convention against importing another draft mission's definitions while chunks are drafted concurrently. A trivializing formalization to rule out explicitly: collapsing Theorem 11.2 to "some intersection cut is valid and cuts off $v$ " (already implied by Theorem 1.1 alone) rather than the literal set-equality with the facet's own inequality, which is this theorem's actual content.

Selected references

E. Balas, Intersection Cuts — A New Type of Cutting Planes for Integer Programming, Operations Research 19 (1971), 19–39. https://doi.org/10.1287/opre.19.1.19
E. Balas and T. Kis, On the relationship between standard intersection cuts, lift-and-project cuts, and generalized intersection cuts, Mathematical Programming A 160 (2016), 85–114. https://doi.org/10.1007/s10107-015-0975-1
E. Balas and M. Perregaard, Generalized intersection cuts and a new cut generating paradigm, Mathematical Programming A 137 (2013), 19–35. https://doi.org/10.1007/s10107-011-0483-x
E. Balas, Disjunctive Programming, Springer, 2018, Chapter 11, §11.1–11.5. https://doi.org/10.1007/978-3-030-00148-3

7 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming XI: The Cut-Generating LP Under a Ray NormalizationTextbook

Motivation

Lift-and-project (L&P) cuts strengthen the linear relaxation of a mixed 0-1 program by separating a fractional point from the convex hull of a disjunction such as $x_k \le 0 \lor x_k \ge 1$ . Generating an optimal L&P cut means solving the cut-generating linear program (CGLP), a linear program lifted to a space with one new pair of variables per constraint of the original tableau — considerably larger than the tableau itself. Balas and Bonami showed that this higher-dimensional LP need not be solved explicitly at all: an optimal (or near-optimal) L&P cut can instead be produced by ordinary simplex pivots in the original LP tableau, each such pivot implicitly performing an entire block of pivots in the CGLP (E. Balas and P. Bonami, Generating lift-and-project cuts from the LP simplex tableau: open source implementation and testing of new variants, Mathematical Programming Computation 1 (2009), 165–199, https://doi.org/10.1007/s12532-009-0006-4). This correspondence is what made L&P cuts practical in commercial solvers: Perregaard's implementation in XPRESS needed only 5% of the iterations and 1.5% of the time of solving the CGLP explicitly, and Bonami's public implementation in COIN-OR put the method within reach of any solver.

A second, independent line of work asks how the CGLP's feasible region should be normalized. The textbook normalization (fixing the sum of the CGLP multipliers to $1$ ) is scale-dependent — rescaling one constraint of the original system changes which cut the CGLP returns — so Balas and Perregaard proposed the ray normalization $\alpha y = 1$ instead (E. Balas and M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154, https://doi.org/10.1016/S0166-218X(01)00340-7). Under this normalization the CGLP's optimal value has a clean geometric meaning: it is exactly the distance, measured along a fixed ray from the point being separated, to the convex hull of the disjunctive set. This mission formalizes both results: the pivot correspondence (Theorem 10.1) and the optimal-value characterization under the ray normalization (Theorem 10.2, Theorem 10.3, and Corollary 10.4).

Setting

Fix a finite index set $M$ for the rows of a simplex tableau over $n$ variables, a matrix $A \in \mathbb R^{M \times n}$ , and a right-hand side $b : M \to \mathbb R$ , so that the tableau reads $A x \ge b$ (a "tilde" is dropped from the informal $\tilde A, \tilde b$ notation for the optimal-basis tableau of the linear relaxation). A basis is an injection $\iota : \mathrm{Fin}\, n \to M$ picking out $n$ of the rows; write $\hat A$ for the $n \times n$ submatrix $\hat A_{ij} = A_{\iota(i), j}$ and $\hat b$ for the corresponding subvector. From these, the standard tableau quantities are read off: $\bar a_{k0} := e_k \hat A^{-1} \hat b$ , $\bar a_{kj} := -(\hat A^{-1})_{kj}$ , and the surplus of row $i \in M$ at a point $x$ , $\mathrm{Surplus}_i(x) := (Ax - b)_i$ .

Fix a distinguished row $k$ with a fractional basic variable, and a candidate pivot row $i \ne k$ . For $\ell$ ranging over the nonbasic columns $J$ , set $\gamma_\ell := -\bar a_{k\ell}/\bar a_{i\ell}$ ; this is the value of a parameter $\gamma$ at which the combined source row

x_k + \gamma x_i + \sum_{j \in J} (\bar a_{kj} + \gamma \bar a_{ij}) x_j = \bar a_{k0} + \gamma \bar a_{i0} \tag{10.1$_\gamma$}

has its $j$ -th coefficient pass through $0$ . The simple disjunctive cut obtained by applying the split disjunction $z \le 0 \lor z \ge 1$ (where $z$ is the left side of (10.1 $_\gamma$ )) to this row is the object CombinedCutSet.

On the CGLP side, $(\mathrm{CGLP})_k$ is the cut-generating LP associated with the disjunction $-x_k \ge 0 \lor x_k \ge 1$ from Chapter 8: it has one pair of nonnegative multiplier variables $(u_\rho, v_\rho)$ per row $\rho \in M$ , plus $u_0, v_0 \ge 0$ , tied together by the normalization $\sum_\rho u_\rho + u_0 + \sum_\rho v_\rho + v_0 = 1$ , and its feasible solutions $(\alpha, u, u_0, v, v_0, \beta)$ correspond exactly to valid cuts $\alpha x \ge \beta$ for the disjunction. A basic feasible solution to $(\mathrm{CGLP})_k$ is described by a valid partition $(M_1, M_2)$ of the nonbasic rows, with $u_\rho = 0$ off $M_1$ and $v_\rho = 0$ off $M_2$ .

Separately, fix a disjunctive set and write $P_D \subseteq \mathbb R^n$ for its convex hull — the object every cut ultimately wants to separate a point from. For a fixed direction $y \in \mathbb R^n$ and point $\bar x \in \mathbb R^n$ , $(\mathrm{CGLP})_y$ is the cut-generating LP under the ray normalization: pairs $(\alpha, \beta)$ with $\alpha x \ge \beta$ valid for every $x \in P_D$ and $\alpha y = 1$ , minimizing the objective $\alpha \bar x - \beta$ .

Formalization targets

Theorem 10.1. For a genuine ordered pivot chain $j_1, \dots, j_t$ inside $J$ (no repeats, each consecutive pair flipping the sign of $\bar a_{k,\cdot}$ as $\gamma$ increases — rule (b) of the theorem), the simple disjunctive cut from the combined row at $\gamma = \gamma_{j_t}$ equals the lift-and-project cut $\{x : \beta \le \alpha x\}$ associated with a basic feasible solution to $(\mathrm{CGLP})_k$ for the resulting basis $J' := (J \cup \{i\}) \setminus \{j_t\}$ :

\mathrm{CombinedCutSet}(k, i, J, \gamma_{j_t}) = \{x : \beta \le \alpha x\}.

Theorem 10.2. If $(\mathrm{CGLP})_y$ is feasible, it has a finite minimum if and only if the ray meets the disjunctive hull:

\text{finite min} \iff \exists\, \lambda \in \mathbb R,\ \bar x + \lambda y \in P_D.

Theorem 10.3 (goal). If $(\mathrm{CGLP})_y$ has an optimal solution $(\tilde\alpha, \tilde\beta)$ , its optimal value is exactly the signed distance to $P_D$ along the ray, and the corresponding boundary point lies exactly on the optimal hyperplane:

\bar x^{\mathsf T} \tilde\alpha - \tilde\beta = \lambda^* := \min\{\lambda : \bar x + \lambda y \in P_D\}, \qquad (\bar x + \lambda^* y)^{\mathsf T} \tilde\alpha = \tilde\beta.

Corollary 10.4. Taking $y := x^* - \bar x$ for a point $x^*$ in the lifted polyhedron $P_Q$ gives an optimal solution whose hyperplane separates $\bar x$ and meets the segment $(\bar x, x^*]$ at the point closest to $x^*$ .

The targets are ordered from the purely combinatorial pivot correspondence (10.1, independent of the ray normalization) through the abstract feasibility/boundedness dichotomy (10.2) to the concrete value formula that is this mission's goal (10.3), with the geometric illustration (10.4) as a companion result using the same machinery with a specific choice of ray.

Significance

Theorem 10.1 is the theoretical justification for every commercial L&P-cut implementation cited above: it says the pivot correspondence is not an approximation or a heuristic shortcut but an exact identity between a single LP pivot and a specific, describable sequence of CGLP pivots, which is what lets a solver generate an (quasi-)optimal L&P cut at the cost of ordinary simplex pivots instead of solving a much larger LP. Theorem 10.3 gives the ray-normalized CGLP an exact geometric meaning — its value is a distance, not merely a linear-programming optimum — which is what makes the ray normalization the more robust alternative to the scale-dependent constant-sum normalization used elsewhere in the book (§9), and is the basis for the geometric picture (Corollary 10.4, Fig. 10.3) of how a lift-and-project cut relates to the lifted polyhedron $P_Q$ .

Both directions are proved in the source text (Balas and Bonami 2009 for Theorem 10.1; Balas and Perregaard 2002 for Theorems 10.2/10.3 and Corollary 10.4) but have no formalized counterpart on this platform: no existing item treats cut-generating LPs, ray normalizations of a projection cone, or the correspondence between two different pivoting processes. This mission produces the first Lean statements of both.

Difficulty

The obvious temptation for Theorem 10.1 is to existentially weaken "the sequence of $t$ pivots defined as follows" to "there exists some sequence of pivots realizing the same cut" — which would be true but not what the theorem says, and would erase the entire content that makes the result useful (an algorithm, not just an existence claim). The formalization instead carries the explicit ordered chain j1 :: middle ++ [jt] as data, with the three-part construction (rules (a), (b), (c)) encoded as hypotheses on that specific list via List.IsChain, so the theorem proved is the constructive one the book states, not a weaker existential shadow of it.

For Theorem 10.3, the proof pattern in the book resists a shortcut: showing $\lambda_0 = \lambda^*$ requires deriving a contradiction from each strict inequality ( $\lambda_0 > \lambda^*$ violates optimality of the point on $P_D$ 's boundary; $\lambda_0 < \lambda^*$ contradicts optimality of $(\tilde\alpha, \tilde\beta)$ for $(\mathrm{CGLP})_y$ via a competing separating hyperplane), so there is no way to avoid formalizing both directions of the boundedness dichotomy already needed for Theorem 10.2 first.

Formalization scope

The ambient space is $\mathrm{Fin}\ n \to \mathbb R$ throughout, matching the rest of the series. $(\mathrm{CGLP})_y$ 's feasibility (IsCGLPYFeasible) is stated directly as validity of $(\alpha, \beta)$ for $P_D$ under $\alpha y = 1$ , not through an explicit representation of the projection cone's extreme rays — this matches how the book's own Theorems 10.2/10.3 and Corollary 10.4 are phrased purely in terms of $(\alpha,\beta)$ -validity for $P_D$ , never in terms of a specific disjunction's multipliers, so this is not a weakening relative to the source. $P_D$ (the disjunctive hull that $(\mathrm{CGLP})_y$ is defined against) and $P_Q$ (the lifted polyhedron whose supporting hyperplane Corollary 10.4 describes) are kept as two independent Set (Fin n → ℝ) parameters with no assumed relationship between them, matching the book's own text, which never states one; conflating them would be a trivializing formalization that this mission explicitly avoids. "The point closest to $x^*$ " on the segment $(\bar x, x^*]$ is formalized via IsGreatest on the parameter $t \in (0, 1]$ at which the optimal hyperplane meets the segment, rather than via an unformalized Euclidean-distance minimization, since that is what "closest" means for points colinear with $\bar x$ and $x^*$ on a single ray.

Corollary 10.4 corrects a typo in the printed text: the corollary as printed reads "let $y := \bar x$ for some $x^* \in P_Q$ ", omitting " $x^* -$ " before $\bar x$ ; the very next line's figure caption gives the intended formula unambiguously as $y = x^* - \bar x$ , and the formalization uses the corrected formula (see MODERATION_NOTES.md).

This mission depends on no other chunk's Lean definitions — the CGLP and tableau apparatus needed here (originally introduced in Chapters 8 and 9) is restated locally, per the series' convention against importing another draft mission's definitions across chunks that are being drafted concurrently. A complete development needs: Farkas-type separation for the boundedness dichotomy in Theorem 10.2, and careful bookkeeping of finite index sets and their images under the basis maps $\iota, \iota'$ for Theorem 10.1. The tableau infrastructure (Ahat, Bhat, Abar0, Abar, GammaOf) is reusable by any later mission touching the simplex-tableau side of lift-and-project cuts.

Selected references

E. Balas and P. Bonami, Generating lift-and-project cuts from the LP simplex tableau: open source implementation and testing of new variants, Mathematical Programming Computation 1 (2009), 165–199. https://doi.org/10.1007/s12532-009-0006-4
E. Balas and M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154. https://doi.org/10.1016/S0166-218X(01)00340-7
E. Balas, Disjunctive Programming, Springer, 2018, Chapter 10, §10.1 and §10.6. https://doi.org/10.1007/978-3-030-00148-3

7 thms2 active usersReviewed

Linear Optimization

Missions

Understanding and Using Linear Programming VII: LP Rounding Schedules Unrelated Machines Within Twice the Optimal MakespanTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 8.3.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming VI: The Minimax Theorem for Zero-Sum GamesTextbook

Why zero-sum games belong in a linear programming course

Setting

Formalization targets

Goal: Theorem 8.1.3 (minimax theorem for zero-sum games)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming II: Optimal Basic Feasible Solutions and Vertices in Equational FormTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 4.2.3 (p. 46)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming I: Integral Bipartite Matchings, Total Unimodularity and König's TheoremTextbook

Motivation

Setting

Formalization targets

Goal: König's theorem (Theorem 8.2.2)

Total unimodularity (Lemmas 8.2.3–8.2.5)

Integrality of the perfect-matching relaxation (Theorem 3.2.1)

Consequences on the same objects

Significance

Difficulty

Formalization scope

Selected references

An Introduction to the Theory of Mechanism Design VII: Crémer–McLean Full Surplus Extraction with Correlated TypesTextbook

Motivation

Setting

Formalization targets

Goal: Crémer–McLean (Proposition 6.4)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Extended Smale's 9th Problem I: no algorithm computes K digits of LP minimisersResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.4(i), deterministic part, for LP

Milestones

Significance

Difficulty

Formalization scope

Selected references

Odd Minimum Cut-Sets and b-Matchings 2: A Capacitated b-Matching Blossom Inequality Is Violated iff G(x, d) Has an Odd Cut of Capacity Less Than OneResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Selected Topics in Column Generation II: A Strictly Redundant Column Is Never Optimal for the Ratio Pricing ProblemResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (p. 1016)

Milestone: the cost shift (§5.1, p. 1016)