Linear Optimization

Completed

Combinatorics Operations Research·Captain: mikedeng1

A Linear Programming Approach to the Cutting Stock Problem—Part II 1: The Lexicographic Knapsack Method Terminates, and M_1 Equals max(c_1, the Knapsack Optimum for the Longest Stock Length L_1)Research Paper

Motivation

The cutting stock problem asks how to cut standard stock rolls of length $L$ into pieces of demanded lengths $l_1,\dots,l_m$ so that the demands are met at least cost. Gilmore and Gomory solved its linear programming relaxation by column generation (Part I, Opns. Res. 9 (1961)): every cutting pattern is a column, and the column to bring into the basis is found by solving an integer knapsack problem whose objective is given by the current dual prices. In Part II (Opns. Res. 11 (1963)) they replaced the dynamic-programming knapsack solver of Part I by a lexicographic enumeration with a bound test, the Knapsack Method, and reported it to be about five times as fast as dynamic programming on their problem set (p. 866). The method is an early enumeration-with-bounds (branch-and-bound type) procedure for the integer knapsack, and the same pricing problem remains the inner loop of column generation for cutting stock, bin packing and their many variants.

Setting

There are $m$ demanded lengths $l_1,\dots,l_m>0$ with linear programming prices $b_1,\dots,b_m\ge0$ , and $k$ standard stock lengths $L_1,\dots,L_k$ with costs $c_1,\dots,c_k$ . A column for $L_j$ is a vector $(\alpha)_m=(a_1,\dots,a_m)$ of nonnegative integers with $\sum_i l_ia_i\le L_j$ . The knapsack problem (1) for $L_j$ is

\bar M_j=\max\Big\{\sum_{i=1}^m b_ia_i : a_i\in\mathbb Z_{\ge0},\ \sum_{i=1}^m l_ia_i\le L_j\Big\},

and the quantity to compute is $M_j=\max(c_j,\bar M_j)$ : a column improves the linear program exactly when $\bar M_j>c_j$ .

For a prefix $(\alpha)_s=(a_1,\dots,a_s)$ write $\lambda\cdot(\alpha)_s=\sum_{i\le s}l_ia_i$ and $\beta\cdot(\alpha)_s=\sum_{i\le s}b_ia_i$ . Step (1) sorts the data, $b_1/l_1\ge\dots\ge b_m/l_m$ and $L_1>\dots>L_k$ , and appends a slack item $a_{m+1}$ with $b_{m+1}=0$ , $l_{m+1}=1$ . The method then generates vectors in decreasing lexicographic order:

Steps (2) and (7) fill the coefficients after a prefix greedily, $a_i=[(L-\text{used})/l_i]$ , for $L=L_1$ at the start and $L=L_t$ later.
Step (3) records $\beta\cdot(\alpha)_m$ as the new $M_j$ for each $j\ge t$ with $L_j\ge\lambda\cdot(\alpha)_m$ and $\beta\cdot(\alpha)_m>M_j$ .
Step (4) finds the last nonzero coefficient $a_s$ .
Step (5) lowers $a_s$ by one and looks for the smallest $j$ with $L_j\ge\lambda\cdot(\alpha)_s$ and $(L_j-\lambda\cdot(\alpha)_s)b_{s+1}>(M_j-\beta\cdot(\alpha)_s)l_{s+1}$ . This is the bound obtained by relaxing the integrality of $a_{s+1}$ .
Step (6) backs up to the previous nonzero coefficient when no such $j$ exists, and stops when there is none.

In Lean the method is a transition system Step on states (a, s, t, M, phase). Reachable means reachable from the start state of Step (2).

Formalization targets

Goal: the method terminates and computes $M_1$

Under Step (1)'s ordering, with $l_i>0$ and $b_i\ge0$ :

\text{every run is finite},\quad \text{a non-final state has a successor},\quad M_1^{\text{final}}=\max\big(c_1,\bar M_1\big),

and at the end every $M_j$ is $c_j$ or the price of a column for $L_j$ , with $c_j\le M_j$ . With one stock length ( $k=1$ ) this is the paper's correctness claim in full: the method solves the knapsack problem (1).

Milestones

Steps (2)/(7): the greedy completion is the lexicographically largest extension of a prefix that fits the capacity.
Step (4): the lexicographic predecessor of a fitting vector extends $(\alpha^1)_s$ .
The relaxation bound $\beta\cdot(\alpha')_m\le\beta\cdot(\alpha)_s+b_{s+1}(L-\lambda\cdot(\alpha)_s)/l_{s+1}$ for every fitting extension.
After the inequality of Step (5)'s test fails, no vector between $(\alpha)_s$ and the successor of Step (6) improves $M$ .
The vectors tested in Step (3) strictly decrease lexicographically.
The invariant on entry to Step (3).
Identical prices: among lengths with equal prices only the shortest is needed (p. 869).

Significance

The goal certifies the pricing oracle of the Gilmore–Gomory column-generation method: the knapsack solver it calls returns the true optimum. The pricing step is exact only if that holds, and so is the conclusion "no improving column exists, the LP is solved". Milestones 1–4 are reusable on their own. They are the textbook ingredients of lexicographic and depth-first branch-and-bound for the integer knapsack: the greedy completion, the density-ordered LP bound, and the pruning rule.

The paper's argument is a short paragraph, "clear from the order in which the $m$ -vectors are generated". Writing it out shows that the claim is false for several stock lengths as the steps are printed. With $m=1$ , $l_1=b_1=1$ , $L=(5,2)$ and $c=(0,0)$ , the method tests $(5)$ . The test of Step (5) at $(4)$ then fails for $j=2$ only because $4>L_2$ , Step (6) stops, and the run ends with $M_2=0$ while the column $(2)$ has price 2. This mission therefore states what the printed algorithm does achieve. The result is the full claim for $k=1$ and for the longest stock length in general. A sorry-free Lean proof of the counterexample run accompanies the mission. No part of the method or its correctness has been formalized before, as far as a search of the platform shows.

Difficulty

The method skips large parts of the lexicographic order in three ways:

Step (7) jumps to the greedy completion for $L_t$ rather than $L_1$ .
Step (6) jumps past every smaller value of $a_s$ once one test fails.
Step (3) updates only $j\ge t$ .

Each skip has to be justified by a bound that holds for every vector skipped, and the justifications interact. A skipped vector may fit a longer stock length but not $L_t$ , and the bound for $L_1$ must cover exactly those vectors. The invariant that survives all three moves is not the naive "every vector above the current one has been examined": the vectors are not examined, only bounded. Termination needs the lexicographic decrease together with finiteness of the fitting vectors, and progress needs the reachability invariants $1\le s\le m$ and $a_s\ne0$ that make Step (5) meaningful.

Formalization scope

Items are Fin m from 0. The paper's level $s$ is a natural number, and the prefix $(\alpha)_s$ is the coordinates with index < s. Stock lengths are Fin k, and $L_1$ is index 0. The slack item enters only through $b_{s+1}$ and $l_{s+1}$ at $s=m$ . The lexicographic order is Mathlib's Pi.Lex, and $[x]$ is Nat.floor.
$M_j=\max(c_j,\bar M_j)$ is the predicate IsKnapsackMax, never a real supremum, which would be 0 on an empty set. The algorithm's output is never defined as the maximum. The goal includes termination and progress, so its correctness clause is not vacuous. Every invariant is stated for reachable states only.
The goal adds two disclosed hypotheses:
- $l_i>0$ : demanded lengths.
- $b_i\ge0$ : with a negative price the method is wrong, and the paper applies it to cutting-stock prices, which are nonnegative.
Step (1) is a hypothesis on the data, not a step.
The goal also makes these corrections:
- The claim is narrowed. For every $j$ it states $c_j\le M_j$ and attainment, and the upper bound for $L_1$ only (see Significance).
- The lexicographic order is repaired. The page's definition misses vectors that differ in their first coefficient.
- Step (7) reads λ·(α)_m. The page's "satisfies $L_t\ge\lambda\cdot(\alpha)_s$ " is read as $\lambda\cdot(\alpha)_m$ .
- Step (4) gets a stopping case. On the zero vector, where the page has no case, the method stops.
- Milestone 4 is stated for the failed inequality, not for a failed test, because the failed test is what makes the page's successor claim false.
Not formalized:
- Step (3′), the variant computing $\max_j(M_j-c_j)$ .
- The record of patterns.
- The dynamic-programming recursion and the timing estimates.

Contributions welcome: proofs of the milestones, and a corrected multi-length variant of the method with a proof that it computes every $M_j$ .

Selected references

P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting stock problem—Part II, Operations Research 11(6) (1963), 863–888. https://doi.org/10.1287/opre.11.6.863
P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6) (1961), 849–859. https://doi.org/10.1287/opre.9.6.849
G. B. Dantzig, Discrete-variable extremum problems, Operations Research 5(2) (1957), 266–288. https://doi.org/10.1287/opre.5.2.266

10 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

A Linear Programming Approach to the Cutting Stock Problem—Part II 2: For a Linear-Fractional Objective, a Basic Feasible Solution with No Improving Edge Is a Global MinimumResearch Paper

Motivation

In the cutting stock problem, stock rolls of length $L$ are cut into pieces of lengths $l_1,\dots,l_m$ to fill orders. Part I of Gilmore and Gomory's work (Opns. Res. 9 (1961)) solved its linear programming relaxation by the simplex method with column generation: the columns (cutting patterns) are too many to list, so each simplex iteration finds an improving column by solving a knapsack problem. Part II (Opns. Res. 11 (1963)) extends the method in several directions. One of them, customer tolerances, lets the amount produced of each length lie in a range $[N_i',N_i'']$ instead of matching a fixed demand. Total roll usage then stops being a good measure of quality, because overproducing within the tolerance is free. The natural objective becomes the fraction of waste: total waste divided by total material cut. This objective is a ratio of two linear functions, not a linear one.

The paper's answer, on p. 882, is that the ordinary simplex method still works for such an objective. It moves from vertex to vertex, at each vertex asks whether some edge improves the objective, and stops when none does. Ratio objectives of this kind, called linear-fractional programs, were studied in the same years by Isbell and Marlow (1956), Martos (1960–61, in Hungarian; in English in 1964), Charnes and Cooper (1962) and Dinkelbach (1962; see also 1967). Gilmore and Gomory say that their method is closest to Martos's. They derive the edge test for the ratio and show that, for cutting stock, choosing the entering column is again a knapsack problem.

Setting

Let $A$ be a real $m\times n$ matrix, $b\in\mathbb R^m$ and $c,d\in\mathbb R^n$ . The linear-fractional program is

\text{minimize}\quad \zeta(x)=\frac{z_1(x)}{z_2(x)}=\frac{\sum_i c_ix_i}{\sum_i d_ix_i}\qquad\text{subject to}\quad Ax=b,\ x\ge 0 .

In the cutting stock instance (p. 881), column $j$ is either a cutting pattern $a_j\in\mathbb Z^m_{\ge0}$ with $\sum_ia_{ij}l_i\le L$ or a slack column $-e_i$ . The right-hand side is $b_i=N_i'$ . The numerator coefficient of a pattern is its waste $w_j=L-\sum_ia_{ij}l_i$ (eq. (4)), and $d_j=1$ on patterns and $0$ on slacks, so $\zeta$ is waste per roll cut. The paper drops the upper bounds $s_i\le N_i''-N_i'$ on the slacks from the discussion (p. 882), and so does this mission.

A basis is a set $B$ of $m$ column indices whose columns of $A$ are linearly independent. A basic feasible solution $\bar x$ with basis $B$ is a feasible point with $\bar x_k=0$ for every $k\notin B$ . For a nonbasic $j\notin B$ , the edge direction of $x_j$ is the vector $v$ with $Av=0$ , $v_j=1$ and $v_k=0$ for the other nonbasic $k$ . This is "the edge that would be traced out if $x_j$ were increased, but all other nonbasic variables kept zero" (p. 883). The quantity the simplex test inspects is the rate of change along the edge,

\frac{d\zeta}{dx_j}=\frac{d}{d\tau}\,\zeta(\bar x+\tau v)\Big|_{\tau=0}.

Formalization targets

Goal: the edge criterion (p. 882)

Assume $\sum_id_ix_i>0$ for every feasible $x$ . Let $\bar x$ be a basic feasible solution with basis $B$ , and suppose $d\zeta/dx_j\ge0$ for every $j\notin B$ and every edge direction of $x_j$ . Then

\zeta(\bar x)\le\zeta(x)\qquad\text{for every } x\ge0 \text{ with } Ax=b .

Milestones (p. 882–883)

Monotonicity along lines. On an interval where the denominator does not vanish, $\tau\mapsto\zeta(x+\tau v)$ is strictly increasing, strictly decreasing or constant. Moreover $f'(\tau)\,D(\tau)^2$ is constant, where $D$ is the denominator.
Equation (5), first line.

\frac{d\zeta}{dx_j}=\frac{z_2\,(dz_1/dx_j)-z_1\,(dz_2/dx_j)}{z_2^2}.

The edge test. If $d\zeta/dx_j<0$ , increasing $x_j$ strictly decreases $\zeta$ along any segment where the denominator does not vanish. Otherwise $\zeta$ does not decrease anywhere on that segment.
Column choice is a knapsack problem. With $k=Lz_2-z_1$ and $\bar\Pi_i=-(z_1\Pi^2_i-z_2\Pi^1_i-z_2l_i)$ , the numerator of $d\zeta/dx_j$ for pattern $a$ equals $k-\sum_i\bar\Pi_ia_i$ . Hence, for $z_2\ne0$ , the most negative $d\zeta/dx_j$ is attained exactly by the patterns maximizing $\sum_i\bar\Pi_ia_i$ subject to $\sum_ia_il_i\le L$ .

Significance

The result. The edge criterion turns a nonconvex problem into one the simplex method solves. A ratio of linear functions is neither convex nor concave, so a point where no feasible direction improves the objective locally is not obviously a global minimum. The criterion says that, on a polyhedron where the denominator keeps its sign, this local test at a vertex certifies global optimality, exactly as for a linear objective. It underlies the convergence of Martos's method and of every simplex-type algorithm for linear-fractional programming. Together with milestone 4, it is what makes column generation with a knapsack pricing step applicable to the waste-fraction objective of cutting stock.

Formalizing it. The result is classical and proved; no machine-checked version is known to exist. The published platform items closest to it are Derman's Charnes–Cooper transformation of a linear-fractional program into a linear program and Matoušek's reduced-cost optimality criterion for a linear objective. Neither states an edge criterion for a ratio. A formal proof here also settles the paper's own imprecisions (see below), and yields reusable lemmas about ratios of affine functions along lines.

Difficulty

The obvious argument does not reach the goal. Along any single segment the objective is monotone (milestone 1), so a nonnegative derivative at $\bar x$ in the direction of the segment would settle it. But the test at $\bar x$ inspects only the $n-m$ edge directions, while a feasible point $x$ lies in the direction $x-\bar x$ , which is in general not an edge. Monotonicity along each edge says nothing directly about other directions, and $\zeta$ is neither convex nor concave, so local optimality along a few lines does not by itself transfer to the whole polyhedron. The step that has to be supplied is the passage from the edges to all feasible directions at a basic solution. It fails without the basis: at a feasible point that is not basic, or with linearly dependent columns, the edge directions need not reach every feasible point. At a degenerate vertex some edge directions leave the feasible set at once, and a test restricted to the feasible edges does not certify optimality.

Formalization scope

The feasible set and the objective are the published definitions DermanSeqDecisions.LinProg.IsFeasible11 ( $x\ge0$ , $Ax=b$ ) and DermanSeqDecisions.LinProg.fracObj ( $(\sum c_ix_i)/(\sum d_ix_i)$ ). The basis is the published MatousekLP.BFS.IsBasis. Indices are 0-based. A mission definition adds the basic feasible solution and the relational edge direction. The edge direction is given by its defining equations, not through a basis inverse, and is not required to be feasible.

Committed conventions and disclosed choices:

