The OR Formalization Drive

Motivation

Whitney's 1935 paper introduced matroids as an abstraction of linear dependence among the columns of a matrix. Most of the paper works over the real numbers; its appendix asks which matroids arise from matrices of integers mod 2, that is, matrices with entries 0 and 1 in which rank and dependence are computed over the two-element field. These are today's binary matroids. They include the cycle matroids of graphs (Whitney closes the paper by noting that graphs correspond to mod-2 matrices with exactly two ones in each column) and they are the setting of several later structure theorems: Tutte's excluded-minor characterization of binary matroids (Tutte 1958), Seymour's decomposition of regular matroids (Seymour 1980) and Seymour's theory of binary clutters and max-flow min-cut (Seymour 1977), which underlies parts of combinatorial optimization.

Whitney's answer is an intrinsic postulate, (C*), on the circuits of the matroid, stated without reference to any matrix, and a constructive representation theorem (Theorem 37): a matroid satisfying (C*) is the matroid of a mod-2 matrix, and the matrix is unique once the columns of one base are fixed.

Setting

A matroid $M$ on elements $e_1, \dots, e_n$ is given by its independent sets; its circuits are its minimal dependent sets, its rank $r(M)$ is the size of a base, and its nullity is $n(M) = n - r(M)$. Here $M$ is a Mathlib Matroid (Fin n) whose ground set is all of Fin n.

Subsets of the elements are added mod 2: a sum of finitely many sets is the set of elements lying in an odd number of them (for two sets, the symmetric difference). A cycle is a sum mod 2 of circuits; the empty sum is the null cycle $\emptyset$. A set is a true sum of sets that have no common elements and whose union it is. Postulate (C*) requires that each cycle be a true sum of circuits.

With $n = r + q$, a family $P_1, \dots, P_q$ is a strict fundamental set of circuits with respect to $e_{n-q+1}, \dots, e_n$ if $q = n(M)$, each $P_i$ is a circuit, and $P_i$ contains $e_{n-q+i}$ but no other $e_{n-q+j}$.

For a matrix $\mathbf M$ over the integers mod 2 with columns $C_1, \dots, C_n$, columns are independent (mod 2) if no non-null subset of them sums to the zero column. The matroid corresponding to $\mathbf M$ has the column indices as elements and these independent sets.

Formalization targets

Goal: Theorem 37 (p. 533)

Let $M$ satisfy (C*), with elements $e_1, \dots, e_n$ and base $\{e_1, \dots, e_{n-q}\}$. For every matrix $\mathbf M_1$ mod 2 (any number of rows) whose $n - q$ columns are independent mod 2,

$$\exists!\ \mathbf M = (\mathbf M_1 \mid C_{n-q+1} \cdots C_n) \ \text{ whose corresponding matroid is } M.$$

Milestones

1. Theorem 9 (p. 517): if $e_1, \dots, e_{n-q}$ is a base, there is a unique strict fundamental set of circuits with respect to $e_{n-q+1}, \dots, e_n$.
2. Appendix, p. 531: (C*) implies the circuit postulate (C₂), for any family of sets.
3. Theorem 33: under (C*), the circuits are exactly the minimal non-null cycles.
4. Theorem 34: under (C*), the cycles are exactly the $2^q$ sums mod 2 of a strict fundamental set.
5. Theorem 35: two (C*)-matroids with a common strict fundamental set have the same circuits.
6. Theorem 36: any $P_1, \dots, P_q$ with $e_{n-q+i} \in P_i \subseteq \{e_1, \dots, e_{n-q}, e_{n-q+i}\}$ is the strict fundamental set of exactly one (C*)-matroid.
7. Appendix, p. 532: the matroid of a matrix mod 2 exists, satisfies (C*), and its cycles are the supports of the mod-2 dependencies among the columns.

Milestone 7 and the goal together characterize binary matroids as the matroids satisfying (C*).

Significance

The result. Theorem 37 and the p. 532 claim give an intrinsic, matrix-free description of the matroids representable over the two-element field, and Theorem 36 parametrizes all of them by $q$ arbitrary subsets of a base. Uniqueness in Theorem 37 says that a binary representation is determined by the columns of one base; in modern terms, binary matroids are uniquely representable over GF(2) up to row operations. Every later theory of binary matroids, including graphic and cographic matroids, Tutte's excluded-minor theorem and Seymour's decomposition, starts from this equivalence.

Formalizing it. The results are proved in the paper and in textbooks (e.g. Oxley, Matroid Theory, Ch. 9) but, at the Mathlib revision used here, there is no notion of a matroid represented by a matrix over a field, and no binary-matroid theory. On Prove2Me, the existing binary objects (SeymourMFMC.Binary.*) are binary clutters defined through blockers, not matroids represented by mod-2 matrices. This mission produces the representation predicate for mod-2 matrices, the cycle space of a matroid, and the equivalence between (C*) and binary representability.

Difficulty

Writing down candidate columns is not the hard part; showing that the matroid of the completed matrix is $M$ itself, and not merely a matroid sharing some of its circuits, is. Whitney's example at the end of §9 exhibits two different matroids with a common strict fundamental set, so agreement on fundamental circuits does not by itself identify a matroid; any argument must use (C*) on both the given matroid and the matroid of the matrix. A naive comparison of independent sets column by column does not close this gap. Uniqueness likewise depends on the independence mod 2 of the prescribed columns: without it, different completions can give the same matroid.

Formalization scope

• Matroids are Mathlib Matroid (Fin (r + q)) with ground set Set.univ; Whitney's $e_k$ is k - 1, his $e_1, \dots, e_{n-q}$ is the range of Fin.castAdd q, and $e_{n-q+i}$ is Fin.natAdd r (i - 1). Writing $n = r + q$ removes natural-number subtraction; $q$ is not a free parameter, since $\{e_1, \dots, e_r\}$ is required to be a base.
• Sums mod 2 count parity of membership (sumMod2); cycles are sums over finite sets of circuits; true sums are unions over finite pairwise-disjoint sets of circuits; (C*) is SatisfiesCStar on the circuit family {C | M.IsCircuit C}. These definitions take the circuit family as a parameter, so that the (C₂) milestone is posed for an arbitrary family of sets, as Whitney poses it.
• A strict fundamental set includes the nullity condition $r(M) + q = \rho(M)$, stated in $\mathbb N_\infty$.
• Matrices are Matrix (Fin m) (Fin n) (ZMod 2) with any $m$; independence mod 2 of columns is LinearIndepOn (ZMod 2) of the columns (the rows of the transpose). IsMatroidOf M A compares all independent sets, not only bases.
• Ruled out: the goal is not satisfied by any statement that compares only the bases of one size, by an existence-only statement without uniqueness, or by real (instead of mod-2) independence.
• Tacit hypotheses made explicit: the matroid's ground set is exactly $e_1, \dots, e_n$ ($\rho(M) = n$); the elements and matroids are finite.

