The OR Formalization Drive

Motivation

A retailer, an airline or an online platform decides which products to show a customer. Showing more is not always better: a customer who would have bought an expensive product may switch to a cheap one once it is offered. The assortment problem asks for the set of products that maximises expected revenue, given a model of how customers choose. It is a central problem of revenue management (Talluri and van Ryzin, 2004), and it is NP-hard even for mixtures of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, 2014).

The standard heuristic in practice is revenue-ordered assortments: sort the products by price and only consider the sets consisting of the most expensive products down to some threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin, 2004), but not in general. Berbeglia and Joret (arXiv:1606.01371) ask how much revenue the heuristic can lose under every reasonable choice model, and answer with guarantees that depend only on the prices.

Timeline:

• 2004: Talluri and van Ryzin prove revenue-ordered assortments optimal under the multinomial logit model.
• 2014: Rusmevichientong et al. show NP-hardness of the assortment problem for mixtures of logits, and prove that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit models.
• 2016–2019: Berbeglia and Joret prove the guarantees $1/k$ and $1/(1+\ln(r_k/r_1))$ under any regular choice model and show them tight (arXiv v1 2016, v3 2019; Algorithmica 2020). Aouad, Farias, Levi and Segev (2018) show that under random utility models no efficient algorithm does essentially better than these ratios.

Setting

There is a finite nonempty set $\mathcal C$ of products. For a choice set $S\subseteq\mathcal C$, $\mathcal P(x,S)$ is the probability that a customer offered $S$ buys product $x$, and $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ is the probability that the customer buys nothing. The system $\mathcal P$ is a regular discrete choice model if

1. $\mathcal P(x,S)\ge0$ for every $x\in\mathcal C\cup\{0\}$;
2. $\mathcal P(x,S)=0$ whenever $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$.

Axiom 4, regularity, says that adding products never makes a given product, or leaving without buying, more likely. Every random utility model is regular.