The goal is stated for minimization, the paper's problem; the paper's sentence says "maximize", which is the same statement for $-c$ .
"In a domain where the denominator does not vanish" is the hypothesis $\sum_id_ix_i>0$ for every feasible $x$ (the paper's footnote: $\sum_jx_j>0$ ). It is not required on all of $\mathbb R^n$ , where it would be unsatisfiable for the cutting stock $d$ .
The derivative in the test is Mathlib's deriv of $\tau\mapsto\zeta(\bar x+\tau v)$ at $0$ : the actual rate of change, not a formula assumed to equal it.
The page says that along a line the derivative "will have the same value". This is false when the denominator varies along the line. Milestone 1 states the correct version: the derivative times the squared denominator is constant, so the sign is constant.
In the formula after substituting (4), the page prints the coefficient $-l_i$ where $-z_2l_i$ is meant. Milestone 4 uses the corrected coefficient.
The slack upper bounds are dropped, as on p. 882.

The following would trivialize the goal and are excluded: an edge hypothesis over all directions $v$ instead of the edge directions, which turns the goal into quasi-convexity along segments; an edge hypothesis stated as the global inequality; a positivity hypothesis on the denominator over all of $\mathbb R^n$ ; and dropping the basis, under which the goal is false.

The development needs elementary real calculus (derivatives of quotients, monotonicity from the sign of the derivative) and the linear algebra of a basis (existence, uniqueness and spanning of the edge directions). The lemmas about ratios of affine functions along lines and about edge directions of a basis are reusable for any simplex-type method. Contributions of proofs of the milestones, and of auxiliary lemmas on edge directions, are welcome.

Selected references

P. C. Gilmore and R. E. Gomory, A linear programming approach to the cutting stock problem—Part II, Operations Research 11(6), 863–888, 1963. https://doi.org/10.1287/opre.11.6.863
P. C. Gilmore and R. E. Gomory, A linear programming approach to the cutting stock problem, Operations Research 9(6), 849–859, 1961. https://doi.org/10.1287/opre.9.6.849
B. Martos, Hyperbolic programming, Naval Research Logistics Quarterly 11(2), 135–155, 1964. https://doi.org/10.1002/nav.3800110204
A. Charnes and W. W. Cooper, Programming with linear fractional functionals, Naval Research Logistics Quarterly 9(3–4), 181–186, 1962. https://doi.org/10.1002/nav.3800090303
W. Dinkelbach, Die Maximierung eines Quotienten zweier linearer Funktionen unter linearen Nebenbedingungen, Zeitschrift für Wahrscheinlichkeitstheorie 1, 141–145, 1962 (cited by the paper as [11]).
W. Dinkelbach, On nonlinear fractional programming, Management Science 13(7), 492–498, 1967. https://doi.org/10.1287/mnsc.13.7.492
J. R. Isbell and W. H. Marlow, Attrition games, Naval Research Logistics Quarterly 3, 71–94, 1956 (cited by the paper as [9]).

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems 5: For Hypercube Uncertainty, Even in the Constraints, the Robust and Adaptive Optima CoincideResearch Paper

Motivation

In two-stage optimization under uncertainty, a first-stage decision $x$ is taken before the data are known, and a second-stage decision $y$ is taken after a scenario $\omega$ is revealed. The fully adaptive formulation lets $y$ depend on $\omega$ and minimizes the worst-case cost. It is the natural model of recourse, but it optimizes over policies, one decision per scenario, and is computationally hard in general. The static robust formulation fixes one $y$ in advance that must be feasible in every scenario. It is a single deterministic mixed integer program and is the standard tractable surrogate (Ben-Tal, Goryashko, Guslitzer, Nemirovski 2004; Bertsimas & Sim 2004).

The question is how much is lost by the surrogate. Bertsimas and Goyal (2010) bound the gap by $2$ against the stochastic problem and by $4$ against the adaptive problem when the uncertainty set is symmetric. Their §5.3 identifies a case with no gap at all: when the uncertainty set is a hypercube (a box), the static robust optimum equals the adaptive optimum, and this holds even when the constraint matrices themselves are uncertain. Box uncertainty is the simplest and most common uncertainty model in practice (interval data on every coefficient), so the result says that for it, adaptivity buys nothing.

This mission formalizes that theorem, Theorem 5.4, together with Theorem 2.4, which shows that under right-hand-side uncertainty the robust problem is a single deterministic problem with the coordinatewise worst right-hand side.

Setting

Fix dimensions $m,n_1,n_2$ and sets $I_1,I_2$ of integer coordinates. The decision domains are

D_{I}=\{x\in\mathbb R^n : x\ge0,\ x_i\in\mathbb Z\ \text{for } i\in I\},

which is $\mathbb R_+^{n-p}\times\mathbb Z_+^{p}$ up to relabelling coordinates, $p=|I|$ .

A scenario set $\Omega$ is given. In scenario $\omega$ the data are a constraint matrix $A(\omega)\in\mathbb R^{m\times n_1}$ , a recourse matrix $B(\omega)\in\mathbb R^{m\times n_2}$ , a right-hand side $b(\omega)\in\mathbb R^m$ and a second-stage cost $d(\omega)\in\mathbb R^{n_2}_+$ . The first-stage cost $c\in\mathbb R^{n_1}_+$ is fixed.

The adaptive problem $\Pi_{\mathrm{Adapt}}(A,B,b,d)$ (5.6) chooses $x\in D_{I_1}$ and $y(\omega)\in D_{I_2}$ for every $\omega$ with $A(\omega)x+B(\omega)y(\omega)\ge b(\omega)$ for all $\omega$ , and has value

z_{\mathrm{Adapt}}=\inf\ c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty(\omega).

The robust problem $\Pi_{\mathrm{Rob}}(A,B,b,d)$ (5.7) chooses one $x\in D_{I_1}$ , $y\in D_{I_2}$ with $A(\omega)x+B(\omega)y\ge b(\omega)$ for all $\omega$ , and has value

z_{\mathrm{Rob}}=\inf\ c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty.

The uncertainty set is $\mathcal U=\{(A(\omega),B(\omega),b(\omega),d(\omega)) : \omega\in\Omega\}$ , a subset of $\mathbb R^N$ with $N=mn_1+mn_2+m+n_2$ . Following Definition 1.1, $\mathcal U$ is a hypercube if $\mathcal U=[l_1,u_1]\times\cdots\times[l_N,u_N]$ for some $l_i\le u_i$ .

For Theorem 2.4, $A$ , $B$ and $d$ are fixed and only $b(\omega)\in\mathbb R^m_+$ varies; $\Pi_{\mathrm{Rob}}(b)$ (1.2) is the robust problem above, and $\Pi$ is the deterministic problem with right-hand side $b^h_j=\max_\omega b_j(\omega)$ .

Formalization targets

Goal: Theorem 5.4 (p. 31)

If $\mathcal U$ is a hypercube, then

z_{\mathrm{Rob}}(A,B,b,d)=z_{\mathrm{Adapt}}(A,B,b,d).

The integer coordinates $I_1,I_2$ are arbitrary, and nothing is assumed about the signs of $A$ , $B$ , $b$ .

Milestones

Theorem 2.4 (p. 17). Under right-hand-side uncertainty, $(x,y)$ is feasible for $\Pi_{\mathrm{Rob}}(b)$ if and only if $Ax+By\ge b^h$ ; hence $z_{\mathrm{Rob}}(b)=z(\Pi)$ .
p. 31 display. $z_{\mathrm{Adapt}}(A,B,b,d)\le z_{\mathrm{Rob}}(A,B,b,d)$ for every uncertainty set.
Eqs. (5.8)–(5.10). If $\mathcal U$ is a hypercube, some scenario $\bar\omega$ has $A(\bar\omega)$ , $B(\bar\omega)$ entrywise minimal and $b(\bar\omega)$ , $d(\bar\omega)$ entrywise maximal over $\Omega$ .
Eqs. (5.11)–(5.13). For such $\bar\omega$ , if $(x,y(\cdot))$ is adaptive feasible, then $(x,y(\bar\omega))$ is robust feasible.
Eq. (5.14). For such $\bar\omega$ , the robust worst-case cost of $(x,y(\bar\omega))$ is at most the adaptive worst-case cost of $(x,y(\cdot))$ .

Significance

The result. Theorem 5.4 says that for interval uncertainty on every coefficient, the static robust program, whose size does not grow with the number of scenarios, solves the adaptive problem exactly. Combined with Theorem 2.4 for right-hand-side uncertainty, the adaptive problem collapses to one deterministic mixed integer program with worst-case data. It marks the boundary case of the paper's adaptability-gap bounds: the gap is at most $4$ for symmetric sets, and exactly $1$ for boxes.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a Lean model of two-stage robust and adaptive mixed integer programs with uncertain constraint matrices, with values as extended-real infima, which other formalizations of adjustable robust optimization can build on.

Difficulty

The mathematics is elementary; the care is in the statement. The step that fails for a general uncertainty set is the existence of a single worst scenario $\bar\omega$ that is simultaneously entrywise smallest in $A$ , $B$ and entrywise largest in $b$ , $d$ . For a set that is only contained in a box, the box's worst corner need not be realized. With two scenarios $b=(1,0)$ and $b=(0,1)$ , $B=I$ , $d=(1,1)$ , the adaptive value is $1$ and the robust value is $2$ . A formalization therefore has to state the hypercube hypothesis as an equality of sets. A second point is the arithmetic of extended reals: the paper argues from optimal solutions, which need not exist, so the inequalities must be transported through infima over feasible sets that may be empty and through suprema that may be infinite.

Formalization scope

Decisions are vectors Fin n → ℝ; matrices are Matrix (Fin m) (Fin n) ℝ; constraints use Mathlib's componentwise order and mulVec.
Mixed-integer domains are "nonnegative, integer on a designated coordinate set $I$ ", the paper's $\mathbb R_+^{n-p}\times\mathbb Z_+^p$ up to relabelling.
Optimal values are EReal infima over the feasible set, $+\infty$ when infeasible; worst-case costs are EReal suprema over $\Omega$ . No optimal solution is assumed.
A scenario datum is a structure with the four blocks $(A,B,b,d)$ ; the box and the hypercube predicate are written entrywise on these blocks, which is Definition 1.1 in $\mathbb R^N$ .
The hypercube hypothesis is IsHypercube (uncertaintySet A B b d), i.e. the realized data are exactly a box. Assuming only that the data lie inside a box would make the statement false (example above); assuming fixed $A$ , $B$ would state Corollary 5.1 instead of Theorem 5.4.
Typos corrected in the Lean: (5.6)–(5.7) print $\mathbb Z^{n_2}_+$ for the second-stage integer block, read as $\mathbb Z^{p_2}_+$ ; §5.3's opening sentence names $\Pi_{\mathrm{Adapt}}(b,d)$ twice where the first is $\Pi_{\mathrm{Rob}}(b,d)$ .
In Theorem 2.4 the paper's $\max_\omega b_j(\omega)$ is a real supremum under the hypothesis that the right-hand sides are bounded above, and the second stage is continuous ( $p_2=0$ ), as in the problem $\Pi$ on the page.

Contributions welcome: proofs of the milestones and of the goal, and lemmas on monotonicity of mulVec for nonnegative vectors and on EReal infima over feasible sets, which are reusable across the other missions of this series.

Selected references

D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited from the authors' manuscript, MIT DSpace).
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99, 2004. https://doi.org/10.1007/s10107-003-0454-y
D. Bertsimas, M. Sim, The price of robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065

11 thms2 active usersReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

On the Convergence of Stochastic Dual Dynamic Programming and Related Methods: DOASA Reaches an Optimal Policy in Finitely Many Iterations Almost SurelyResearch Paper

Motivation

Stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto in 1991, is the standard method for multistage stochastic linear programs with many stages, such as hydro-thermal scheduling and long-term energy planning. It approximates each stage's expected future cost from below by the maximum of finitely many linear functions (cuts), built from LP dual solutions at sampled states, and alternates a forward simulation pass with a backward cut-generation pass. Practitioners stop the method when a simulated upper bound is close to the lower bound $C^k_1$ . Whether this procedure converges at all is the question of this mission.

Timeline:

1991: Pereira and Pinto publish SDDP, with no convergence proof.
1999: Chen and Powell prove almost-sure convergence for CUPPS; Linowsky and Philpott (2005) extend the argument to SDDP, AND and ReSa. Both proofs rely on an unstated independence assumption between sampled outcomes and convergent subsequences of iterates.
2008: Philpott and Guan (Oper. Res. Lett. 36(4), 450–455) give a proof based on the finiteness of the set of distinct cut coefficients, for a class they call DOASA (Dynamic Outer Approximation Sampling Algorithms).
Later work (Shapiro 2011; Girardeau, Leclère and Philpott 2015) extends convergence to convex nonlinear and continuous settings.

Setting

There are $T\ge2$ stages. Stage $t$ has a decision $x_t\ge0$ in $\mathbb R^{n_t}$ , costs $c_t$ , a matrix $A_t$ and, for $t\le T-1$ , a matrix $B_t$ coupling $x_t$ to the next stage. At stage $1$ the constraint is $A_1x_1=b_1$ . For $2\le t\le T$ the right-hand side is random: $A_tx_t=\omega_t-B_{t-1}x_{t-1}$ , where $\omega_t$ takes values $\omega_{t1},\dots,\omega_{tq_t}$ with probabilities $p_{ti}>0$ , independently across stages. The expected cost-to-go is defined backwards from $\mathcal Q_{T+1}\equiv0$ :

Q_t(x_{t-1},\omega_{ti})=\min\{c_t^\top x_t+\mathcal Q_{t+1}(x_t):A_tx_t=\omega_{ti}-B_{t-1}x_{t-1},\ x_t\ge0\},\qquad \mathcal Q_t=\sum_i p_{ti}Q_t(\cdot,\omega_{ti}),

and $Q_1=\min\{c_1^\top x_1+\mathcal Q_2(x_1):A_1x_1=b_1,x_1\ge0\}$ is the problem [LP1]. Assumption (A4) says every stage problem met along the way has a nonempty, bounded feasible region.

The approximate problem [AP $_t^k$ ] replaces $\mathcal Q_{t+1}$ by $\max_j\{\alpha_{t+1,j}-(\beta^j_{t+1})^\top x_t\}$ over the cuts generated before iteration $k$ ; its value is $C^k_t$ . A scenario fixes one outcome per stage $2,\dots,T-1$ . Each DOASA iteration (i) samples one forward scenario $\omega^k$ and solves [AP $_t^k$ ] along it, giving states $x^k_t$ ; (ii) for $t=T,\dots,2$ runs the Cut Calculation Algorithm (CCA): it solves [AP $_t^k$ ] at $x^k_{t-1}$ for the outcomes in a backward sample $\Omega^k_t$ , stores optimal extreme-point dual solutions $(\pi,\rho)$ in a collection $\mathcal D_t$ , picks for every outcome the best stored dual, and averages them into a new cut on $\theta_t$ . DOASA-N instead traverses a fixed list of $N$ scenarios in every iteration.

Formalization targets

Goal: Theorem 4 under the joint sampling property J

If, with probability 1, every scenario prefix is followed by the forward pass jointly with each outcome being in the backward sample infinitely often (property J), then with probability 1 every DOASA run has an iteration $K$ after which the cuts no longer change, the policy $\bar x$ they induce is optimal for [LP1], and

C^K_1=Q_1 .

Milestones

Monotonicity (p. 4): $C^{k+1}_t\ge C^k_t$ and $C^{k+1}_1\ge C^k_1$ .
Lower bound (p. 4): every cut is valid, so $C^k_t\le Q_t$ and $C^k_1\le Q_1$ .
Lemma 1 (p. 6): the set $\mathcal G^k_t$ of distinct generated cuts is bounded in size and eventually constant.
Lemma 2 (p. 10): DOASA-N stops changing after finitely many iterations, with $\lim_kC^k_1\le Q_1$ .
Lemma 3 (p. 10): DOASA-N over all scenarios, with backward sampling infinitely often per scenario, converges almost surely to an optimal policy.

Significance

The theorem justifies SDDP, AND, ReSa and CUPPS as exact methods: on a finite scenario tree, sampling-based cutting-plane schemes reach an optimal policy and a tight lower bound after finitely many iterations, almost surely. The finiteness argument (Lemma 1) is the template for later finite-convergence proofs of SDDP variants.

The paper's proofs are informal. No part of this development is machine-checked, and the printed statement of Theorem 4 is false (see below), so a formal proof also settles exactly which sampling hypothesis is enough. The finite-cut lemma and the cut-validity milestone are reusable for any Benders-type multistage method.

Difficulty

The obvious argument goes: cut sets stabilize (Lemma 1), and every scenario and every outcome is sampled infinitely often, so the limiting cuts must be exact. The last step fails. A cut at a state is exact only if, for every outcome, a dual that is optimal at that state has been collected. Sampling the forward scenario and the backward outcomes infinitely often, but separately, does not ensure this. Lemma 1 itself is also delicate: the dual vectors $\rho$ grow in dimension with $k$ , so the collection of extreme-point duals can be infinite even though the cut coefficients take finitely many values. The algorithm's choices (extreme-point duals, ties among best duals) must be handled for every run, not for a convenient one.

Formalization scope

Stages are numbered $1,\dots,T$ with variable dimensions per stage. B t is the paper's $B_t$ , the matrix multiplying $x_t$ in stage $t+1$ . Value functions are real infima, used only on reachable states. Iterations are numbered from $0$ in Lean. Explicit choices, each recorded in the item statements:

The J correction. The paper states Theorem 4 under FPSP and BPSP. These do not suffice. In a three-stage instance whose last-stage backward sample is $\{c\}$ after forward outcome $a$ and $\{d\}$ after $b$ , alternating, both properties hold but the cuts stabilize at a suboptimal policy with $C^k_1$ below $Q_1$ . The goal is stated under J, which implies FPSP and BPSP and holds for the schemes the paper names. Lemma 3's BPSP is read per scenario of DOASA-N.
Initial cut. The paper's trivial cut $\theta_{t+1}\ge-\infty$ makes [AP $_t^1$ ] unbounded; it is replaced by a finite cut $\theta_{t+1}\ge L_t$ assumed valid on reachable states. Stage $T$ uses the exact cut $\theta_{T+1}\ge0$ .
(A4) is required on reachable states only.
The LP solver is a deterministic oracle on cut sets returning optimal solutions of [AP $_t$ ], so repeated cuts do not change forward solutions.
Duals. Collected duals are optimal extreme points of the dual region; best duals are chosen with arbitrary tie-breaks. No cut is added while the dual collection is empty. Dual multipliers $\rho$ are sequences padded with zeros.
Runs are relations covering DOASA and DOASA-N (batched forward scenarios). The conclusions hold for every run consistent with the samples, inside the almost-sure quantifier.

A trivializing encoding, in which cuts are arbitrary valid hyperplanes, duals are taken for all outcomes, or the sampling hypotheses directly assume exactness of the cuts, is ruled out: the run relation transcribes CCA steps 1–3 as printed.

A complete development needs LP weak and strong duality (published on the platform as LinearOptimization.lp_weak_duality and LinearOptimization.lp_strong_duality, in their own encoding), finiteness of the set of extreme points of a polyhedron, and the almost-sure intersection of finitely many events (Mathlib). Contributions to any milestone, to the proof that J holds for independent sampling, and to the counterexample showing FPSP and BPSP are insufficient are welcome.

Selected references

A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Oper. Res. Lett. 36(4) (2008) 450–455. https://doi.org/10.1016/j.orl.2008.01.013 (cited from the authors' manuscript v24, 2008-02-25)
M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
Z.-L. Chen, W. B. Powell, Convergent cutting-plane and partial-sampling algorithm for multistage stochastic linear programs with recourse, J. Optim. Theory Appl. 102 (1999) 497–524. https://doi.org/10.1023/A:1022641805263
A. Shapiro, Analysis of stochastic dual dynamic programming method, European J. Oper. Res. 209 (2011) 63–72. https://doi.org/10.1016/j.ejor.2010.08.007
P. Girardeau, V. Leclère, A. B. Philpott, On the convergence of decomposition methods for multistage stochastic convex programs, Math. Oper. Res. 40(1) (2015) 130–145. https://doi.org/10.1287/moor.2014.0664

10 thms2 active usersReviewed

Completed

Operations Research Statistics·Captain: mikedeng1

Optimal Estimation of Executive Compensation by Linear Programming I: Least Absolute Deviations under Ranking Constraints Equal a Linear ProgramResearch Paper

Motivation

A firm may know salary bounds and the ranking of positions without having a reliable sample of individual salaries suitable for least-squares estimation. Charnes, Cooper and Ferguson used that kind of partial information to estimate a salary formula from ratings assigned to job factors. Their 1955 paper gives a model in which weights respect the job hierarchy while the implied salaries approach specified salary levels as closely as possible. It then turns the sum of absolute deviations into a linear program that can be handled by the methods available for constrained optimization. The setting and transformation are in §§4–6 of the published paper.

The question here is a precise one: does the transformed program have the same optimal value and the same optimal salary weights as the original absolute-deviation problem? This matters because a linear-program solution should answer the compensation-estimation problem stated before the transformation, even though the transformed program has additional variables and a different feasible set. The mission also records the paper's seven-position numerical example, where the reported salary formula can be checked directly against the table of factor ratings.

Setting

There are $n$ rated factors and $L\ge1$ job levels ordered from highest to lowest. The rating $x_{ik}$ is the amount of factor $i$ required at level $k$ , and $a_i$ is the nonnegative weight assigned to that factor. The estimated salary at level $k$ is

S_k(a)=\sum_{i=1}^{n}a_i x_{ik}.

The salary formula applied to a person's factor amounts $y_i$ is $s=\sum_i a_i y_i$ . For the ranked positions, feasible weights satisfy the four parts of the paper's system (2): each $a_i\ge0$ ; the top-level salary is at most the ceiling $s_M$ ; successive salaries descend, $S_{k+1}(a)\le S_k(a)$ ; and the bottom-level salary is at least the floor $s_m$ . These are one-sided ceiling and floor bounds. They do not force the fitted salaries to equal the bounds.

The firm specifies target salaries $s_k$ at a finite set $K$ of levels, which includes the ceiling and floor levels in the examples and may include intermediate levels. The absolute-deviation objective of (3) is

D(a)=\sum_{k\in K}|S_k(a)-s_k|.

The original problem minimizes $D$ over the feasible weights. At a specified level, let $w_k=S_k(a)-s_k$ . The split-variable program of (4)–(5) introduces $u_k,v_k\ge0$ with $w_k=u_k-v_k$ and minimizes $P(u,v)=\sum_{k\in K}(u_k+v_k)$ . The split variables are constrained only for levels in $K$ . The salary constraints (2) continue to apply to $a$ . This is the paper's transformed linear program, with a feasible set that contains many choices of $(u,v)$ above the same weight vector Charnes, Cooper and Ferguson, §§4–5.

Formalization targets

Equivalence of the two programs

The main target is the paper's claim that the two problems have equal minimal values and that minimizers correspond §6, p. 143. In the formal statement, equal values are expressed by equality of attainable objective thresholds:

\forall t\in\mathbb R,\qquad [\exists a\text{ feasible}:D(a)\le t] \quad\Longleftrightarrow\quad [\exists(a,u,v)\text{ LP-feasible}:P(u,v)\le t].

The goal also says that $a$ minimizes $D$ exactly when the triple formed from $a$ and the positive and negative parts of $w$ minimizes $P$ . Every LP minimizer projects to a minimizer of $D$ . These clauses give the value and solution correspondence the authors use when they call the two problems equivalent.

Supporting claims and numerical result

Three milestones follow the paper's exposition. First, every feasible weight vector has a split-variable lift with the same objective. Second, every transformed feasible point projects to an original feasible weight vector with no larger original objective. Third, the minimal values agree §§5–6, pp. 141–143. Each is recorded under the unnumbered sentence from which it was extracted; the paper has no numbered lemmas.

Two companion statements record other claims: opposite coefficient columns cannot both occur among selected independent simplex columns, and the Table I data have the reported optimum. For the latter, targets are 16 at $R_1$ , 10 at $R_5$ , and 4 at $R_7$ , measured in thousands of dollars. Equation (7) assigns weights $(4,0,0,16,0,4,0,28,0)/11$ , yielding the minimum deviation $14/11$ §7, pp. 145–148. A further companion checks the redundant $R_2\le R_1$ ranking row.

Significance

The equivalence justifies using a linear-program output as an estimate for the earlier salary problem: the transformed objective reaches the same value, and its optimal weight vectors solve the original problem. The numerical claim supplies a fully specified instance with seven job levels and nine factors, including the exact fitted salaries. Without the correspondence, optimizing the enlarged variable set could give no assurance that its weights minimize the deviations the firm intended to measure.

The mathematical result was argued in the 1955 paper; this mission asks for a machine-checked formulation and proof of that known result. The statements compile as open Lean theorems, so compilation alone does not establish their truth. Closing them would add a reusable treatment of absolute-deviation objectives under finite linear inequalities and an exact certificate for the paper's worked example. The consistency claim in the appendix is a separate mission because it concerns perturbations of another linear program, not this transformation.

Difficulty

The split-variable program permits $u_k$ and $v_k$ to be simultaneously positive even when their difference is fixed. Consequently, simply identifying the two feasible sets would misstate the transformation: one has extra degrees of freedom. A proof must relate their objective values and then account for optimal solutions on both sides. The numerical example has a separate difficulty. Substituting the reported weights verifies a feasible objective of $14/11$ , but does not by itself rule out another feasible weight vector with a smaller deviation. The global lower bound is part of the companion theorem.

Formalization scope

The Lean development represents factor and level vectors by functions on Fin n and Fin L, and sums explicitly over finite indices. Paper level 1 is Lean index 0; paper level $L$ is the final Fin L index. The assumption $L\ge1$ is explicit because both the top and bottom level are named. No sign, monotonicity, or boundedness assumptions are imposed on the ratings beyond what the paper states. The weights are componentwise nonnegative. Intermediate target salaries enter the objectives through $K$ but add no constraints to (2), matching the paper's treatment of $R_5$ .

A minimizer is a feasible point whose objective is no larger than that of every feasible point. The equality of minimal values uses the threshold formula above, so an empty feasible set cannot inherit a spurious real infimum. The transformed feasible set is exactly the split-variable system of (4)–(5); defining it as only the image of a chosen lift would make the principal comparison empty of content. The Table I constants are exact rational values in units of $1{,}000$ . The paper rounds some displayed salaries, while Lean records their exact fractions. The generic column-independence companion is stated for an arbitrary finite matrix, with the basis and zero nonbasic coordinates explicit.

The shared definition module provides the salary map, feasibility predicates, objectives, minimizers, and example data. A full development can contribute proofs of the three milestones, the main equivalence, the column claim, the numerical lower bound, and the redundant-row fact. The finite absolute-deviation and split-variable statements can also serve later formalizations with other linear constraints.

Selected references

A. Charnes, W. W. Cooper, and R. O. Ferguson, Optimal Estimation of Executive Compensation by Linear Programming, Management Science 1(2), 138–151, 1955. DOI 10.1287/mnsc.1.2.138.

5 thms2 active usersReviewed

Discrete Geometry Number Theory Operations Research·Captain: mikedeng1

Integer Programming with a Fixed Number of Variables 1: If B(p,r) ⊂ τK ⊂ B(p,R) with R/r ≤ c₁ and τK Misses the Lattice, Fewer Than 1 + c₁c₂√n Lattice Hyperplanes H + kbₙ Meet B(p,R)Research Paper

Motivation

The integer linear programming feasibility problem asks, for an integer $m\times n$ matrix $A$ and $b\in\mathbb Z^m$ , whether some $x\in\mathbb Z^n$ satisfies $Ax\le b$ . It is NP-complete, so no algorithm polynomial in the length of the data is expected. H. W. Lenstra, Jr. (Math. Oper. Res. 8 (1983) 538–548) showed that the picture changes when the number of variables $n$ is fixed: the problem is then solvable in polynomial time. The proof is a short argument from the geometry of numbers, and it became the starting point of lattice methods in integer programming, including Kannan's improved algorithm and the later flatness-based branching schemes.

Lenstra's introduction (p. 538) describes the idea as transforming the problem into an equivalent one in which "either the existence of a vector $x \in \mathbb Z^n$ satisfying $Ax \le b$ is obvious; or it is known that the last coordinate of any such $x$ belongs to an interval whose length is bounded by a constant only depending on $n$ ." This mission formalizes the geometric statement behind that dichotomy, §1 of the paper.

Timeline. For $n = 2$ , Hirschberg and Wong and Kannan gave polynomial algorithms in special cases, and Scarf treated the case $n=2$ completely; the case of general fixed $n$ was conjectured by Hirschberg–Wong and Scarf (as recounted on p. 538). Lenstra's paper (received 1981, published 1983) settled the conjecture. Its lattice reduction step uses the algorithm of Lenstra, Lenstra and Lovász (1982). Kannan (1987) later reduced the dependence on $n$ to $n^{O(n)}$ .

Setting

Work in $\mathbb R^n$ with the Euclidean length $|\cdot|$ , and write $B(p,z)=\{x\in\mathbb R^n : |x-p|\le z\}$ for the closed ball with centre $p$ and radius $z>0$ .

A lattice is $L=\sum_{i=1}^n \mathbb Z b_i$ for a basis $b_1,\dots,b_n$ of $\mathbb R^n$ . Its determinant $d(L)=|\det(b_1,\dots,b_n)|$ (the $b_i$ as columns) is the volume of the parallelepiped $\sum_i[0,1)\,b_i$ and does not depend on the basis. Hadamard's inequality (6) says $d(L)\le\prod_i|b_i|$ . A basis is reduced in Lenstra's sense if, for a constant $c_2$ depending only on $n$ ,

\prod_{i=1}^n |b_i| \le c_2\cdot d(L). \tag{7}

Singling out $b_n$ , let $H=\sum_{i=1}^{n-1}\mathbb R b_i$ be the hyperplane spanned by the other vectors, $L'=\sum_{i=1}^{n-1}\mathbb Z b_i$ the lattice inside it, and $h$ the distance of $b_n$ to $H$ . Then $L\subset\bigcup_{k\in\mathbb Z}(H+kb_n)$ : the lattice lies on a family of parallel hyperplanes $H + kb_n$ at successive distance $h$ .

In the paper, $K=\{x : Ax\le b\}$ is bounded with positive volume, and a linear map $\tau$ makes it "round":

B(p,r)\subset\tau K\subset B(p,R)\quad(3),\qquad R/r\le c_1\quad(4),

with $c_1$ depending only on $n$ . Then $K\cap\mathbb Z^n=\emptyset$ if and only if $\tau K\cap L=\emptyset$ for $L=\tau\mathbb Z^n$ , a lattice with basis $b_i=\tau(e_i)$ .

Formalization targets

Goal (§1, p. 541)

Let $b_1,\dots,b_n$ be a basis with (7), numbered so that $|b_n|=\max_i|b_i|$ , and let $\tau K$ satisfy (3) and (4). Then

\tau K\cap L\neq\emptyset\quad\text{or}\quad t-1<c_1c_2\sqrt n,

where $t$ is the number of hyperplanes $H+kb_n$ , $k\in\mathbb Z$ , that meet $B(p,R)$ (finiteness included).

Milestones, in the order the paper uses them

LEMMA (8), p. 540: every $x$ has $y\in L$ with $|x-y|^2\le\frac14(|b_1|^2+\cdots+|b_n|^2)$ .
(10), p. 540: if $|b_n|$ is maximal, $|x-y|\le\frac12\sqrt n\,|b_n|$ .
(11), p. 540: $d(L)=h\cdot d(L')$ .
(12), pp. 540–541: under (7), $c_2^{-1}|b_n|\le h\le|b_n|$ .
p. 541: if $B(p,r)\subset\tau K$ and $\tau K\cap L=\emptyset$ , then $r<\frac12\sqrt n\,|b_n|$ .
p. 541: if precisely $t$ hyperplanes $H+kb_n$ meet $B(p,R)$ , then $t-1\le 2R/h$ .

The goal leaves $c_1$ and $c_2$ free, so it remains valid for any reduction algorithm and any rounding procedure; the companion mission (Integer Programming with a Fixed Number of Variables 2) supplies $c_1 = 2n^{3/2}$ , and the LLL algorithm supplies $c_2=2^{n(n-1)/4}$ .

Significance

The result. The goal is the branching step of Lenstra's algorithm. It says that a lattice-point-free convex body that is well rounded is "flat" in the lattice direction dual to $H$ : only boundedly many lattice hyperplanes meet it. The search for a lattice point in dimension $n$ therefore reduces to fewer than $1+c_1c_2\sqrt n$ searches in dimension $n-1$ , which with $n$ fixed gives polynomial running time. Sharper forms of the same dichotomy, such as Kannan's bounds, are the basis of later lattice-based integer programming algorithms.

Formalizing it. The results are classical and proved on paper; to our knowledge none of the statements of §1 is machine-checked. Hadamard's inequality (6) is in Mathlib (Orientation.abs_volumeForm_apply_le). The published platform theorem KannanLattice.Core.exists_lattice_point_near_projection (Kannan 1987, Proposition 4.2) proves a stronger form of (8) and (10), with Gram–Schmidt lengths in place of $|b_i|$ ; for $L=\mathbb Z^n$ , (10) is the published QFS.exists_lattice_mem_closedBall. What remains is the "base times height" identity (11) relating a full-rank determinant to the distance of a vector from a hyperplane, the spacing bound (12), the count of hyperplanes meeting a ball, and their assembly. This is one of the two geometric ingredients of Lenstra's polynomial algorithm; the algorithm itself and its running time are not formalized.

Difficulty

The argument is short on paper, and each step is "clear" there. The work lies in connecting three descriptions of the same geometry that Mathlib keeps apart: the determinant of a coordinate matrix ( $d(L)$ ), the metric distance of a point to a subspace ( $h$ ), and the $(n-1)$ -dimensional volume of $L'$ . Identity (11) needs exactly this bridge, and (12) needs Hadamard's inequality for the lower-dimensional lattice $L'$ inside a hyperplane of $\mathbb R^n$ , not for a full-rank matrix. Bounding the number of hyperplanes meeting a ball needs the normal direction of $H$ and the fact that the hyperplanes are $h$ apart along it. A tempting shortcut is to define $h$ as the length of the last Gram–Schmidt vector and $d(L)$ as the product of Gram–Schmidt lengths: that turns (11) into a tautology and is ruled out below.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so norms are Euclidean and balls round; $B(p,z)$ is Metric.closedBall p z with $z>0$ as a hypothesis where the paper writes a ball.
Where $b_n$ is singled out, $n=k+1$ , the basis is b : Fin (k+1) → ℝⁿ, $b_n$ = b (Fin.last k) and $b_1,\dots,b_{n-1}$ = b ∘ Fin.castSucc. "Basis for $L$ " is linear independence of the $n$ vectors over $\mathbb R$ , and $L$ is the published KannanLattice.Core.lattice b, the $\mathbb Z$ -span.
$d(L)$ is the paper's definition, $|\det|$ of the column matrix (latDet). $h$ is Metric.infDist from $b_n$ to the span $H$ . $d(L')$ , for which the paper writes no formula, is the published KannanLattice.Core.latticeDet (the product of Gram–Schmidt lengths of $b_1,\dots,b_{n-1}$ , the $(n-1)$ -volume of their parallelepiped).
The hyperplanes $H+kb_n$ meeting $B(p,R)$ are indexed by the set of integers hitIndices b p R; $t$ is its cardinality, its finiteness is part of every conclusion (the cardinality of an infinite set is $0$ in Lean), and $t-1$ is computed in $\mathbb R$ .
The constants "only depending on $n$ ", $c_1$ and $c_2$ , are arbitrary real numbers. The reducedness (7) is a hypothesis, and so is the maximality $|b_i|\le|b_n|$ , which enters (10), the radius bound and the goal only.
$\tau K$ is an arbitrary set $X\subseteq\mathbb R^n$ satisfying (3); §1 never uses that $K$ is a polyhedron or the map $\tau$ , and every lattice is $\tau\mathbb Z^n$ for $\tau(e_i)=b_i$ . The paper's "for some $p\in\tau K$ " follows from (3).
The identity (11) is stated without (7), which the paper assumes in the surrounding sentence but does not use.
Ruled out: defining $d(L)$ or $h$ through Gram–Schmidt lengths (which makes (11) bookkeeping), dropping finiteness of the hyperplane count, and replacing the dichotomy "some lattice point lies in $\tau K$ " by a statement about one computed lattice point.

Welcome contributions: the bridge between Matrix.det of a basis and products of Gram–Schmidt lengths (reusable for any lattice development), Hadamard's inequality for a family of fewer than $n$ vectors, and the count of lattice hyperplanes meeting a ball.

Selected references

H. W. Lenstra, Jr., Integer Programming with a Fixed Number of Variables, Mathematics of Operations Research 8(4) (1983) 538–548. https://doi.org/10.1287/moor.8.4.538
A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
R. Kannan, Minkowski's convex body theorem and integer programming, Mathematics of Operations Research 12(3) (1987) 415–440. https://doi.org/10.1287/moor.12.3.415

10 thms2 active usersReviewed

Discrete Geometry Operations Research·Captain: mikedeng1

On Linear Characterizations of Combinatorial Optimization Problems III: Zero-One and Integer-Programming-Type Problems Have Small Facial DescriptionsResearch Paper

Motivation

Many discrete optimization problems can be described by linear inequalities, even when their feasible solutions are integer vectors. A linear description lets one study the geometry of the feasible set and connect combinatorial methods with linear programming. The number of inequalities may be large, so a more basic question is whether each inequality needs coefficients of manageable size. Karp and Papadimitriou separated this coefficient-size issue from the number and computational recognizability of the inequalities in their study of facial descriptions Karp and Papadimitriou, MIT/LCS/TM-154, pp. 3–7.

Their Lemma 1 identifies two common families for which small coefficients suffice: zero-one problems and problems given by an integer linear system. This result establishes a geometric premise used by the paper's later complexity discussion. It says nothing by itself about finding the inequalities efficiently or recognizing whether a proposed inequality belongs to a description. Those computational conditions belong to the paper's subsequent theorems Karp and Papadimitriou, pp. 5–8.

Setting

A combinatorial optimization problem here consists of a set $L$ of binary strings, a dimension $n(z)$ for each $z\in L$ , and a set $S(z)$ of feasible nonnegative integer vectors of that dimension. The geometric object is the rational convex hull $\mathrm{CH}(S(z))\subseteq\mathbb Q^{n(z)}$ . The paper calls the rationals $R$ in its notation. The values of $n$ and $S$ outside $L$ carry no meaning. A feasible set may be empty; its convex hull is then empty as well Karp and Papadimitriou, Definition 1 and footnote, p. 3.

A facial description $F$ is a collection of triples $\langle z,f,g\rangle$ , where $z\in L$ , $f\in\mathbb Z^{n(z)}$ , and $g\in\mathbb Z$ . For every rational vector $x$ and every $z\in L$ , membership in $\mathrm{CH}(S(z))$ must be equivalent to satisfying all inequalities $f\cdot x\le g$ indexed by triples of $F$ with first component $z$ . A facial description is small when one polynomial in $|z|+n(z)$ bounds the binary size of every coefficient of every triple in the collection. The collection itself need not be small Karp and Papadimitriou, pp. 4–5.

A zero-one problem has only vectors with entries zero or one in each $S(z)$ . An integer-programming-type problem gives an integral matrix $A(z)$ and right-hand side $b(z)$ and takes $S(z)$ to be all nonnegative integer vectors satisfying $A(z)x\le b(z)$ . The dimensions of these data depend on $z$ . Their total binary coefficient size is controlled by the length of the encoded input Karp and Papadimitriou, pp. 5–6.

Formalization targets

Lemma 1

The mission goal is the complete statement for both classes:

\forall C,\quad \bigl(\operatorname{ZeroOne}(C)\lor\operatorname{IPType}(C)\bigr) \Longrightarrow \exists F,\quad \operatorname{FacialDescription}(C,F)\land\operatorname{Small}(C,F).

The milestone list records three claims used in the paper's proof. In a zero-one hull, every vertex is a zero-one vector and there are no nonzero rays. For integer hulls, the cited vertex-size result gives a uniform polynomial bound on the coordinates of vertices. Finally, the Cramer's-rule calculation bounds an integral normal $f$ and intercept $g$ by $(2nx)^n$ when the geometric data have coordinates bounded by $x$ Karp and Papadimitriou, pp. 5–7.

Significance

Lemma 1 permits descriptions of the whole hull, including lower-dimensional hulls that require equations and unbounded integer hulls that have recession directions. It gives a coefficient bound for every input with one polynomial, rather than a polynomial chosen separately for each instance. This is the premise needed when the paper treats a facial description as a language of short encodable inequalities. The later assertion that an NP-recognizable small facial description places the decision problem in co-NP has a distinct hypothesis and is handled by the first mission of this series Karp and Papadimitriou, Theorem 1, pp. 7–8.

The mathematical result is known; the mission asks for a Lean proof of its precise rational, input-indexed version. The local declarations are proof obligations and do not yet carry verified proofs. Existing platform work includes a rational integer-hull definition reused here, a related open theorem of Cook–Gerards–Schrijver–Tardos that bounds normal coefficients under different hypotheses, and proved real-carrier versions of Meyer's polyhedrality and finite-generation results. The related open theorem does not supply Lemma 1: it has neither this zero-one case nor the bound on the intercept $g$ . The real-carrier theorems supply neither the input-size bound nor the paper's rational convention.

Difficulty

The zero-one case has bounded coordinates, but a complete description must also handle an empty hull and a hull contained in a proper affine subspace. Bounding only the facet inequalities of a full-dimensional nonempty polytope does not describe those cases. The integer-programming case adds unbounded directions, and the paper's printed identification of extreme rays with rows of $A$ is false. A faithful treatment must bound suitable recession directions and then obtain a uniform coefficient bound for the inequalities describing the hull Karp and Papadimitriou, pp. 5–7.

Formalization scope

The Lean model uses List Bool for inputs, Fin (n z) → ℤ for feasible vectors, and Fin (n z) → ℚ for the convex hull. The published CookSensitivity.ChvatalRank.polyhedron and integerHull definitions provide the general rational integer-programming substrate. This mission adds only the paper's input-indexed problem, facial description, smallness condition, and two named problem classes. The three language-recognition requirements in the paper's Definition 1 are omitted because Lemma 1 never uses them; the resulting theorem applies to every such geometric problem, including every c.o.p. in the paper's narrower definition.

The polynomial bound is represented by $(|z|+n(z))^k+k$ with a single natural exponent $k$ chosen before every input and inequality. For an integer-programming-type input, the sum $s(A,b)=\sum_a\lceil\log_2(1+|a|)\rceil$ over all entries of $A$ and $b$ must be at most $|z|$ . This makes the paper's phrase “ $z$ specifies $A$ and $b$ ” an explicit binary-size condition. The cited vertex milestone bounds coordinates in terms of $s$ alone, as the page states: a zero column gives a line direction rather than a vertex. Its statement follows the paper's unrestricted $Ax\le b$ formulation; the IP-type goal additionally imposes $x\ge0$ . The paper calls $b$ an $n$ -vector, but it has one entry per row of $A$ and is an $m$ -vector here. The Cramer's-rule milestone allows rows of size $2x$ , as vertex differences can reach that size.

Empty feasible sets, dimension zero, lower-dimensional hulls, and unbounded IP hulls remain in the goal. A description restricted to full-dimensional facets, or a smallness exponent chosen separately for each input, would not meet it. A complete development needs rational convex hulls, integer-hull geometry, finite descriptions of rational polyhedra, bounds on vertices and recession generators, and finite-dimensional determinant estimates. The rational integer-hull definitions and the coefficient estimates are reusable beyond this mission; contributions that establish the three listed milestones or the remaining geometric steps are in scope.

Selected references

Richard M. Karp and Christos H. Papadimitriou, On Linear Characterizations of Combinatorial Optimization Problems, MIT/LCS/TM-154, February 1980, pp. 3–7. Report scan. Later published in SIAM Journal on Computing 11 (1982), 620–632, DOI.

6 thms2 active usersReviewed

Completed

Graph Theory Operations Research Optimization·Captain: mikedeng1

Finding Minimum-Cost Circulations by Successive Approximation I: The Generic Refine Subroutine Stops Within 3n(n − 1) + 3nm + 3n²(m + n) Update Operations at an ε-Optimal CirculationResearch Paper

Motivation

Minimum-cost circulation asks how to route flow around a directed network without accumulating flow at any vertex, while minimizing the total cost of the routed units. It is a basic network optimization problem: lower-bound and demand constraints in many flow models can be converted into circulation form. Goldberg and Tarjan's 1987 technical report develops a successive-approximation approach in which a local repair subroutine, refine, improves an approximately optimal circulation. The report was followed by a 1990 journal article; all theorem numbers and page citations in this mission refer to the 1987 report.

The mission isolates the generic form of refine, where an implementation may choose any applicable update at each step. Its question is whether every such choice sequence finishes after a controlled number of operations and returns a circulation with a stronger optimality certificate. The related Goldberg–Tarjan maximum-flow algorithm uses push and relabel operations with distance labels; here the labels are real-valued prices tied to arc costs. The authors' cycle-canceling work uses the same circulation network model and supplies published definitions reused in this development.

Setting

A circulation network has a finite vertex set $V$ and a symmetric set $E$ of directed arcs: whenever $(v,w)$ is an arc, so is $(w,v)$ . Let $n=|V|$ and $m=|E|$ , counting both orientations. Each arc has a real capacity $u(v,w)$ and cost $c(v,w)$ , with $c(v,w)=-c(w,v)$ . A pseudoflow $f$ respects capacities and the paired-arc relation $f(v,w)=-f(w,v)$ . Its excess $e_f(v)$ is the sum of flow entering $v$ . A circulation is a pseudoflow with zero excess everywhere. The already published CycleCanceling.MinMean.Network supplies this network, its circulation predicate, and residual capacity $u_f(v,w)=u(v,w)-f(v,w)$ . An arc is residual when this capacity is positive.

A price function $p:V\to\mathbb R$ changes an arc's reduced cost to $c_p(v,w)=c(v,w)-p(v)+p(w)$ . A pseudoflow is $\varepsilon$ -optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$ . A vertex is active when its excess is positive. An admissible arc is a residual arc of negative reduced cost. Refine takes an input circulation that is $2\varepsilon$ -optimal, saturates every arc whose reduced cost is negative, and then repeatedly applies an available update. A push sends flow from an active vertex along an admissible arc. A relabel raises the price of an active vertex with no outgoing admissible arc to the largest value permitted by $\varepsilon$ -optimality. These rules are Figures 4 and 5, printed pages 18–19.

Formalization targets

The supporting targets are the paper's progress and correctness results, its price bound, and the three operation counts. For any generic refine run from a $2\varepsilon$ -optimal circulation, Lemma 5.8 bounds each vertex's price increase by $3n\varepsilon$ . Lemmas 5.9–5.11 bound the numbers $R,S,T$ of relabelings, saturating pushes, and nonsaturating pushes:

R\leq 3n(n-1),\qquad S\leq 3nm,\qquad T\leq 3n^2(m+n).

The goal combines the resulting bound on the number $K$ of updates with progress and correctness:

K\leq 3n(n-1)+3nm+3n^2(m+n).

If the final state has an active vertex, another update exists. If no update applies, the final pseudoflow is a circulation and is $\varepsilon$ -optimal with respect to its final prices. This is the explicit operation-count content behind the generic subroutine's analysis in Section 5. It does not claim a bound for a particular data structure or a complete minimum-cost algorithm.

Significance

The theorem gives an order-independent finite bound: the choice of which applicable push or relabel to perform cannot cause generic refine to run forever or stop with an active vertex. Its output is a circulation whose approximate-optimality tolerance has been halved. That output can serve as the next input in the successive-approximation framework. For integral costs, the report's Theorem 2.3 later turns a sufficiently small tolerance into exact minimum cost; that outer-loop result is outside this mission.

This mission specifies the generic cost-scaling state machine in Lean and poses its quantitative analysis as open formalization targets. The shared network and circulation definitions from the published Goldberg–Tarjan 1989 series are available, and a related generic maximum-flow theorem in the 1988 series has a machine-checked proof. Those results do not prove refine's price-based bounds. Contributions that establish the paper's progress, price, or counting statements for this state machine, and reusable facts about finite residual networks, advance the open goal.

Difficulty

A push respects a capacity, but it can create activity at another vertex; a relabel changes which arcs are admissible. Thus checking a single update does not bound an arbitrary sequence. The price bound also depends on the circulation and prices supplied at entry, not merely on the current pseudoflow being $\varepsilon$ -optimal. Finally, a vertex with no admissible outgoing arc may appear to be stuck when the relabel minimum is over an empty set. Feasibility of the original circulation network is needed to establish that an active vertex still has a genuine next update. The operation bound requires accounting for the three update types across every possible choice sequence.

Formalization scope

Vertices form a finite type, and capacities, costs, flows, and prices are real-valued functions. The network has symmetric ordered arcs and antisymmetric costs. There is no separate nonnegativity assumption on capacities; feasibility is supplied by the input circulation. The new $\varepsilon$ is positive, so the entry circulation is $2\varepsilon$ -optimal before Figure 4 halves the error parameter. The run starts from the resulting saturated pseudoflow and records one applicable push or relabel per index $k<K$ . Counts classify those actual steps by the selected arc's residual capacity after a push. Termination is the negation of the paper's loop guard, not a definition that assumes zero excess.

The reduced-cost sign is $c-p(v)+p(w)$ , and relabel raises $p(v)$ . This differs from the published 1989 epsilon-optimality definition, so only its network model is imported. The relabel relation requires an attained minimum over a nonempty set of outgoing residual arcs; it assigns no default value to an empty minimum. Loops may occur in the reused network model, but cost antisymmetry makes their reduced cost zero, so they cannot be push arcs. The explicit constants are the report's $3n\varepsilon$ , $3n(n-1)$ , $3nm$ , and $3n^2(m+n)$ ; the goal sums the last three. The report's RAM-model $O(\cdot)$ running times are outside the formal statements. A definition that makes termination equivalent to conservation or assigns an arbitrary relabel price at an empty set would miss the target.

Selected references

Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987. Technical report.
Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI. The report above supplies this mission's numbering.
Andrew V. Goldberg and Robert E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4), 1988. DOI.
Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, Journal of the ACM 36(4), 1989. DOI.