Contributions welcome: the general fact that the matroid of a vector family over a field exists (a reusable Matroid.ofFun-style construction over any field), the cycle-space lemmas, and proofs of the milestones in any order.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• W. T. Tutte, A homotopy theorem for matroids, I, II, Transactions of the AMS 88 (1958), 144–174. https://doi.org/10.2307/1993244
• P. D. Seymour, The matroids with the max-flow min-cut property, Journal of Combinatorial Theory Ser. B 23 (1977), 189–222. https://doi.org/10.1016/0095-8956(77)90031-4
• P. D. Seymour, Decomposition of regular matroids, Journal of Combinatorial Theory Ser. B 28 (1980), 305–359. https://doi.org/10.1016/0095-8956(80)90075-1
• J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001

Motivation

Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets equipped with a rank function, or equivalently a family of independent sets, obeying a few postulates abstracted from the linear dependence of the columns of a matrix. The obvious first question about such an abstraction is whether it is genuinely more general than its model, that is, whether there are matroids that do not arise from any matrix. Section 16 of the paper answers it with a seven-element example, now called the Fano matroid $F_7$, and proves that no real matrix corresponds to it.

The question has had a long life. Representability of matroids over a given field is a central theme of matroid theory: Tutte (1958) characterized the matroids representable over the field with two elements by a single excluded minor, the four-point line $U_{2,4}$, and the regular matroids by three excluded minors, $U_{2,4}$, $F_7$ and its dual; and Seymour's decomposition of regular matroids (1980) rests on the same objects. Whitney's §16 is the starting point of this line: the first proof that the abstract postulates admit matroids outside linear algebra over $\mathbb R$.

Timeline:

• 1935. Whitney defines matroids, the circuit matrix of a matrix, and proves (§16) that the seven-element matroid $M'$ corresponds to no real matrix; in a footnote he credits Saunders MacLane with finding that $M'$ corresponds to no matrix and identifying it with a finite projective geometry. On p. 533 he exhibits a matrix of integers mod 2 for $M'$.
• 1958. Tutte characterizes binary and regular matroids by excluded minors; $F_7$ appears as an excluded minor for regularity (Tutte 1958).

Setting

Let $\mathbf M=(a_{ij})$ be an $m\times n$ matrix with columns $C_1,\dots,C_n$. For a set $N$ of columns, let $r(N)$ be the rank of the submatrix formed by those columns. Regarding the columns as abstract elements gives a matroid $M$ on $\{C_1,\dots,C_n\}$ with rank function $r$: the matroid of $\mathbf M$. A matroid corresponds to $\mathbf M$ if it is the matroid of $\mathbf M$, with elements matched to columns.

A circuit of a matroid is a minimal dependent set. For a circuit $P=\{i_1,\dots,i_p\}$ of the matroid of $\mathbf M$, there are numbers $b_1,\dots,b_n$ with $\sum_j a_{ij}b_j=0$ for every row $i$, and $b_j\neq 0$ exactly for $j\in P$; the set of such vectors is written $Z_{i_1\cdots i_p}$ when only the support condition is meant. Stacking one such row per circuit gives the circuit matrix $\mathbf M'$ of $\mathbf M$, determined up to nonzero factors on its rows.

A fundamental set of circuits of a matroid $M$ with nullity $n(M)=\rho(M)-r(M)$ ($\rho$ the number of elements) is a family of circuits $P_1,\dots,P_q$ with $q=n(M)$ such that the elements can be ordered $e_1,\dots,e_n$ with $e_{n-q+i}\in P_i$ and $e_{n-q+j}\notin P_i$ for $j>i$; it is strict if $e_{n-q+j}\notin P_i$ for every $j\neq i$.

The matroid $M'$ of §16 has elements $1,\dots,7$; its bases (maximal independent sets) are all three-element sets except

$$124,\quad 135,\quad 167,\quad 236,\quad 257,\quad 347,\quad 456. \qquad (16.1)$$

Formalization targets

Goal: §16, pp. 529–530

$$\exists\,M' \quad\text{and}\quad \forall m\ \forall\,\mathbf M\in\mathbb R^{m\times 7}:\ M' \text{ is not the matroid of } \mathbf M .$$

The number of rows is arbitrary; the existence clause makes the non-existence statement non-vacuous.

Milestones

