Linear Optimization

Motivation

Airline and hotel revenue-management systems have traditionally been built around nesting by fare order: classes are ranked by price, and as capacity runs short the cheapest open class is closed first, so that the set of open fares is always a top segment $\{1, \dots, k\}$ of the fare ladder. This structure is what makes booking limits, protection levels and bid-price controls work, and it is optimal in the classical independent-demand model of Lee and Hersh (1993), where each customer wants one specific class.

When customers instead choose among the classes on offer (buying down to a cheaper fare, or not buying at all when their preferred fare is closed), the optimal policy need not be nested by fare order. Talluri and van Ryzin (2001 working paper; Management Science 2004) formulate single-resource capacity control under a general discrete choice model and ask which choice models still have optimal policies nested by fare order. Their Theorem 2 answers this with a characterization in terms of the choice probabilities alone. The paper's later sections use it to show that the independent-demand and multinomial-logit models have the property; the mission on the multinomial-logit model in this series builds on that.

Setting

There are $n$ fare products $N = \{1, \dots, n\}$, indexed so that $r_1 \ge r_2 \ge \dots \ge r_n \ge 0$. A choice model assigns to every offer set $S \subseteq N$ and product $j$ a probability $P_j(S) \ge 0$ that an arriving customer buys $j$ when $S$ is offered, with $P_j(S) = 0$ for $j \notin S$ and purchase probability $Q(S) = \sum_{j \in S} P_j(S) \le 1$; the remainder $P_0(S) = 1 - Q(S)$ is the probability of no purchase.

A set is complete if it has the form $A_k = \{1, \dots, k\}$, $k = 0, 1, \dots, n$ (with $A_0 = \emptyset$), and incomplete otherwise. For values $x_1 \ge x_2 \ge \dots \ge x_n$ (in the dynamic program, $x_j = r_j - v$ for a marginal value of capacity $v$), consider the static problem

$$\max_{S \subseteq N} \sum_{j=1}^n x_j P_j(S). \tag{9}$$

The choice model has the nesting-by-fare-order property (Definition 4) if (i) $Q$ is increasing, $Q(S) \le Q(T)$ for $S \subseteq T$, and (ii) for every $x_1 \ge \dots \ge x_n$, problem (9) has an optimal solution that is complete. For convex weights $\alpha_0, \dots, \alpha_n$ write $\bar P_j(\alpha) = \sum_{k=0}^n \alpha_k P_j(A_k)$ for the purchase probabilities of the corresponding randomized mixture of complete sets.

Formalization targets

Goal: Theorem 2 (p. 19)

The choice model has the nesting-by-fare-order property if and only if $Q$ is increasing and, for every incomplete set $T$, there are convex weights $\alpha$ such that

$$\sum_{j=1}^i \bar P_j(\alpha) \ge \sum_{j=1}^i P_j(T) \quad (i = 1, \dots, n-1), \qquad \sum_{j=1}^n \bar P_j(\alpha) = \sum_{j=1}^n P_j(T).$$

That is, some mixture of complete sets majorizes $(P_1(T), \dots, P_n(T))$ in fare order. Both directions are part of the goal, and the right-hand side contains no optimization over $x$.