Each product has a positive price $r(x)>0$. The revenue of $S$ is $\operatorname{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\operatorname{rev}(S)$. Let $0<r_1<\cdots<r_k$ be the distinct prices, so $k$ counts price levels and not products, and set $r_0=0$. The revenue-ordered assortments are $S_i=\{x\in\mathcal C : r(x)\ge r_i\}$, $i=1,\dots,k$, and the heuristic earns

$$\mathrm{RO}=\max_{1\le i\le k}\operatorname{rev}(S_i).$$

Formalization targets

Goal: Theorem 3.2

$$\mathrm{OPT}\;\le\;\Big(\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\Big)\,\mathrm{RO} \qquad\text{and}\qquad \sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\;\le\;1+\ln\frac{r_k}{r_1}.$$

The goal fixes no constant beyond the paper's own quantities. Both parts are required: the sum form is the sharper bound, and the paper shows it is attained (Theorem 3.4, a later mission of this series).

Milestones

• Lemma 2.1: $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$.
• Inequality (5): $\operatorname{rev}(S_i)\ge r_i\sum_{x\in S^*\cap S_i}\mathcal P(x,S^*)$ for every $S^*$ and $i\in[k]$.
• Theorem 3.1: $\mathrm{OPT}\le k\cdot\mathrm{RO}$.
• Rearrangement (proof of Theorem 3.2): $\operatorname{rev}(S^*)=\sum_{\ell}(r_\ell-r_{\ell-1})\sum_{x\in S^*\cap S_\ell}\mathcal P(x,S^*)$, and $\operatorname{rev}(S^*)\le\sum_\ell\frac{r_\ell-r_{\ell-1}}{r_\ell}\operatorname{rev}(S_\ell)$.
• Logarithmic bound: $\sum_{\ell=1}^k\frac{a_\ell-a_{\ell-1}}{a_\ell}\le1+\ln(a_k/a_1)$ for $0=a_0<a_1<\cdots<a_k$.

Significance

The theorem shows that a pricing-only quantity controls the loss of the most common heuristic in revenue management, uniformly over all regular choice models, including every random utility model, mixtures of logits and Markov chain models. Combined with the hardness result of Aouad et al., it shows that revenue-ordered assortments achieve essentially the best ratio, as a function of $k$ or of $r_k/r_1$, that an efficient algorithm can achieve. The same analysis transfers to the envy-free pricing and Stackelberg problems studied in the later sections of the paper.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a Lean formalization of regular choice models, the revenue-ordered heuristic and its two guarantees, on which the paper's tightness examples, the purchase-probability bound (Theorem 3.3) and the applications to pricing can build.

Difficulty

The argument is short, but two points are easy to get wrong. First, revenues of $S_i$ and of an optimal $S^*$ involve choice probabilities evaluated at different sets, so the comparison must pass through $S^*\cap S_i$, using regularity once for products and once for the no-purchase option. A model that only assumes regularity for products does not satisfy the theorem. Second, the bound runs over distinct price levels, not products, and the first summand uses the convention $r_0=0$; indexing by products or dropping $r_0$ gives a different quantity. The comparison of the sum with $\ln(r_k/r_1)$ is a Riemann-sum estimate for $\int dt/t$ and needs a real-analysis lemma not phrased this way in Mathlib.

Formalization scope

• Products are a finite nonempty type C with decidable equality; choice sets are Finset C. The choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S = 1 - ∑ x ∈ S, P x S.
• IsRegular P carries axioms (i)–(iv), with (i) and (iv) each split into a product case and a no-purchase case. The no-purchase case of (i) is redundant with (iii) and is kept to match the page.
• r : C → ℝ with the hypothesis ∀ x, 0 < r x. revenue P r S is $\operatorname{rev}(S)$ and opt P r is the maximum over all Finset C (Finset.sup'), including the empty set.
• Price levels are 1-based: level r i is $r_i$ for $1\le i\le k$ and level r 0 = 0; numVals r is $k$, the number of distinct values. roSet r i is $S_i$; roValue P r is the maximum over $i\in\{1,\dots,k\}$ only.
• Approximation guarantees are stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$, never as a ratio. $\ln$ is Real.log, applied to $r_k/r_1\ge1$.
• Ruled out: a maximum over all subsets in place of $\mathrm{RO}$ (which makes the bound trivial), a regularity axiom without its no-purchase case, the logarithmic form alone in place of the sum form, and any specific choice model (logit, Markov chain, random utility) in place of an arbitrary regular $\mathcal P$.

Needed infrastructure: finite sums over price levels and summation by parts, the comparison of $(b-a)/b$ with $\ln(b/a)$, and the sorted enumeration of a finite set of reals (Finset.orderEmbOfFin). The regular model and the revenue-ordered sets are shared with the other missions of this series. Contributions of any milestone, alternative proofs of the logarithmic bound, and proofs that specific choice models are regular are welcome.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• A. Aouad, V. Farias, R. Levi and D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1724
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191

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

1. 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.
2. 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$.
3. 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$.
4. 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$.
5. 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

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

1. Lemma 4: $z_{\mathrm{Adapt}}(\mathcal U)\le1$, with a feasible solution attaining cost at most $1$.
2. Lemma 5: $\mathcal U$ is permutation-invariant under every $\sigma\in S^m$.
3. Lemma 6: the permuted instance $\mathcal I(\sigma)$ of (22) equals $\mathcal I$.
4. Lemma 7: if $y(b)=Pb+q$ is an optimal affine solution, so is $y^\sigma(b)=P^\sigma b+q^\sigma$.
5. Lemma 8: some optimal affine solution has $\hat P_{ij}=\mu$ ($i\ne j$), $\hat P_{jj}=\theta$, $\hat q_j=\lambda$.
6. 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

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

1. Lemma 12. $\mathcal U^0$ dominates $\mathcal U$: every $b\in\mathcal U$ has some $b'\in\mathcal U^0$ with $b\le b'$.
2. 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).$$

3. 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