1. §12. Every real matrix has a matroid: the ranks of column submatrices satisfy the rank postulates.
2. §14, (14.1). Every real matrix has a circuit matrix.
3. Theorem 29. The rows of a fundamental set of circuits form a base for the rows of the circuit matrix, so $r(\mathbf M')=q=n(\mathbf M)$.
4. Lemma 10. The support of a vector in the row space $H$ of a circuit matrix is a union of circuits.
5. Lemma 11. Two vectors of $H$ with the same circuit as support are proportional.
6. Theorem 32. For a circuit matrix normalised along a strict fundamental set, a minor $D$ vanishes iff an associated $q\times q$ minor $D'$ vanishes, iff some circuit avoids a prescribed set of columns.
7. §16, rank of $M'$. The rank of a $k$-set is $k$ for $k\le 2$, $3$ for $k\ge 4$, and for $k=3$ it is $2$ on (16.1) and $3$ otherwise.
8. p. 533. $M'$ is the matroid of an explicit $3\times 7$ matrix of integers mod 2.

Significance

The result. The theorem separates the abstract notion of matroid from linear dependence over $\mathbb R$: some matroids are not real-representable. It also exhibits that representability depends on the field, because the same matroid is the matroid of a matrix over the integers mod 2 (milestone 8). Everything later written about representability over particular fields, excluded-minor characterizations, and the gap between abstract and linear matroids starts from this distinction. Theorem 32 is of independent interest: it translates statements about circuits of a represented matroid into the vanishing of minors of a normalised circuit matrix.

Formalizing it. The result is classical and its proof is short on paper, but it is not formalized in Mathlib, which has matroids (Matroid, circuits, ranks) but no column matroid of a matrix with a rank-of-submatrix characterization, no circuit matrix, and no Fano matroid. The mission produces those objects and the bridge lemmas (Theorem 29, Lemmas 10–11, Theorem 32) that connect matroid circuits with linear algebra of the circuit matrix. No machine-checked proof of the non-representability of the Fano matroid over $\mathbb R$ in Lean is known to the curators.

Difficulty

The obvious attempt is a direct search: suppose a real $m\times 7$ matrix has $M'$ as its matroid and derive a contradiction from the seven dependent triples. This does not work as stated. Each rank condition is a determinantal (nonlinear) condition on the entries, the number of rows $m$ is unbounded, and a representation is determined only up to row operations and column scalings, so there is no finite case check and no single linear computation that settles the question. The contradiction has to come from an argument that is invariant under these symmetries, and the milestones (circuit vectors determined up to scaling, fundamental sets spanning, circuits detected by minors) are what such an argument needs to be stated in. The field also matters: the argument must use that $2\neq 0$ in $\mathbb R$, since over a field of characteristic 2 the statement is false (milestone 8).

Formalization scope

• Elements and matrices. Matroids are Mathlib Matroids whose ground set is the whole (finite) type. The Fano matroid lives on Fin 7, Whitney's element $k$ being k - 1; the seven triples are written out literally. Matrices are Matrix (Fin m) ι K; "the matroid of $\mathbf M$" means: ground set everything, and the rank M.eRk N of every finite set $N$ of columns equals Matrix.rank of the column submatrix.
• Field. The goal and Lemmas 10–11, Theorems 29 and 32 are stated over $\mathbb R$, as in the paper; the predicate "matroid of a matrix" is stated over any field so that the mod-2 milestone uses the same notion.
• Circuit matrix. Rows are determined up to nonzero factors, so "circuit matrix" is a predicate on a matrix together with a bijection between its rows and the circuits; every theorem holds for every such choice.
• Nullity and indices. $q=n(M)$ is written $q+r(M)=\rho(M)$ in extended naturals, with no truncated subtraction. In Theorem 32, $n=p+q$, the complement of $i_1,\dots,i_s$ is given as an order embedding of Fin t with $s+t=q$, and determinants are of square submatrices in the paper's row and column order.
• Ruling out trivial readings. The goal includes the existence of $M'$; without it "every matroid with these bases has no real matrix" could hold vacuously. The goal quantifies over every number of rows; fixing $m=3$ would be a weaker statement.

Reusable beyond this mission: the matroid of a matrix over a field, the circuit matrix, fundamental sets of circuits, and the Fano matroid. Contributions welcome: proofs of the milestones, and a proof of the goal by any route, including one that does not go through Theorem 32.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• W. T. Tutte, A homotopy theorem for matroids, I, II, Transactions of the American Mathematical Society 88 (1958), 144–174. https://doi.org/10.2307/1993244
• J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• O. Veblen and J. W. Young, Projective Geometry, Vol. I, Ginn, 1910 (cited by Whitney for the finite projective geometry).

Motivation

Two-stage adaptive optimization models decisions taken in two rounds: a first-stage decision $x$ is fixed before an uncertain parameter is revealed, and a second-stage decision $y(b)$ is chosen after the parameter $b$ is observed, so that the second stage may depend on $b$ arbitrarily. The objective is the worst case over an uncertainty set $\mathcal U$ of possible parameters. Such models arise in robust network design, capacity planning and two-stage covering problems, and they generalize the two-stage robust combinatorial problems (set cover, facility location) studied by Dhamdhere, Goyal, Ravi and Singh.

Optimizing over all functions $y(\cdot)$ is intractable in general: Bertsimas and Goyal note that the optimal second stage is piecewise linear in $b$ with possibly exponentially many pieces (Bemporad, Borrelli and Morari, 2003). A standard remedy, introduced for robust linear programs by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), restricts the second stage to affine policies (linear decision rules) $y(b)=Pb+q$; the best affine policy is computable by a single convex program and performs well empirically. The question is when this restriction loses nothing.

Timeline of the relevant results:

• 2004. Ben-Tal, Goryashko, Guslitzer and Nemirovski introduce affinely adjustable robust counterparts and show that the best affine policy is tractable for many uncertainty sets (doi:10.1007/s10107-003-0454-y).
• 2010. Bertsimas, Iancu and Parrilo prove that affine policies are optimal for a class of multistage robust problems with one-dimensional uncertainty per stage and box uncertainty sets (doi:10.1287/moor.1100.0444).
• 2012. Bertsimas and Goyal, the source of this mission, prove that an affine policy is optimal for model (1) whenever $\mathcal U$ is a simplex (Theorem 1), and show that this exactness breaks down for slightly larger sets (doi:10.1007/s10107-011-0444-4).

Setting

Let $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$, $c\in\mathbb R^{n_1}_+$ and $d\in\mathbb R^{n_2}_+$. The problem $\Pi_{Adapt}(\mathcal U)$ of model (1) 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\ge 0,\ \ y(b)\ge 0\quad\forall b\in\mathcal U,$$

where inequalities between vectors are componentwise. A pair $(x,y)$ satisfying the constraints is feasible; its worst-case cost is $c^Tx+\max_{b\in\mathcal U}d^Ty(b)$. A feasible pair is optimal when its worst-case cost equals $z_{Adapt}(\mathcal U)$, and an affine policy is a second stage of the form $y(b)=Pb+q$ with $P\in\mathbb R^{n_2\times m}$, $q\in\mathbb R^{n_2}$, still required to be nonnegative on $\mathcal U$. The value $z_{Aff}(\mathcal U)$ is the same minimum restricted to affine policies.

A simplex in $\mathbb R^m$ is the convex hull

$$\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$$