Milestones (the paper's proof, in order)

1. Condition (ii) of Definition 4 holds iff, for every incomplete $T$, the linear system (10)–(11) — values $x_1 \ge \dots \ge x_n$ and a scalar $u$ with $u < \sum_{j \in T} x_j P_j(T)$ and $\sum_{j \in A_k} x_j P_j(A_k) \le u$ for all $k$ — has no solution (p. 20).
2. For one set $T$: (10)–(11) has no solution iff the dual system in $(\alpha, z)$ is solvable (Farkas' lemma, p. 20).
3. For one set $T$: eliminating $z$, the dual system is solvable iff the prefix-sum conditions above hold (pp. 20–21).
4. A mixture satisfying the prefix-sum conditions earns at least as much as $T$ in (9) for every $x_1 \ge \dots \ge x_n$ (pp. 19–20).

Companions

The paper remarks (p. 21) that the proof never uses completeness: the same characterization holds for any specified family of offer sets $F_1, \dots, F_m$ in place of the complete sets. Example 2 (pp. 18–19) gives a three-product model, arising from a mixture of two customer types, in which the incomplete set $\{1, 3\}$ is the unique maximizer of (9) at $x = (400, 100, 50)$, so the property fails.

Significance

Theorem 2 turns a statement quantified over all value vectors $x$ and all $2^n$ offer sets into a finite collection of linear feasibility problems, one per incomplete set, involving only the choice probabilities. Combined with the paper's Theorem 1 (the optimal policy offers nondominated sets, nested in capacity and time), it gives a checkable criterion for when a nested-by-fare-order booking-limit or bid-price policy is optimal under customer choice. The paper uses it to verify the property for the independent-demand model (Proposition 5) and the multinomial-logit model (Proposition 6), and the p. 21 remark makes it a tool to test conjectures that optimal offer sets come from another structured family.

The result is proved in the paper; the mission's contribution is a machine-checked version of the characterization and of each proof step, which are the reusable pieces for the follow-up mission on the multinomial-logit model. Farkas' lemma in inequality form is already formalized on the platform (LinearOptimization.farkas_inequality_form, referenced here); the theorem of this mission is not.

Difficulty

The argument is short on paper but the bookkeeping is where the content sits. The reduction of Definition 4(ii) to infeasibility of (10)–(11) needs care with ties: (9) only needs some complete optimum, so the system asks that $T$ beat every complete set strictly, not that $T$ be the unique optimum. The dual system must then be matched exactly to the primal: the multiplier of the ordering constraint $x_j \ge x_{j+1}$ enters two adjacent equations, the boundary multipliers $z_0$ and $z_n$ are fixed at zero, and the inhomogeneous constraint on $u$ is what forces $\sum_k \alpha_k = 1$. A naive application of Farkas' lemma to the strict system, without homogenizing in $u$, gives the wrong normalization. The boundary case $j = n$ is what produces the equality of totals rather than a further inequality, and the fare order of $x$ is the only link between the prefix-sum conditions and revenue.

Formalization scope

Products are Fin n (product $j$ is the element $j - 1$), offer sets are Finset (Fin n), probabilities are real. The choice-model axioms are the platform definition RevenueManagement.IsChoiceModel ($P_j(S) \ge 0$ and $Q(S) \le 1$), reused by reference, together with the model's own standing convention $P_j(S) = 0$ for $j \notin S$ (SupportedOn), which is needed because $\bar P_j$ and the totals sum over all products. The order $x_1 \ge \dots \ge x_n$ is Antitone x. The maximum in (9) is over all subsets of $N$.

Complete sets are $A_k$ for $k = 0, \dots, n$, so $A_0 = \emptyset$ is complete and the weights $\alpha$ live on $n + 1$ sets. The page indexes the weights by $k = 1, \dots, n$; with $A_0$ included the property is the one the paper's applications need (for the multinomial-logit model and all $x_j < 0$ the unique optimum of (9) is $\emptyset$), and the family companion contains the page's literal $k = 1, \dots, n$ version as an instance. The prefix conditions are stated for $i = 0, \dots, n - 1$, where $i = 0$ is trivial.

A formalization that put an optimization over $x$ on the right-hand side of the goal, or dropped condition (i) from either side, would be a restatement rather than the characterization; the goal's right-hand side mentions only the choice probabilities.

The development needs finite sums over Fin n, and a Farkas lemma (available on the platform). Proofs of the milestones and of the companions are welcome individually; the family version of the characterization is reusable for any conjectured family of optimal offer sets.

Selected references

• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, working paper, October 21, 2001 (UPF Economics Working Paper 533); published in Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• T. C. Lee, M. Hersh, A model for dynamic airline seat inventory control with multiple seat bookings, Transportation Science 27(3):252–265, 1993. https://doi.org/10.1287/trsc.27.3.252
• A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-0-387-68276-1
• K. Talluri, G. van Ryzin, The Theory and Practice of Revenue Management, Kluwer, 2004, §2.6.2. https://doi.org/10.1007/b139000

Motivation

A cutting-stock shop receives orders for pieces of several lengths and cuts them from a limited menu of longer stock lengths. Each stock length has a cost. The shop can repeat any cutting pattern, so the central optimization question is which patterns meet the demand at least cost. The direct linear program has a variable for every possible pattern. Even a modest menu of piece lengths can yield too many columns to list before optimization begins. Gilmore and Gomory's 1961 article addresses this large-column obstacle by testing whether an as-yet-unlisted pattern could lower the cost of a current basic solution.

The article studies the linear programming relaxation: cutting activities may have nonnegative real weights rather than integer repetition counts. It does not claim that the resulting fractional optimum is always an integer cutting plan. Its worked example happens to have an integer optimum of cost 170; the authors explicitly note that this integrality is fortuitous (Gilmore and Gomory 1961, p. 858). The target here is the exact stopping condition for the relaxation.

Setting

An instance has $m$ ordered piece lengths $\ell_i$, demand $N_i\in\mathbb N$ for each piece length, and $k$ stock lengths $L_j$ with real costs $c_j$. A cutting pattern for stock $j$ is a vector of nonnegative integer counts $a_i$ with $\sum_i\ell_i a_i\le L_j$. An activity consists of that stock choice and its fitting pattern. Its demand column is $a=(a_i)$ and its cost is $c_j$. A surplus column for demand row $i$ has coefficient $-1$ in that row, zero elsewhere, and zero cost. The paper uses such columns to turn its demand inequalities into equations (Gilmore and Gomory 1961, p. 850, (1)–(3)).

A feasible solution assigns nonnegative real weights to finitely many activities and surplus columns so that activity output minus surplus equals $N_i$ in every row. Its cost is the weighted sum of stock costs. A basis $\beta$ lists $m$ columns with invertible coefficient matrix $A$ and cost row $C$. The associated bordered matrix, demand column, tableau column, and multipliers are

$$B=\begin{pmatrix}1&-C\\0&A\end{pmatrix},\qquad N'=(0,N_1,\ldots,N_m)^T,\qquad \bar N=B^{-1}N',\qquad b_i=(B^{-1})_{0,i+1}.$$

A feasible basis has nonnegative basic values, the last $m$ entries of $\bar N$. Those values on the basic columns, with zero on every other column, form the current basic solution. The first entry of $\bar N$ is its cost. These definitions follow the matrix and tableau of routine steps (2)–(4) (Gilmore and Gomory 1961, pp. 854–855).

Formalization targets

The goal is the stopping statement of step (4). If no nonbasic surplus column has a negative multiplier, and no available stock $j$ has a fitting pattern satisfying $\sum_i b_i a_i>c_j$, then the current solution is feasible and minimizes cost across all feasible activity and surplus assignments:

$$\bigl(\forall i\text{ with surplus }i\notin\beta,\ b_i\ge0\bigr) \quad\land\quad \bigl(\forall j,a,\ \sum_i\ell_i a_i\le L_j\Rightarrow\sum_i b_i a_i\le c_j\bigr) \quad\Longrightarrow\quad \operatorname{cost}(z_\beta)=\bar N_0\le\operatorname{cost}(z) \quad\text{for every feasible }z.$$

The six milestones record the paper's ingredients: the first row of $B^{-1}$ and the meaning of $\bar N$; the entering-column price test (4)–(5); the surplus-column test of step (3); the integer-pattern form (6)–(7); the maximum-pattern test; and the dynamic programming recurrence for $F_s(x)$ (Gilmore and Gomory 1961, pp. 852–855). The paper has no numbered theorems or lemmas; each milestone is drawn from a sentence or display on those pages.

Significance

The result makes a finite tableau a certificate for an optimization problem whose set of potential cutting activities is much larger than the current basis. A failed pricing search is meaningful only when it covers every fitting pattern for every stock length; the goal makes that full scope explicit. In the example, the final multipliers are $(2,3,5)$ and the relevant knapsack maxima for stock lengths $5$, $6$, and $9$ are $5$, $7$, and $10$, matching their stopping prices and the cost 170 (Gilmore and Gomory 1961, p. 858).

The mathematical argument is known from the 1961 article. This mission asks for a machine-checked Lean proof of its particular cutting-stock formulation, including the bounded-pattern search, bordered tableau, surplus columns, and global optimality conclusion. The proposal statements compile with proof placeholders; they are not already proved by those placeholders. Published general LP results are listed as references, but their finite-indexed formulations do not directly state the cutting-stock theorem.

Difficulty

Checking only the columns already in a tableau cannot establish optimality: an unlisted pattern might still fit a stock length and have a price greater than its cost. The article reduces this large search to an integer knapsack maximum for each stock length (Gilmore and Gomory 1961, pp. 852–853). Formalization must retain the distinction between a basis of $m$ columns and the full collection of possible columns. Strict improvement also needs care at a degenerate basic solution. The paper directs zero-ratio pivots to a separate degeneracy procedure (Gilmore and Gomory 1961, p. 855); the sufficient directions of the pricing milestones therefore require positive basic values, while the goal's optimality direction does not.

Formalization scope

Lean indexes piece types from zero and uses a separate initial cost coordinate followed by the $m$ demand coordinates for $B$. Thus the paper's $(i+1)$st bordered row corresponds to Lean demand index $i$. Patterns are vectors in $\mathbb N^m$; the zero pattern is included. A solution is a finitely supported real weighting of all activity and surplus columns. Global minimality quantifies over every such feasible weighting, including activities not in the current basis. No sign condition is imposed on stock costs or stock lengths in the goal; the goal is a conditional optimality statement and remains valid whenever its hypotheses hold.

The knapsack value $F_s(x)$ uses extended real numbers, giving $-\infty$ when no pattern fits, rather than an accidental real value from an empty supremum. The maximum-pattern milestone assumes positive piece lengths and nonnegative stock length, so the feasible set is finite and nonempty. The recursion milestone assumes positive lengths for all types through the newly added one; without the earlier positivity, a negative earlier length could let the new piece count exceed the displayed upper bound. The nondegeneracy hypotheses are confined to the sufficient directions of the three improvement milestones.

Reusable contributions include lemmas connecting the bordered inverse with $C A^{-1}$, finite-support linear program identities, and the integer knapsack recurrence. The source's rounding discussion, heuristic search, and under-specified anti-cycling device are outside this mission. An encoding that compares the current solution only with basis columns or generated columns would miss the paper's stopping claim.

Selected references

• P. C. Gilmore and R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6):849–859, 1961. DOI: 10.1287/opre.9.6.849.

Motivation

A Markov decision process with finitely many states and actions and a discounted cost criterion can be solved in three classical ways: policy iteration, value iteration, and linear programming. The third goes back to F. d'Epenoux's paper A Probabilistic Production and Inventory Problem (Management Science 10(1), 1963, partly redrafted from a translation of d'Epenoux's 1960 article in the Revue Française de Recherche Opérationnelle), which showed that the optimal discounted cost of a stochastic production and inventory model is the solution of a single linear program. Together with Manne's linear program for the average-cost case (1960), it is the origin of the linear programming approach to dynamic programming, which underlies occupation-measure methods, constrained Markov decision processes, and approximate linear programming for large models.

Timeline:

• 1957–1960. Bellman's Dynamic Programming (value iteration, the principle of optimality); Howard's policy iteration for average costs (1960); Manne's linear program for average costs (Linear programming and sequential decisions, Management Sci., 1960).
• 1960/1963. d'Epenoux treats the discounted case: policy iteration and value iteration (Sections 2–4), then the linear program $(P_2)$ and its dual (Sections 5–6). Footnote 2 credits Guilbaud (1957) with an earlier observation of an equivalent linear program in another context.
• 1967. Denardo, Contraction mappings in the theory underlying dynamic programming, places the linear programs in an abstract contraction framework.

Setting

The stock at the beginning of a period is $i \in \{0, 1, \dots, \sigma\}$, where $\sigma$ is the stock capacity. The decision is the potential $j$, the quantity available for the period (output plus initial stock), with $i \le j \le \sigma$. Given the potential $j$, the stock at the end of the period is $s$ with probability $p_{js}$; each row $(p_{js})_s$ is a probability vector. The expected cost of a period with initial stock $i$ and potential $j$ is a real number $d_{ij}$. Costs one period ahead are discounted by $\lambda$, $0 < \lambda < 1$.

A strategy is a map $J$ with $i \le J(i)$ for every $i$: the potential depends only on the current stock. It has the transition matrix $(P_J)_{is} = p_{J(i)s}$ and the cost vector $(d_J)_i = d_{iJ(i)}$. The cost of following $J$ forever is the solution $u$ of (2), $u = d_J + \lambda P_J u$. The optimal cost $u^*$ solves the fundamental equation (7),

$$u^*_i = \min_{j \ge i}\Big( d_{ij} + \lambda \sum_{s=0}^{\sigma} p_{js} u^*_s \Big), \qquad i = 0, \dots, \sigma .$$

For a vector $u$ put $U_{ij} = u_i - \lambda \sum_s p_{js} u_s - d_{ij}$. The set $A$ consists of the vectors satisfying the linear constraints (9), $U_{ij} \le 0$ for all admissible pairs $i \le j$. The set $B$ consists of the vectors with $\prod_{j \ge i} U_{ij} = 0$ for every $i$.

Formalization targets

Goal: $u^* = \max(u \in A)$, and $(P_2)$

The system (7) has a solution, and every solution $u^*$ is the greatest element of $A$:

$$u^* \in A, \qquad u \le u^* \ \text{componentwise for every } u \in A .$$

Moreover, for every weight vector $c$ with all $c_i > 0$ and $\sum_i c_i = 1$, $u^*$ is the unique optimal solution of

$$(P_2) \qquad \text{maximize } (1-\lambda) \sum_i c_i u_i \quad \text{subject to } U_{ij} \le 0 \ \ (i \le j).$$

Milestones

1. Eq. (3). For a stochastic matrix $P$ and $0<\lambda<1$, $I - \lambda P$ is invertible and $(I-\lambda P)^{-1} = \sum_{k \ge 0} \lambda^k P^k$.
2. Eq. (4). $u - \lambda P u \ge 0$ implies $u \ge 0$.
3. Eq. (5). If moreover $u - \lambda P u \ne 0$ and $P$ is indecomposable, then $u_i > 0$ for all $i$.
4. Eq. (7). (7) has a unique solution, the cost of an optimal strategy (referenced, Proved).
5. Section 5. $u$ solves (7) iff $u \in A \cap B$; the points of $B$ are exactly the costs of strategies.
6. Section 5. Every point of $A$ lies below every point of $B$.
7. Section 5. If every $P_J$ is indecomposable, $u^*$ is a strict vectorial maximum of $A$: $u \in A$, $u \ne u^*$ imply $u_i < u^*_i$ for all $i$.

Significance

The result turns a fixed-point equation with a minimum in it into a linear program with $\tfrac12(\sigma+1)(\sigma+2)$ linear constraints. Its consequences are the ones the paper draws in Section 6: the dual of $(P_2)$ has a probabilistic interpretation (discounted state–action frequencies), its optimal basic solutions are optimal strategies, and every linear programming algorithm becomes an algorithm for discounted dynamic programs. The uniqueness clause is what makes the weighted objective recover the whole cost vector; with a single objective $u_e$, as the paper notes, the optimum need not determine the complete optimal strategy when the states decompose into several groups.

The dynamic programming half of the paper (Sections 2–4: policy evaluation, policy iteration, value iteration) is already formalized and proved on the platform for the general finite discounted model, as Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.3.1 (BertsekasDP.discounted_main_theorem); it enters this mission as a reference item, and the mission's model is an instance of the same published structure BertsekasSSPModel. The linear programming half is not formalized. Related items in other models are posed elsewhere: Bäuerle and Rieder's Theorem 7.5.9 (finite-state linear program in a measure-theoretic reward model, open) and Denardo's Programs I–II in an abstract contraction model; neither states the componentwise maximality of $u^*$ in $A$ in this model.

Difficulty

The individual steps are short, but the goal combines several facts that are easy to state wrongly. The paper calls the invertibility of $I-\lambda P$ and the positivity of its inverse "known and obvious"; in Lean they are statements about an arbitrary stochastic matrix over Fin m, for which Mathlib provides no default matrix norm, and the comparison of $A$ with $B$ depends on them. Uniqueness of the optimum of $(P_2)$ needs both strict positivity of the weights and the componentwise maximality; with a zero weight it fails. The obvious first idea for the strict maximum, that indecomposability of the optimal strategy's matrix alone suffices, is not the formalized statement: only the sufficient condition over all strategies is posed.

Formalization scope

Stock levels and potentials are Fin (σ + 1), $0$-based. The kernel $p_{js}$ is an arbitrary stochastic kernel indexed by the potential, and the costs $d_{ij}$ are arbitrary reals; the paper's demand-driven kernel and its cost decomposition $d_{ij} = d'(j-i) + \sum_n p_n d''(i,j,n)$ are an instance and are not built in, because the arguments of Sections 2–5 use only stochasticity (the paper itself remarks on p. 101 that its methods apply far beyond the inventory problem). Only admissible pairs $i \le j$ enter $A$, $B$, the minimum in (7), and strategies. The discount is called lam in Lean. Equation (7) is the fixed-point equation of the Bellman operator BertsekasDiscountedBellmanOp of the model.

Explicit readings of the paper's phrases:

• "$u^* = \max(u \in A)$" is IsGreatest in the componentwise order.
• "the complete solution" of $(P_2)$ is uniqueness of its optimal solution, for every admissible weight vector.
• "$u > 0$" in (5) and "strict vectorial maximum" mean every component strictly positive, respectively strictly smaller.
• "indecomposable" means irreducible: for all $i,k$ some power $P^n$ has $(P^n)_{ik} > 0$. The weaker reading (one closed class plus transient states) makes (5) false.
• "the points of the set $B$ correspond to the costs associated with every possible strategy" is the equivalence between membership in $B$ and solving (2) for some strategy.

Ruled out: defining $u^*$ as the optimum of the linear program, as a supremum of $A$, or as a limit (which would make the goal circular); assuming a solution of (7) without the existence conjunct; constraining also the inadmissible pairs $j < i$ (which can exclude $u^*$ from $A$); and weakening the weights to $c_i \ge 0$.

Not formalized: the demand-driven kernel, the finite-horizon recursion of Section 2, the monotone convergence remark of Section 4 (c), the count of strategies, the reformulations $(P_1)$ and $(P_3)$, and all of Section 6 (duality). Contributions welcome: proofs of the milestones and of the goal, and, as a follow-up mission, the dual programs of Section 6. The matrix facts (3)–(5) are stated for arbitrary stochastic matrices and are reusable beyond this mission.

Selected references

• F. d'Epenoux, A Probabilistic Production and Inventory Problem, Management Science 10(1), 98–108, 1963. https://doi.org/10.1287/mnsc.10.1.98
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3), 259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press and John Wiley, 1960.
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.
• E. V. Denardo, Contraction Mappings in the Theory Underlying Dynamic Programming, SIAM Review 9(2), 165–177, 1967. https://doi.org/10.1137/1009030
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Prop. 7.3.1.
• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Section 7.5. https://doi.org/10.1007/978-3-642-18324-9