10 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Solving Large-Scale Zero-One Linear Programming Problems: A Minimal Cover Inequality Cuts Off x̄ iff the Knapsack Problem (2.12) Has Optimal Value Less Than OneResearch Paper

Motivation

Large zero–one linear programs can contain constraints involving only a small fraction of their variables. Crowder, Johnson and Padberg study how to extract useful inequalities from one such row while solving the larger program. Their computational method identifies a violated inequality at a current linear programming solution, adds it, and resolves the relaxation. The mathematical question behind that step is whether a minimal cover inequality can be found by a separate optimization problem. The authors answer it in Section 2.3 of their 1983 paper, after developing cover and configuration inequalities in Section 2.2. Crowder, Johnson and Padberg (1983)

The target is a known result from that paper. It is a precise statement about a finite knapsack row and a point in the unit cube, independent of the paper's implementation and numerical experiments. The paper also discusses $(1,k)$ -configurations and lifting, which turn the identified inequalities into valid cuts involving additional row variables. Those statements supply the mission's milestones and make the separation result useful in its original setting. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4

Setting

Fix a finite index set $K$ , positive rational coefficients $a_j$ for $j\in K$ , and a rational right-hand side $a_0$ . A zero–one solution is a vector with each $x_j\in\{0,1\}$ satisfying the single row

\sum_{j\in K}a_jx_j\le a_0. \tag{2.5}

The model uses the support set $x=\{j:x_j=1\}$ for such a vector. A set $S\subseteq K$ is a minimal cover when its total coefficient exceeds $a_0$ , but removing any one member makes the total at most $a_0$ :

\sum_{j\in S}a_j>a_0, \qquad \sum_{j\in S}a_j-a_k\le a_0\quad(k\in S). \tag{2.6}

It yields the cover inequality $\sum_{j\in S}x_j\le |S|-1$ for every feasible zero–one vector. The right-hand side is interpreted as a real number, so the expression also has its usual meaning when $S$ is empty.

A $(1,k)$ -configuration consists of $S^*\subseteq K$ , $t\notin S^*$ and an integer $2\le k\le |S^*|$ . The set $S^*$ itself fits the row, while $Q\cup\{t\}$ is a minimal cover for every $k$ -element subset $Q$ of $S^*$ . For any $k\le r\le |S^*|$ and $r$ -element $T\subseteq S^*$ , its inequality is $(r-k+1)x_t+\sum_{j\in T}x_j\le r$ . Crowder, Johnson and Padberg (1983), pp. 810–811

For a point $\bar x\in[0,1]^K$ , the separation problem asks for a cover $s\subseteq K$ minimizing $\sum_{j\in s}(1-\bar x_j)$ , subject to the strict condition $\sum_{j\in s}a_j>a_0$ . This is problem (2.12). The set of attainable values is finite, but it is empty if the row has no cover. An optimal value $z$ is therefore asserted only when a least attainable value exists.

Formalization targets

Cover separation

The goal is the paper's Section 2.3 equivalence:

\left(\exists S\subseteq K\text{ minimal}: \sum_{j\in S}\bar x_j>|S|-1\right) \quad\Longleftrightarrow\quad z<1,

where $z$ is the attained optimum of (2.12). A cover inequality cuts off $\bar x$ precisely when its left-hand side exceeds $|S|-1$ . If there is no cover, (2.12) has no optimal value; the theorem does not assign it an artificial value. Crowder, Johnson and Padberg (1983), pp. 812–813

Valid inequalities and lifting

The milestones state the validity of (2.7) and every inequality in (2.9), the two assertions used in the separation equivalence, and the relaxed lifting claims of Section 2.4. For lifting, $z_k$ is the maximum integer objective value in (2.10), $\bar z_k$ is the maximum in its linear relaxation, and $z_k^*=\lfloor\bar z_k\rfloor$ . The claims are $z_k\le z_k^*$ and validity after adding variable $k$ with coefficient $f_k=f_0-z_k^*$ . They concern attained optima, as the paper's “maximum” language requires. Crowder, Johnson and Padberg (1983), pp. 811, 814

Significance

The equivalence turns a geometric question about which cover inequality excludes $\bar x$ into a finite optimization test with a numerical threshold of one. It identifies when a minimal cover cut exists for a row, while the validity milestones certify that the inequalities can be added without removing zero–one feasible points. The lifting claims explain how an inequality first written on a subset of variables remains valid as further variables enter it. These are the mathematical guarantees used by the paper's cutting plane procedure. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4

The paper proves the separation equivalence and states the surrounding validity claims. This mission records their exact statements in Lean; its theorem proofs remain open. A complete development would add machine-checked proofs for the finite cover argument, configuration inequalities, and lifting validity. The resulting definitions of feasible supports, attained optimization values and intermediate inequality validity can also be reused in other finite knapsack formalizations.

Difficulty

Checking all subsets of $K$ directly grows rapidly with the row size. A separation result must relate a minimum over all covers to an inequality indexed by a minimal cover, while accounting for objective coefficients that may be zero when $\bar x_j=1$ . The same boundary matters for lifting: the zero–one maximum is compared with a continuous relaxation, and rounding is justified by the integer coefficients of the current inequality. If the lifting problem is infeasible, neither maximum exists. Crowder, Johnson and Padberg (1983), pp. 812–814

Formalization scope

Lean uses an arbitrary finite index type for $K$ , replacing the paper's indices $1,\ldots,n$ . A zero–one vector is a finite support set. Row coefficients and $a_0$ are rational, as on p. 810; the point $\bar x$ and separation values are real. The target asks only that $\bar x$ lie in the unit cube. Although the paper obtains it as an optimum of the full LP relaxation (2.11), that additional property is not used in the row-level equivalence. No sign condition is imposed on $a_0$ .

The strict knapsack condition in (2.12) is retained. “Chops off” means strict violation of (2.7). “Optimal value” means membership and leastness in the attainable value set; for lifting it means membership and greatestness. Thus rows with no cover or infeasible lifting subproblem do not acquire a default zero optimum. The size expressions $|S|-1$ and $r-k+1$ are evaluated in the reals, so natural-number truncation cannot change them. Integer lifting coefficients and the floor of the relaxed optimum express the paper's “truncating to its integer part”; the feasible relaxed problem includes the zero vector, so this agrees with truncation toward zero there.

Validity during an intermediate lifting step ranges over feasible zero–one vectors supported in the current set $S$ . After adding $k$ , it ranges over support in $S\cup\{k\}$ . The final inequality covers the whole row when that set is $K$ . The development must preserve the full quantifier over every $k$ -subset in (2.8) and every $r$ and $T$ in (2.9); restricting these would weaken the paper's claim. Contributions proving the named milestones, adding concrete examples, or developing general finite optimization lemmas are in scope. The facet assertions attributed to Padberg are outside the target. A related lifted-cover facet statement already appears on the platform as NemhauserWolsey.partitioned_cover_lifting_defines_facet; its conventions and claim differ from this mission's validity results.

Selected references

H. Crowder, E. L. Johnson and M. Padberg, Solving Large-Scale Zero-One Linear Programming Problems, Operations Research 31(5), 803–834, 1983. DOI: 10.1287/opre.31.5.803

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems 4: For Symmetric Cost and Right-Hand-Side Uncertainty, the Adaptability Gap Is at Most FourResearch Paper

Motivation

Two-stage optimization separates a decision made before uncertainty is observed from one made after a scenario is known. A fully adaptive policy can choose a different second-stage decision in each scenario, while a static robust solution commits to a single second-stage decision that works in every scenario. Static solutions can be simpler to implement, but their worst-case cost may be higher. Bertsimas and Goyal ask how large this cost difference can be when both the right-hand sides of the constraints and the second-stage prices vary. Their Theorem 5.1 gives a factor of four when the paired uncertainty set is symmetric and nonnegative, even when both stages contain integer variables.

The distinction matters in planning problems where one policy is fixed in advance and another could respond to realized demand or prices. A uniform bound lets a planner assess the cost of the static restriction without solving every adaptive policy exactly. The source is the authors' manuscript; all page and result numbers in this mission refer to that manuscript, not to the journal pagination.

Setting

Fix matrices $A\in\mathbb R^{m\times n_1}$ and $B\in\mathbb R^{m\times n_2}$ . A scenario $\omega\in\Omega$ supplies a right-hand side $b(\omega)\in\mathbb R_+^m$ and a second-stage cost vector $d(\omega)\in\mathbb R_+^{n_2}$ . The first-stage cost vector is $c\in\mathbb R_+^{n_1}$ . For a set $I$ of designated integer coordinates, write $D_I$ for the nonnegative real vectors whose coordinates in $I$ are integers. After relabelling, this is the paper's $\mathbb R_+^{n-p}\times\mathbb Z_+^p$ .

In the robust problem $\Pi_{\mathrm{Rob}}(b,d)$ , one first-stage decision $x\in D_{I_1}$ and one second-stage decision $y\in D_{I_2}$ must satisfy $Ax+By\ge b(\omega)$ for every scenario. Their cost is $c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty$ . In the adaptive problem $\Pi_{\mathrm{Adapt}}(b,d)$ , $x$ is still chosen once, but $y(\omega)\in D_{I_2}$ may depend on the scenario. Its constraints are $Ax+By(\omega)\ge b(\omega)$ for every $\omega$ , and its cost is $c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty(\omega)$ . The optimal values $z_{\mathrm{Rob}}(b,d)$ and $z_{\mathrm{Adapt}}(b,d)$ are infima over feasible decisions in these respective problems; these are models (1.5)–(1.6).

The paired uncertainty set is $I_{(b,d)}(\Omega)=\{(b(\omega),d(\omega)): \omega\in\Omega\}$ . It is symmetric when it contains a point $u^0$ such that $u^0+z$ belongs to the set exactly when $u^0-z$ does, for every displacement $z$ . The point $u^0$ is itself a scenario realization. The smallest coordinatewise bounding hypercube has lower and upper corners $(b^l,d^l)$ and $(b^h,d^h)$ ; its center is $((b^l+b^h)/2,(d^l+d^h)/2)$ . These are Definition 1.2 and displays (2.5)–(2.7).

Formalization targets

The adaptability gap

The goal is Theorem 5.1:

z_{\mathrm{Rob}}(b,d)\le 4z_{\mathrm{Adapt}}(b,d).

The factor applies to every nonnegative symmetric paired uncertainty set and to both continuous and mixed-integer decisions. The theorem does not require an optimal adaptive policy to attain its infimum. The milestones record the source's geometric Lemma 2.3 and the estimates labelled (5.1)–(5.4), which supply the center-scenario cost and feasibility statements with the explicit factor four. They are stated for arbitrary feasible adaptive policies so the conclusion also covers nonattained infima.

Significance

The result bounds the price of committing to a single second-stage decision, despite uncertainty in both the constraints and the objective. In this setting the comparison is independent of the number of scenarios and of the dimensions $m,n_1,n_2$ . The paper also considers right-hand-side-only uncertainty, positive sets, and hypercubes; this mission isolates its symmetric paired-uncertainty result §5.1.

The theorem is proved in the paper. The remaining formalization work is a machine-checked development of the model, the bounding-hypercube geometry, the cost inequalities, and the passage from arbitrary feasible policies to the optimal values. The resulting definitions of mixed-integer domains, robust and adaptive feasibility, and extended-real optimal values can also support the other results in this paper's mission series. The theorem statements here are open proof targets, with no machine-checked proofs claimed.

Difficulty

The worst-case maximizer of $d(\omega)^Ty(\omega)$ can vary with $\omega$ , and an adaptive policy can choose a different integer vector in every scenario. Selecting one of those vectors as a static decision therefore gives no immediate cost or feasibility guarantee. The point of symmetry is a realizable scenario, but it must control both components of every other paired scenario. Without nonnegative data, doubling the center-scenario decision may fail to cover a positive right-hand side, and the cost comparison can fail as well. Integer coordinates also constrain which scalings preserve the decision domain; the exact factor in the theorem is compatible with doubling, unlike arbitrary fractional rescalings.

Formalization scope

Vectors are real functions on finite index types, matrices use Mathlib's matrix-vector product, and inequalities are componentwise. The scenario set is the range of $\omega\mapsto(b(\omega),d(\omega))$ , with a product-space symmetry predicate. No probability measure or measurability structure is used in these worst-case problems. Both stages may have integer coordinates designated by sets $I_1,I_2$ ; no continuous-only second-stage restriction is imposed.

Optimal values and worst-case costs use extended real numbers. An infeasible problem has value $+\infty$ ; a real infimum over an empty feasible set would incorrectly return a default zero. Symmetry includes a center belonging to the scenario range, so the scenario set is nonempty. Combined with nonnegative coordinates, symmetry bounds every scenario coordinate and makes the bounding-hypercube endpoints meaningful. The hypotheses retain $c\ge0$ , $b(\omega)\ge0$ , and $d(\omega)\ge0$ , which the source uses in its factor-four estimate. A statement restricted to continuous recourse, an assumed optimal adaptive policy, or a zero-valued infeasible problem would not express this target.

The source prints $\mathbb Z_+^{n_2}$ in (1.5)–(1.6), although the model's second-stage integer count is $p_2$ ; the domain here follows the surrounding $p_2$ convention. Lemma 2.3 is stated here for nonnegative sets, the regime needed for its second inequality. Its coordinatewise suprema and infima agree with the printed maxima and minima in this bounded symmetric setting. Contributions to the shared domain and geometry lemmas, the mixed-integer scaling fact, and the optimal-value comparison are all useful to the goal.

Selected references

Dimitris Bertsimas and Vineet Goyal, On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems, authors' manuscript of Mathematics of Operations Research, 2010. DOI: 10.1287/moor.1090.0440.

9 thms2 active usersReviewed

Completed

Algebraic Geometry Differential Geometry Operations Research+1·Captain: mikedeng1

Log-Barrier Interior Point Methods Are Not Strongly Polynomial 2: The Total Curvature of the Central Path of LW_r(t) Exceeds (2^(r−2) − 1)π/2 − ε for All Large tResearch Paper

Motivation: curvature of the central path as a complexity measure

Path-following interior point methods solve a linear program by tracking its central path, a smooth curve that runs through the interior of the feasible set and ends at an optimal solution. Their number of iterations is polynomial in the bit size of the input, and whether some interior point method is strongly polynomial (bounded by a polynomial in the number of variables and constraints alone) is open. Bayer and Lagarias called the central path "a fundamental mathematical object underlying Karmarkar's algorithm". Dedieu and Shub proposed its total curvature as an informal complexity measure: a path that turns little should be easy to follow with straight steps. Several results bound that curvature:

2005. Dedieu and Shub conjecture that the total curvature of the central path is bounded linearly in the dimension. Dedieu, Malajovich and Shub prove an $O(n)$ bound on average over the regions of a hyperplane arrangement. De Loera, Sturmfels and Vinzant later obtain the same averaged bound with matroid methods (arXiv:1012.3978).
2008–2009. Deza, Terlaky and Zinchenko build redundant Klee–Minty cubes and "snakes" with curvature $\Omega(m)$ for $m$ inequalities, which refutes the dimension version. They then conjecture the continuous analogue of the Hirsch conjecture: the total curvature is bounded linearly in the number of constraints.
2014–2017. Allamigeon, Benchimol, Gaubert and Joswig disprove that conjecture with a family of linear programs whose central paths have curvature exponential in the number of constraints. The bound first appeared in arXiv:1405.4161 and was given an elementary tropical proof in arXiv:1708.01544v2, Theorem 25, which is the result of this mission.

Setting

A linear program in slack form has a real $m\times n$ matrix $A$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ and $N:=n+m$ :

\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. } Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .

For $\mu>0$ the point of the central path $(x^\mu,w^\mu,s^\mu,y^\mu)\in\mathbb R^{2N}$ is the unique solution of

Ax+w=b,\quad s-A^\top y=c,\quad x_js_j=\mu,\quad w_iy_i=\mu,\quad x,w,s,y>0. \tag{1}

The primal central path is $\mu\mapsto(x^\mu,w^\mu)\in\mathbb R^N$ .

For $r\ge1$ and $t>0$ , the program $\mathbf{LW}_r(t)$ minimizes $x_1$ over $x\in\mathbb R^{2r}$ subject to

x_1\le t^2,\quad x_2\le t,\quad x_{2j+1}\le t\,x_{2j-1},\quad x_{2j+1}\le t\,x_{2j},\quad x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ \ (1\le j<r),\quad x\ge0 .

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$ , $m=3r-1$ , $N=5r-1$ .

For points $U,V,W$ of Euclidean space with $U\ne V\ne W$ , the turning angle $\angle UVW\in[0,\pi]$ is the angle between the vectors $V-U$ and $W-V$ . For a curve $\sigma$ parameterized over $I\subseteq\mathbb R$ , the total curvature is

\kappa(\sigma,I)=\sup\Big\{\sum_{k=1}^{p-1}\angle\,\sigma(\mu_{k-1})\sigma(\mu_k)\sigma(\mu_{k+1})\ :\ \mu_0<\dots<\mu_p\ \text{in } I\Big\}\in[0,+\infty].

The milestones also use the field $\mathbb K$ of absolutely convergent generalized real Puiseux series $\sum_{\alpha\in\mathbb R}a_\alpha t^\alpha$ . Such a series can be evaluated at large real $t$ , and it has a valuation $\mathrm{val}\in\mathbb T=\mathbb R\cup\{-\infty\}$ , its leading exponent. Read over $\mathbb K$ , $\mathbf{LW}_r$ is one linear program. The valuation of its central path at $\mu=t^\lambda$ is the tropical central path $\mathcal C^{\mathrm{trop}}(\lambda)\in\mathbb R^{2N}$ , a piecewise-linear curve with an explicit recursive description (Propositions 20–21 of the paper).

Formalization targets

Goal: Theorem 25

For every $r\ge1$ and $\epsilon>0$ there is $t_0$ such that for all $t>t_0$ ,