of $m+1$ affinely independent points, that is, points for which $b^1-b^{m+1},\dots,b^m-b^{m+1}$ are linearly independent. The proof works with the $m\times m$ matrix $Q=[(b^1-b^{m+1})\cdots(b^m-b^{m+1})]$, the matrix $Y=[(y^*(b^1)-y^*(b^{m+1}))\cdots(y^*(b^m)-y^*(b^{m+1}))]$ of display (2), and the affine rule $\tilde y(b)=YQ^{-1}(b-b^{m+1})+y^*(b^{m+1})$. In Lean these are Qmat v, Ymat v g and interpolant v g, with vertices v : Fin (m+1) → Fin m → ℝ.

Formalization targets

Goal: Theorem 1

If $\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$ with affinely independent $b^j\in\mathbb R^m_+$ and $\Pi_{Adapt}(\mathcal U)$ is feasible, then there exist $\hat x$, $P\in\mathbb R^{n_2\times m}$ and $q\in\mathbb R^{n_2}$ such that

$$(\hat x,\ \hat y),\qquad \hat y(b)=Pb+q\ \ (b\in\mathcal U),$$

is an optimal solution of $\Pi_{Adapt}(\mathcal U)$, optimal among all (not only affine) two-stage solutions. In particular $z_{Aff}(\mathcal U)=z_{Adapt}(\mathcal U)$.

Milestones

The proof of Theorem 1 has no numbered lemma; the milestones are its displayed steps, in attack order:

1. $Q$ is invertible (PDF p. 6).
2. For $b=\sum_j\alpha_jb^j$ with $\sum_j\alpha_j=1$: $Q^{-1}(b-b^{m+1})=(\alpha_1,\dots,\alpha_m)^T$ (PDF p. 6).
3. $\tilde y\big(\sum_j\alpha_jb^j\big)=\sum_j\alpha_j\,y^*(b^j)$ (PDF pp. 6–7).
4. Displays (3)–(5): for any feasible $(x^*,y^*)$, the pair $(x^*,\tilde y)$ is feasible and every bound on the worst-case cost of $(x^*,y^*)$ also bounds that of $(x^*,\tilde y)$ (PDF p. 7).

Significance

The result. Theorem 1 identifies a class of uncertainty sets on which the tractable affine restriction is exact, for every constraint matrix $A$ and $B$ and every nonnegative cost. It is the positive anchor of the paper: Sections 3 and 4 show that with $m+3$ extreme points the best affine policy can already be worse by a factor $2-\delta$, and that on sets with exponentially many extreme points the gap can be $\Omega(m^{1/2-\delta})$; Section 6 uses a dominating simplex, on which affine policies are exact, to build an $O(\sqrt m)$-approximation for general $\mathcal U$. The theorem also says that on a simplex the whole adaptive problem reduces to $m+1$ scenario copies of a linear program.

Formalizing it. The result is proved on paper; no machine-checked version is known on Prove2Me. This mission produces the model (1) in Lean, the barycentric-coordinate identity for a simplex in matrix form, and a statement of optimality that asserts attainment of the minimum in (1), which the paper's proof takes for granted.

Difficulty

Two steps are not routine to formalize. First, the paper starts from "an optimal solution $x^*,y^*(b)$", that is, it assumes the minimum in (1) is attained. Over arbitrary functions $y(\cdot)$ this is not automatic; on a simplex it follows because the problem reduces to a finite linear program on the vertices, whose optimum is attained, but Mathlib has no theory of linear-programming attainment, so this reduction has to be built. Second, the affine-independence step needs the passage from affine independence of $m+1$ points to invertibility of the $m\times m$ matrix $Q$, and the identity $Q^{-1}(b-b^{m+1})=\alpha$ requires the barycentric coordinates and the inverse matrix to be matched index by index. The naive idea of comparing $z_{Aff}$ and $z_{Adapt}$ as real infima does not prove the goal: equality of the two infima says nothing about the existence of an optimal solution.

Formalization scope

Vectors in $\mathbb R^m$ are Fin m → ℝ, with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ. The paper's indices start at $1$, Lean's at $0$: $b^j$ is v (j-1) and $b^{m+1}$ is v (Fin.last m). The simplex is convexHull ℝ (Set.range v); it is compact, convex and, by affine independence, full-dimensional, so these standing assumptions of (1) are not stated separately. Nonnegativity of $\mathcal U$ is the hypothesis that all $m+1$ vertices are nonnegative (the page writes $j=1,\dots,m$, a slip for $m+1$). Feasibility of (1) is a hypothesis, as the paper assumes. Optimality (IsOptimalAdapt) means: feasible, and every worst-case cost bound achieved by any feasible two-stage solution is achieved by this one. The values $z_{Adapt}$ and $z_{Aff}$ are infima of the sets of achievable bounds; they are provided for reference and the goal does not depend on them.

The goal must not be replaced by $z_{Aff}(\mathcal U)\le z_{Adapt}(\mathcal U)$, by optimality among affine policies only, or by a version that assumes an optimal solution exists: each of these drops the content "there is an optimal solution and it is affine". The goal does not mention $Q$, $Y$ or the interpolant.

A complete development needs: linear-programming attainment for a finite system of linear inequalities with a cost bounded below (reusable well beyond this mission), the linear-algebra lemmas relating affine independence to an invertible edge matrix (reusable for barycentric coordinates in general), and the convex-hull representation of points of a simplex. Contributions of any of these as separate 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, 2012. doi: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(2), 351–376, 2004. doi: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(2), 363–394, 2010. doi:10.1287/moor.1100.0444
• A. Bemporad, F. Borrelli, M. Morari, Min–max control of constrained uncertain discrete-time linear systems, IEEE Trans. Autom. Control 48(9), 1600–1606, 2003. doi:10.1109/TAC.2003.816984

Motivation