Motivation

Every linear program comes with a second linear program, its dual, whose feasible solutions certify bounds on the optimum of the first. The duality theorem of linear programming says that these certificates are perfect: when both programs are feasible, the best bound equals the optimum. The theorem underlies the analysis of the simplex method, sensitivity analysis and shadow prices in operations research, the minimax theorem for zero-sum games, max-flow/min-cut and König-type min-max theorems in combinatorial optimization, and the primal–dual design of approximation and online algorithms.

The Farkas lemma, a theorem of the alternative for linear systems, contains the essence of duality: a system of linear equations or inequalities either has a (nonnegative) solution, or a single linear combination of its rows proves that it has none. It goes back to Farkas (1902) and Minkowski's work on finitely generated cones; the duality theorem itself is due to von Neumann (1947) and Gale, Kuhn and Tucker (1951).

This mission formalizes Chapter 6 of Matoušek and Gärtner's textbook Understanding and Using Linear Programming (Springer, 2007): the duality theorem in the book's form, weak duality, the Farkas lemma in its algebraic, geometric and three-variant forms, and the lemmas of two self-contained proofs of the Farkas lemma, one analytic (nearest points in finitely generated cones) and one via minimally infeasible systems.

Setting

Let $A$ be a real matrix with $m$ rows and $n$ columns, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$. Vector inequalities are componentwise. The primal and dual linear programs are