\kappa\big(\mu\mapsto(x^\mu,w^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon\quad\text{and}\quad\kappa\big(\mu\mapsto(x^\mu,w^\mu,s^\mu,y^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon

for the central path of $\mathbf{LW}^=_r(t)$ . Here $t_0$ may depend on $r$ and $\epsilon$ . Both the primal and the primal-dual curves are part of the goal, as in the paper.

Milestones, in the order of the paper's argument

Lemma 22: for non-null $\mathbf x,\mathbf y\in\mathbb K^d$ , the angle $\angle\mathbf x(t)\mathbf y(t)$ has a limit, which is $\pi/2$ when the arg maxes of $\mathrm{val}\,\mathbf x$ and $\mathrm{val}\,\mathbf y$ are disjoint.
Lemma 23: the turning angle $\angle\mathbf U(t)\mathbf V(t)\mathbf W(t)\to\pi/2$ when $\max\mathrm{val}\,\mathbf U<\max\mathrm{val}\,\mathbf V<\max\mathrm{val}\,\mathbf W$ and the arg maxes of $\mathrm{val}\,\mathbf V$ and $\mathrm{val}\,\mathbf W$ are disjoint.
Proposition 24: $\liminf_{t}\kappa(\mathcal C_t,[t^{\lambda_0},t^{\lambda_p}])\ge\sum_{k=1}^{p-1}\angle^*\mathcal C^{\mathrm{trop}}(\lambda_{k-1})\mathcal C^{\mathrm{trop}}(\lambda_k)\mathcal C^{\mathrm{trop}}(\lambda_{k+1})$ , where $\angle^*$ is the weak tropical angle ( $\pi/2$ under the conditions of Lemma 23, else $0$ ).
Table 1: the coordinates of the tropical central path of $\mathbf{LW}_r$ at $\lambda=(4k+2c)/2^j$ .
Claims in the proof of Theorem 25 (p. 23): on $[0,2]$ the dual coordinates of $\mathcal C^{\mathrm{trop}}$ are at most $\max(0,\lambda-1)$ . At $\lambda_k=4k/2^{r-1}$ the largest coordinate is $r-1+(2k+2)/2^{r-1}$ , attained only by $w_{3(r-1)}$ or $w_{3(r-1)+1}$ . Hence $\angle^*=\pi/2$ at each interior subdivision point.

Significance

The theorem shows that the total curvature of the central path is not bounded by any polynomial in the number of constraints: $\mathbf{LW}_r$ has $3r+1$ constraints and curvature at least about $2^{r-2}\pi/2$ . This settles the conjecture of Deza, Terlaky and Zinchenko in the negative. It also shows that the averaged upper bounds of Dedieu–Malajovich–Shub and De Loera–Sturmfels–Vinzant cannot hold for every region. A companion mission of this series formalizes the paper's second main result, an exponential lower bound on the number of iterations of log-barrier path-following methods on the same family.

The result is proved on paper. As far as is known, it has not been formalized in any proof assistant, and Mathlib has no notion of the total curvature of a curve, of Puiseux-series evaluation and valuation, or of the tropical central path. Formalizing the theorem would give a machine-checked reference point for a much-cited negative result in interior point theory. The Lean definitions of total curvature and of the turning angle are general and reusable.

Difficulty

The total curvature is a supremum over inscribed polygons, and a lower bound needs explicit polygons whose angles can be estimated for every large $t$ . The central path of $\mathbf{LW}^=_r(t)$ has no closed form, so its points cannot be written down at given parameters $\mu$ . Numerical evidence at a fixed $t$ says nothing uniform in $r$ . The natural first idea, to compute the path's angles directly from system (1) for a fixed instance, gives no handle on how the number of turns grows with $r$ . What is needed is control of the path's geometry uniformly over the whole scale of $t$ , with $2^{r-2}$ turns located at once, and the threshold $t_0$ is not explicit.

Formalization scope

Vectors in which angles are measured are EuclideanSpace ℝ (Fin d). The turning angle is InnerProductGeometry.angle (V - U) (W - V), not Mathlib's vertex angle ∠ U V W, which is $\pi$ minus it. A degenerate triple ( $U=V$ or $V=W$ ) contributes angle $0$ . Total curvature is an EReal-valued supremum over strictly increasing parameter sequences in the parameter set, and the goal uses the set $(0,\infty)$ . The primal and primal-dual curves are the vectors $(x,w)\in\mathbb R^{5r-1}$ and $(x,w,s,y)\in\mathbb R^{2(5r-1)}$ . System (1) is the published Vanderbei central-path system with objective $-c$ . The goal quantifies over every curve solving (1) for all $\mu>0$ . Existence and uniqueness of that curve is the referenced platform statement VanderbeiLP.CentralPath.central_path_exists_unique and is not posed again. Indices are the paper's, 1-based, mapped to Fin by subtracting one. Powers $2^{r-2}$ use integer exponents of the real number $2$ .

A trivializing formalization is ruled out explicitly: the curvature is a supremum in EReal (a real sSup of an unbounded set would be $0$ ), the turning angle is not the vertex angle, and degenerate polygons cannot add spurious right angles.

Lemmas 22–24 are stated over a model of $\mathbb K$ by coefficient functions with the paper's support and absolute-convergence conditions. Equalities, products and order in $\mathbb K$ are expressed through evaluation at all sufficiently large $t$ , which is how the paper characterizes them. Table 1 and the claims of the proof are stated for the explicit tropical central path of $\mathbf{LW}_r$ given by Propositions 20–21 (milestones of the companion mission), written as a definition here. One repair: the paper's "uniquely attained" claim fails at $r=2$ , $k=0$ , where $w_1=w_4=2$ . It is stated with that case excluded, which the proof does not use.

Welcome contributions: a general theory of total curvature of curves (monotonicity under refinement, behaviour under limits), asymptotics of evaluated Puiseux series, and the comparison between the central path over $\mathbb K$ and its real specializations.

Selected references

X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-Barrier Interior Point Methods Are Not Strongly Polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; preprint v2 (cited throughout) arXiv:1708.01544, doi:10.1137/17M1142132.
X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Long and winding central paths, preprint, 2014. arXiv:1405.4161
J. A. De Loera, B. Sturmfels, C. Vinzant, The central curve in linear programming, Found. Comput. Math. 12(4), 2012. arXiv:1012.3978
J.-P. Dedieu, G. Malajovich, M. Shub, On the curvature of the central path of linear programming theory, Found. Comput. Math. 5(2), 2005.
J.-P. Dedieu, M. Shub, Newton flow and interior point methods in linear programming, Int. J. Bifurcation and Chaos 15(3), 2005.
A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Springer, 2009.
L. van den Dries, P. Speissegger, The real field with convergent generalized power series, Trans. Amer. Math. Soc. 350(11), 1998.

18 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Maximum Pressure Policies in Stochastic Processing Networks IV: In Reversed Leontief Networks Extreme Allocations Are Integral and Maximum Pressure Separates by ProcessorResearch Paper

Motivation

Maximum pressure policies schedule a stochastic processing network by choosing, at each decision time, an allocation of processors to activities that maximizes a linear "pressure" built from the current buffer levels and the network's input-output matrix. Dai and Lin (Oper. Res. 53(2), 2005) prove that such policies are throughput optimal: they stabilize the network whenever any policy can. The policies descend from the back-pressure rule of Tassiulas and Ephremides (IEEE TAC 37(12), 1992) for wireless networks and are now standard in switching, manufacturing and data-center scheduling.

The general theory lets a processor split its capacity among several activities at once. In many systems this is impossible: a machine works on one job type at a time. Section 7 of the paper shows that with this restriction Harrison's static planning LP no longer characterizes stability, and Section 8 shows that forbidding preemption can make a maximum pressure policy unstable. Both difficulties disappear for one structural class, the reversed Leontief networks, in which every activity needs exactly one processor. This mission formalizes the two lemmas that make that class work: extreme allocations are integral (Lemma 1), and a maximum pressure allocation is found processor by processor (Lemma 3).

Setting

A network has buffers $0,1,\dots,I$ , where Buffer $0$ is the outside world and $\mathcal I=\{1,\dots,I\}$ are the internal buffers; activities $\mathcal J=\{1,\dots,J\}$ ; and processors $\mathcal K=\{1,\dots,K\}$ . The resource consumption matrix $A$ has $A_{kj}=1$ if activity $j$ requires processor $k$ and $0$ otherwise. The constituency indicator $B_{ji}=1$ records that activity $j$ processes buffer $i$ . An input activity processes only Buffer $0$ ; a service activity never processes Buffer $0$ . Each processor runs input activities only (an input processor) or service activities only (a service processor). Each activity $j$ has a mean processing requirement $m_j$ , rate $\mu_j=1/m_j$ , and a routing matrix $P^j$ .

The input-output matrix is

R_{ij}=\mu_j\Big(B_{ji}-\sum_{i'\in\mathcal I\cup\{0\}}B_{ji'}P^j_{i'i}\Big),\qquad i\in\mathcal I,\ j\in\mathcal J.

An allocation is $a\in\mathbb R^J_+$ with $\sum_j A_{kj}a_j\le1$ for every processor and $\sum_j A_{kj}a_j=1$ for every input processor; $\mathcal A$ is the set of allocations, $\mathcal E$ its set of extreme points, and $\mathcal N\subseteq\mathcal A$ the allocations with integer coordinates. For a buffer-level vector $z\in\mathbb R^I_+$ , the network pressure is $p(a,z)=z\cdot Ra$ and the activity pressure is $p(j,z)=\sum_{i\in\mathcal I}R_{ij}z_i$ , with $p(0,z)=0$ for the idle Activity $0$ .

The network is reversed Leontief if each activity requires exactly one processor. The possible activities of processor $k$ are $\mathcal J(k)=\{j:A_{kj}=1\}$ for an input processor and $\mathcal J(k)=\{0\}\cup\{j:A_{kj}=1\}$ for a service processor. Under an integer allocation $a$ , $j_k(a)$ is the activity processor $k$ works on, or $0$ if $k$ is idle.

Formalization targets

Goal: Lemma 3 (p. 208)

For a reversed Leontief network, $z\in\mathbb R^I_+$ and $a\in\mathcal E$ ,

p(a,z)=\max_{a'\in\mathcal E}p(a',z)\iff j_k(a)\in\operatorname*{arg\,max}_{j\in\mathcal J(k)}p(j,z)\ \text{ for all }k\in\mathcal K.

Milestones

the pressure identity $p(a,z)=\sum_j a_j\,p(j,z)$ (§8, p. 208);
$\mathcal N\subseteq\mathcal E$ (proof of Lemma 1, p. 215);
Lemma 1 (p. 207): for a reversed Leontief network, $\mathcal E=\mathcal N$ ;
for $a\in\mathcal E$ : $j_k(a)\in\mathcal J(k)$ and $p(a,z)=\sum_k p(j_k(a),z)$ (proof of Lemma 3);
the single-processor exchange $\tilde a=a-e_{j_k(a)}+e_j$ stays in $\mathcal E$ and shifts the pressure by $p(j,z)-p(j_k(a),z)$ (proof of Lemma 3).

A further supporting item, not a milestone, states the decomposition $a=\sum_{j\in\mathcal J(\tilde k)}a_j b^j$ of an allocation along one processor (proof of Lemma 1, p. 215).

Significance

The result. Lemma 1 says that, in a reversed Leontief network, the maximum pressure policies of the processor-splitting theory are automatically non-processor-splitting, so the paper's throughput optimality theorem holds in the setting where machines cannot be shared. Lemma 3 says that the maximization over the (exponentially large) set $\mathcal E$ decouples into one small maximization per processor: each processor picks an activity of largest activity pressure among its own options. This separability is what makes the nonpreemptive version of the policy well defined and is the key step towards Theorem 9 (throughput optimality of nonpreemptive maximum pressure policies). It also covers multiclass queueing networks with alternate routes (§9.1), which are reversed Leontief.

Formalizing it. Both lemmas are proved in the paper; to our knowledge neither is machine-checked. The mission produces a reusable Lean model of the allocation polytope of a processing network with input processors, its integer and extreme points, and the activity and network pressures. The integrality of $\mathcal E$ is a total-unimodularity-type fact for a block structure that is not available in Mathlib in this form.

Difficulty

The pressure is linear, so maximizing over $\mathcal E$ equals maximizing over $\mathcal A$ ; the substance is the description of $\mathcal E$ . The polytope $\mathcal A$ is not a box: input processors carry equality constraints and service processors inequality constraints, and in general networks (an activity needing several processors) $\mathcal E$ contains fractional points, as the paper's example in §7 shows. The step that fails for general networks is the decomposition of a fractional allocation along a single processor: it needs every activity of that processor to use no other processor. In Lean, extreme points must be handled through Mathlib's Set.extremePoints, and the argmax over $\mathcal J(k)$ must keep track of the idle option, which exists for service processors and not for input processors.

Formalization scope

Indices are 0-based: internal buffers Fin I, buffers with Buffer $0$ Fin (I+1) (Buffer $0$ is 0, internal buffer $i$ is i.succ), activities Fin J, processors Fin K. The idle Activity $0$ is none : Option (Fin J), with activity pressure $0$ and unit vector $e_0=0$ . $\mathcal E$ is Set.extremePoints ℝ 𝒜. "Maximizes the pressure over $\mathcal E$ " is stated by domination ( $p(a',z)\le p(a,z)$ for all $a'\in\mathcal E$ ), never through a supremum. $j_k(a)$ is defined by choice of an activity of $k$ at level $1$ ; it is used only for $a\in\mathcal E$ , where it is unique.

The standing assumptions of §2 are carried as one hypothesis: $A$ and $B$ are $0$ – $1$ , constituencies are nonempty, every activity is an input or service activity and needs a processor, processors are input-only or service-only, at least one input activity exists, $P^j\ge0$ and $P^j_{00}=0$ . Two disclosed additions: every input processor has at least one activity (otherwise (2) is infeasible and $\mathcal A=\emptyset$ ), and $m_j>0$ (needed for $\mu_j=1/m_j$ ). The goal keeps $z\ge0$ as on the page; two milestones drop it, which strengthens them.

A trivializing formalization would make $\mathcal E$ empty or give input processors an idle option; both are excluded: $\mathcal E$ is the extreme-point set of the real polytope $\mathcal A$ , which is nonempty for a reversed Leontief network under the standing assumptions, and the idle option belongs to $\mathcal J(k)$ only for service processors, as in (60).

Contributions welcome: proofs of the milestones, a general lemma that $0$ – $1$ points of a subset of the unit cube are extreme, and the separable description of extreme points of products of simplices, which is reusable beyond this mission.

Selected references

J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. https://doi.org/10.1287/opre.1040.0170
J. M. Harrison, Brownian models of open processing networks: canonical representation of workload, Annals of Applied Probability 10(1):75–103, 2000. https://doi.org/10.1214/aoap/1019737665
L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479

7 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Maximum Pressure Policies in Stochastic Processing Networks III: Strict Leontief Networks Satisfy the Extreme-Allocation-Available (EAA) AssumptionResearch Paper

Motivation

A stochastic processing network (Harrison 2000) models a system in which processors carry out activities and each activity draws jobs from one or more buffers. Manufacturing lines, call centers with cross-trained agents, and data switches all fit this model. A central question is which scheduling policies are throughput optimal, meaning they stabilize the network whenever any policy can.

Dai and Lin (Oper. Res. 53(2), 2005) show that maximum pressure policies are throughput optimal. These policies generalize the back-pressure rule of Tassiulas and Ephremides (1992) for wireless and switch networks, and at each moment they choose the allocation that maximizes a linear "network pressure". Their main theorem (Theorem 2) has one structural hypothesis, the extreme-allocation-available (EAA) assumption (Assumption 1). It holds for many familiar networks and fails for some (§6.2 gives a counterexample). Theorem 6 identifies a broad class where it always holds: strict Leontief networks, in the sense of Bramson and Williams (2003). This mission formalizes that theorem.

Setting

A network has internal buffers $\mathcal I=\{1,\dots,I\}$ , an outside Buffer $0$ , activities $\mathcal J=\{1,\dots,J\}$ and processors $\mathcal K=\{1,\dots,K\}$ .

$A_{kj}=1$ if activity $j$ needs processor $k$ , and $0$ otherwise.
$B_{ji}=1$ if activity $j$ processes buffer $i\in\mathcal I\cup\{0\}$ , and $0$ otherwise. The set $\mathcal B_j=\{i:B_{ji}=1\}$ is the constituency of $j$ .
An input activity has $\mathcal B_j=\{0\}$ ; a service activity has $0\notin\mathcal B_j$ . Every activity is one of the two.
Each processor serves input activities only (an input processor) or service activities only.
Activity $j$ has processing rate $\mu_j=1/m_j$ and a nonnegative routing matrix $P^j$ .

The input-output matrix is

R_{ij}=\mu_j\Big(B_{ji}-\sum_{i'\in\mathcal I\cup\{0\}}B_{ji'}P^j_{i'i}\Big),\qquad i\in\mathcal I,\ j\in\mathcal J.

An allocation $a\in\mathbb R^J_+$ gives the level at which each activity runs. The allocation set $\mathcal A$ consists of the allocations with $\sum_jA_{kj}a_j\le1$ for every processor and $\sum_jA_{kj}a_j=1$ for every input processor. Write $\mathcal E$ for the set of its extreme points, the extreme allocations. For a buffer-level vector $z\in\mathbb R^I_+$ the network pressure is $p(a,z)=z\cdot Ra$ . Buffer $i$ is a constituent buffer of $a$ if $\sum_ja_jB_{ji}>0$ .

Assumption 1 (EAA). For every $z\in\mathbb R^I_+$ there is $a^*\in\mathcal E$ with $p(a^*,z)=\max_{a\in\mathcal E}p(a,z)$ such that $z_i>0$ for every constituent buffer $i$ of $a^*$ .

A network is strict Leontief if every service activity has exactly one buffer in its constituency, denoted $i(j)$ .

Formalization targets

Goal: Theorem 6 (p. 204)

\text{strict Leontief}\ \Longrightarrow\ \forall z\in\mathbb R^I_+\ \exists a^*\in\mathcal E:\ p(a^*,z)=\max_{a\in\mathcal E}p(a,z)\ \text{ and }\ z_i>0\ \text{for every constituent buffer } i \text{ of } a^*.

Milestones

(§3, p. 201) For every $z\in\mathbb R^I_+$ , $\max_{a\in\mathcal A}p(a,z)$ is attained at an extreme allocation.
(p. 204) $B_{ji}=0$ and $R_{ij}\le0$ whenever $i\in\mathcal I$ , $i\ne i(j)$ .
(p. 204) Let $\mathcal J_0$ be the set of service activities $j$ with $z_{i(j)}=0$ . Setting the coordinates of $\hat a\in\mathcal A$ in $\mathcal J_0$ to zero gives $\tilde a\in\mathcal A$ with $z'R\tilde a\ge z'R\hat a$ .
(p. 204) It suffices to find $a^*\in\arg\max_{a\in\mathcal E}z'Ra$ with $a^*_j=0$ on $\mathcal J_0$ .
(p. 204) If $\tilde a\in\mathcal A$ maximizes $z'Ra$ over $\mathcal A$ and vanishes on $\mathcal J_0$ , some extreme allocation does both.

Significance

The result. Theorem 2 of the paper states that, under EAA, a maximum pressure policy is pathwise stable whenever the static planning problem has a feasible solution with $\rho\le1$ . Theorem 6 removes the EAA hypothesis for strict Leontief networks. In that class maximum pressure is therefore throughput optimal with no further structural condition. The class includes multiclass queueing networks with alternate routes and networks of input-queued data switches (§9), so Theorem 6 is the step that turns the abstract main theorem into a statement about these concrete systems.

Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Formalizing it fixes the exact standing assumptions of the model, several of which the paper uses without stating (see below). It also yields a reusable Lean vocabulary for stochastic processing networks with input activities: $R$ from (5), the allocation polytope with the input-processor equality (2), extreme allocations, network pressure and EAA. The companion missions of this series on maximum pressure policies build on the same vocabulary.

Difficulty

The naive argument stops at "take a maximizing extreme allocation". A maximizer $\hat a$ may run a service activity whose buffer is empty, in which case EAA fails at $\hat a$ . Removing such activities gives $\tilde a$ , which has the right support and pressure but is in general not extreme. The pressure inequality depends on the sign pattern of $R$ , which holds only because every service activity has a single buffer. In the network of §6.2 this sign pattern fails and so does EAA. Returning from $\tilde a$ to an extreme allocation without losing the support property needs a convex-geometry argument about the polytope $\mathcal A$ . In Lean this means relating Set.extremePoints of a compact polyhedron to maximizers of a linear functional and to supports.

Formalization scope

Indexing. Internal buffers are Fin I. Buffers including Buffer 0 are Fin (I+1), with Buffer $0$ as 0 and internal buffer $i$ as i.succ. Activities and processors are 0-based.
Standing assumptions (§2), one predicate Network.Standing.
- $A$ and $B$ are $0$ – $1$ matrices.
- Every constituency is nonempty, and every activity is an input or a service activity.
- Every activity needs a processor.
- Each processor serves input activities only or service activities only.
- There is an input activity.
- $P^j\ge0$ and $P^j_{00}=0$ .
Disclosed additions to the page.
1. Every input processor has an activity. "The input processors are never idle" presupposes it.
2. $m_j>0$ . The page writes "nonnegative" but sets $\mu_j=1/m_j$ .
3. $\mathcal A\neq\emptyset$ , an explicit hypothesis of the goal and of milestone 1. The paper presupposes it by listing $\mathcal E=\{a^1,\dots,a^E\}$ . It does not follow from the standing assumptions: two input activities needing input processors $\{1,2\}$ and $\{2,3\}$ make (2) infeasible, so $\mathcal E=\emptyset$ and EAA fails in a network that is vacuously strict Leontief. A verification file checks this example in Lean.
Conventions.
- $\mathcal E$ is Mathlib's Set.extremePoints ℝ 𝒜.
- Every "max" and "argmax" is in domination form ( $p(a',z)\le p(a^*,z)$ for all $a'$ ), never sSup. Without attainment the statement would be vacuous.
- Constituent buffers are internal buffers only. Buffer $0$ has no level.
- $i(j)$ is written relationally.
- Row sums of $P^j$ are not imposed.
Trivializing formalizations ruled out. EAA must not be weakened to a supremum over a possibly empty $\mathcal E$ , and Buffer $0$ must not be counted as a constituent buffer. Either change would make the goal trivially true or impossible.
Infrastructure. Solvers need two results:
- attainment of a linear maximum on extreme points of a compact convex polyhedron, via IsCompact.extremePoints_nonempty and Krein–Milman;
- the fact that every extreme point in a convex decomposition of a maximizer with positive weight is a maximizer.
Both are reusable beyond this mission. Contributions proving them as general Mathlib-style lemmas are welcome.

Selected references

J. G. Dai and W. Lin, Maximum pressure policies in stochastic processing networks, Operations Research 53(2):197–218, 2005. https://doi.org/10.1287/opre.1040.0170
J. M. Harrison, Brownian models of open processing networks: canonical representation of workload, Annals of Applied Probability 10(1):75–103, 2000. https://doi.org/10.1214/aoap/1019737665
M. Bramson and R. J. Williams, Two workload properties for Brownian networks, Queueing Systems 45(3):191–221, 2003. (no link verified; see the reference list of Dai & Lin 2005)
L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479

7 thms2 active usersReviewed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Precedence-Constrained Scheduling Problems on Parallel Machines That Run at Different Speeds: A min{K + 2√K + 1, 1.89 log m + O(√log m)}-Approximation for Q|prec|CmaxResearch Paper

Scheduling precedence-constrained jobs on machines of different speeds

Graham (1966) showed that list scheduling finds a schedule within a factor $2$ of optimal for precedence-constrained jobs on identical parallel machines, the first performance guarantee for an approximation algorithm. When the machines run at different speeds (uniformly related machines), the same analysis breaks down, and for two decades the problem $Q|prec|C_{\max}$ resisted a guarantee independent of the speeds better than $O(\sqrt m)$ .

Timeline:

1974, Liu and Liu: list scheduling on machines of different speeds, with a guarantee that depends on the speeds and can be arbitrarily large even for a fixed number of machines.
1980, Jaffe: list scheduling on the machines whose speed is within a factor $\sqrt m$ of the fastest gives an $O(\sqrt m)$ -approximation.
1978, Lenstra and Rinnooy Kan: with precedence constraints, no $\rho$ -approximation with $\rho < 4/3$ exists unless P = NP. This bound already holds for identical machines.
1997–1999, Chudak and Shmoys: an LP-guided variant of list scheduling achieves $O(\log m)$ , and $K + 2\sqrt K + 1$ when there are only $K$ distinct speeds (J. Algorithms 30 (1999) 323–343; conference version SODA 1997).

The mission formalizes the makespan half of that paper, up to its Theorem 3.7.

Setting

An instance has $n$ jobs and $m \ge 1$ machines. Job $j$ requires $p_j > 0$ units of processing, and machine $i$ runs at speed $s_i > 0$ , so job $j$ takes $p_j/s_i$ time units on machine $i$ . A strict partial order $\prec$ on the jobs gives precedence constraints: $j \prec k$ means that job $k$ may not start until job $j$ has completed.

A schedule runs each job $j$ without interruption on one machine $\mu(j)$ , from a start time $S_j \ge 0$ to its completion time $C_j = S_j + p_j/s_{\mu(j)}$ . A machine processes at most one job at a time, and $j \prec k$ forces $C_j \le S_k$ . Its length is $C_{\max} = \max_j C_j$ . $C^*_{\max}$ is the length of an optimal schedule.

Let $\bar s_1 > \bar s_2 > \cdots > \bar s_K$ be the distinct speeds and $m_k$ the number of machines of speed $\bar s_k$ . An assignment $k(j)$ names the speed class at which job $j$ is to run. Its loads are $D_k = \frac{1}{m_k}\sum_{j:k(j)=k} p_j/\bar s_k$ , and its chain bound $C$ is the largest value of $\sum_{j\in\mathcal C} p_j/\bar s_{k(j)}$ over chains $\mathcal C$ of $\prec$ . Speed-based list scheduling is Graham's rule restricted by the assignment: whenever a machine of speed $\bar s_k$ is idle, it starts the first available job $j$ on the list with $k(j) = k$ .

The linear program LP has variables $x_{kj} \ge 0$ , $C_j$ and $D$ . It minimizes $D$ subject to the following constraints:

$\sum_k x_{kj} = 1$ ;
$\frac{1}{m_k\bar s_k}\sum_j p_j x_{kj} \le D$ ;
$\sum_k (p_j/\bar s_k)x_{kj} \le C_j$ , and $\sum_k (p_j/\bar s_k)x_{kj} \le C_j - C_{j'}$ whenever $j' \prec j$ ;
$C_j \le D$ .

From a solution, with $\bar p_j = \sum_k (p_j/\bar s_k)x_{kj}$ , the assignment algorithm gives each job $j$ the speed class $k \notin B_j = \{k : p_j/\bar s_k > \gamma\bar p_j\}$ of largest capacity $\bar s_k m_k$ .

Formalization targets

Goal: Theorem 3.7 (p. 10)

There is an absolute constant $c$ such that for every instance with $m \ge 2$ machines and $K$ distinct speeds, the better of the two schedules below has length at most

\min\bigl\{K + 2\sqrt K + 1,\ 1.89\log_2 m + c\sqrt{\log_2 m}\bigr\}\cdot C^*_{\max}.

(A) An optimal LP solution, the assignment algorithm with $\gamma = \sqrt K + 1$ , and speed-based list scheduling.
(B) The same algorithm run on speeds rounded down to powers of $e$ , with machines slower than $\bar s_1/(m\log_2 m)$ dropped, and read back on the original machines.

Milestones, in proof order

Existence of speed-based list schedules (p. 4).
Theorem 2.1: $C_{\max} \le C + \sum_k D_k$ .
The LP lower bound $\bar D \le C^*_{\max}$ (p. 6).
Lemmas 3.1–3.4: chain bounds $2\bar D$ and $(\sqrt K + 1)\bar D$ , and load bounds $2K\bar D$ and $(K + \sqrt K)\bar D$ .
Theorem 3.5 and Corollary 3.6: the factor $K + 2\sqrt K + 1$ against $C^*_{\max}$ and against $\bar D$ .
Rounded schedules serve the original instance (p. 9).
The speed rounding: at most $\lfloor\log_\beta(\alpha m)\rfloor + 1$ speeds, and the LP value grows by a factor of at most $\beta(1 + 1/\alpha)$ (p. 10).
The "In fact" form of the guarantee, relative to any feasible LP solution (p. 10).

Significance

The result gives the first $O(\log m)$ guarantee for $Q|prec|C_{\max}$ , independent of the speeds, and a guarantee depending only on the number of distinct speeds. Through the batching technique of Shmoys, Wein and Williamson it extends to release dates (Corollary 3.8). Since LP also relaxes the preemptive problem, it gives an $O(\log m)$ bound on the ratio between the nonpreemptive and preemptive optima (Corollaries 3.9, 3.10). The "In fact" form, relative to an arbitrary feasible LP solution, drives the paper's $\sum w_jC_j$ algorithm in §4.

The result is proved in the literature but, as far as is known, not formalized. A formal proof requires machine-checking the following:

the continuous-time list-scheduling argument for different speeds;
the filtering argument of Lin and Vitter;
the reduction to logarithmically many speeds, including the off-by-one count of rounded speeds that the page leaves implicit.

Later work gave a combinatorial $O(\log m)$ -approximation (Chekuri and Bender, 2001) and an $O(\log m/\log\log m)$ -approximation (Li, 2017). These are not part of this mission.

Difficulty

Graham's argument has two lower bounds:

the total processing along a chain;
the time during which every machine is busy.

With different speeds, the first bound fails: a chain may have been run on slow machines, and its length then says nothing about $C^*_{\max}$ . Forcing every job onto a fast machine repairs chains but can leave most machines idle, so the second bound fails. The paper only guarantees that all machines of one speed are busy at each moment of an idle period. Making this pay off requires an assignment that controls chain lengths and per-class loads simultaneously. That assignment is the delicate part: Theorem 2.1 is the bookkeeping, while Lemmas 3.2 and 3.4 rely on the LP. Two of the formal steps are routine on paper but fiddly in Lean: time-interval accounting over a continuous-time schedule, and the counting of rounded speed classes.

Formalization scope

Representation. Jobs are Fin n and machines Fin m with $m \ge 1$ . $p_j > 0$ and $s_i > 0$ . $\prec$ is a strict partial order, and a chain is a finite set of pairwise comparable jobs. $C_{\max}$ is the maximum completion time, or $0$ with no jobs.
Speed classes. The classes are computed from the speeds, so $m_k \ge 1$ and $\bar s_k > 0$ by construction. The Lean index $0$ is the paper's fastest class $\bar s_1$ .
The algorithm as predicates. Speed-based list scheduling is the predicate the proof of Theorem 2.1 uses: jobs run at their assigned speed, and no machine of a job's speed idles while that job is available and unstarted. Every list order and every order of idle machines satisfies it. The assignment algorithm is a predicate allowing every maximizer, since the page does not break ties. Theorems 3.5 and 3.7 quantify over all optimal LP solutions, all such assignments and all such schedules. Existence is supplied by the milestones.
Comparator. The bound is stated against every feasible schedule of the same instance, never against the LP value or a best schedule of the rounded instance. A statement asserting only that some good schedule exists would be trivially true (the optimum witnesses it); the goal bounds the schedule the algorithm returns.
Constants and logarithms. $\log m$ is $\log_2 m$ , as the paper specifies. $m \ge 2$ is assumed in Theorem 3.7 and in the "In fact" remark, which are asymptotic in $m$ . The $O(\sqrt{\log m})$ term is one absolute constant $c$ , quantified before the instance, and $1.89$ is the page's number.
Generalizations and corrections. Lemmas 3.1–3.4 are stated for every feasible LP solution, since their proofs use only feasibility. The speed rounding is relative to $\bar s_1$ , with no normalization. The count of rounded speeds is $\lfloor\log_\beta(\alpha m)\rfloor + 1$ ; the page writes $\log_\beta(\alpha m)$ .
Not formalized. Polynomial running time is not formalized.
Out of scope. Corollaries 3.8–3.10, Theorem 3.11 and §4 are excluded.

Proofs of any milestone are welcome. Reusable beyond this mission are the following: the model of nonpreemptive schedules on uniformly related machines with precedence, the speed-based list-scheduling predicate with Theorem 2.1, and the LP.

Selected references

F. A. Chudak and D. B. Shmoys, Approximation algorithms for precedence-constrained scheduling problems on parallel machines that run at different speeds, J. Algorithms 30 (1999) 323–343 (authors' manuscript used here). https://doi.org/10.1006/jagm.1998.0987
R. L. Graham, Bounds for certain multiprocessing anomalies, Bell System Technical Journal 45 (1966) 1563–1581. https://doi.org/10.1002/j.1538-7305.1966.tb01709.x
J. M. Jaffe, Efficient scheduling of tasks without full use of processor resources, Theoretical Computer Science 12 (1980) 1–17. https://doi.org/10.1016/0304-3975(80)90002-4
J.-H. Lin and J. S. Vitter, ε-approximations with minimum packing constraint violation, STOC 1992, 771–782. https://doi.org/10.1145/129712.129787
D. B. Shmoys, J. Wein and D. P. Williamson, Scheduling parallel machines on-line, SIAM J. Computing 24 (1995) 1313–1331. https://doi.org/10.1137/S0097539793248317
C. Chekuri and M. A. Bender, An efficient approximation algorithm for minimizing makespan on uniformly related machines, J. Algorithms 41 (2001) 212–224. https://doi.org/10.1006/jagm.2001.1184
S. Li, Scheduling to minimize total weighted completion time via time-indexed linear programming relaxations, SIAM J. Computing 46 (2017) 409–440. https://doi.org/10.1137/15M1053163

16 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

A Robust Optimization Approach to Inventory Theory: The Optimal Robust Policy Is the Optimal Nominal Policy for an Explicit Modified Demand, at Extra Cost (2ph/(p+h))·ΣA_kResearch Paper

Motivation

Classical inventory theory chooses order quantities against a probability distribution of demand. The resulting dynamic programs are optimal in expectation but need the distribution, and they become intractable once several installations, capacities or fixed costs interact. Robust optimization replaces the distribution by an uncertainty set and asks for the order sequence whose worst-case cost over that set is smallest. Bertsimas and Thiele (Operations Research 54(1), 2006) applied the budget-of-uncertainty approach of Bertsimas and Sim (The Price of Robustness, Operations Research 52(1), 2004) to finite-horizon inventory control. Their main structural result says that robustness does not destroy the structure of the classical problem. The robust problem is a deterministic (nominal) inventory problem with an explicitly modified demand, and the price of robustness is an explicit constant.

Setting

A single item is ordered at a single installation over periods $k = 0, \dots, T-1$ . The stock at the beginning of the horizon is $x_0$ . Orders $u_k \ge 0$ arrive immediately, demand $w_k$ is subtracted, and excess demand is backlogged, so the stock at the end of period $k$ is

x_{k+1} = x_0 + \sum_{i=0}^{k} (u_i - w_i).

The demand of period $k$ is uncertain: $w_k = \bar w_k + \hat w_k z_k$ with a nominal demand $\bar w_k$ , a maximal deviation $\hat w_k \ge 0$ and a scaled deviation $z_k \in [-1, 1]$ . A budget of uncertainty $\Gamma_k$ limits the total scaled deviation up to period $k$ . The budgets satisfy $0 \le \Gamma_0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$ .

Each period costs $C(u_k) + R(x_{k+1})$ . The purchasing cost is $C(u) = K + cu$ for $u > 0$ and $C(0) = 0$ , with $c > 0$ and $K \ge 0$ . The holding/shortage cost is $R(x) = \max(hx, -px)$ , with $h \ge 0$ and $p > c$ . The nominal problem with demand $w$ minimizes $\sum_{k<T} (C(u_k) + R(x_{k+1}))$ over $u \ge 0$ for a fixed demand sequence $w$ .

For each $k$ , $A_k$ is the optimal value of the linear program

A_k = \max\Big\{\sum_{i=0}^{k} \hat w_i z_i \;:\; \sum_{i=0}^{k} z_i \le \Gamma_k,\ 0 \le z_i \le 1\Big\} \qquad (13)

It is the worst-case deviation of the cumulative demand up to $k$ from its nominal value, with $A_{-1} = 0$ . Write $\bar x_{k+1} = x_0 + \sum_{i\le k}(u_i - \bar w_i)$ for the nominal stock. The robust formulation (14) minimizes $\sum_{k<T} (C(u_k) + y_k)$ over $(u, y, q, r)$ subject to the following constraints for every $k < T$ :

$u_k \ge 0$ , $q_k \ge 0$ , and $r_{ik} \ge 0$ , $q_k + r_{ik} \ge \hat w_i$ for $i \le k$ ;
$y_k \ge h(\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$ ;
$y_k \ge p(-\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$ .

The variables $q, r$ are the dual of (13). Formulation (14) is equivalent to requiring the holding and shortage constraints of period $k$ for every demand whose scaled deviations satisfy $|z_i| \le 1$ and $\sum_{i \le k}|z_i| \le \Gamma_k$ .

Formalization targets

Goal: Theorem 3.2 (a), (b), (d)

Let the modified demand be

w'_k = \bar w_k + \frac{p-h}{p+h}\,(A_k - A_{k-1}). \qquad (20)

Write $N_{w'}(u)$ for the nominal cost of $u$ under demand $w'$ . Then:

For every $u \ge 0$ , the minimum of the objective of (14) over the feasible $(y, q, r)$ is attained and equals

N_{w'}(u) + \frac{2ph}{p+h}\sum_{k=0}^{T-1} A_k.

$u$ is the order part of an optimal solution of (14) if and only if $u$ is optimal for the nominal problem with demand $w'$ .
The optimal cost of (14) is the optimal nominal cost under $w'$ plus $\frac{2ph}{p+h}\sum_k A_k$ .
If $K = 0$ and $w'_k \ge 0$ , the order-up-to policy with levels $S_k = w'_k$ is robust-optimal.

Milestones

The milestones are the steps of the paper's proof, in order:

LP (13) and its dual are attained with the common value $A_k$ .
The constraints of (14) are the robust counterpart of the $k$ -th holding/shortage pair (10)–(11).
For fixed orders, the value of (14) is the sum (21).
The modified stock (22) satisfies $x'_{k+1} = \bar x_{k+1} - \frac{p-h}{p+h}A_k$ .
The max identity (23): $\max(h(\bar x+A), p(-\bar x+A)) = \max(hx', -px') + \frac{2ph}{p+h}A$ .
Lemma 3.1(b): for nonnegative demand, the nominal problem without fixed cost is solved by ordering up to $S_k = w_k$ .
Remark 1: $A_{k-1} \le A_k$ , so $w'_k \ge \bar w_k$ when $p \ge h$ .
Remark 3: under i.i.d. demand, $A_k = \hat w\Gamma_k$ , which gives the closed-form thresholds.

Significance

The theorem reduces robust inventory control to nominal inventory control. Every structural fact known for the deterministic problem then transfers to the robust one. These include the optimality of base-stock policies without fixed cost and the threshold structure with a fixed cost. The robust base-stock levels are explicit: they shift the nominal levels by $\frac{p-h}{p+h}(A_k - A_{k-1})$ , upward when shortage is more expensive than holding. The extra cost $\frac{2ph}{p+h}\sum_k A_k$ quantifies the price of protection as a function of the budgets. The paper uses the same reduction for capacitated orders (Theorem 3.3) and for supply networks (§4).

The result has been proved since 2006, and no machine-checked proof of it, or of any budgeted robust counterpart, is known to exist. This mission provides several formalizations for reuse:

the budgeted robust counterpart of a pair of piecewise-linear constraints;
the duality of the fractional knapsack LP (13);
the optimality of base-stock orders for a deterministic backlogged inventory problem.

Difficulty

The algebraic core, identity (23), is elementary. The work is in the reductions around it. The first is that (14) really is the worst case of (10)–(11): this needs strong duality for (13), together with attainment on both sides, and the observation that the minimizing and maximizing deviations of a constraint pair differ. The second is that the minimum of (14) over the auxiliary variables, for fixed orders, is (21). This requires the dual optimum to be attained with the value of (13), and $h, p \ge 0$ so that the cost is monotone in $A_k$ . The third is the base-stock part, which needs Lemma 3.1(b), a global optimality statement for a $T$ -period problem with backlogging. The paper proves that lemma by an explicit dual certificate. An argument through first-order conditions in each period is not enough, because orders in one period affect every later stock level.

Formalization scope

All data are real numbers and sequences are ℕ → ℝ; only indices $k < T$ matter. stock w u k denotes $x_{k+1}$ , the stock at the end of period $k$ . The standing assumptions of §3.1 are fields of the model:

$c > 0$ , $K \ge 0$ , $h \ge 0$ , $p > c$ ;
$\hat w_k \ge 0$ ;
$\Gamma_0 \ge 0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$ .

The conventions and corrections are:

Fixed cost. The paper writes it with binary variables and a big- $M$ constraint. Here it is the indicator $C(u_k)$ in the objective, as in the paper's own (21).
"Optimal". It always means minimality over all feasible points.
The policy. It is the order sequence chosen at time 0.
$A_k$ . It is the value of (13), as in Remark 1 after the theorem, not "the optimal $q^*, r^*$ of (14)", which need not be unique.
The robust formulation. (14) is formalized as printed: the $k$ -th constraint pair is protected by the budget $\Gamma_k$ alone, not by the intersection of all budgets up to $k$ .
Sign slip. The page's $x_{k+1} = \bar x_{k+1} + \sum \hat w_i z_i$ is a sign slip for $\bar x_{k+1} - \sum \hat w_i z_i$ . The formal statements use the correct sign; the result is unaffected because the deviation set is symmetric.
Part (b). It is stated under $w'_k \ge 0$ . As printed it fails when $p < h$ makes $w'$ negative, for example $T = 2$ , $\bar w = \hat w = (10, 0)$ , $\Gamma = (0, 1)$ , $c = 1$ , $h = 4$ , $p = 2$ , $x_0 = 0$ . Lemma 3.1(b) carries the matching hypothesis of nonnegative demand.
Remark 3. It adds $\Gamma_0 \le 1$ .
Remark 1. Its inequalities are weak.
Not stated. The (s, S) clause of (a) and part (c) are excluded. They rest on a stochastic theorem cited from Bertsekas (1995) and on thresholds stated through the optimal ordering times.

A trivializing formalization is ruled out: the robust cost is formulation (14) with its variables $y, q, r$ , and $A_k$ is the value of LP (13). Neither is the closed-form objective (21) nor an arbitrary sequence. Contributions are welcome on the LP duality of (13) (a fractional knapsack), on the robust counterpart milestone, and on Lemma 3.1(b), each of which is independent of the others.

Selected references

D. Bertsimas, A. Thiele, A Robust Optimization Approach to Inventory Theory, Operations Research 54(1):150–168, 2006. https://doi.org/10.1287/opre.1050.0238
D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1):35–53, 2004. https://doi.org/10.1287/opre.1030.0065
A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. 1, Athena Scientific, 1995.

12 thms2 active usersReviewed

Completed

Algebraic Geometry Complexity Theory Operations Research+1·Captain: mikedeng1

Log-Barrier Interior Point Methods Are Not Strongly Polynomial 1: Every Polygonal Curve in the Wide Neighborhood of the Central Path of LW_r(t) from μ̄ ≤ 1 to μ̄ ≥ t² Has at Least 2^(r−1) SegmentsResearch Paper

Motivation

Interior point methods solve linear programs in a number of arithmetic operations polynomial in the bit length of the input (Karmarkar 1984). Whether linear programming admits a strongly polynomial algorithm, one whose number of arithmetic operations is bounded by a polynomial in the number of variables and constraints alone, is open; it is the ninth of Smale's problems for the next century (Smale 1998/2000, see the references). A natural question is whether some interior point method is strongly polynomial. Primal-dual path-following methods follow the central path of a log-barrier problem and are the methods used in practice.

Allamigeon, Benchimol, Gaubert and Joswig (arXiv:1708.01544, SIAM J. Appl. Algebra Geom. 2018) gave such a family. For linear programs $\mathbf{LW}_r(t)$ with $2r$ variables and $3r+1$ constraints, every path-following method that stays in the wide neighborhood of the central path needs at least $2^{r-1}$ iterations once $t$ is large enough. The same family disproves the "continuous Hirsch conjecture" of Deza, Terlaky and Zinchenko (DTZ09, see the references) on the total curvature of the central path. That curvature result is the subject of a separate mission. This mission formalizes the iteration bound.

Setting

For a real $m\times n$ matrix $A$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ and $N:=n+m$ , the paper considers the linear program in slack form and its dual,

\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. }\ Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .

A primal-dual point is $z=(x,w,s,y)\in\mathbb R^{2N}$ . The set $\mathcal F^\circ$ of strictly feasible points consists of the $z$ with all $2N$ coordinates positive that satisfy both equality systems. The duality measure is

\bar\mu(z)=\frac1N\big(\langle x,s\rangle+\langle w,y\rangle\big),

and for $0<\theta<1$ the wide neighborhood of the central path is

\mathcal N^{-\infty}_\theta=\Big\{z\in\mathcal F^\circ:\ x_js_j\ge(1-\theta)\bar\mu(z)\ \forall j,\ \ w_iy_i\ge(1-\theta)\bar\mu(z)\ \forall i\Big\}.

The central path itself is the set of points where all products $x_js_j$ , $w_iy_i$ are equal. The neighborhood bounds the products only from below. It contains the $\ell_2$ and $\ell_\infty$ neighborhoods used by short-step, long-step and predictor-corrector methods.

The instance is $\mathbf{LW}_r(t)$ , for $r\ge1$ and $t>0$ :

\min\ x_1\ \text{ s.t. }\ x_1\le t^2,\ x_2\le t,\ x_{2j+1}\le t\,x_{2j-1},\ x_{2j+1}\le t\,x_{2j},\ x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ (1\le j<r),\ x_{2r-1},x_{2r}\ge0 .

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$ , $m=3r-1$ , $N=5r-1$ . Its wide neighborhood is written $\mathcal N^{-\infty}_{\theta,t}$ . A polygonal curve is a union $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ of $p$ segments, and it is contained in the neighborhood when every point of every segment is.

The milestones use the tropical semifield $\mathbb T=\mathbb R\cup\{-\infty\}$ with $a\oplus b=\max(a,b)$ and $a\odot b=a+b$ . The tropical segment $\mathsf{tsegm}(u,v)$ is the set of points $\lambda\odot u\oplus\mu\odot v$ with $\lambda\oplus\mu=0$ . The Funk metric is $\delta_F(x,y)=\max(0,\max_k(y_k-x_k))$ , with $d_\infty(x,y)=\max(\delta_F(x,y),\delta_F(y,x))$ and the directed Hausdorff distance $d_\infty(X,Y)=\sup_{x\in X}\inf_{y\in Y}d_\infty(x,y)$ . Finally, $\log_t$ is applied coordinatewise, with $\log_t0=-\infty$ .

Formalization targets

Goal: Theorem 30 (p. 27)

Let $r\ge1$ and $0<\theta<1$ , and suppose that

t>\Big(\max\Big((10r-2)!,\ \frac{((10r-1)!)^{24}}{(1-\theta)^3}\Big)\Big)^{2^{r-1}} .\tag{36}

If a polygonal curve $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ is contained in $\mathcal N^{-\infty}_{\theta,t}$ with $\bar\mu(z^0)\le1$ and $\bar\mu(z^p)\ge t^2$ , then

p\ge2^{r-1}.

The threshold (36) is the paper's own explicit constant. Corollary 31 (Theorem B of the introduction) restates the result for algorithms. Any method whose iterates and the segments joining them stay in the wide neighborhood performs at least $2^{r-1}$ iterations to reduce the duality measure from $t^2$ to $1$ .

Milestones

Proposition 1 (p. 5). On the primal-dual feasible set, $\bar\mu((1-\alpha)z+\alpha z')=(1-\alpha)\bar\mu(z)+\alpha\bar\mu(z')$ for all $\alpha\in\mathbb R$ .
Lemma 5 (p. 10). For $u\le v$ in $\mathbb T^d$ , $\mathsf{tsegm}(u,v)$ is a polygonal curve whose segments, oriented from $u$ to $v$ , have directions $e^{K_1},\dots,e^{K_\ell}$ with $K_1\subsetneq\dots\subsetneq K_\ell$ and $\ell\le d$ .
Lemma 8 (p. 11). For a segment $S=[u,v]$ in $\mathbb R^d_+$ and $t>1$ ,

d_\infty\big(\mathsf{tsegm}(\log_tu,\log_tv),\ \log_tS\big)\le\log_t2 .

Lemma 11 (p. 13). For a $d\times d$ matrix $\mathbf M$ with monomial entries $\pm t^{\alpha_{ij}}$ and $t>1$ , $\log_t|\det\mathbf M(t)|$ and $\operatorname{val}(\det\mathbf M)$ differ by at most $\log_td!$ ; the lower bound holds once $t\ge(d!)^{1/\eta(\mathbf M)}$ .
Proposition 20 (p. 19). The explicit recursion for $x^\lambda$ gives the greatest point of the tropical polyhedron $\{x\in\mathcal P':x_1\le\lambda\}$ , where $\mathcal P'\subseteq\mathbb T^{2r}$ is cut out by the tropicalized constraints (26) of $\mathbf{LW}_r$ .

Significance

The theorem shows that the iteration count of a large class of primal-dual log-barrier interior point methods cannot be bounded by any function of $r$ that grows more slowly than $2^{r-1}$ , uniformly in the data. The class includes the methods of Kojima–Mizuno–Yoshise, Monteiro–Adler and Mizuno–Todd–Ye. No such method is strongly polynomial. The constraint matrix of $\mathbf{LW}_r(t)$ is fixed by $r$ and $t$ alone, so the bound concerns the combinatorial dimension, not the bit length. The only property of the method used is that its trajectory stays in $\mathcal N^{-\infty}_{\theta,t}$ . The lower bound therefore applies to every method with that property, whatever rule chooses its steps.

The result is proved in the paper; no machine-checked proof of it or of its tropical ingredients is known. A formalization would check the explicit threshold (36), which the paper derives in a few lines from bounds on Puiseux polyhedra. It would also produce reusable statements about tropical segments, the Funk and Hilbert metrics on $\mathbb T^d$ , and determinants of monomial matrices.

Difficulty

Following the central path is not hard in principle: the obvious argument tracks the duality measure, which decreases by a constant factor per iteration in a neighborhood of the path. That argument gives only upper bounds. The lower bound requires showing that the neighborhood itself, for large $t$ , is too thin to be crossed in a few straight steps, uniformly over every possible trajectory. The paper does this by passing to the limit $t\to\infty$ on logarithmic scale. The image of $\mathcal N^{-\infty}_{\theta,t}$ under $\log_t$ collapses onto a piecewise-linear tropical central path, and a segment of $\mathbb R^{2N}$ becomes, up to $\log_t2$ , a tropical segment. The tropical central path of $\mathbf{LW}_r$ then has to be shown to need $2^{r-1}$ tropical segments. The limit argument has to be made quantitative at a finite, explicit $t$ . That is where the Puiseux-series machinery (Theorems 12, 15 and 19 of the paper) and the explicit constant enter.

Formalization scope

Everything is stated over $\mathbb R$ and $\mathbb T$ ; the goal typechecks without the field of Puiseux series. A primal-dual point is an element of $\mathbb R^n\times\mathbb R^m\times\mathbb R^n\times\mathbb R^m$ . The dual equation is $s-A^\top y=c$ with Mathlib's transpose, $\bar\mu$ divides by $N=n+m$ (equal to $5r-1$ for $\mathbf{LW}^=_r$ ), and the wide neighborhood is one-sided. The instance matrix is generated from the paper's 1-based row and column numbers; Lean indices are 0-based. A polygonal curve is a map $z:\{0,\dots,p\}\to\mathbb R^{2N}$ with segment ℝ (z i) (z (i+1)) ⊆ N. The power $2^{r-1}$ in (36) is a natural-number power and the factorials are natural-number factorials. $\mathbb T$ is WithBot ℝ, and distances that can be infinite take values in EReal, with the convention $-\infty+(+\infty)=-\infty$ encoded explicitly.

Two statements are repaired or restated. Lemma 11 is printed for all $t>0$ , but its first inequality fails for $0<t<1$ (for $\mathbf M=\begin{pmatrix}t&1\\1&1\end{pmatrix}$ at $t=1/2$ ), so it is stated for $t>1$ . Lemma 8 makes explicit its implicit hypotheses $t>1$ and $u,v\ge0$ . Proposition 20 is stated in the form its proof establishes, as the greatest point of a tropical polyhedron. Its identification with the valuation of the Puiseux central path is not part of the item. Monomial matrices are given by sign and exponent matrices, and the valuation of the determinant is computed from the permutation expansion.

A trivializing formalization is ruled out: $\mathcal N^{-\infty}_{\theta,t}$ is not empty, since the build includes a sorry-free proof that it contains an explicit point for $r=1$ , $t=2$ , $\theta=1/2$ . A curve with $p=0$ cannot satisfy both duality-measure conditions, since $t^2>1$ .

The paper's Puiseux-series results are not posed: Theorems 12, 15, 19 and 29, Propositions 14, 16, 21 and 28, Corollary 17, and the count $\gamma([0,2])\ge2^{r-1}$ of §6.2. They need a faithful model of the field of absolutely convergent generalized Puiseux series and of the tropical central path. Contributions of that infrastructure, and of these statements as further milestones, are welcome. So are proofs of the five milestones, which need no Puiseux series. Proposition 1, Lemma 5 and Proposition 20 are elementary, and Lemma 8 and Lemma 11 are estimates with explicit constants.

Selected references

X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; arXiv:1708.01544v2. https://arxiv.org/abs/1708.01544
A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Adv. Mech. Math. 17, Springer, 2009, pp. 223–256. https://doi.org/10.1007/978-0-387-75714-8
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2), 1998, 7–15; reprinted in Mathematics: Frontiers and Perspectives, AMS, 2000. https://doi.org/10.1007/BF03025291
M. Develin, B. Sturmfels, Tropical convexity, Doc. Math. 9, 2004. https://arxiv.org/abs/math/0308254
S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453
X. Allamigeon, S. Gaubert, M. Skomra, Tropical spectrahedra, Discrete Comput. Geom. 63, 2020; arXiv:1610.06746. https://arxiv.org/abs/1610.06746

12 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On the Power and Limitations of Affine Policies in Two-Stage Adaptive Optimization V: The Optimal First Stage over a Dominating Simplex Is a 4√m-ApproximationResearch Paper

Motivation

Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision $x$ is fixed before an uncertain right-hand side $b$ is revealed, and a second-stage decision $y(b)$ is chosen afterwards, with the worst case over an uncertainty set $\mathcal U$ to be minimized. Problems of this form arise in capacity planning, network design and inventory control, where the first stage is an investment and the second stage a recourse. Computing the fully adaptable optimum is hard in general, so tractable restrictions are used in practice, most prominently affine policies $y(b)=Pb+q$ (Ben-Tal, Goryashko, Guslitzer, Nemirovski, Math. Program. 2004).

Bertsimas and Goyal (Math. Program. Ser. A, DOI 10.1007/s10107-011-0444-4) characterize how well affine policies perform. Their Section 5 shows a factor $O(\sqrt m)$ when the first-stage matrix satisfies $A\ge 0$ . Section 6, the subject of this mission, drops the sign condition on $A$ : it constructs, from $\mathcal U$ , a polytope $\mathcal U^0$ with at most $m+1$ vertices that dominates $\mathcal U$ , and shows that an optimal first stage for $\mathcal U^0$ is a $4\sqrt m$ -approximate first stage for the original problem.

Timeline. Ben-Tal et al. (2004) introduced affinely adjustable robust counterparts. Bertsimas, Iancu and Parrilo (Math. Oper. Res. 2010) proved optimality of affine policies for one-dimensional multistage problems. Bertsimas and Goyal (Math. Oper. Res. 2010) analysed static robust solutions for two-stage problems. The present paper (received 2009, published 2011) gives the $\Theta(m^{1/2})$ picture for affine policies and the general-case first-stage approximation formalized here.

Setting

Fix matrices $A\in\mathbb R^{m\times n_1}$ , $B\in\mathbb R^{m\times n_2}$ and cost vectors $c\in\mathbb R^{n_1}_+$ , $d\in\mathbb R^{n_2}_+$ . The uncertainty set $\mathcal U\subseteq\mathbb R^m_+$ is convex, compact and full-dimensional. A feasible solution of $\Pi_{Adapt}(\mathcal U)$ is a pair $(x,y)$ with $x\ge0$ and, for every $b\in\mathcal U$ , $y(b)\ge0$ and $Ax+By(b)\ge b$ , componentwise. Its worst-case cost is $\sup_{b\in\mathcal U}\, c^Tx+d^Ty(b)$ , and the fully adaptable optimum is

z_{Adapt}(\mathcal U)=\inf_{(x,y)\ \text{feasible}}\ \sup_{b\in\mathcal U}\ c^Tx+d^Ty(b).

An optimal solution attains this value.

For $j=1,\dots,m$ let $\mu_j=\max\{b_j: b\in\mathcal U\}$ and let $\beta^j\in\mathcal U$ be a maximizer, $\beta^j_j=\mu_j$ (display (38)). Algorithm $\mathcal A$ (Fig. 1 of the paper) starts with the index set $J_1=\{1,\dots,m\}$ ; while some $b\in\mathcal U$ has $\sum_{j\in J_1}b_j/\mu_j>\sqrt m$ , it picks a maximizer $u^k$ of that scaled sum over $\mathcal U$ , adds $u^k$ to a running total on the coordinates of $J_1$ , and removes from $J_1$ every coordinate whose total has reached $\mu_j$ . It stops after $K$ iterations and returns $\beta=u^1+\dots+u^K$ . The dominating set is

\mathcal U^0=\operatorname{conv}\{2\sqrt m\cdot\beta^1,\dots,2\sqrt m\cdot\beta^m,\ 2\beta\}.\tag{66}

Formalization targets

Goal: Theorem 6

For every run of Algorithm $\mathcal A$ , every choice of the maximizers $\beta^j$ , and every optimal solution $(\tilde x,\tilde y)$ of $\Pi_{Adapt}(\mathcal U^0)$ ,

\forall b\in\mathcal U\ \ \exists y\ge 0:\quad A\tilde x+By\ge b,\qquad c^T\tilde x+d^Ty\le 4\sqrt m\cdot z_{Adapt}(\mathcal U).

The page states the factor as $O(\sqrt m)$ ; $4\sqrt m$ is the constant its proof establishes.

Milestones

Lemma 12. $\mathcal U^0$ dominates $\mathcal U$ : every $b\in\mathcal U$ has some $b'\in\mathcal U^0$ with $b\le b'$ .
Lemma 13 (inequality). $\Pi_{Adapt}(\mathcal U^0)$ is feasible with finite worst-case cost, and

z_{Adapt}(\mathcal U^0)\le 4\sqrt m\cdot z_{Adapt}(\mathcal U).

The domination claim in the proof of Theorem 6. If $V$ dominates $W$ and $(\tilde x,\tilde y)$ is optimal for $\Pi_{Adapt}(V)$ with finite worst-case cost, then every $b\in W$ can be served from $\tilde x$ at cost at most $z_{Adapt}(V)$ .

Significance

The result gives a first-stage decision with a guarantee of order $\sqrt m$ for two-stage problems with an arbitrary first-stage matrix, a setting where the affine-policy analysis of Section 5 does not apply. The decision is obtained from a problem whose uncertainty set has at most $m+1$ extreme points, so it reduces an adaptive problem over a general convex set to one over a polytope with few vertices. Together with the paper's lower bounds (Theorems 2 and 3, $\Omega(m^{1/2-\delta})$ for affine policies), it places the general-case approximability of the first stage at the same order as the affine-policy gap.

The result is proved in the paper. It has no machine-checked proof that we know of. The formalization produces, beyond the theorem itself, an encoding of model (1) with values that are honest infima, a relational encoding of Algorithm $\mathcal A$ usable for its termination and output properties, and a reusable domination lemma for two-stage problems. Mission IV of this series (the case $A\ge0$ ) formalizes Lemmas 9 and 10 on Algorithm $\mathcal A$ , which the proofs here use.

Difficulty

The obvious argument replaces $\mathcal U$ by a simple set that contains or dominates it, such as the box $\prod_j[0,\mu_j]$ , and solves over that set. This loses a factor $m$ , not $\sqrt m$ : for $\mathcal U=\operatorname{conv}\{0,e_1,\dots,e_m\}$ with $A=0$ , $B=I$ , $c=0$ , $d=e$ , the optimum over $\mathcal U$ is $1$ while the optimum over the box is $m$ . A dominating set with few vertices whose cost is only $O(\sqrt m)$ times the original optimum has to be built from $\mathcal U$ itself, and controlling the cost of its vertex $2\beta$ depends on the number $K$ of iterations of Algorithm $\mathcal A$ , which is bounded only through the potential argument of Lemma 10 in the paper.

A second difficulty is that $z_{Adapt}$ is an infimum, not an attained minimum, over second-stage rules that are arbitrary functions; the cost comparison must work from near-optimal solutions of $\Pi_{Adapt}(\mathcal U)$ .

Formalization scope

Vectors are functions on Fin m, matrices are Matrix (Fin m) (Fin n) ℝ, and inequalities between vectors are componentwise. The paper's coordinate $j$ is Fin index $j-1$ . $z_{Adapt}(\mathcal U)$ is the infimum of the set of bounds $t$ such that some feasible $(x,y)$ satisfies $c^Tx+d^Ty(b)\le t$ for all $b\in\mathcal U$ ; this avoids a real supremum of a possibly unbounded worst case. An optimal solution is a feasible one that achieves every achievable bound. $\mu$ and the maximizers $\beta^j$ enter the theorems as data with their defining properties. Algorithm $\mathcal A$ is a relation on a choice sequence $u^1,u^2,\dots$ : the theorems hold for every run and every choice of maximizers, never for "some simplex dominating $\mathcal U$ ".

Standing assumptions of (1) carried by the goal and Lemma 13: $c\ge0$ , $d\ge0$ , $\mathcal U\subseteq\mathbb R^m_+$ convex, compact and with nonempty interior, and (1) feasible. There is no sign condition on $A$ . Lemma 12 keeps only nonnegativity and full-dimensionality of $\mathcal U$ ; the domination claim is stated for arbitrary scenario sets $V$ and $W$ with $V$ dominating $W$ and assumes that the optimal solution over $V$ has a finite worst-case cost.

The printed Lemma 13 also asserts $z_{Aff}(\mathcal U^0)=z_{Adapt}(\mathcal U^0)$ on the grounds that $\mathcal U^0$ is a simplex. Its $m+1$ generators need not be affinely independent, so this equality is not part of the mission; Theorem 6 does not use it.

A bound on $z_{Adapt}(\mathcal U^0)$ alone is not the goal: the goal requires, for each scenario of the original set $\mathcal U$ , a feasible second stage completing the fixed first stage $\tilde x$ at the stated cost. Lemma 13 also asserts feasibility over $\mathcal U^0$ with a finite bound, so its inequality cannot hold through the value of an infimum over an empty set.

A complete development needs elementary facts about convex hulls of finitely many points (representation by convex weights), the properties of Algorithm $\mathcal A$ (its output bound and termination, Lemmas 9 and 10 of the paper), and $\varepsilon$ -approximation arguments for infima. The encoding of model (1) and of Algorithm $\mathcal A$ is shared with the other missions of this series. Contributions of these supporting lemmas are welcome.

Selected references

D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Math. Program. Ser. A, 2011. https://doi.org/10.1007/s10107-011-0444-4
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99, 2004. https://doi.org/10.1007/s10107-003-0454-y
D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Math. Oper. Res. 35, 2010. https://doi.org/10.1287/moor.1100.0444
D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Math. Oper. Res. 35, 2010. https://doi.org/10.1287/moor.1090.0440

7 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On the Power and Limitations of Affine Policies in Two-Stage Adaptive Optimization III: The Best Affine Policy Can Cost More Than m^(1/2−δ)/4 Times the Fully Adaptable OptimumResearch Paper

Motivation

Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision $x$ is fixed before an uncertain right-hand side $b$ is revealed, and a second-stage recourse $y(b)$ is chosen afterwards, with the worst case over an uncertainty set $\mathcal U$ to be minimized. The fully-adaptable problem, in which $y$ may be an arbitrary function of $b$ , is intractable in general. The standard tractable restriction, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), requires $y$ to be an affine policy $y(b)=Pb+q$ ; it turns the problem into a single convex program and is used throughout robust inventory, network design and energy planning.

How much is lost by this restriction? Bertsimas and Goyal (Math. Program. 2012) answer the question for problems with a nonnegative constraint matrix. On one side, affine policies are optimal when $\mathcal U$ is a simplex, and are within a factor $O(\sqrt m)$ of the optimum on every instance of the class, where $m$ is the number of constraints. On the other side, the bound is nearly tight: Section 4 of the paper constructs an instance on which the best affine policy costs $\Omega(m^{1/2-\delta})$ times the fully-adaptable optimum, for any $\delta>0$ . This mission formalizes that lower bound.

Timeline: Ben-Tal et al. (2004) propose affinely adjustable robust counterparts; Bertsimas, Iancu and Parrilo (2010) prove optimality of affine policies for one-dimensional multistage problems; Bertsimas and Goyal (2012) give the $O(\sqrt m)$ upper bound and the matching lower-bound example formalized here.

Setting

The two-stage problem $\Pi_{\mathrm{Adapt}}(\mathcal U)$ has data $A\in\mathbb R^{m\times n_1}$ , $B\in\mathbb R^{m\times n_2}$ , $c\in\mathbb R^{n_1}_+$ , $d\in\mathbb R^{n_2}_+$ and $\mathcal U\subseteq\mathbb R^m_+$ :

z_{\mathrm{Adapt}}(\mathcal U)=\min_{x,\,y(\cdot)}\ c^\top x+\max_{b\in\mathcal U}d^\top y(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ x\ge0,\ y(b)\ge0\ \ \forall b\in\mathcal U .

The value $z_{\mathrm{Aff}}(\mathcal U)$ is the same minimum over policies of the form $y(b)=Pb+q$ ; such a policy must be nonnegative on all of $\mathcal U$ .

The large-gap instance $\mathcal I$ of display (19) has $n_1=n_2=m$ , a parameter $\delta>0$ with $m^\delta>200$ (condition (18)), and

\theta_0=\frac{1}{m^{(1-\delta)/2}},\qquad r=\lceil m^{1-\delta}\rceil,

c=0,\quad d=e=(1,\dots,1)^\top,\quad A=0,\quad B_{ij}=\begin{cases}1,&i=j,\\ \theta_0,&i\ne j,\end{cases}

\mathcal U=\operatorname{conv}\Bigl(\{0,\ e_1,\dots,e_m,\ \tfrac{1}{\sqrt m}e\}\cup\{\theta_0\mathbf 1_S:\ |S|=r\}\Bigr),

where $e_j$ are the unit vectors and $\mathbf 1_S$ is the indicator vector of a set $S$ of coordinates. A permutation $\sigma$ of the coordinates acts on vectors by $b^\sigma=(b_{\sigma(1)},\dots,b_{\sigma(m)})$ and on matrices by $P^\sigma_{ij}=P_{\sigma(i),\sigma(j)}$ .

Formalization targets

Goal: Theorem 3, explicit form

z_{\mathrm{Aff}}(\mathcal U)>\frac{m^{1/2-\delta}}{4}\cdot z_{\mathrm{Adapt}}(\mathcal U)\qquad\text{for all }\delta>0\text{ and }m\text{ with }m^\delta>200 .

The paper writes $z_{\mathrm{Aff}}(\mathcal U)=\Omega(m^{1/2-\delta})\cdot z_{\mathrm{Adapt}}(\mathcal U)$ ; the constant $1/4$ is the one the proof establishes, so the explicit statement is the stronger one.

Milestones

Lemma 4: $z_{\mathrm{Adapt}}(\mathcal U)\le1$ , with a feasible solution attaining cost at most $1$ .
Lemma 5: $\mathcal U$ is permutation-invariant under every $\sigma\in S^m$ .
Lemma 6: the permuted instance $\mathcal I(\sigma)$ of (22) equals $\mathcal I$ .
Lemma 7: if $y(b)=Pb+q$ is an optimal affine solution, so is $y^\sigma(b)=P^\sigma b+q^\sigma$ .
Lemma 8: some optimal affine solution has $\hat P_{ij}=\mu$ ( $i\ne j$ ), $\hat P_{jj}=\theta$ , $\hat q_j=\lambda$ .
The three Claims of the proof of Theorem 3: for a symmetric feasible affine policy with worst-case cost at most $m^{1/2-\delta}/4$ , one has $0\le\lambda\le m^{-1/2-\delta}$ , $\theta\ge1/3$ , and $-m^{-1-\delta/2}\le\mu<0$ .

Significance

The result shows that the $O(\sqrt m)$ approximation guarantee for affine policies on problems with $A\ge0$ (Theorem 4 of the same paper) cannot be improved beyond a factor $m^{\delta}$ , so the uncertainty set that looks like a portion of the unit sphere in the nonnegative orthant is essentially the worst case for affine recourse. It also explains why later work moved to piecewise-affine and finitely adaptable policies to close the gap. The example satisfies $c,d\ge0$ , $A,B\ge0$ and $\mathcal U\subseteq\mathbb R^m_+$ , so the lower bound applies to every larger problem class.

The theorem is proved in the paper; to our knowledge no machine-checked version exists. A formalization adds checked statements of the symmetrization argument (an optimal affine policy may be taken invariant under the symmetry group of the instance), which applies to any symmetric robust linear program, and a checked derivation of the explicit constant.

Difficulty

The upper bound $z_{\mathrm{Adapt}}\le1$ is a direct construction. The difficulty lies in the lower bound on $z_{\mathrm{Aff}}$ , which must hold for every affine policy, a family with $m^2+m$ free parameters. Bounding the cost of a policy at a few chosen points of $\mathcal U$ does not suffice without first reducing the parameters, and the reduction requires that an optimal affine solution exists (attainment of the minimum over an unbounded parameter set) and that averaging over the symmetric group preserves both feasibility and optimality. The remaining argument balances three different generators of $\mathcal U$ against each other, and the exponents of $m$ must be tracked exactly through ceilings and real powers.

Formalization scope

Vectors are Fin m → ℝ with the componentwise order and 0-based indices; matrices are Matrix (Fin m) (Fin m) ℝ. The values $z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$ are infima of the sets of worst-case cost bounds achieved by feasible solutions (epigraph form), so they do not rely on a supremum of a possibly unbounded function. Affine policies must be nonnegative on $\mathcal U$ . Optimal solutions are defined as feasible solutions whose worst-case cost is bounded by every achievable bound, so Lemma 8 asserts attainment. Powers $m^{a}$ are real powers; $\theta_0=1/m^{(1-\delta)/2}$ and $r=\lceil m^{1-\delta}\rceil$ exactly as on the page. $\mathcal U$ is the convex hull of its listed generators; the generator count $N$ printed in (19) plays no role.

The parameter $\delta$ is not restricted beyond $\delta>0$ and $m^\delta>200$ , as in the paper. Lemma 4's proof on the page uses $\delta\le1$ ; the statement is kept for all $\delta>0$ , where it remains true with a different witness. The Claims are stated for any symmetric feasible affine policy with cost at most $m^{1/2-\delta}/4$ ; their hypotheses are jointly unsatisfiable by Theorem 3, which is inherent in steps of a proof by contradiction.

A trivializing formalization is excluded: the goal mentions only the instance data and the two optimal values, not the symmetric parameters $\mu,\theta,\lambda$ , and the nonemptiness of the feasible sets is established by Lemma 4 and by the existence of a feasible affine policy, so neither value is a junk infimum of an empty set.

A complete development needs: convex hulls of finite point sets in $\mathbb R^m$ and their extreme points; the action of $S^m$ by coordinate permutation; averaging over the finite group $S^m$ ; and existence of minimizers for linear programs over a polytope. The symmetrization lemmas (5–8) are reusable for other symmetric robust problems. Proofs of any milestone, including partial infrastructure for linear-programming attainment, are welcome.

Selected references

D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming Ser. A 134 (2012) 491–531. https://doi.org/10.1007/s10107-011-0444-4
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Mathematics of Operations Research 35 (2010) 363–394. https://doi.org/10.1287/moor.1100.0444

12 thms2 active usersReviewed

Completed

Convex Optimization Operations Research·Captain: mikedeng1

Constructing Uncertainty Sets for Robust Linear Optimization 3: The Largest Centrally Symmetric Distortion Inner Approximation of a Polytope Solves a Linear ProgramResearch Paper

Motivation

A robust linear constraint $a'x \ge b$ for all $a \in \mathcal U$ protects a decision $x$ against every realization of the data $a$ in an uncertainty set $\mathcal U$ . Robust optimization took this form in the work of Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Oper. Res. Lett. 1999), where $\mathcal U$ is chosen by the modeller. Bertsimas and Brown (Oper. Res. 2009) tie the choice of $\mathcal U$ to the decision maker's attitude towards risk: on a finite sample $\mathcal A = \{a_1,\dots,a_N\}$ , a coherent risk measure constraint $\mu(\tilde a'x - b) \le 0$ is equivalent to a robust constraint over a convex set built from $\mathcal A$ , and for the distortion risk measures (the law-invariant, comonotone coherent measures, which include CVaR) that set is a polytope of a special kind, a permutohull.

An uncertainty set in practice is often an arbitrary polyhedron, given by the modeller or by previous analysis. Section 4.5 of the paper asks which distortion risk measure best approximates such a polyhedron from inside: the largest permutohull of a given shape contained in it. A positive answer quantifies how conservative a given polyhedral uncertainty set is relative to a distortion risk measure, and gives the risk measure that is closest to it. This mission is the third of a series of three on the paper; the first establishes the permutohull representation of distortion risk constraints, the second the generators of the centrally symmetric distortion measures.

Setting

Fix $N \ge 1$ and data $a_1,\dots,a_N \in \mathbb R^n$ , the columns of a matrix $A$ . Let $e_N \in \mathbb R^N$ have $1/N$ at each entry, so the sample mean is $\hat a = Ae_N$ .

The restricted simplex $\hat\Delta^N$ is the set of probability vectors $q \in \mathbb R^N$ with $q_1 \ge \dots \ge q_N$ . Under the uniform probability on $N$ points, the distortion risk measures are exactly the maps $\mu_q(X) = -\sum_i q_i x_{(i)}$ , $q \in \hat\Delta^N$ , with $x_{(1)} \le \dots \le x_{(N)}$ the ordered values of $X$ (Theorem 4.2 of the paper).
For $q \in \mathbb R^N$ , the $q$ -permutohull is $\Pi_q(\mathcal A) = \operatorname{conv}\{\sum_i q_{\sigma(i)} a_i : \sigma \in S_N\}$ . The robust constraint over $\Pi_q(\mathcal A)$ is the risk constraint for $\mu_q$ .
The symmetric restricted simplex $\hat\Delta^N_{\mathrm{sym}}$ is the set of $q \in \hat\Delta^N$ with $q = 2e_N - q_\sigma$ for some permutation $\sigma$ , where $(q_\sigma)_i = q_{\sigma(i)}$ . For these $q$ the permutohull is centrally symmetric about $\hat a$ .
With $\tilde\pi_q(\mathcal A) = \Pi_q(\mathcal A) - \hat a$ , the Minkowski functional

\|w\|_{q,\mathcal A} = \inf\{\alpha > 0 : w/\alpha \in \tilde\pi_q(\mathcal A)\}

measures $w = a - \hat a$ against the shifted permutohull (12).

The polyhedron is $\mathcal U = \{a \in \mathbb R^n : u_k'a \ge v_k,\ k = 1,\dots,m\}$ (14), with $\hat a \in \mathcal U$ .

The family of candidate inner approximations is obtained by mixing a fixed $\hat q \in \hat\Delta^N_{\mathrm{sym}}$ with the uniform generator: $q = \lambda\hat q + (1-\lambda)e_N$ , $\lambda \in \mathbb R$ .

Formalization targets

Goal: Theorem 4.5

Let $\lambda^*$ be the optimal value of the linear program

\max\ \lambda\quad\text{s.t.}\quad q = \lambda\hat q + (1-\lambda)e/N,\quad e'(s_k + t_k) \ge v_k\ \forall k,\quad s_{k,i} + t_{k,j} \le (u_k'a_j)\,q_i\ \forall i,j,k, \tag{15}

in $s_k, t_k, q \in \mathbb R^N$ and $\lambda \in \mathbb R$ , and $q^* = \lambda^*\hat q + (1-\lambda^*)e_N$ . Then

\Pi_{q^*}(\mathcal A) \subseteq \mathcal U,\qquad \Pi_{\lambda\hat q + (1-\lambda)e_N}(\mathcal A) \subseteq \mathcal U \implies \Pi_{\lambda\hat q + (1-\lambda)e_N}(\mathcal A) \subseteq \Pi_{q^*}(\mathcal A),

and, when $\hat q \ne e_N$ , $q^* \in \hat\Delta^N$ if and only if

\lambda^* \le \frac{1}{1 - N\hat q_{\min}}. \tag{16}

Milestones

Proposition 4.2: for $q \in \hat\Delta^N_{\mathrm{sym}}$ with $\Pi_q(\mathcal A)$ of nonempty interior, $\|\cdot\|_{q,\mathcal A}$ is a norm.
Scaling (proof of Lemma 4.2): $\Pi_{\lambda q + (1-\lambda)e_N}(\mathcal A) = \hat a + \lambda\,\tilde\pi_q(\mathcal A)$ for every $q \in \mathbb R^N$ , $\lambda \in \mathbb R$ .
Lemma 4.2: $\|a - \hat a\|_{\lambda q + (1-\lambda)e_N,\mathcal A} = \frac{1}{|\lambda|}\|a - \hat a\|_{q,\mathcal A}$ for $q \in \hat\Delta^N_{\mathrm{sym}}$ , $\lambda \ne 0$ .
Containment as linear constraints (proof of Theorem 4.5): $\Pi_q(\mathcal A) \subseteq \mathcal U$ iff vectors $s_k, t_k$ satisfying the constraints of (15) exist, for every $q \in \mathbb R^N$ .
Nonnegativity (proof of Theorem 4.5): for $\lambda \ge 0$ and $N\hat q_{\min} < 1$ , $\lambda\hat q + (1-\lambda)e_N \in \hat\Delta^N$ iff $\lambda \le 1/(1 - N\hat q_{\min})$ .

Significance

The theorem reduces a geometric question — the largest member of a one-parameter family of centrally symmetric polytopes, each with $N!$ potential vertices, that fits inside an arbitrary polyhedron — to a linear program with $O(mN)$ variables and $O(mN^2)$ constraints. Its solution identifies a distortion risk measure $\mu = \lambda^*\mu_{\hat q} + (1-\lambda^*)\mathbb E[-X]$ , which the paper reads as a mean–deviation measure in the style of a Sharpe ratio, and the bound (16) decides whether the optimal set is itself a distortion set or must be shrunk further.

The results are proved in the paper, with short proofs that pass over several points: the scaling identity is asserted, the duality step leaves the assignment-problem structure implicit, and the norm claim requires a nondegeneracy condition that the page does not state. No machine-checked proof of any of them is known. A formalization fixes the exact hypotheses (nonempty interior for the norm, $\lambda \ne 0$ in (13), $\hat q \ne e_N$ in (16)), and the containment equivalence for arbitrary real weight vectors $q$ is a reusable fact about permutohulls and assignment duality.

Difficulty

The goal combines three ingredients of different nature. The containment equivalence needs that minimizing a linear function over the permutohull is a linear program over the Birkhoff polytope of doubly stochastic matrices, followed by linear programming duality for that program; neither the Birkhoff–von Neumann theorem nor assignment duality is a one-line consequence of what is in Mathlib. The scaling identity is a statement about convex hulls under an affine map and holds for all real $\lambda$ , including the reflected case $\lambda < 0$ ; the maximality claim then needs the central symmetry of $\Pi_{\hat q}(\mathcal A)$ about $\hat a$ , which is a property of $\hat\Delta^N_{\mathrm{sym}}$ (Proposition 4.1 of the paper) and not of a general $q$ . The tempting shortcut — comparing gauges directly — fails at $\lambda = 0$ , where the permutohull is the single point $\hat a$ and the gauge is degenerate.

Formalization scope

Vectors in $\mathbb R^N$ and $\mathbb R^n$ are Fin N → ℝ and Fin n → ℝ, with $0$ -based indices; $a_i$ is a i, $u_k'a$ is a dot product. $\hat\Delta^N$ uses Mathlib's stdSimplex and Antitone. The permutohull is convexHull of the range over Equiv.Perm (Fin N), defined for every real $q$ because (15) evaluates it at mixtures with possibly negative entries. The Minkowski functional is Mathlib's gauge, which takes the value $0$ (not $+\infty$ ) on points no positive multiple of the set reaches; this is why Proposition 4.2 assumes $\Pi_q(\mathcal A)$ has nonempty interior and why the goal states "largest" as set containment. $\hat q_{\min}$ is $\min_i \hat q_i$ . The optimal value $\lambda^*$ is a hypothesis (it is the greatest element of the feasible set of (15)), not a supremum defined by sSup.

Standing assumptions and disclosed additions: $N \ge 1$ ; the polyhedron (14) is not assumed bounded (a generalization); in (13) the right-hand norm is that of $q$ , not $\tilde q$ as printed, and $\lambda \ne 0$ ; in (16), $N\hat q_{\min} < 1$ ; "corresponds to a distortion risk measure" is read, as the proof reads it, as $q^* \in \hat\Delta^N$ . A formalization that assumes $\Pi_{q^*}(\mathcal A) \subseteq \mathcal U$ or the maximality of $\lambda^*$ trivializes the theorem: both are conclusions, and the linear program enters only through its constraints and its optimal value.

A complete development needs: convex hulls under affine maps; the Birkhoff–von Neumann theorem (doubly stochastic matrices are convex combinations of permutation matrices); duality for the assignment linear program; gauge calculus for centrally symmetric convex bodies. The containment equivalence and the scaling identity are reusable beyond this mission. Proofs of any milestone, and of the Birkhoff and assignment-duality infrastructure, are welcome.

Selected references

D. Bertsimas and D. B. Brown, Constructing uncertainty sets for robust linear optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0646
A. Ben-Tal and A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal and A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068

7 thms2 active usersReviewed

Completed

Convex Optimization Operations Research·Captain: mikedeng1

Robust Solutions of Uncertain Linear Programs II: With Ellipsoidal Uncertainty the Robust Counterpart Is Equivalent to a Conic Quadratic ProgramResearch Paper

Motivation

The data of a linear program are often not known exactly: they are measured or estimated, or they are forecasts. The robust counterpart approach, going back to Soyster (1973), asks for a solution that is feasible for every data matrix in a prescribed uncertainty set and is best among such solutions. Ben-Tal and Nemirovski's 1999 paper [1] showed that the method stays computationally tractable for a broad class of uncertainty sets, the ellipsoidal uncertainties: the robust counterpart of an uncertain LP is then a conic quadratic program (CQP), solvable by interior point methods at roughly the cost of an LP of similar size. This result is the basis of robust linear optimization as it is used today [2], [3]. It is also the reason ellipsoidal sets are the default choice in robust portfolio selection (§4 of the paper) and in many later robust models.

Timeline. Soyster (1973) treated column-wise box uncertainty, for which the counterpart is again an LP [4]. Ben-Tal and Nemirovski (1998) developed the general theory of robust convex optimization [5]. The present paper (1999) proved the ellipsoidal-to-CQP reduction for LPs (Theorem 3.1). Its proof relies on the conic duality theory of Nesterov and Nemirovski (1994) [6].

Setting

An uncertain linear program in the homogeneous form (6) is

\min\{c^Tx \mid Ax \ge 0,\ f^Tx = 1\},

where $c, f \in \mathbb R^n$ are fixed and the matrix $A \in \mathbb R^{m\times n}$ lies in an uncertainty set $\mathcal U$ . A point $x$ is robust feasible if $f^Tx = 1$ and $Ax \ge 0$ for every $A \in \mathcal U$ . The robust counterpart $(P_{\mathcal U})$ minimizes $c^Tx$ over the robust feasible set

G_{\mathcal U} = \{x \mid Ax \ge 0\ \forall A \in \mathcal U,\ f^Tx = 1\}.

An ellipsoid in $\mathbb R^{m\times n}$ (display (14)) is a set

U(\Pi, Q) = \{\Pi(u) \mid \|Qu\| \le 1\},

where $\Pi(u) = P^0 + \sum_{j=1}^L u_jP^j$ is affine in $u \in \mathbb R^L$ , $Q$ is an $M\times L$ matrix, and $\|\cdot\|$ is the Euclidean norm. A singular $Q$ gives an ellipsoidal cylinder, which may be unbounded. An ellipsoidal uncertainty is a set

\mathcal U = \bigcap_{\ell=0}^k U(\Pi_\ell, Q_\ell)

(condition A) that is bounded (condition B) and contains a matrix $A$ with $A = \Pi_\ell(u^\ell)$ and $\|Q_\ell u^\ell\| < 1$ for every $\ell$ (condition C, a Slater condition).

Formalization targets

Goal: Theorem 3.1

For every $x \in \mathbb R^n$ ,

x \in G_{\mathcal U} \iff f^Tx = 1 \ \text{ and }\ \forall i \le m\ \ \exists\, \lambda^{(i)}, \mu^{(i)}, \nu^{(i)} :\ (x, \lambda^{(i)}, \mu^{(i)}, \nu^{(i)}) \text{ satisfies } (\mathcal C_i).

Here $(\mathcal C_i)$ is an explicit system: linear equations and one linear inequality in $(x, \lambda, \mu, \nu)$ , together with the second-order cone constraints $\|\mu^{(i)}_\ell\| \le \nu^{(i)}_\ell$ . Its coefficients are the matrices $P^j_\ell$ and $Q_\ell$ . The robust feasible set is therefore the projection of the feasible set of the conic quadratic program (CQP), which minimizes $c^Tx$ subject to $(\mathcal C_1), \dots, (\mathcal C_m)$ and $f^Tx = 1$ .

Milestones, in the order of the Appendix's proof

$\mathcal U$ equals the image of the feasible set of the problem $(P_i[x])$ under $u \mapsto \Pi_0(u^0)$ (p. 15).
Claim (I): with $f^Tx = 1$ , $x$ is robust feasible iff every $(P_i[x])$ has nonnegative optimal value (p. 15).
Claim (II): conic quadratic duality. A strictly feasible primal that is bounded below has a solvable dual with equal optimal value (p. 15).
Conditions B and C make every $(P_i[x])$ strictly feasible and bounded below (p. 16).

Companion results

The CQP forms (16) and (17) of the simplest cases (a single ellipsoid; constraint-wise ellipsoids), Remark 3.1 (bounded polytopes are ellipsoidal uncertainties), and the robust portfolio counterpart (22).

Significance

The result. Theorem 3.1 turns a semi-infinite constraint system (one constraint for every $A \in \mathcal U$ ) into finitely many conic quadratic constraints whose size is polynomial in the data. Robust LPs with ellipsoidal uncertainty, which by Remark 3.1 include polytopic uncertainty, can therefore be solved by standard conic solvers. Later robust optimization results, such as budgeted uncertainty, affinely adjustable policies and distributionally robust LPs, refine this pattern.

Formalizing it. The theorem is classical and its proof is complete, but no machine-checked proof exists. A formal proof needs a conic quadratic strong duality theorem with dual attainment (claim (II)), which Mathlib does not have in this form. That duality theorem can be reused well beyond this mission. The companion results (16), (17) and (22) are self-contained computations of a minimum of a linear function over a Euclidean ball.

Difficulty

The "if" direction is weak duality: a solution of $(\mathcal C_i)$ certifies that the $i$ -th constraint holds for all of $\mathcal U$ . The content is the "only if" direction. It requires dual attainment, not merely equality of optimal values, because a solution of $(\mathcal C_i)$ must exist. Dual attainment fails without a constraint qualification. Condition C must hold strictly for every ellipsoid, including $\ell = 0$ , and the ellipsoids may be cylinders, so the variables $u^\ell$ can range over unbounded sets even though $\mathcal U$ is bounded. Projecting the problem onto a single parameter space is not available in general, because the maps $\Pi_\ell$ need not be injective.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. The indices $\ell = 0, \dots, k$ are Fin (k + 1), and the $k$ equality multipliers $\lambda_\ell$ , $\ell \ge 1$ , are indexed by Fin k. Every norm is Euclidean, written out as euclidNorm v = √(∑ v_j²), because Mathlib's norm on Fin M → ℝ is the sup norm, under which ellipsoids would become boxes. Condition B is a uniform bound on all matrix entries, and condition C is required for every $\ell = 0, \dots, k$ . The page's words say " $\ell = 1, \dots, k$ ", but its display and the proof use every $\ell$ . Injectivity of $\Pi_\ell$ is not assumed, and neither is §2.1's standing assumption that $\mathcal U$ is convex and closed. An ellipsoidal uncertainty is convex automatically, and closedness is not used, so both omissions generalize the statement. Three printed slips are corrected and disclosed: the sum in the equality constraint of (CQP $_d$ ) runs over $\ell = 0, \dots, k$ ; $(\mathcal C_i)$ has $\varphi^{(i)}[x]$ where the page prints $f^{(i)}[x]$ ; and Remark 3.1 has the factor $2/(r_i - s_i)$ where the page prints $(r_i - s_i)/2$ .

The goal is not the contentless statement "some conic quadratic program has $G_{\mathcal U}$ as a projection", which holds for every closed convex set. It names the system $(\mathcal C_i)$ built from the data $P^j_\ell$ , $Q_\ell$ . The goal also does not mention optimal values, (CQP $_p$ ) or strict feasibility; those are milestones.

Contributions are welcome on the conic duality theorem (II) as a standalone result, on the finite-dimensional facts that minimize a linear function over a Euclidean ball (used in (16), (17) and (22)), and on the goal itself.

Selected references

A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
D. Bertsimas, D. B. Brown, C. Caramanis, Theory and applications of robust optimization, SIAM Review 53(3):464–501, 2011. https://doi.org/10.1137/080734510
A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Operations Research 21(5):1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
Yu. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791

9 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Constructing Uncertainty Sets for Robust Linear Optimization 1: A Distortion Risk Constraint Equals a Robust Constraint over a Permutohull and an Explicit Linear SystemResearch Paper

Motivation

Robust linear optimization replaces an uncertain constraint $\tilde a'x \ge b$ by the requirement that $a'x \ge b$ hold for every $a$ in an uncertainty set $\mathcal U$ (Ben-Tal and Nemirovski 1999). The method leaves open where $\mathcal U$ should come from. Risk theory answers a related question from the other side: a decision maker's attitude to an uncertain reward is described by a risk measure $\mu$ , and the constraint is imposed as $\mu(\tilde a'x - b) \le 0$ .

Bertsimas and Brown (2009) connect the two. When $\mu$ is coherent and $\tilde a$ is supported on finitely many observed data points $a_1, \dots, a_N$ , the risk constraint is exactly a robust constraint whose uncertainty set is built from the data and the family of probability vectors generating $\mu$ . For the class of distortion risk measures, the uncertainty set has an explicit polyhedral form, the $q$ -permutohull of the data, and the robust constraint has a reformulation of polynomial size. This mission formalizes that chain of results, Sections 2–4.3 of the paper.

Setting

The sample space is finite, $\Omega = \{\omega_1, \dots, \omega_N\}$ , and a random variable is a vector $X \in \mathbb R^N$ , read as a reward; $X \ge Y$ means $X_i \ge Y_i$ for every $i$ . The probability simplex is $\Delta^N = \{p \in \mathbb R^N_+ : e'p = 1\}$ , and $\mathbb E_q[X] = \sum_i q_i X_i$ .

A risk measure is a function $\mu : \mathbb R^N \to \mathbb R$ with $X \ge Y \Rightarrow \mu(X) \le \mu(Y)$ and $\mu(X + c) = \mu(X) - c$ . It is coherent if it is moreover convex and positively homogeneous. A set $\mathcal Q \subseteq \Delta^N$ generates $\mu$ if $\mu(X) = \sup_{q \in \mathcal Q} \mathbb E_q[-X]$ for all $X$ . The conditional value-at-risk under a probability vector $p$ is $\mathrm{CVaR}_\alpha(X) = \inf_{\nu \in \mathbb R}\{\nu + \frac1\alpha \mathbb E_p[(-\nu - X)^+]\}$ for $\alpha \in (0,1]$ .

Two random variables are comonotone if $(X(\omega) - X(\omega'))(Y(\omega) - Y(\omega')) \ge 0$ for all $\omega, \omega'$ ; $\mu$ is comonotonic if it is additive on comonotone pairs, and law invariant if it takes equal values on random variables with the same distribution. A distortion risk measure is a coherent, comonotonic, law-invariant risk measure. From Section 4.2 on, $\Omega$ carries the uniform distribution $\mathbb P\{\omega_i\} = 1/N$ .

The restricted simplex is $\hat\Delta^N = \{q \in \Delta^N : q_1 \ge \cdots \ge q_N\}$ . For $q \in \hat\Delta^N$ put

\mu_q(X) = -\sum_{i=1}^N q_i x_{(i)},

where $x_{(1)} \le \cdots \le x_{(N)}$ are the increasing order statistics of $X$ . The data are $\mathcal A = \{a_1, \dots, a_N\} \subseteq \mathbb R^n$ , the uncertain vector $\tilde a$ takes the value $a_i$ at $\omega_i$ , and the $q$ -permutohull of $\mathcal A$ is

\Pi_q(\mathcal A) = \operatorname{conv}\Big\{\sum_{i=1}^N q_{\sigma(i)} a_i : \sigma \in S_N\Big\}.

Formalization targets

Goal: Theorem 4.3

Under the uniform distribution, for every distortion risk measure $\mu$ there is $q \in \hat\Delta^N$ with $\mu = \mu_q$ , and for this $q$ , all data and every $b$ ,

\{x : \mu(\tilde a'x - b) \le 0\} = \{x : a'x \ge b\ \forall a \in \Pi_q(\mathcal A)\} = \{x : \exists y_1, y_2 \in \mathbb R^N,\ e'y_1 + e'y_2 \ge b,\ y_{1,i} + y_{2,j} \le q_i\, a_j'x\ \forall i, j\}.

The vector $q$ depends on $\mu$ only; the data are quantified after it.

Milestones

Theorem 2.1. $\mu$ is coherent if and only if some family $\mathcal Q \subseteq \Delta^N$ generates it.
Theorem 3.1. For coherent $\mu$ generated by $\mathcal Q$ , $\{x : \mu(\tilde a'x - b) \le 0\} = \{x : a'x \ge b\ \forall a \in \operatorname{conv}\{Aq : q \in \mathcal Q\}\}$ ; conversely every nonempty $\mathcal U \subseteq \operatorname{conv}(\mathcal A)$ arises from the coherent measure generated by $\{q \in \Delta^N : Aq \in \mathcal U\}$ .
Generation of (4). $\mu_q$ is generated by the permuted vectors $q \circ \sigma$ , $\sigma \in S_N$ .
Theorem 4.1 (Schmeidler). A coherent $\mu$ is comonotonic if and only if $\mu(X) = \int (-X)\,dg$ (Choquet integral) for a monotone, normalized, submodular $g : 2^\Omega \to [0,1]$ .
Second differences (proof of Lemma 4.1). A submodular $g$ depending only on $|A|$ has nonincreasing increments along $\emptyset \subset \{\omega_1\} \subset \{\omega_1, \omega_2\} \subset \cdots$ .
Lemma 4.1. A risk measure is a distortion risk measure if and only if $\mu(X) = \int_{(0,1]} \mathrm{CVaR}_\alpha(X)\,\nu(d\alpha)$ for a probability measure $\nu$ .
The CVaR display (proof of Theorem 4.2). $\mathrm{CVaR}_\alpha(X) = \sup\{\mathbb E_q[-X] : q \in \Delta^N,\ q_i \le 1/(N\alpha)\} = \mu_{q^\alpha}(X)$ with $q^\alpha \in \hat\Delta^N$ .
Theorem 4.2. A risk measure is a distortion risk measure if and only if $\mu = \mu_q$ for some $q \in \hat\Delta^N$ ; every such $q$ is a convex combination of the generators $\hat q^j$ of $\mathrm{CVaR}_{j/N}$ .
Assignment duality (proof of Theorem 4.3). $a'x \ge b$ on $\Pi_q(\mathcal A)$ if and only if the linear system in $(y_1, y_2)$ above is feasible.

A companion item states Corollary 4.3: $\Pi_{\sum_j \lambda_j \hat q^j}(\mathcal A) = \operatorname{conv}\{\sum_j \lambda_j \frac1j \sum_{i \le j} a_{\sigma_j(i)} : \sigma_j \in S_N\}$ , and the class equality it yields: the uncertainty sets $\Pi_q(\mathcal A)$ of all distortion risk measures $\mu = \mu_q$ are exactly the polytopes $\mathcal U_\lambda(\mathcal A)$ , $\lambda \ge 0$ , $\sum_j \lambda_j = 1$ .

Significance

The goal theorem identifies the uncertainty set implied by any distortion risk measure: it is a permutohull of the data, a polytope with up to $N!$ vertices that is nevertheless representable with $2N$ extra variables and $N^2$ linear constraints. Combined with Theorem 4.2, the uncertainty sets of distortion measures are exactly the mixtures of the sets of $j$ -point averages of the data (Corollary 4.3), with $\mathrm{CVaR}_{j/N}$ as the generators. The later sections of the paper build on this: centrally symmetric permutohulls (Section 4.4) and the construction of a distortion risk measure from a given polyhedral uncertainty set (Section 4.5) are the subjects of the two companion missions.

The results are proved in the paper; no machine-checked version is known. The formalization adds checked statements of the finite-space representation theory of coherent and distortion risk measures, which the paper obtains partly by citing general results, and records the corrections the printed statements need.

Difficulty

The two equalities of the goal have unequal weight. The second is a statement about one polytope with up to $N!$ vertices and a linear system of size $O(N^2)$ ; it is finite-dimensional linear programming. The first requires the complete characterization of distortion risk measures on a finite uniform space, and that is where the obvious approach fails. The known representation of law-invariant comonotonic coherent measures as mixtures of CVaR (Kusuoka 2001) is proved for atomless spaces and does not transfer to a discrete $\Omega$ . The uniform distribution is essential, not a convenience: Remark 4.2 of the paper gives a two-point space with probabilities $1/3, 2/3$ and a monotone, normalized, submodular set function depending only on probability whose induced distortion is not concave, so the conclusion of Theorem 4.2 fails there.

Formalization scope

$\Omega$ is Fin N with $N \ge 1$ ; random variables are Fin N → ℝ; indices are 0-based throughout, so qhat j is the paper's $\hat q^{j+1}$ and $q_1 \ge \cdots \ge q_N$ is Antitone q. Order statistics are X ∘ Tuple.sort X.
Probability measures on $\Omega$ are probability vectors in stdSimplex ℝ (Fin N). Generation (1) is an IsLUB over an arbitrary set of probability vectors, not a maximum over a finite family (that version is false).
Sign of the risk constraint. Display (2) and Theorem 4.3 print $\mu(\tilde a'x - b) \ge 0$ . The paper introduces the constraint as $\mu(\tilde a'x - b) \le 0$ (p. 1486) and the proof of Theorem 3.1 computes $\mu(\tilde a'x - b) = -\inf_{a \in \mathcal U} a'x + b$ ; all statements use $\le 0$ .
Standing assumptions. Theorems 2.1 and 3.1 assume a probability vector $p$ with $p_i > 0$ (full support makes $\mathbb Q \ll \mathbb P$ vacuous; with a null atom Theorem 2.1 fails for functions on $\Omega$ ). From Lemma 4.1 on the distribution is uniform (Assumption 4.1). Theorem 3.1's converse adds $\mathcal U \neq \emptyset$ .
CVaR is a real infimum, used only for $\alpha \in (0,1]$ , where the objective is bounded below by $\mathbb E[-X]$ . In Lemma 4.1 the mixing measure $\nu$ is a probability measure on $(0,1]$ ; the page's $\int_0^1$ is read over $(0,1]$ . The CVaR display uses the corrected coefficient $(N\alpha - \lfloor N\alpha \rfloor)/(N\alpha)$ in place of the printed $/\lfloor N\alpha \rfloor$ . The assignment-duality milestone is stated for every $q \in \mathbb R^N$ .
The goal must assert the representation $\mu = \mu_q$ together with the set equalities: a statement "there is some $q$ for which the sets coincide" would let $q$ depend on the data and is not Theorem 4.3. The goal does not assume $\mu = \mu_q$ , which is Theorem 4.2's conclusion.
Needed infrastructure: Birkhoff's theorem (in Mathlib), LP duality, the rearrangement inequality, Choquet integrals of step functions. Lemmas about $\mu_q$ and order statistics are reusable beyond this mission; proofs of any milestone are welcome.

Selected references

D. Bertsimas, D. B. Brown, Constructing uncertainty sets for robust linear optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0646
A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
D. Schmeidler, Integral representation without additivity, Proceedings of the AMS 97(2):255–261, 1986. https://doi.org/10.1090/S0002-9939-1986-0835875-8
R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
S. Kusuoka, On law invariant coherent risk measures, Advances in Mathematical Economics 3:83–95, 2001. https://doi.org/10.1007/978-4-431-67891-5_4
H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 2nd ed., de Gruyter, 2004. https://doi.org/10.1515/9783110212075

11 thms2 active usersReviewed

Completed

Convex Optimization Operations Research·Captain: mikedeng1

Constructing Uncertainty Sets for Robust Linear Optimization 2: The Distortion Risk Measures with Centrally Symmetric Permutohulls Are the Mixtures of ⌊N/2⌋+1 GeneratorsResearch Paper

Motivation

A linear decision made with uncertain coefficients can be protected by requiring the constraint to hold for every coefficient vector in an uncertainty set. Choosing that set determines how conservative the decision is. Bertsimas and Brown connect this choice to a risk measure: a functional that assigns a cost to the random reward left by a decision. Their construction turns certain risk constraints into robust linear constraints over a convex hull of weighted samples. This mission isolates the structural question asked in §4.4 of their paper: which such risk measures always produce uncertainty sets that are centrally symmetric about the sample mean? The answer matters because this symmetric family is the class used in the paper's subsequent approximation of general polyhedral uncertainty sets. Bertsimas and Brown (2009), §§4.3–4.5.

Setting

There are $N\ge1$ observations, indexed by $i=1,\ldots,N$ , with equal reference probabilities. A probability weight vector $q=(q_1,\ldots,q_N)$ has nonnegative entries summing to one. The restricted simplex $\widehat\Delta^N$ contains those vectors whose entries are nonincreasing: $q_1\ge\cdots\ge q_N$ . For a reward vector $X=(x_1,\ldots,x_N)$ , write $x_{(1)}\le\cdots\le x_{(N)}$ for its increasing order statistics. The associated distortion risk measure is $\mu_q(X)=-\sum_iq_i x_{(i)}$ . A larger reward therefore reduces risk. Under the uniform distribution, the paper's Theorem 4.2 identifies these functionals, for $q\in\widehat\Delta^N$ , with its distortion risk measures. Bertsimas and Brown (2009), Theorem 4.2.

Take arbitrary sample vectors $a_1,\ldots,a_N\in\mathbb R^n$ . For a permutation $\sigma$ of their indices, form the weighted vector $\sum_iq_{\sigma(i)}a_i$ . The $q$ -permutohull $\Pi_q(\mathcal A)$ is the convex hull of all these vectors. Its center of interest is the sample mean $\widehat a=N^{-1}\sum_i a_i$ . A set $P$ is centrally symmetric through $x_0\in P$ when $x_0+x\in P$ implies $x_0-x\in P$ for every $x$ . The quantifier “for any data” ranges over every dimension $n$ and every choice of $N$ sample vectors. It is stronger than symmetry for one selected data set. Bertsimas and Brown (2009), Definitions 4.7–4.8.

Formalization targets

The first target is Proposition 4.1's characterization of weights giving universal symmetry. If $e_N$ is the vector with every entry $1/N$ , then

\bigl[\Pi_q(\mathcal A)\text{ is centrally symmetric through }\widehat a \text{ for every }n,\mathcal A\bigr] \quad\Longleftrightarrow\quad \exists\sigma\in S_N:\ q=2e_N-q_\sigma.

This condition defines the symmetric restricted simplex $\widehat\Delta^N_{\mathrm{sym}}$ inside $\widehat\Delta^N$ . Bertsimas and Brown (2009), Proposition 4.1 and Definition 4.9.

The main target is Theorem 4.4. Put $\widehat N=\lfloor N/2\rfloor+1$ . For $1\le j\le\widehat N$ , define a generator $\bar q^{\,j}$ by

\bar q_i^{\,j}= \begin{cases} 2/N,&i<j,\\ 1/N,&j\le i\le N-j+1,\\ 0,&\text{otherwise}. \end{cases}

A functional represented by a $q\in\widehat\Delta^N$ whose permutohull is symmetric for every data set is exactly a convex mixture of the $\widehat N$ generator functionals:

\mu(X)=\sum_{j=1}^{\widehat N}\lambda_j\mu_{\bar q^{\,j}}(X), \qquad \lambda_j\ge0,\qquad\sum_{j=1}^{\widehat N}\lambda_j=1.

The milestones also state the two set inclusions behind the equality of $\widehat\Delta^N_{\mathrm{sym}}$ with the convex hull of these generators, including the coordinate reversal identity. Bertsimas and Brown (2009), Theorem 4.4 and its proof.

Significance

The result gives a finite list of risk functionals from which every member of the universally symmetric distortion subclass can be formed. The number of generators is $\lfloor N/2\rfloor+1$ , rather than an unspecified family. It also connects a geometric property of a robust uncertainty set to a checkable condition on its weights. The paper uses this symmetric subclass to formulate the inner approximation problem in §4.5, where a symmetric permutohull is fitted inside another polytope. Bertsimas and Brown (2009), §§4.4–4.5.

The mathematical result is proved in the 2009 paper. This formalization task is to obtain Lean proofs of the classification and its source-stated intermediate claims. The definition layer is a reusable interface for finite distortion risk measures, permutohulls, and symmetry under coordinate permutations. Formal proofs here would provide a checked foundation for later robust optimization statements using the same finite sample model. The proposed goal and milestones are open Lean statements; compiling them verifies their syntax and types, not their proofs.

Difficulty

Symmetry of one pictured polygon does not determine its weight vector. The hypothesis demands symmetry for every possible collection of sample vectors, so the converse in Proposition 4.1 must recover a relation among weights from a universal geometric property. Another difficulty is that the explicit generators change shape at the midpoint, and the odd and even cases have different middle ranges. The paper writes the calculation for odd $N$ and says the even case is analogous; the theorem itself makes no parity restriction. A proof therefore has to cover the even boundary, including the generator whose $1/N$ band is empty. Bertsimas and Brown (2009), Proposition 4.1 and proof of Theorem 4.4.

Formalization scope

The Lean sample space is Fin N, with $N>0$ . Its indices start at zero; the prose and source formulas above start at one. The source's $\widehat N$ is N / 2 + 1 in natural numbers. Probability vectors use Mathlib's standard simplex together with antitone coordinate order. Permutohulls use convexHull of the finite permutation family, and order statistics use Tuple.sort. The reference distribution is uniform, as in the paper's Assumption 4.1. Real vector spaces of dimension zero are allowed because the claim quantifies over every dimension; the nonempty sample condition excludes division by zero.

The goal takes an arbitrary functional $\mu$ and requires an actual representation $\mu=\mu_q$ by a restricted-simplex weight. This is the paper's Theorem 4.2 parametrization of distortion risk measures, stated directly because that theorem is being drafted in a separate mission of the same series. Universal symmetry is derived from the data quantifier; it is not assumed as a condition on $q$ . The generator mixture is likewise the conclusion, with its coefficients nonnegative and summing to one. Central symmetry includes membership of the center in the set.

Useful contributions include proofs of the source's permutation characterization, validity and symmetry of generator mixtures, and their converse spanning property. The definitions of finite probability weights and weighted permutation hulls can support further finite sample robust optimization results. The paper's inconsistent accent on the generator risk measure in Theorem 4.4 is read as the functional of the displayed generator vector; its intermediate sum on p. 1492 does not alter the stated normalized mixture.

Selected references

Dimitris Bertsimas and David B. Brown, Constructing Uncertainty Sets for Robust Linear Optimization, Operations Research 57(6), 1483–1495, 2009. DOI: 10.1287/opre.1080.0646.

6 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Assortment Optimization under Variants of the Nested Logit Model 1: If the Restricted LP Optimum Scaled by α Is Feasible for the Full LP, Its Assortment Earns Within a Factor α of the Optimal RevenueResearch Paper

Motivation

A retailer that sells products in several categories, channels or stores has to decide which products to offer in each. Customers substitute: a product left out of the assortment sends some of its demand to other products, and some of it away. The nested logit model (McFadden 1974, 1981) is the standard choice model for this situation. It groups products into nests, so that substitution within a nest differs from substitution across nests. Assortment optimization under this model asks which products to offer in each nest so as to maximize expected revenue.

Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) split the problem into four cases: dissimilarity parameters at most one or unrestricted, and nests that are fully or only partially captured. The problem is polynomially solvable in the first case and NP-hard in the other three. Every approximation guarantee in the paper for the hard cases (Theorems 7, 10, 11, 12) comes from one general framework, set up in §2: a linear program equivalent to the assortment problem, and Theorem 1, which turns a feasibility certificate for that linear program into a performance guarantee. This mission formalizes that framework.

Setting

There are $m$ nests $M$ and $n$ products $N = \{1, \dots, n\}$ in each nest. Product $j$ of nest $i$ has revenue $r_{ij} \ge 0$ and preference weight $v_{ij} > 0$ , and the products in each nest are ordered so that $r_{i1} \ge \dots \ge r_{in}$ . Nest $i$ has a no-purchase weight $v_{i0} \ge 0$ and a dissimilarity parameter $\gamma_i > 0$ . The weight of choosing no nest at all is $v_0 \ge 0$ . If the assortment $S_i \subseteq N$ is offered in nest $i$ , write

V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j\in S_i} r_{ij} v_{ij}}{V_i(S_i)}, \quad R_i(\emptyset) = 0 .

A customer picks nest $i$ with probability $Q_i = V_i(S_i)^{\gamma_i} / (v_0 + \sum_{l\in M} V_l(S_l)^{\gamma_l})$ , and then a product of that nest by the multinomial logit model. The expected revenue is

\Pi(S_1, \dots, S_m) = \sum_{i \in M} Q_i(S_1, \dots, S_m)\, R_i(S_i),

and problem (2) is $Z^* = \max_{S_i \subseteq N} \Pi(S_1, \dots, S_m)$ .

The linear program (3) in the variables $(x, y_1, \dots, y_m)$ minimizes $x$ subject to

v_0 x \ge \sum_{i\in M} y_i, \qquad y_i \ge V_i(S_i)^{\gamma_i}\big(R_i(S_i) - x\big) \quad \forall S_i \subseteq N,\ i \in M.

Given candidate collections $\{A_{it} : t \in \mathcal T_i\}$ of assortments for each nest, the linear program (4) is (3) with the second family of constraints imposed only for $S_i$ in the collection of nest $i$ .

Formalization targets

Goal: Theorem 1 (p. 13)

Let $(\hat x, \hat y)$ be an optimal solution of (4), and let $\hat S_i$ solve $\max_{S_i \in \{A_{it}\}} V_i(S_i)^{\gamma_i}(R_i(S_i) - \hat x)$ , problem (5), in every nest. If $(\alpha \hat x, \beta \hat y)$ is feasible for (3) for some $\alpha, \beta$ , then, with $\hat Z = \Pi(\hat S_1, \dots, \hat S_m)$ ,

\alpha \hat Z \ \ge\ Z^* \ \ge\ \hat Z .

The theorem fixes no candidate collection and no value of $\alpha$ . Each later section of the paper instantiates it with its own collection and its own factor, so a formal proof applies to all of them.

Milestones (§2, pp. 11–12)

Problem (2) is equivalent to (3): $Z^*$ is the least $x$ for which some $y$ makes $(x, y)$ feasible for (3).
At an optimal solution of (4), the first constraint binds at the maximizers $\hat S_i$ of (5), and $\hat x = \Pi(\hat S_1, \dots, \hat S_m)$ .
Problem (4) relaxes (3), so $\hat x \le Z^*$ .

Companions (§7, pp. 29–30)

The tighter program (16), which lets each nest's assortment be a fractional vector $z_i \in [0,1]^n$ , has every feasible $x$ above $Z^*$ .
Proposition 13: $\hat F_i(x) = \max_{z_i \in [0,1]^n} F_i(z_i \mid x)$ is convex, with subgradient $-(v_{i0} + \sum_j v_{ij}\hat z_{ij}(x))^{\gamma_i}$ at $x$ .

Significance

Theorem 1 is the common step behind the paper's four approximation guarantees: the factor $\rho$ or $2\kappa$ of Theorem 7, the factor 2 of Theorem 10, the factor of Theorem 11, and the $\delta^{2\bar\gamma+1}$ of Theorem 12. Each of these reduces to checking that a scaled optimum of a small linear program is feasible for (3). With Theorem 1 formalized, those guarantees reduce to inequalities about candidate collections, which are the subject of the sister missions of this series. The upper bound (16) and Proposition 13 give the instance-specific bound that the paper uses to assess its assortments numerically.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The formal work adds two things: the statements below are made exact at the degenerate inputs the prose passes over (an empty assortment, $v_0 = 0$ ), and a formal proof certifies the framework once for every later instantiation.

Difficulty

The equivalence of (2) and (3) rests on decomposing a maximum over joint assortments into a sum of per-nest maxima, and on reading the fractional objective $\Pi \le x$ as a linear constraint. Both steps need care where a denominator $v_0 + \sum_i V_i(S_i)^{\gamma_i}$ can vanish. The binding argument for (4) is a perturbation argument: lowering $\hat x$ must keep every constraint satisfiable, which needs a continuity and monotonicity property of the right-hand side in $x$ . The obvious one-line reading of Theorem 1, " $\hat x = \hat Z$ and $\alpha\hat x \ge Z^*$ ", is correct only once both of these facts are established with their hypotheses. In particular, it is false when $v_0 = 0$ (see below). Proposition 13 requires that the supremum over the box be finite, which comes from the boundedness of $F_i$ on $[0,1]^n$ .

Formalization scope

Nests are a finite type ι and products are Fin n, indexed $0, \dots, n-1$ . An assortment is a finite set of products per nest, and a candidate collection is a set of such finite sets. Powers are real powers, and Lean's $x / 0 = 0$ gives $R_i(\emptyset) = 0$ . $Z^*$ is $\Pi(S^*)$ for an arbitrary optimal assortment $S^*$ ; no supremum over assortments is taken. "Optimal solution of (4)" means feasible with minimal $x$ , and " $\hat S_i$ solves (5)" means $\hat S_i$ belongs to the collection of nest $i$ and maximizes the objective of (5) over it at $\hat x$ .

Standing assumptions and pins. These are $v_0, v_{i0} \ge 0$ and ordered revenues, together with $v_{ij} > 0$ , $r_{ij} \ge 0$ and $\gamma_i > 0$ . The paper allows zero-weight padding products and $\gamma_i = 0$ , but its own conventions fail there. Theorem 1 and the binding milestone add $v_0 > 0$ . The page allows $v_0 = 0$ , but then Theorem 1 is false: take one nest with $v_{10} = 0$ , $\gamma_1 = 1$ , $r_{11} = v_{11} = 1$ and candidates $\{\emptyset, \{1\}\}$ . Then $\hat x = 1$ and $\hat S_1 = \emptyset$ meet every hypothesis with $\alpha = \beta = 1$ , yet $\hat Z = 0 < Z^* = 1$ . The equivalence of (2) and (3) and the bound from (16) keep $v_0 \ge 0$ , as the page does, and assume at least one nest and one product: with neither and $v_0 = 0$ , every $x$ is feasible for (3).

A formalization that assumes the binding equality, the identity $\hat x = \hat Z$ , or the inequality $\hat x \le Z^*$ in the goal would trivialize it. Those facts appear only as milestones. Likewise, reading "optimal solution of (4)" as mere feasibility would make the goal false rather than easier.

The development needs only finite sums, real powers and elementary order reasoning. Proposition 13 also needs the boundedness of a continuous function on a box and the convexity of a pointwise supremum of affine functions. Welcome contributions include proofs of the milestones, the goal from them, and reusable lemmas on the per-nest decomposition of maxima, which the sister missions of this series use as well.

Selected references

J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014 (revised manuscript of June 18, 2013, cited here). https://doi.org/10.1287/opre.2014.1256
D. McFadden, Econometric models of probabilistic choice, in C. Manski, D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981. https://eml.berkeley.edu/~mcfadden/discrete.html
P. Rusmevichientong, D. Shmoys, H. Topaloglu, Assortment optimization with mixtures of logits, Technical report, Cornell University, 2010. https://people.orie.cornell.edu/huseyin/publications/publications.html
M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993. https://doi.org/10.1002/0471787779

6 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On the Power and Limitations of Affine Policies in Two-Stage Adaptive Optimization IV: When A ≥ 0 the Best Affine Policy Costs at Most 3√m Times the Fully Adaptable OptimumResearch Paper

Motivation

Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision $x$ is fixed before an uncertain right-hand side $b$ is revealed, and a second-stage decision $y(b)$ is chosen after it, as a function of $b$ . The objective protects against the worst $b$ in an uncertainty set $\mathcal U$ . Computing an optimal fully adaptable solution is intractable in general (Feige, Jain, Mahdian and Mirrokni, IPCO 2007), so practitioners restrict the second stage to affine policies $y(b)=Pb+q$ , introduced in robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004). An optimal affine policy is computed by a single convex program, but its cost may exceed the adaptive optimum.

Bertsimas and Goyal (Math. Program. Ser. A, 2012) quantify this loss. Earlier, Bertsimas, Iancu and Parrilo (Math. Oper. Res. 2010) proved affine policies optimal for a class of one-dimensional multistage problems. The present paper shows that affine policies are optimal when $\mathcal U$ is a simplex (Theorem 1), that they can lose a factor $\Omega(m^{1/2-\delta})$ in general (Theorem 3), and — the subject of this mission — that when the first-stage constraint matrix is nonnegative they never lose more than $3\sqrt m$ (Theorem 4). Nonnegative first-stage matrices occur in network design, facility location, capacity planning and other covering problems.

Setting

Let $A\in\mathbb R^{m\times n_1}$ , $B\in\mathbb R^{m\times n_2}$ , $c\in\mathbb R^{n_1}_+$ , $d\in\mathbb R^{n_2}_+$ , and let $\mathcal U\subseteq\mathbb R^m_+$ be convex, compact and full-dimensional. The problem $\Pi_{Adapt}(\mathcal U)$ is

z_{Adapt}(\mathcal U)=\min\; c^Tx+\max_{b\in\mathcal U}d^Ty(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ \ x\ge0,\ \ y(b)\ge0\quad\forall b\in\mathcal U,

where the minimum is over first-stage vectors $x$ and arbitrary maps $b\mapsto y(b)$ . The problem is assumed feasible. The value $z_{Aff}(\mathcal U)$ is the same minimum restricted to affine second stages $y(b)=Pb+q$ , which must still satisfy $Pb+q\ge0$ on $\mathcal U$ .

For each coordinate $j$ put $\mu_j=\max\{b_j : b\in\mathcal U\}$ and fix a maximizer $\beta^j\in\mathcal U$ with $\beta^j_j=\mu_j$ (display (38)). The scaled sum of $b$ over an index set $J$ is $\sum_{j\in J}b_j/\mu_j$ .

Algorithm $\mathcal A$ (Fig. 1 of the paper) starts with $J_1=\{1,\dots,m\}$ and $b^0=0$ . While some $b\in\mathcal U$ has scaled sum over $J_1$ larger than $\sqrt m$ , it picks a maximizer $u^k\in\mathcal U$ of that scaled sum, adds $u^k$ to the running vector on the coordinates of $J_1$ , and moves to $J_2$ every coordinate $j$ whose running value has reached $\mu_j$ . It returns the number of iterations $K$ , the vectors $u^1,\dots,u^K$ , their sum $\beta=u^1+\dots+u^K$ , and the partition $J_1,J_2$ .

In the $k$ -uncertain variant (60)–(63), only $k$ right-hand sides $b\in\mathcal U\subseteq\mathbb R^k_+$ are uncertain and the remaining $m-k$ are fixed at $b^0$ ; all data are nonnegative. Its values are $z^k_{Adapt}(\mathcal U)$ and $z^k_{Aff}(\mathcal U)$ .

Formalization targets

Goal: Theorem 4

If $A\ge0$ entrywise, then a feasible affine solution exists and

z_{Aff}(\mathcal U)\le 3\sqrt m\cdot z_{Adapt}(\mathcal U).

Milestones

$\mu_j>0$ for every $j$ (after (38)).
Lemma 9. For every complete run of Algorithm $\mathcal A$ : $\sum_{j\in J_1}b_j/\mu_j\le\sqrt m$ for all $b\in\mathcal U$ , and $b_j\le\beta_j$ for all $j\in J_2$ and $b\in\mathcal U$ .
Lemma 10. Algorithm $\mathcal A$ executes at most $K\le2\sqrt m$ iterations.
Feasibility (48)–(55). For any feasible $(x^*,y^*)$ , the solution $\tilde x=3\sqrt m\,x^*$ , $\tilde y(b)=\sum_{j\in J_1}\frac{b_j}{\mu_j}y^*(\beta^j)+\hat y$ with $\hat y=\frac{2\sqrt m}{K}\sum_{k=1}^Ky^*(u^k)$ is feasible.
Cost (56)–(59). If $t$ bounds the worst-case cost of $(x^*,y^*)$ , then $3\sqrt m\cdot t$ bounds that of $(\tilde x,\tilde y)$ .

Companion results

Algorithm $\mathcal A$ has a complete run when $\mathcal U$ is compact.
Lemma 11. $z(\Pi_1)\le z^k_{Adapt}(\mathcal U)$ and $z(\Pi_2)\le z^k_{Adapt}(\mathcal U)$ for the uncertain and deterministic parts of the $k$ -uncertain problem.
Theorem 5. $z^k_{Aff}(\mathcal U)\le(3\sqrt k+1)\cdot z^k_{Adapt}(\mathcal U)$ , the paper's $O(\sqrt k)$ bound with its proof's constant.
Special case (39)–(45). If $\sum_{j=1}^m b_j/\mu_j\le\sqrt m$ on $\mathcal U$ , then $z_{Aff}(\mathcal U)\le\sqrt m\cdot z_{Adapt}(\mathcal U)$ .

Significance

Theorem 4 is an upper bound on the price of restricting to affine policies, and Theorem 3 of the same paper shows it is tight up to a constant factor: for every $\delta>0$ there are instances with $A\ge0$ where the gap is $\Omega(m^{1/2-\delta})$ . Together they settle the order of the approximation ratio of affine policies for covering-type two-stage problems. Theorem 5 refines the bound to $O(\sqrt k)$ when only $k$ of the $m$ right-hand sides are uncertain, which is the regime of many applications. The construction is also the template for the paper's Theorem 6, a $4\sqrt m$ -approximation for general $A$ obtained from a single dominating simplex.

The results are proved in the paper. To the knowledge of this mission, none of them has a machine-checked proof. Formalizing them produces a reusable model of two-stage adaptive linear programs with affine policies, a verified analysis of a greedy covering procedure (Algorithm $\mathcal A$ ), and an explicit-constant version of an $O(\cdot)$ statement.

Difficulty

The obvious attempt scales the fully adaptable solution at the extreme points $\beta^j$ linearly in $b$ : $\tilde y(b)=\sum_j (b_j/\mu_j)\,y^*(\beta^j)$ . This is feasible at cost factor $\sqrt m$ only when the scaled sums $\sum_j b_j/\mu_j$ stay below $\sqrt m$ on $\mathcal U$ (condition (39)); in general they can reach $m$ , and the linear rule then costs a factor $m$ . The difficulty is to handle the coordinates where $\mathcal U$ has large scaled mass. Algorithm $\mathcal A$ isolates them, and the delicate point is the iteration count: each round must add scaled mass above $\sqrt m$ , while the total scaled mass that can be absorbed before every coordinate leaves $J_1$ is at most $2m$ . A formal proof must also track the algorithm's state through its recursion, because the argmax choices are not unique and the statements must hold for every run.

Formalization scope

Vectors are Fin m → ℝ with the componentwise order, indices are 0-based, and matrices are Matrix (Fin m) (Fin n) ℝ. Nonnegativity of a matrix is stated entrywise. $z_{Adapt}$ and $z_{Aff}$ are infima of the set of worst-case cost bounds achieved by feasible solutions; the goal and Theorem 5 assert the existence of a feasible affine solution, which rules out the trivializing reading in which $z_{Aff}$ is the infimum of an empty set (Lean's junk value $0$ ) and the inequality holds for free. The goal does not mention $\mu$ , $\beta^j$ or Algorithm $\mathcal A$ ; these appear only in milestones.

$\mu$ and $\beta^j$ are given with their defining properties ( $\mu_j$ is the greatest value of $b_j$ on $\mathcal U$ , and $\beta^j\in\mathcal U$ with $\beta^j_j=\mu_j$ ). Algorithm $\mathcal A$ is encoded as a recursion on a choice sequence $u$ , with step 2(d) read as $J_1^k=\{j\in J_1^{k-1}: b^k_j<\mu_j\}$ . A complete run requires the loop test and the argmax property at each iteration and the failure of the loop test at the end. The milestones on the constructed policy are stated for every feasible $(x^*,y^*)$ and every cost bound $t$ , so that no attainment of the optimum is assumed.

Standing assumptions of (1) carried by the goal: $c,d\ge0$ ; $\mathcal U\subseteq\mathbb R^m_+$ convex, compact, with nonempty interior; feasibility. Milestones drop the ones they do not use. Theorem 5 carries compactness and full-dimensionality of $\mathcal U$ , which §5.1 does not repeat but its proof uses through Theorem 4. Lemma 11 assumes that $z^k_{Adapt}(\mathcal U)$ is finite, since the paper's inequality is between extended reals.

A complete development needs: finite-dimensional linear programming facts (existence of optimal solutions is not needed), compactness arguments for the argmax in Algorithm $\mathcal A$ , and manipulation of finite sums over Finset. The model of (1) and the analysis of Algorithm $\mathcal A$ are reusable by the companion mission on Theorem 6. Contributions of proofs of any milestone, and of supporting lemmas about the recursion of Algorithm $\mathcal A$ , are welcome.

Selected references

D. Bertsimas and V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Math. Program. Ser. A, 2012. https://doi.org/10.1007/s10107-011-0444-4
A. Ben-Tal, A. Goryashko, E. Guslitzer and A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99(2), 351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
D. Bertsimas, D. A. Iancu and P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Math. Oper. Res. 35(2), 363–394, 2010.
U. Feige, K. Jain, M. Mahdian and V. Mirrokni, Robust combinatorial optimization with exponential scenarios, Lect. Notes Comput. Sci. 4513, 439–453, 2007.

7 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On the Power and Limitations of Affine Policies in Two-Stage Adaptive Optimization II: With m + 3 Extreme Points the Best Affine Policy Can Cost More Than (2 − δ) Times the OptimumResearch Paper

Motivation

Two-stage adaptive optimization models decisions made in two steps: a first-stage decision is fixed before an uncertain parameter is revealed, and a second-stage (recourse) decision may then depend on the realized value. In the robust version, the uncertain parameter ranges over an uncertainty set and the objective is the worst-case cost. Such models arise in capacity planning, network design and inventory problems with uncertain demand, where the demand is the right-hand side of the constraints.

Computing an optimal fully adaptable second-stage policy is intractable in general: the recourse is an arbitrary function of the uncertain parameter. The standard tractable surrogate, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004), restricts the recourse to an affine policy $y(b) = Pb + q$ , whose optimization is a finite convex program. Practitioners report that affine policies often perform well, which raises the question of when they are optimal and how much they can lose.

Bertsimas and Goyal (Math. Program. Ser. A, 2012) answer this for problems with an uncertain right-hand side. Their Theorem 1 shows that affine policies are optimal when the uncertainty set is a simplex, that is, the convex hull of $m+1$ affinely independent points of $\mathbb R^m_+$ . Their Theorem 2, the subject of this mission, shows that this is almost tight: one additional extreme point can make the best affine policy almost twice as expensive as the optimum.

Setting

Let $A \in \mathbb R^{m\times n_1}$ , $B \in \mathbb R^{m\times n_2}$ , $c \in \mathbb R^{n_1}_+$ , $d \in \mathbb R^{n_2}_+$ and let $\mathcal U \subseteq \mathbb R^m_+$ be an uncertainty set. The problem $\Pi_{\mathrm{Adapt}}(\mathcal U)$ is

z_{\mathrm{Adapt}}(\mathcal U)=\min\ c^{T}x+\max_{b\in\mathcal U} d^{T}y(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ \ x\ge 0,\ \ y(b)\ge 0\quad\forall b\in\mathcal U .

Here $x$ is the first-stage decision and $y : \mathcal U \to \mathbb R^{n_2}$ is the second-stage policy; all inequalities between vectors are componentwise. The value $z_{\mathrm{Aff}}(\mathcal U)$ is the same minimum restricted to affine policies $y(b) = Pb + q$ with $P \in \mathbb R^{n_2\times m}$ and $q \in \mathbb R^{n_2}$ ; an affine policy must still satisfy $Pb + q \ge 0$ for every $b \in \mathcal U$ . Always $z_{\mathrm{Adapt}}(\mathcal U) \le z_{\mathrm{Aff}}(\mathcal U)$ .

The instance $\mathcal I$ of (6) is defined for $\delta > 0$ and an even integer $m > 200/\delta^2$ . It has $n_1 = n_2 = m$ , $c = 0$ , $d = (1,\dots,1)^T$ , $A = 0$ , and

B_{ij}=\begin{cases}1,& i=j,\\ 1/\sqrt m,& i\ne j,\end{cases}\qquad \mathcal U=\operatorname{conv}\{b^0,b^1,\dots,b^{m+2}\},

where $b^0 = 0$ , $b^j = e_j$ is the $j$ -th unit vector for $j = 1,\dots,m$ , $b^{m+1}$ has entries $1/\sqrt m$ in its first $m/2$ coordinates and $0$ in the others, and $b^{m+2}$ has $0$ in its first $m/2$ coordinates and $1/\sqrt m$ in the others. Thus $\mathcal U$ is generated by $m+2$ nonzero points. The last two are also extreme points when $m\ge 6$ ; for $m=2$ or $4$ they lie in the convex hull of $0,e_1,\dots,e_m$ .

For a permutation $\tau$ of $\{1,\dots,m\}$ , write $x^\tau = (x_{\tau(1)},\dots,x_{\tau(m)})$ . A set $U$ is permutation-invariant with respect to $\tau$ if $x \in U \iff x^\tau \in U$ (Definition 2), and $\Gamma$ is the set (10) of permutations with $i \le m/2 \iff \tau(i) \le m/2$ .

Formalization targets

Goal: Theorem 2

z_{\mathrm{Aff}}(\mathcal U)>(2-\delta)\cdot z_{\mathrm{Adapt}}(\mathcal U)\qquad\text{for the instance }\mathcal I\text{ of (6), every }\delta>0\text{ and every even }m>200/\delta^2 .

Milestones

Lemma 1. On $\mathcal I$ there is a feasible fully adaptable solution with worst-case cost $1$ , so $z_{\mathrm{Adapt}}(\mathcal U) \le 1$ .
Lemma 2. The set $\mathcal U$ of (6) is permutation-invariant with respect to every $\tau \in \Gamma$ .
Lemma 3. There is an optimal affine solution $\hat y(b) = \hat Pb + \hat q$ whose intercept is constant: $\hat q_i = \hat q_j$ for all $i, j$ .
First Claim of the proof of Theorem 2. For any feasible affine solution with intercept $\hat q \equiv \beta$ and worst-case cost at most $2-\delta$ : $\beta \le (2-\delta)/m$ .
Second Claim. Under the same assumption, $\hat P_{jj} \ge 1 - 2/\sqrt m - 2/m$ for every $j$ .
Third Claim. Under the same assumption, $\hat P_{ij} \ge -(2-\delta)/m$ for all $i, j$ .

Significance

Together with Theorem 1 of the same paper, Theorem 2 delimits exactly where affine policies are optimal for right-hand-side uncertainty: for a simplex they are, and with one more nonzero extreme point the gap can approach $2$ . The ratio is measured against the fully adaptable optimum, which is the quantity a practitioner gives up by choosing affine recourse. Later sections of the paper push the same construction to $m^{1/2-\delta}$ for sets with polynomially many extreme points and prove a matching $O(\sqrt m)$ upper bound; Theorem 2 is the simplest member of this family and isolates the mechanism.

The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a formal model of two-stage adaptive linear optimization with uncertain right-hand side, the values $z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$ , and a verified lower-bound instance. The symmetrization statement (Lemma 3) is an instance of a general principle, that a convex problem invariant under a group has an invariant optimum, which is reusable well beyond this paper.

Difficulty

The upper bound $z_{\mathrm{Adapt}} \le 1$ requires a feasible policy, which can be written down. The lower bound on $z_{\mathrm{Aff}}$ is a statement about all affine policies, an $m^2 + m$ dimensional family, and cannot be checked policy by policy. The obvious attempt, testing an arbitrary affine policy against a few extreme points, fails because an asymmetric policy can trade cost between coordinates. The argument needs an optimal policy that is symmetric, which in turn needs both the existence of an optimal affine solution (attainment of a minimum over a non-compact set of policies) and the invariance of the instance under the permutations of $\Gamma$ and the swap of the two halves. Without the attainment step, a contradiction for every policy of cost at most $2-\delta$ yields only $z_{\mathrm{Aff}} \ge 2-\delta$ , not the strict inequality.

Formalization scope

Vectors are Fin m → ℝ with the componentwise order, matrices are Matrix (Fin m) (Fin n) ℝ, $Bx$ is B *ᵥ x and $d^Ty$ is d ⬝ᵥ y. Indices are 0-based: the paper's coordinate $i$ is index $i - 1$ , so " $i \le m/2$ " is (i : ℕ) < m / 2, with natural-number division (exact since $m$ is even). $x^\tau$ is x ∘ τ for τ : Equiv.Perm (Fin m).

$z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$ are the infima of the sets of real numbers $t$ for which some feasible (respectively feasible affine) solution satisfies $c^Tx + d^Ty(b) \le t$ for all $b \in \mathcal U$ . This epigraph form avoids a supremum of a possibly unbounded function; on an infeasible instance the infimum would be Lean's junk value $0$ , which is why Lemma 1 also asserts the existence of the feasible solution of cost $1$ . Optimal solutions are stated by IsOptimalAff: feasible, with worst-case cost bounded by every bound achieved by any feasible affine solution. Affine policies must be nonnegative on $\mathcal U$ , as in (1).

The instance is concrete, so the standing assumptions of (1) (nonnegative costs, compact convex full-dimensional $\mathcal U \subseteq \mathbb R^m_+$ , feasibility) are properties of the data rather than hypotheses. The goal adds no hypothesis to the page: $\delta > 0$ , $m$ even and $m > 200/\delta^2$ . For $\delta \ge 2$ the statement is easy but still true. The three Claims are stated for any feasible affine solution with constant intercept and worst-case cost at most $2-\delta$ , which is exactly what the paper's proof uses about the symmetric optimal solution under its contradiction hypothesis (12). Lemma 1 drops the unused hypothesis $m > 200/\delta^2$ . Definition 2 prints " $x \in P \iff x^\tau \in P$ "; the formalization reads $P$ as the set $U$ .

Replacing $z_{\mathrm{Aff}}$ by the cost of one particular affine policy, stating the goal with $\ge$ , or bounding only policies with constant intercept would not be Theorem 2, and is ruled out: the goal compares the two optimal values with a strict inequality.

A complete development needs convex hulls of finite point sets in Fin m → ℝ, the existence of a minimizer for the affine problem (a linear program in $(x, P, q)$ with infinitely many constraints indexed by $\mathcal U$ , reducible to the extreme points), averaging of optimal solutions over a permutation group, and elementary estimates with $\sqrt m$ . Contributions of general lemmas on attainment of semi-infinite linear programs and on symmetrization of convex programs are welcome.

Selected references

D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming Ser. A (online first 2011; received 31 Oct 2009, accepted 17 Jan 2011). https://doi.org/10.1007/s10107-011-0444-4
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Mathematics of Operations Research 35 (2010) 363–394. https://doi.org/10.1287/moor.1100.0444

8 thms2 active usersReviewed

Linear Optimization

Missions

A Linear Programming Approach to the Cutting Stock Problem—Part II 1: The Lexicographic Knapsack Method Terminates, and M_1 Equals max(c_1, the Knapsack Optimum for the Longest Stock Length L_1)Research Paper

Motivation

Setting

Formalization targets

Goal: the method terminates and computes M1M_1M1​

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Linear Programming Approach to the Cutting Stock Problem—Part II 2: For a Linear-Fractional Objective, a Basic Feasible Solution with No Improving Edge Is a Global MinimumResearch Paper

Motivation

Setting

Formalization targets

Goal: the edge criterion (p. 882)

Milestones (p. 882–883)

Significance

Difficulty

Formalization scope

Selected references

On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems 5: For Hypercube Uncertainty, Even in the Constraints, the Robust and Adaptive Optima CoincideResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.4 (p. 31)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Convergence of Stochastic Dual Dynamic Programming and Related Methods: DOASA Reaches an Optimal Policy in Finitely Many Iterations Almost SurelyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 under the joint sampling property J

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Estimation of Executive Compensation by Linear Programming I: Least Absolute Deviations under Ranking Constraints Equal a Linear ProgramResearch Paper

Motivation

Setting

Formalization targets

Equivalence of the two programs

Supporting claims and numerical result

Significance

Difficulty

Formalization scope

Selected references

Integer Programming with a Fixed Number of Variables 1: If B(p,r) ⊂ τK ⊂ B(p,R) with R/r ≤ c₁ and τK Misses the Lattice, Fewer Than 1 + c₁c₂√n Lattice Hyperplanes H + kbₙ Meet B(p,R)Research Paper

Motivation

Setting

Formalization targets

Goal (§1, p. 541)

Milestones, in the order the paper uses them

Significance

Difficulty

Formalization scope

Selected references

On Linear Characterizations of Combinatorial Optimization Problems III: Zero-One and Integer-Programming-Type Problems Have Small Facial DescriptionsResearch Paper

Motivation

Setting

Formalization targets

Lemma 1

Significance

Difficulty

Formalization scope

Selected references

Finding Minimum-Cost Circulations by Successive Approximation I: The Generic Refine Subroutine Stops Within 3n(n − 1) + 3nm + 3n²(m + n) Update Operations at an ε-Optimal CirculationResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Solving Large-Scale Zero-One Linear Programming Problems: A Minimal Cover Inequality Cuts Off x̄ iff the Knapsack Problem (2.12) Has Optimal Value Less Than OneResearch Paper

Goal: the method terminates and computes $M_1$