A retailer choosing which products to display, or an airline choosing which fare classes to open, solves an assortment optimization problem: pick the set of offered products that maximizes expected revenue when customers choose among what is offered according to a discrete choice model. Under the multinomial logit model the answer has a simple form: an optimal assortment consists of the few highest-revenue products (Talluri and van Ryzin, 2004). The multinomial logit model, however, forces every pair of products to compete in the same way. The nested logit model relaxes this by grouping products into nests (brands, store sections, departure times) and letting a customer first choose a nest and then a product inside it.

Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) study how much of the multinomial logit structure survives under the nested logit model. Their first answer is the theorem this mission targets: when the nest dissimilarity parameters are at most one and no customer who chose a nest leaves it without buying, offering the top products of each nest is still optimal. The other missions of this series treat the cases where this fails: dissimilarity parameters above one (the problem becomes NP-hard) and nests with their own no-purchase option.

Setting

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

An assortment is a tuple $(S_1, \dots, S_m)$ of subsets $S_i \subseteq N$. 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, inside the nest, product $j$ with probability $v_{ij}/V_i(S_i)$. The expected revenue is

$$\Pi(S_1, \dots, S_m) = \sum_{i \in M} Q_i\, R_i(S_i) = \frac{\sum_{i \in M} V_i(S_i)^{\gamma_i} R_i(S_i)}{v_0 + \sum_{i \in M} V_i(S_i)^{\gamma_i}},$$

and problem (2) asks for $Z^* = \max \Pi(S_1, \dots, S_m)$ over all assortments. The nested-by-revenue assortment $N_{ij} = \{1, \dots, j\}$ collects the $j$ highest-revenue products of nest $i$, with $N_{i0} = \emptyset$ and $N_+ = \{0, 1, \dots, n\}$.

This mission works under the standing assumptions of §3 of the paper: competitive products, $\gamma_i \le 1$, and fully-captured nests, $v_{i0} = 0$, for every nest $i$.

Formalization targets

Goal: Theorem 4 (p. 15)

If $\gamma_i \le 1$ and $v_{i0} = 0$ for all $i \in M$, there exists an optimal solution $(S^*_1, \dots, S^*_m)$ of problem (2) such that

$$S^*_i = N_{ij} \ \text{ for some } j \in N_+, \qquad \text{for all } i \in M.$$

Milestones

1. The case $v_0 = 0$ (p. 14). Offering only the single product with the largest revenue $\max_{i} r_{i1}$ is optimal.
2. Proposition 2 (p. 14). If $S^*$ is optimal and $S^*_i \ne \emptyset$, then $R_i(S^*_i) \ge Z^*$.
3. Lemma 3 (p. 14). If $Z = \Pi(S)$, $R_i(S_i) \ge Z$ and some $j \in S_i$ has $r_{ij} < \gamma_i Z + (1-\gamma_i) R_i(S_i)$, removing $j$ strictly increases the expected revenue.
4. $g(\alpha) \le \gamma$ (p. 15). For $0 < \gamma \le 1$ and $0 < \alpha < 1$: $(1 - \alpha^{\gamma})/(\alpha^{\gamma-1} - \alpha^{\gamma}) \le \gamma$.
5. Revenue threshold (p. 15). Every $j \in S^*_i$ of an optimal $S^*$ has $r_{ij} \ge \gamma_i Z^* + (1-\gamma_i) R_i(S^*_i)$.
6. $h(\alpha) \ge \gamma$ (p. 16). For $0 < \gamma \le 1$ and $0 < \alpha < 1$: $(1 - \alpha^{\gamma})/(1 - \alpha) \ge \gamma$.
7. Exchange step (p. 15). If $S^*$ is optimal, $j \in S^*_i$, $k \notin S^*_i$ and $k < j$, then adding $k$ to $S^*_i$ keeps the assortment optimal.

A companion item (not a milestone) states the algorithmic consequence at the end of §3: solving the linear program (4) over the candidates $\{N_{ij} : j \in N_+\}$ and choosing in each nest a maximizer of problem (5) gives an optimal solution of (2).

Significance

Theorem 4 reduces problem (2), a search over $2^{mn}$ assortments, to $(n+1)^m$ nested-by-revenue combinations, and the paper then finds the best one with a linear program with $1 + m$ variables and $1 + m(1+n)$ constraints. It marks the exact boundary of the classical multinomial logit structure inside the nested logit model: the paper's §4 shows that a single nest with $\gamma_i > 1$ already breaks it, and that the general problem is NP-hard. The structural statement is also the base case for the approximation guarantees of §§5–6, which compare against nested-by-revenue assortments.

The theorem is proved in the paper; to our knowledge it has no machine-checked proof. A formal proof would supply a verified reduction from a combinatorial revenue maximization over the nested logit model to a polynomial-size search, with every boundary case (empty nests, $v_0 = 0$, ties in revenues) handled explicitly.

Difficulty

The obvious argument copies the multinomial logit proof: take an optimal assortment and swap a low-revenue product for a missing higher-revenue one. Under the nested logit model this exchange changes the nest's attraction $V_i(S_i)^{\gamma_i}$ non-linearly, so the revenue of the modified assortment is not an affine function of the change, and a simple swap can lower the expected revenue. The argument must instead control how adding or removing one product moves the nest weight relative to the nest revenue, and this is exactly where $\gamma_i \le 1$ enters, through two scalar inequalities in the ratio $\alpha$ of nest weights. With $\gamma_i > 1$ these inequalities fail and so does the theorem.

A second subtlety is ties: several optimal assortments may exist, and only some of them are nested by revenue. The statement asserts existence, not that every optimum has this form.

Formalization scope

All statements live in the namespace NestedLogitVariants.Competitive and share one definition file. Nests form a finite type ι with decidable equality; products are Fin n, indexed $0, \dots, n-1$, so $N_{ij}$ is nbr n j $= \{k : k < j\}$ with $j \le n$, and $j = 0$ gives $\emptyset$. Powers are Real.rpow, and $x / 0 = 0$, which gives $R_i(\emptyset) = 0$. Optimality of an assortment means its revenue is at least that of every assortment.

Standing assumptions carried as hypotheses: $v_0 \ge 0$, $v_{i0} \ge 0$, revenues ordered within each nest, and §3's $\gamma_i \le 1$ and $v_{i0} = 0$. Three pins are disclosed: $v_{ij} > 0$ (the paper allows zero-weight padding products, under which Proposition 2 fails), $r_{ij} \ge 0$, and $\gamma_i > 0$ (the paper's $\gamma_i \ge 0$; its convention $V_i(\emptyset)^{\gamma_i} = 0$ fails at $\gamma_i = 0$). The section's "without loss of generality $v_0 > 0$" is a hypothesis of Proposition 2, Lemma 3, the threshold, the exchange step and the LP item; the goal itself only assumes $v_0 \ge 0$, and the case $v_0 = 0$ is milestone 1. The two scalar inequalities are stated as inequalities, not as monotonicity claims.