$$\text{(P)}\quad\max\ c^{T}x \ \text{ s.t. } Ax\le b,\ x\ge 0, \qquad\qquad \text{(D)}\quad\min\ b^{T}y \ \text{ s.t. } A^{T}y\ge c,\ y\ge 0.$$

A feasible solution of (P) is an $x\in\mathbb{R}^n$ satisfying its constraints; an optimal solution is a feasible $x^*$ with $c^{T}x\le c^{T}x^*$ for every feasible $x$. (P) is unbounded if its objective takes arbitrarily large values on feasible solutions. For the minimization (D) the notions are mirrored: an optimal $y^*$ has $b^{T}y^*\le b^{T}y$ for all feasible $y$, and (D) is unbounded if $b^{T}y$ takes arbitrarily small values.

For $a_1,\dots,a_n\in\mathbb{R}^m$, the convex cone generated by them is $C=\{t_1a_1+\dots+t_na_n : t_i\ge 0\}$; a primitive cone is one generated by $k\le m$ linearly independent vectors. A system $Ax\le b$ of $m$ inequalities is minimally infeasible if it has no solution but dropping any one inequality makes it solvable.

Formalization targets

Goal: the duality theorem (§6.1, p. 83)

For (P) and (D) as above, exactly one of the following occurs:

1. neither (P) nor (D) is feasible;
2. (P) is unbounded and (D) is infeasible;
3. (P) is infeasible and (D) is unbounded;
4. both are feasible; then both have optimal solutions, and every optimal $x^*$ of (P) and optimal $y^*$ of (D) satisfy

$$c^{T}x^*=b^{T}y^*.$$

Milestones

• Proposition 6.1.1 (weak duality). $c^{T}x\le b^{T}y$ for all feasible $x$ of (P) and $y$ of (D); hence (P) unbounded forces (D) infeasible, and (D) unbounded forces (P) infeasible.
• Proposition 6.4.1 (Farkas lemma). Exactly one of: $Ax=b$ has a solution $x\ge 0$; some $y$ has $y^{T}A\ge 0^{T}$ and $y^{T}b<0$. Already on the platform as LinearOptimization.farkas_lemma (Proved) and linked as a reference.
• Proposition 6.4.3 (three variants). Solvability of $Ax=b$, $x\ge0$; of $Ax\le b$, $x\ge 0$; and of $Ax\le b$ with $x$ free, each characterized by a certificate condition on $y$.
• Proposition 6.4.2 (geometric Farkas lemma). $b$ lies in the cone generated by $a_1,\dots,a_n$, or a hyperplane through $0$ separates the cone from $b$ strictly — exactly one.
• Lemmas 6.5.4, 6.5.5, 6.5.3, 6.5.1. Primitive cones are closed; a finitely generated cone is a finite union of primitive cones; hence it is closed (6.5.3, on the platform as Polyhedral.isClosed_conicSpan, Proved); hence it has a point nearest to any $b\notin C$.
• Lemmas 6.6.2 and 6.6.1. $Ax=b$ is solvable iff every $y$ with $y^{T}A=0^{T}$ has $y^{T}b=0$; in a minimally infeasible system, for every $i$ some $\tilde x^{(i)}$ satisfies all inequalities except the $i$th with equality.

Significance

The result. The duality theorem converts optimality into feasibility: a pair $(x,y)$ of primal and dual feasible solutions with $c^{T}x=b^{T}y$ is a short, checkable certificate that both are optimal, and the theorem guarantees such a certificate exists whenever an optimum does. It classifies every primal–dual pair into four behaviours and excludes the other five combinations of feasible-bounded, unbounded and infeasible. Later chapters of the same book rest on it: the minimax theorem for zero-sum games, the integrality of bipartite matching polytopes, the LP rounding for unrelated-machine scheduling, and the Delsarte bound for codes.

Formalizing it. All results here are classical and fully proved in the book; the work is formalization. Mathlib contains a Farkas lemma for proper cones in Hilbert spaces and closedness facts for finitely generated cones, and the platform already has Bertsimas–Tsitsiklis-style duality for a general-form minimization (LinearOptimization.lp_strong_duality) and matrix Farkas lemmas. What is missing is the textbook statement in Matoušek's inequality form (P)/(D), with its four-case exclusive classification, together with the chain of named lemmas that make two different elementary proofs of the Farkas lemma machine-checkable. The analytic chain (6.5.x) and the minimally-infeasible chain (6.6.x) are reusable independently of LP.