The goal is not trivialized by any hypothesis: it assumes none of the milestones, and stating "some nested-by-revenue assortment exists" (always true) or "every optimal assortment is nested by revenue" (false under ties) would be a different theorem.

Needed infrastructure is light: finite sums, real powers, and concavity of $x \mapsto x^{\gamma}$ for $\gamma \le 1$. The scalar lemmas are reusable for other nested logit results. Proofs of any milestone are welcome independently.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 250–273, 2014. https://doi.org/10.1287/opre.2014.1256 (cited from the authors' revised manuscript of June 18, 2013)
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• D. McFadden, Modelling the choice of residential location, in A. Karlqvist et al. (eds.), Spatial Interaction Theory and Planning Models, North-Holland, 75–96, 1978.

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)

1. Problem (2) is equivalent to (3): $Z^*$ is the least $x$ for which some $y$ makes $(x, y)$ feasible for (3).
2. 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)$.
3. 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

Motivation

Assortment optimization asks which set of products a firm should offer when customers choose among the offered products according to a discrete choice model; it underlies shelf-space planning in retail and fare-class control in airline revenue management (Talluri and van Ryzin, 2004). Under the nested logit model products are grouped into nests, and a customer first picks a nest and then a product inside it. Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) map out how hard this problem is across variants of the model.

When every nest dissimilarity parameter is at most one and a customer who chose a nest always buys there, offering the top-revenue products of each nest is optimal (Theorem 4 of the paper, the subject of an earlier mission of this series). Once a customer may leave a nest without buying — a partially-captured nest — that structure breaks and the problem becomes NP-hard (Theorem 8). This mission targets the paper's response: a small, explicitly constructed family of candidate assortments per nest from which a linear program recovers a solution within a factor of two of optimal.

Setting

There are $m$ nests $M$ and, in each nest, $n$ products $N = \{1, \dots, n\}$. Product $j$ of nest $i$ has a revenue $r_{ij} \ge 0$ and a preference weight $v_{ij} > 0$, with $r_{i1} \ge \dots \ge r_{in}$. Nest $i$ has a dissimilarity parameter $\gamma_i > 0$ and a within-nest no-purchase weight $v_{i0} \ge 0$; $v_0 \ge 0$ is the weight of choosing no nest. For an assortment $S_i \subseteq N$,

$$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,$$

and the expected revenue of $(S_1, \dots, S_m)$ is $\Pi = \sum_i V_i(S_i)^{\gamma_i} R_i(S_i) / (v_0 + \sum_i V_i(S_i)^{\gamma_i})$. The optimal expected revenue $Z^*$ is the optimal value of the linear program

$$\text{(3)}\quad \min\ x \quad\text{s.t.}\quad 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)\ \ \forall S_i \subseteq N,\ i \in M,$$

and problem (4) is the same program with the second family of constraints imposed only for a chosen collection of candidate assortments in each nest.

Throughout, $\gamma_i \le 1$ for every nest and the $v_{i0}$ are arbitrary. For a capacity $\epsilon_i \ge 0$, the knapsack value $K_i(\epsilon_i)$ is the largest $\sum_{j \in S} r_{ij} v_{ij}$ over assortments $S$ with $\sum_{j \in S} v_{ij} \le \epsilon_i$ (display (9)). Its continuous relaxation (11) allows fractional $z_{ij} \in [0, \mathbf 1(v_{ij} \le \epsilon_i)]$ under the same capacity. The greedy solution $\hat z_i(\epsilon_i)$ of (11) fills the capacity with the products of weight at most $\epsilon_i$ in revenue order, each fully while it fits and the next one fractionally, and

$$\hat S_i(\epsilon_i) = \{ j \in N : \hat z_{ij}(\epsilon_i) = 1 \}.$$

Problem (10) replaces the per-assortment constraints of (3) by $y_i \ge \max_{\epsilon_i \ge 0} (v_{i0}+\epsilon_i)^{\gamma_i}[K_i(\epsilon_i)/(v_{i0}+\epsilon_i) - x]$.

Formalization targets

Goal: Theorem 10 (p. 24)

Let $(\hat x, \hat y)$ be an optimal solution of (4) with candidate collections $\{\hat S_i(\epsilon_i) : \epsilon_i \in [0,\infty]\} \cup \{\{j\} : j \in N\}$. Then

$$(2\hat x,\ 2\hat y) \ \text{ is feasible for (3).}$$

Milestones

1. Per-nest identity (proof of Lemma 9, p. 23). For $x \ge 0$, $\max_{S_i} V_i(S_i)^{\gamma_i}(R_i(S_i) - x) = \max_{\epsilon_i \ge 0}(v_{i0}+\epsilon_i)^{\gamma_i}[K_i(\epsilon_i)/(v_{i0}+\epsilon_i) - x]$.
2. Lemma 9 (p. 23). Problems (3) and (10) have the same optimal solutions.
3. Relaxation (p. 23). Every feasible point of (9) is feasible for (11), so $\hat K_i(\epsilon_i) \ge K_i(\epsilon_i)$.
4. Greedy solution (pp. 23–24). $\hat z_i(\epsilon_i)$ is optimal for (11) and has at most one fractional component.
5. Sign (A.3, p. 45). $\hat x \ge 0$.
6. Inequalities (28) and (29) (A.3, pp. 45–46). In both cases — $\hat z_i(\epsilon)$ with and without a fractional component — $2\hat y_i \ge (v_{i0}+\epsilon)^{\gamma_i}[K_i(\epsilon)/(v_{i0}+\epsilon) - 2\hat x]$.

Two further statements accompany the goal: the factor-two revenue guarantee obtained from Theorem 10 and Theorem 1 of the paper, and the fact that every $\hat S_i(\epsilon_i)$ is one of the at most $1 + n^2$ assortments $N^k_{ij}$, the first $j$ products by revenue among the $k$ lightest.