Difficulty

Weak duality is a two-line computation. The difficulty is entirely in the reverse direction, that a feasible bounded (P) forces the dual to be feasible with the same value. Any proof must use something beyond linear algebra over $\mathbb{R}$: either the termination of the simplex method with an anticycling rule, a topological fact (a finitely generated cone is closed), or an extremal argument (an optimal solution of an auxiliary LP). The naive geometric argument — take the nearest point of the cone to $b$ — fails without closedness, and closedness of the cone generated by a set is false for infinitely generated cones (the cone over a disc touching the origin is an open half-plane plus a point), so finiteness has to be used, which is the role of the primitive-cone decomposition. In the four-case theorem itself, the remaining obstacle is attainment: "bounded and feasible" must be upgraded to "an optimum exists" for both programs, which is not a consequence of Farkas-type statements alone.

Formalization scope

• Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ become $0,\dots,n-1$. The row vector $y^{T}A$ is Aᵀ *ᵥ y, so $y^{T}A\ge 0^{T}$ is 0 ≤ Aᵀ *ᵥ y; scalar products are ⬝ᵥ.
• Optimal solutions and unboundedness are stated against every feasible point; no sSup/sInf is used, so no junk value of an empty or unbounded supremum enters. "Exactly one of the four cases" is ∃! k : Fin 4, DualityCase A b c k, with the book's case $k$ at index $k-1$; a plain disjunction would be weaker than the book.
• Cone items live in EuclideanSpace ℝ (Fin m), so the nearest point of Lemma 6.5.1 is Euclidean and $y^{T}x$ is the inner product. The convex cone generated by $a_1,\dots,a_n$ is the set of nonnegative combinations (it contains $0$, also for $n=0$).
• A trivializing formalization — case 4 read as "if both have optimal solutions then their values agree", which is weak duality plus nothing — is ruled out: case 4 asserts the existence of both optima from feasibility alone.
• Lemma 6.3.1 (the dual solution read off the final simplex tableau) and Lemma 6.5.2 (nearest point in a nonempty closed set, available in Mathlib as IsClosed.exists_infDist_eq_dist) are not separate targets. The Fourier–Motzkin elimination of §6.7 has no numbered result.
• Contributions welcome: proofs of any milestone, the two Farkas-lemma chains, and bridges to the general-form duality already on the platform.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, Chapter 6. https://doi.org/10.1007/978-3-540-30717-4
• J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
• D. Gale, H. W. Kuhn and A. W. Tucker, Linear programming and the theory of games, in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.
• M. Conforti, M. Di Summa and G. Zambelli, Minimally infeasible set-partitioning problems with balanced constraints, Mathematics of Operations Research (cited in the book as to appear; the source of the proof in §6.6).
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 4.

Motivation

Dantzig–Wolfe decomposition and column generation solve large integer programs by replacing a set of "easy" constraints with a description of its feasible points, and then pricing out the points one at a time. For linear programs this rests on the Minkowski–Weyl representation: every point of a polyhedron is a convex combination of its extreme points plus a nonnegative combination of its extreme rays. For integer programs that representation is not enough. Imposing integrality on the convex multipliers of the extreme points of $\mathrm{conv}(X)$ does not give back the integer program, because an optimal integer point may lie in the interior of $\mathrm{conv}(X)$.

Lübbecke and Desrosiers, in their survey Selected Topics in Column Generation (Operations Research 53(6), 2005), present discretization (Johnson 1989, Vanderbeck 2000) as the true integer analogue of the decomposition principle. Its basis is their Theorem 1: the integer points of a rational polyhedron are generated by finitely many integer points and finitely many integer rays with integer multipliers. The paper states this result and refers its proof to Nemhauser and Wolsey, Integer and Combinatorial Optimization (1988). It underlies the integer master problem (25) of branch-and-price.

Setting

Let $D$ be an $m \times n$ matrix and $\mathbf d$ an $m$-vector with rational entries. The polyhedron is

$$P = \{\mathbf x \in \mathbb R^n \mid D\mathbf x \geqslant \mathbf d,\ \mathbf x \geqslant \mathbf 0\},$$

and its set of integer points is $X = P \cap \mathbb Z^n$, the points of $P$ whose coordinates are all integers. Because $P \subseteq \mathbb R^n_+$, $X = P \cap \mathbb Z^n_+$.

The recession cone of $P$ is $\{\mathbf r \in \mathbb R^n \mid D\mathbf r \geqslant \mathbf 0,\ \mathbf r \geqslant \mathbf 0\}$. An integer ray of $P$ is a nonzero vector of $\mathbb Z^n$ in this cone. Extreme rays are not required.

In Lean these are polyhedronP D d, integerPoints D d, recessionConeP D and IsIntegerRay D w in the namespace Lubbecke2005.Discretization, with integer vectors cast to real vectors by castVec.

Formalization targets

Goal: Theorem 1 (pp. 1011–1012)

If $P \neq \emptyset$, there exist a finite set of integer points $\{\mathbf p_q\}_{q \in Q} \subseteq X$ and a finite set of integer rays $\{\mathbf p_r\}_{r \in R}$ of $P$ such that

$$X = \Bigl\{\mathbf x \in \mathbb R^n_+ \ \Big|\ \mathbf x = \sum_{q \in Q} \mathbf p_q \lambda_q + \sum_{r \in R} \mathbf p_r \lambda_r,\ \sum_{q \in Q} \lambda_q = 1,\ \boldsymbol\lambda \in \mathbb Z_+^{|Q|+|R|}\Bigr\}. \qquad (24)$$

Since the multipliers are nonnegative integers summing to one over $Q$, (24) says that $X$ is the union, over $q \in Q$, of the translates $\mathbf p_q + \mathbb Z_+\{\mathbf p_r\}_{r\in R}$ of the monoid generated by the rays. No bound on $|Q|$ or $|R|$ is part of the goal.

Milestone: Remark in §3.3 (p. 1012)

If $X \subseteq [0,1]^n$, every point of $X$ is a vertex of $\mathrm{conv}(X)$. In this case convexification and discretization coincide.

Significance

The result. Theorem 1 converts an integer program $\min\{c(\mathbf x) \mid A\mathbf x \geqslant \mathbf b,\ \mathbf x \in X\}$ into the integer master program (25) over the multipliers $\boldsymbol\lambda$, with one column per generating point and per generating ray. When $X$ is bounded the rays disappear, exactly one $\lambda_q$ equals one, and (25) is a linear integer program even for a nonlinear cost $c$. The representation is what makes branching on master variables, and the passage between compact and extensive formulations, well defined in branch-and-price.