Significance

Theorem 10 turns an NP-hard assortment problem into a linear program with $1 + m$ variables and $1 + m(1 + n + n^2)$ constraints whose solution is within a factor of two of optimal. The construction is explicit: the candidates are defined by a greedy rule, not by an optimization oracle. The same template, a restricted linear program whose doubled optimum is feasible for the full one, is reused in §6 of the paper for the most general instances, and Lemma 9's knapsack reformulation is the link to the classical approximation theory of knapsack problems (Williamson and Shmoys, 2011).

The theorem is proved in the paper. No machine-checked proof of it, of Lemma 9, or of greedy optimality for the continuous knapsack with an eligibility bound exists on the platform. Formalizing it yields a checked factor-two guarantee and a reusable fractional-knapsack development.

Difficulty

The obvious argument would compare the restricted program (4) with (3) constraint by constraint. That fails: (3) has one constraint per subset of products, and most subsets are not candidates. The comparison has to pass through the knapsack reformulation (10), which requires showing that a maximum over all subsets equals a maximum over a one-dimensional capacity parameter, using $\gamma_i \le 1$ and $x \ge 0$ in an essential way. The second obstacle is that the greedy assortment $\hat S_i(\epsilon_i)$ keeps only the fully taken products, so its value can fall short of the continuous knapsack value, and no single candidate assortment need attain the knapsack bound. With dissimilarity parameters above one the monotonicity behind the reformulation is lost, and §6 of the paper needs a different factor.

Formalization scope

Products are Fin n (indices $0, \dots, n-1$), nests a finite type, and every quantity is real. Powers are Real.rpow; $x/0 = 0$, which gives $R_i(\emptyset) = 0$. An optimal solution of a linear program is a feasible pair whose $x$ is minimal among feasible pairs. The constraint "$y_i \ge \max_{\epsilon_i \ge 0}(\dots)$" of (10) is stated in constraint form, for every $\epsilon_i \ge 0$, so no real supremum is taken. $K_i(\epsilon)$ is defined for $\epsilon \ge 0$ only; its placeholder value for $\epsilon < 0$ is never used. Ties in revenue (and, for $N^k_{ij}$, in weight) are broken by index. The candidate collection is taken over real $\epsilon_i \ge 0$; $\epsilon_i = \infty$ adds nothing, since every capacity of at least $\sum_j v_{ij}$ already gives $\hat S_i = N$.

Standing assumptions and added hypotheses: $\gamma_i \le 1$ for every nest (the section's assumption) on the goal and on every model milestone; the pins $v_{ij} > 0$, $r_{ij} \ge 0$, $\gamma_i > 0$ and the revenue ordering, shared by the series; $n \ge 1$ on Lemma 9, on $\hat x \ge 0$ and on (28)/(29), the paper's nonempty $N$; and $v_0 > 0$ on the factor-two revenue guarantee, where Theorem 1 of the paper fails without it.

The greedy assortments $\hat S_i(\epsilon_i)$ are defined explicitly. Quantifying over arbitrary optimal solutions of (11) instead would change the candidate collection and is not the paper's theorem. The goal states feasibility for the full program (3) and does not mention knapsack values, the greedy solution or the case split. A formalization that weakens the conclusion to feasibility for (10), or that drops the singletons from the candidate collection, is not a solution.

Needed infrastructure: fractional knapsack optimality of the greedy rule with an eligibility bound, monotonicity of $t \mapsto t^{\gamma}$ and $t \mapsto t^{\gamma - 1}$ for $\gamma \le 1$, and finite maximization over subsets. The fractional-knapsack lemmas are reusable beyond this mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.

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). DOI 10.1287/opre.2014.1256
• K. T. Talluri, G. J. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 15–33, 2004. DOI 10.1287/mnsc.1030.0147
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. DOI 10.1017/CBO9780511921735

Motivation

Robust optimization protects a decision against every realization of uncertain data in a prescribed uncertainty set. The standard approach replaces the uncertain constraints by a deterministic robust counterpart and solves that counterpart directly (Ben-Tal, El Ghaoui, Nemirovski, Robust Optimization, 2009). The counterpart is often a harder problem than the original: a robust linear program with ellipsoidal uncertainty becomes a second-order cone program, and a robust quadratic program can become a semidefinite program. A practitioner who has an efficient, specialised solver for the nominal problem may therefore have no efficient solver for its robust version.

Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) ask whether the robust problem can be solved by repeatedly calling a solver of the nominal problem, with the number of calls independent of the dimension. Their first answer, the dual-subgradient meta-algorithm of §3.1, does so whenever the constraints are concave in the noise and the uncertainty set is convex. It is a primal–dual scheme: an online-learning algorithm picks the noise, and the nominal solver answers. This mission formalizes that result, Theorem 3.

Setting

Let $\mathcal D\subseteq\mathbb R^n$ be a convex domain, $\mathcal U\subseteq\mathbb R^d$ a convex uncertainty set, and $f_1,\dots,f_m:\mathbb R^n\times\mathbb R^d\to\mathbb R$ constraint functions. The robust feasibility problem (3) is

$$\exists\,x\in\mathcal D:\qquad f_i(x,u_i)\le 0\quad\forall u_i\in\mathcal U,\ i=1,\dots,m .$$

(An objective is handled by binary search on its value, so feasibility is the core question.) A point $x\in\mathcal D$ is an $\epsilon$-approximate solution if $f_i(x,u)\le\epsilon$ for all $u\in\mathcal U$ and all $i$.

An $\epsilon$-approximate oracle $\mathcal O_\epsilon$ (Figure 1) takes a noise vector $u=(u_1,\dots,u_m)\in\mathcal U^m$ and either returns some $x\in\mathcal D$ with $f_i(x,u_i)\le\epsilon$ for all $i$, or answers "infeasible", which it may do only if no $x\in\mathcal D$ has $f_i(x,u_i)\le 0$ for all $i$.

The standing assumptions of §3.1 are: each $f_i(\cdot,u)$ is convex on $\mathcal D$; each $f_i(x,\cdot)$ is concave on $\mathcal U$ for $x\in\mathcal D$; $D\ge\|u-v\|_2$ for all $u,v\in\mathcal U$; and $\|\nabla_u f_i(x,u)\|_2\le G$ for $x\in\mathcal D$, $u\in\mathcal U$. Write $P$ for the Euclidean projection onto $\mathcal U$.