Formalizing it. The result is classical (Nemhauser–Wolsey 1988, going back to Giles and Pulleyblank and to Meyer's theorem that the integer hull of a rational polyhedron is a polyhedron). On Prove2Me, the real representation (8) is formalized as LinearOptimization.polyhedron_resolution (Bertsimas–Tsitsiklis Thm 4.15) and the integer hull theorem as LinearOptimization.integer_hull_is_polyhedron (Thm 11.3); both are included as reference items. The convexification counterpart of §3.2, that the Lagrangian dual equals the LP over $\mathrm{conv}(X)$, is LinearOptimization.lagrangean_dual_eq_lp_over_hull. No machine-checked statement of the integer representation (24), with integer multipliers and integer rays, was found on the platform. The mission produces that statement and, once solved, its proof.

Difficulty

The obvious attempt applies the real representation (8) and rounds. It fails twice. First, the extreme points of $P$ need not be integral, and an integer point written as a real combination of vertices and rays has no reason to have integer multipliers. Second, the extreme rays of $P$ generate the recession cone over $\mathbb R_+$, but the integer points of that cone are not in general nonnegative integer combinations of the (scaled) extreme rays; a generating set of the lattice points of a cone must usually contain non-extreme vectors. The finiteness of $Q$ is also not automatic: $X$ itself is typically infinite, and taking $Q = X$ trivializes the statement.

Rationality of the data is essential. For $P = \{\mathbf x \in \mathbb R^2_+ \mid \sqrt2\,x_1 - x_2 \geqslant 0\}$, every integer ray has slope below $\sqrt 2$, so finitely many base points and rays generate only points with $x_2 \leqslant \rho x_1 + C$ for some $\rho < \sqrt 2$, while $X$ contains $(k, \lfloor\sqrt2 k\rfloor)$ for every $k$.

Formalization scope

• Vectors are Fin n → ℝ; integer vectors are Fin n → ℤ cast coordinatewise. Both sides of (24) are sets of real vectors.
• $D$ and $\mathbf d$ are ℚ-valued and cast to ℝ. This is an addition: the paper names no field, and the theorem is false for irrational data (see Difficulty). The cited source, Nemhauser–Wolsey, works with rational data.
• The hypothesis $P \neq \emptyset$ is kept as on the page. $X$ may still be empty (e.g. $P = \{1/2\}$); then $Q = \emptyset$ and both sides of (24) are empty. The statement allows this.
• $Q$ and $R$ are Fin k and Fin l for existentially chosen $k, l \in \mathbb N$; the finiteness is the content of the theorem. The multiplier vector $\boldsymbol\lambda \in \mathbb Z_+^{|Q|+|R|}$ is written as a pair of ℕ-valued vectors.
• "Integer rays of $P$" is read as nonzero integer vectors in the recession cone $\{D\mathbf r \geqslant \mathbf 0, \mathbf r \geqslant \mathbf 0\}$; extremality is not required, as the page does not require it (contrast (8), which says "extreme rays").
• The constraint $\mathbf x \in \mathbb R^n_+$ on the right side of (24) is kept although it is implied.
• In the Remark, "vertices of $\mathrm{conv}(X)$" is read as extreme points of the convex hull; $X$ is finite there, so the two notions agree.

A formalization with real multipliers would be the resolution theorem (8), already on the platform, and one with $Q$ or $R$ infinite would be trivial; both are excluded by the statement.

Useful infrastructure: lattice points of rational polyhedral cones (Hilbert bases, Gordan's lemma), the integer hull theorem, and the real resolution theorem. A proof of Gordan's lemma for rational cones in this vocabulary would be reusable well beyond this mission. Contributions toward any of these are welcome.

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
• G. L. Nemhauser and L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
• R. R. Meyer, On the existence of optimal solutions to integer and mixed-integer programming problems, Mathematical Programming 7:223–235, 1974. https://doi.org/10.1007/BF01585518
• F. Vanderbeck, On Dantzig–Wolfe decomposition in integer programming and ways to perform branching in a branch-and-price algorithm, Operations Research 48(1):111–128, 2000. https://doi.org/10.1287/opre.48.1.111.12453
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

Motivation

The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how $k$ mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is $2$ on every metric space with at least three points.

Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is $3/2$. Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths $1$, $d$, $d$. These exact values are among the few known optimal randomized ratios for server problems.

Timeline:

• 1990: Manasse, McGeoch and Sleator introduce the $k$-server problem and prove the deterministic two-server ratio is $2$.
• 1990–1994: Karlin, Manasse, McGeoch and Owicki submit this paper (received August 1990, revised September 1991) and publish it in Algorithmica in 1994, with the isosceles-triangle ratios of Theorem 12 and the 3-4-5 triangle ratio $1652/1069$ of Theorem 13.
• Later: Karloff, Rabani and Ravid extend the technique to $\Omega(\log\log k)$ and $\Omega(\log k)$ randomized lower bounds (cited on p. 564); Bubeck, Coester and Rabani (STOC 2023) refute the randomized $k$-server conjecture.

Setting

Fix an integer $d\ge1$. The isosceles triangle $M$ has three points $a$, $b$, $c$ with

$$\operatorname{dist}(a,b)=1,\qquad \operatorname{dist}(a,c)=\operatorname{dist}(b,c)=d.$$

A configuration $C:\{0,1\}\to M$ places two labelled servers on points of $M$. A deterministic on-line algorithm assigns to every finite request sequence $\sigma=(r_1,\dots,r_n)$ a configuration, computed from $\sigma$ alone and covering the last request; its value on the empty sequence is its initial configuration. Its cost $C_A(\sigma)$ is the total distance its servers move while serving $\sigma$ request by request. The off-line optimum $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the least total movement of any schedule that starts at $C_0$ and covers each request in turn, knowing $\sigma$ in advance.

A randomized algorithm is a probability distribution on deterministic on-line algorithms; its expected cost is $\mathbf{E}C_A(\sigma)$. It is $\rho$-competitive against an oblivious adversary from $C_0$ if every algorithm in its support starts at $C_0$ and there is a constant $a$ such that

$$\mathbf{E}C_A(\sigma)\le\rho\cdot C_{opt}(\sigma)+a\qquad\text{for every request sequence }\sigma.$$

The request sequence is fixed in advance and does not react to the algorithm's coin flips.

Write $e_p=(1+1/p)^p$ and

$$\alpha_d=\frac{e_{2d-1}+1/4d}{(e_{2d-1}-1)+1/2d},\qquad e_{2d-1}=\left(\frac{2d}{2d-1}\right)^{2d-1}.$$

In Lean this is NonuniformCompetitive.Isosceles.isoscelesRatio d.

Formalization targets

Goal: Theorem 12

For every $d\ge1$ and every initial configuration $C_0$:

$$\forall A,\ \forall\rho,\quad A\text{ is }\rho\text{-competitive from }C_0\ \Longrightarrow\ \rho\ge\alpha_d,$$ $$\exists A:\ A\text{ is }\alpha_d\text{-competitive from }C_0.$$

The two claims are also milestones of their own (no_better_ratio, ratio_attained).

The phase LP (§5, pp. 565–566)

For free real $\pi_1,\dots,\pi_{2d-1}$ and real $\alpha$ with

$$(\pi_k)2d+\sum_{i=1}^k(1-\pi_i)\le\alpha k\ \ (1\le k<2d),\qquad 2d+\sum_{i=1}^{2d-1}(1-\pi_i)+\tfrac12\le\alpha\cdot2d,$$

one has $\alpha\ge\alpha_d$ (lp_lower_bound); and $\pi_k=(\alpha_d-1)\big((2d/(2d-1))^k-1\big)$, $\pi_{2d}=1$ is nondecreasing from $\pi_1\ge0$ to $1$ and makes every constraint an equality (lp_attained).

The limit remark (§5, p. 566)

$$\alpha_1<\alpha_2<\alpha_3<\cdots,\qquad \lim_{d\to\infty}\alpha_d=\frac{e}{e-1}$$

(ratio_increases_to_e_ratio).

Significance

The theorem gives an exact optimal randomized ratio for an infinite family of metric spaces. It shows that the optimal randomized two-server ratio is not a constant: it runs from $3/2$ on the equilateral triangle to $e/(e-1)\approx1.582$ as the triangle becomes long and thin, where the problem resembles ski rental. With the deterministic ratio $2$, it quantifies exactly how much randomization gains on these spaces.

The results are proved in the paper; none is formalized on Prove2Me, and no machine-checked proof of them is known. A formal proof would require the paper's phase framework (Theorems 1–3 and the appendix's Theorem 15) for server problems, which this mission does not state separately, and a concrete randomized algorithm as a measurable mixed strategy. Both would be reusable for Theorem 13 (the 3-4-5 triangle) and for other exact ratios on small metric spaces.

Difficulty

The phase LP milestones are finite real arithmetic. The difficulty is the passage between them and the goal. The lower bound must hold for every randomized algorithm, not only phase-based lazy ones: an arbitrary algorithm may condition on the whole history, move non-lazily, and randomize in ways that do not reduce to the probabilities $\pi_k$. The paper handles this with Theorem 3, which says that the LP bound of phase-based algorithms bounds the competitive factor of all algorithms; its proof uses an averaging argument over histories that must be made rigorous. The upper bound needs a mixed strategy over infinitely many phases, with measurable costs, an explicit additive constant covering the first partial phase from an arbitrary initial configuration, and an accounting of $C_{opt}$ across phase boundaries.

Formalization scope

The model is the platform's published KServer_model and KServer_randomized (reference items): labelled servers Fin 2 → M; a deterministic on-line algorithm as a map from request prefixes to configurations; a randomized algorithm as a probability measure over deterministic algorithms, with the cost of each fixed sequence measurable in the random outcome; expected cost as a lower Lebesgue integral in $[0,\infty]$; the off-line optimum as a real infimum over schedules from $C_0$ (nonempty and bounded below by $0$); and IsCompetitiveFrom A C₀ c with a real additive constant.

Committed conventions:

• The triangle is any metric space whose points are exactly $a,b,c$ at distances $1,d,d$, with $d$ a natural number and $d\ge1$. Every such space is isometric to the paper's triangle; at $d=0$ it would not be a triangle.
• Both claims are stated for every initial configuration, including both servers on one point. The paper treats the initial state $\{a,b\}$ separately and absorbs the first partial phase into the additive constant.
• The lower bound quantifies over all randomized algorithms (deterministic ones are point masses), never over phase-based ones only.
• In the LP milestones the $\pi_k$ are free reals, as printed; no box $0\le\pi_k\le1$ is imposed.
• "Grows" in the limit remark is read as strictly increasing.
• The paper prints the recurrence on p. 565 as $\pi_k=\frac{\alpha-1+(\pi_{k-1})2d-1}{2d}$; the equations $(*)$ give $\pi_k=\frac{\alpha-1+2d\,\pi_{k-1}}{2d-1}$. The recurrence is not used; the closed form printed on p. 566 is correct and is the one stated.

Without the measurability field of a randomized algorithm the lower integral would under-report expected cost and the attainment claim would become easier than the paper's; the published definition includes it. The lower bound is not vacuous: the triangle hypotheses are satisfiable for every $d\ge1$.

Welcome contributions: a formal version of the phase framework (Theorems 1–3, 15) for finite metric spaces, reusable across missions III and IV; a measurable construction of phase-based randomized algorithms; and proofs of the LP milestones.

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
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
• H. Karloff, Y. Rabani, Y. Ravid, Lower Bounds for Randomized k-Server and Motion-Planning Algorithms, SIAM J. Comput. 23 (1994) 293–312. https://doi.org/10.1137/S0097539792224838
• S. Bubeck, C. Coester, Y. Rabani, The Randomized k-Server Conjecture Is False!, STOC 2023. https://arxiv.org/abs/2211.05753

Motivation

An algorithm for linear programming is strongly polynomial if the number of arithmetic operations it performs is bounded by a polynomial in the dimension of the problem alone (the number of variables and constraints), independently of the bit lengths of the numbers in the input. Many combinatorial optimization problems are linear programs over polyhedra of the form $P = \{x \in \mathbb{R}^n : Ax \le b\}$ whose constraint matrix $A$ has entries $0, +1, -1$, but whose objective vector $w$ is an arbitrary rational weight vector. Polynomial-time algorithms for such problems (for instance the ellipsoid-based algorithms of Grötschel, Lovász and Schrijver for maximum-weight cliques in perfect graphs, submodular flows, and matroid polyhedra) have running times that depend on the length of $w$.

Frank and Tardos (Combinatorica 1987) remove this dependence once and for all: they replace $w$ by an integral objective $\tilde w$ whose entries have $O(n^3)$ bits and which has exactly the same optimal solutions and the same optimal dual bases as $w$ over every such polyhedron. Any algorithm that is polynomial in $n$ and in the length of the objective then becomes strongly polynomial. The tool is simultaneous Diophantine approximation, used through the lattice-basis-reduction algorithm of Lenstra, Lenstra and Lovász (Math. Ann. 1982). The technique extends Tardos's strongly polynomial algorithm for linear programs with small constraint matrices (Oper. Res. 1986), which applies only to explicitly given programs.

Setting

For $x \in \mathbb{R}^n$ write $\|x\|_\infty = \max_j |x(j)|$ and $\|x\|_1 = \sum_j |x(j)|$; $\operatorname{sign}$ takes the values $-1, 0, +1$.

Decomposition. Fix a positive integer $N$. A decomposition of $w \in \mathbb{R}^n$ is an expression

$$w = \sum_{i=1}^k \lambda_i v_i, \qquad \lambda_i > 0,\ v_i \in \mathbb{Z}^n.$$

It satisfies condition (iii) if for $i = 2, \dots, k$ the vector $v_i$ is nonzero and $\lambda_i/\lambda_{i-1} \le 1/(N\|v_i\|_\infty)$: the coefficients decrease so quickly that each term is negligible against the previous one.

Preprocessing. Given a rational $w$ and $N$, the paper's preprocessing algorithm finds a decomposition with $k \le n$, condition (iii), and the size bound (ii)' $\|v_i\|_\infty \le 2^{n^2+n}N^n$, and outputs

$$\tilde w = \sum_{i=1}^k M^{k-i} v_i, \qquad M = 2^{n^2+n} N^{n+1}.$$

Linear programs. Let $A$ be an $m \times n$ matrix with entries in $\{0, \pm 1\}$ and $b \in \mathbb{R}^m$. The primal program is $\max\{wx : Ax \le b\}$ and the dual program is $\min\{yb : yA = w,\ y \ge 0\}$. A point $\bar x \in P$ is $w$-maximal if $w\bar x = \max(wx : x \in P)$. A dual basis is a maximal set of row indices of $A$ whose rows are linearly independent; it determines at most one $y$ with $yA = w$ supported on it (the basic dual solution), and it is an optimal dual basis if that $y$ exists and is optimal for the dual program.

Formalization targets

Goal — Theorem 4.2 (p. 58)

For every $w \in \mathbb{Q}^n$, with $N = (n+1)! + 1$, there is $\tilde w \in \mathbb{Z}^n$ with

$$\|\tilde w\|_\infty \le 2^{4n^3} N^{n(n+2)}$$

such that for every $0, \pm1$ matrix $A$ with $n$ columns and every $b$: (i) $x \in P$ is $w$-maximal if and only if it is $\tilde w$-maximal; (ii) a set of rows of $A$ is an optimal dual basis for $w$ if and only if it is one for $\tilde w$. The vector $\tilde w$ depends on $w$ only, not on $A$ or $b$.

Milestones

1. Dirichlet's theorem (p. 52): for $N \ge 1$ and $\alpha \in \mathbb{R}^n$ there are $p \in \mathbb{Z}^n$ and $1 \le q \le N^n$ with $|q\alpha(i) - p(i)| < 1/N$ for all $i$.
2. Theorem 3.1 (p. 53): every $w \in \mathbb{R}^n$ has a decomposition with $k \le n$, $\|v_i\|_\infty \le N^n$ and condition (iii).
3. Lemma 3.2 (pp. 54–55): under condition (iii), for integral $b$ with $\|b\|_1 \le N - 1$, $\operatorname{sign}(b \cdot w) = \operatorname{sign}(b \cdot v_j)$ for the smallest $j$ with $b \cdot v_j \ne 0$, and $b \cdot w = 0$ if there is no such $j$.
4. Theorem 3.3 (p. 56): the preprocessed $\tilde w$ satisfies $\|\tilde w\|_\infty \le 2^{4n^3}N^{n(n+2)}$ and $\operatorname{sign}(w \cdot b) = \operatorname{sign}(\tilde w \cdot b)$ for all integral $b$ with $\|b\|_1 \le N-1$.
5. The case $N = n+1$ (p. 55): an integral $\tilde w$ with $\|\tilde w\|_\infty \le 2^{4n^3}(n+1)^{n(n+2)}$ and $\tilde w(X) \le \tilde w(Y) \iff w(X) \le w(Y)$ for all subsets $X, Y$ of coordinates.
6. Lemma 4.1 (i) (p. 57): if $\operatorname{sign}(w' \cdot h) = \operatorname{sign}(w'' \cdot h)$ for all integral $h$ with $\|h\|_1 \le (n+1)!$, then $w'$ and $w''$ have the same maximizers over $\{Ax \le b\}$ for every $0, \pm1$ matrix $A$.
7. Lemma 4.1 (ii) (p. 57): under the same hypothesis, a dual basis is optimal for $w'$ if and only if it is optimal for $w''$.

Significance

The result gives a general reduction: whenever a class of polyhedra with $0, \pm1$ constraint matrices admits an optimization algorithm that is polynomial in $n$ and in the length of the objective, it admits a strongly polynomial one. The paper applies this to maximum-weight cliques in perfect graphs, optimization over submodular flow polyhedra, and matroid polyhedra membership, and its Section 5 applies the same rounding to the integer programming algorithms of Lenstra and Kannan. The subset-sum corollary (milestone 5) is independently useful: every rational weight function on a finite set can be replaced by an integral one with $O(n^3)$-bit entries that orders all subset sums identically.

All statements of this mission have been proved on paper since 1987. None is formalized on Prove2Me, and Mathlib contains only the one-dimensional Dirichlet approximation theorem. The mission produces a machine-checked version of the exact statements, with the explicit constants of the paper; the complexity claims (operation counts, strong polynomiality) are not part of it.

Difficulty

The goal combines two independent parts. The number-theoretic part (milestones 1–5) needs a multidimensional Dirichlet theorem, an induction producing the decomposition, and exact inequality chains with the constants $2^{n^2+n}N^n$ and $2^{4n^3}N^{n(n+2)}$. The linear-programming part (milestones 6–7) needs bounds on the entries of inverses of nonsingular $0, \pm1$ submatrices, the existence of optimal dual solutions supported on a dual basis, LP duality and complementary slackness. The obvious first idea, scaling $w$ to an integer vector by a common denominator, preserves every sign but gives no bound on $\|\tilde w\|_\infty$ in terms of $n$; the bound is the content of the theorem. Likewise, rounding each coordinate of $w$ separately to a fixed precision does not preserve the sign of $w \cdot b$ when $w \cdot b$ is tiny but nonzero.

Formalization scope

Vectors are functions on Fin n: the input $w$ is rational (Fin n → ℚ) in the goal, in Theorem 3.3 and in the subset-sum corollary, as in the algorithm's input line; it is real in Theorem 3.1, Lemma 3.2 and Lemma 4.1, as on the page. Integral vectors are Fin n → ℤ, and $A$ is a Matrix (Fin m) (Fin n) ℤ with every entry in $\{-1, 0, 1\}$, cast to $\mathbb{R}$; $b \in \mathbb{R}^m$ is unrestricted. Decompositions are indexed by $i \in \{1, \dots, k\} \subseteq \mathbb{N}$ as in the paper. $\|b\|_1$ is always the explicit sum $\sum_j |b(j)|$, compared with $N - 1$ in $\mathbb{Z}$; $\|v\|_\infty$ of an integer vector is a natural number (supNorm). Sign equality uses SignType.sign and includes the zero case. Condition (iii) is stated multiplicatively together with $v_i \ne 0$, which the paper's quotient presupposes; without $v_i \ne 0$ Lemma 3.2 fails. An optimal dual basis is a maximal linearly independent set of row indices together with an optimal dual solution supported on it.

Two formalizations would make the goal trivial and are excluded: dropping the bound on $\|\tilde w\|_\infty$ (a multiple of $w$ then works), and letting $\tilde w$ depend on $A$ and $b$ (the goal states $\exists \tilde w$ before $\forall A, b$). The $0, \pm1$ assumption on $A$ is part of every Section 4 statement.

A complete development needs a multidimensional pigeonhole argument, determinant and adjugate bounds for $0, \pm 1$ matrices, and basic LP duality (strong duality, complementary slackness, basic optimal dual solutions); the last two are reusable across linear-programming missions. Proofs of individual milestones, reusable lemmas on LP duality, and alternative proofs of Dirichlet's theorem are all welcome.

Selected references

• A. Frank and É. Tardos, An application of simultaneous diophantine approximation in combinatorial optimization, Combinatorica 7(1) (1987) 49–65. https://doi.org/10.1007/BF02579200
• A. K. Lenstra, H. W. Lenstra Jr. and L. Lovász, Factoring polynomials with rational coefficients, Math. Ann. 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Operations Research 34(2) (1986) 250–256. https://doi.org/10.1287/opre.34.2.250
• M. Grötschel, L. Lovász and A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981) 169–197. https://doi.org/10.1007/BF02579273
• J. W. S. Cassels, An Introduction to the Theory of Numbers (title as printed in the paper's reference [2]), Springer, Berlin, 1971; cited in the paper as [2, Sect. 1.10] for Dirichlet's theorem.