Algorithm 1 sets $T=\lceil G^2D^2/\epsilon^2\rceil$ and $\eta=D/(G\sqrt T)$, starts from $u^0_1,\dots,u^0_m\in\mathcal U$, and for $t=1,\dots,T$ updates

$$u^t_i=P\bigl(u^{t-1}_i+\eta\,\nabla_u f_i(x^{t-1},u^{t-1}_i)\bigr),\qquad x^t=\mathcal O_\epsilon(u^t_1,\dots,u^t_m),$$

stopping with "infeasible" as soon as the oracle says so, and otherwise returning $\bar x=\frac1T\sum_{t=1}^T x^t$. In Lean these are alg1T, alg1Eta, alg1U, alg1X, alg1Output and alg1Calls in the namespace OracleRO.DualSubgrad.

Formalization targets

Goal: Theorem 3 (p. 7)

For every $\epsilon$-approximate oracle,

$$\text{output}=\text{"infeasible"}\ \Longrightarrow\ \neg\,\exists x\in\mathcal D\ \forall i\ \forall u\in\mathcal U:\ f_i(x,u)\le 0,$$ $$\text{output}=\bar x\ \Longrightarrow\ \bar x\in\mathcal D\ \text{ and }\ f_i(\bar x,u)\le 2\epsilon\ \ \forall i,\ \forall u\in\mathcal U,$$

and the number of oracle calls is at most $\lceil G^2D^2/\epsilon^2\rceil$.

Milestones

1. Lemma 1 (p. 5, Zinkevich 2003): projected online gradient ascent with step $\eta=D/(G\sqrt T)$ on concave rewards has regret $\sum_t f_t(x^*)-\sum_t f_t(x_t)\le GD\sqrt T$ for every $x^*$ in the decision set.
2. (6) (p. 7): if a point is returned, $\frac1T\sum_{t=1}^T f_i(x^t,u^t_i)\le\epsilon$ for every $i$.
3. (7) (p. 8): for every $i$ and $u\in\mathcal U$, $\frac1T\sum_t f_i(x^t,u)-\frac1T\sum_t f_i(x^t,u^t_i)\le GD/\sqrt T\le\epsilon$.
4. Final inequality of the proof (p. 8): $f_i(\bar x,u)\le\frac1T\sum_t f_i(x^t,u)$ for $u\in\mathcal U$.

Significance

The result. Theorem 3 turns any approximate solver of the nominal problem into an approximate solver of its robust counterpart, at a cost of $\lceil G^2D^2/\epsilon^2\rceil$ solver calls, a number that depends on the geometry of $\mathcal U$ and the sensitivity of the constraints to the noise but not on $n$, $d$ or $m$. It is the prototype of the paper's oracle-based reductions: the same primal–dual template, with a different online learner, gives the dual-perturbation algorithm of §3.2–3.3 for non-convex uncertainty sets, and the applications of §4 (robust linear programs, quadratic programs, semidefinite programs) instantiate it.

Formalizing it. The theorem is proved in the paper; none of it is machine-checked. A formal development adds a checked statement of the reduction with an explicit call count in place of the paper's $O(\cdot)$, and a reusable regret bound for projected online gradient ascent on concave rewards (Lemma 1), which the paper quotes from Zinkevich without proof and which many other online-learning results rest on.

Difficulty

The obvious argument for the dual side fails at one point: in round $t$ the primal point $x^t$ is computed from $u^t$, so the reward $f_i(x^t,\cdot)$ that the dual player faces depends on its own current move. A regret bound that assumed rewards fixed in advance, or drawn independently of the learner's play, would not apply. Lemma 1 must be used in its adversarial form, valid for every sequence of reward functions, including adaptively chosen ones. A second point is that the projection step requires the variational characterization of a nearest point in a convex set, which a mere "map into $\mathcal U$" does not provide.

Formalization scope

Points are elements of EuclideanSpace ℝ (Fin k), so every norm is the $\ell_2$ norm. The projection is a predicate IsProjOnto U P (each $P(y)$ is a nearest point of $\mathcal U$ to $y$), not a construction; the oracle is a function (Fin m → E d) → Option (E n) with none for "infeasible", constrained by the predicate IsApproxOracle on inputs in $\mathcal U^m$. The goal is quantified over every oracle meeting that specification. The gradient $\nabla_u f_i(x,u)$ is a given map gradU with HasGradientAt at points of $\mathcal U$; no differentiability in $x$ is assumed. Rounds are indexed by natural numbers with index $0$ for the initialization; the starting primal point $x^0\in\mathcal D$, used by the first update and left undefined by the algorithm, is an input. Hypotheses $D>0$ and $G>0$ are added so that $\eta$ and $T\ge1$ are meaningful. Maxima over $\mathcal U$ are stated as "for every $u\in\mathcal U$".

Explicit instantiations and corrections:

• The paper's "$O(G^2D^2/\epsilon^2)$ calls" is stated as at most $\lceil G^2D^2/\epsilon^2\rceil$ calls (one call per round, $T$ rounds).
• Lemma 1's "$G\ge\max_t\|f_t(x_t)\|$" is read as the gradient bound $\|\nabla f_t(x_t)\|\le G$, as the same sentence describes it.
• The proof's "Combining (10) and (12)" refers to (6) and (7).

Trivializing formalizations are ruled out: an oracle specification under which "infeasible" is never returned, or an output that is not the average of the oracle's answers, would not be Theorem 3. The "infeasible" conclusion is about the robust problem, not the nominal one.

A complete development needs the variational inequality for nearest points in a convex set, the gradient (supergradient) inequality for a concave function differentiable at a point of a convex set, Zinkevich's telescoping argument, and Jensen's inequality for finite averages. The first two and Lemma 1 are reusable beyond this mission. Proofs of the milestones, in any order, are welcome.

Selected references

• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-Based Robust Optimization via Online Learning, arXiv:1402.6361v1, 2014; Operations Research 63(3), 2015. https://arxiv.org/abs/1402.6361v1
• M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016. https://arxiv.org/abs/1909.05207