Linear Optimization

Why space-constrained assortments matter

A retailer choosing which products to display faces a physical limit: different products consume different amounts of shelf space. Under a nested logit choice model, the value of an assortment also depends on how customers substitute among products within a nest and on whether they leave without buying. Gallego and Topaloglu study this combination of choice and feasibility constraints in Constrained Assortment Optimization for the Nested Logit Model. Their authors' manuscript of September 11, 2013 is the numbered source for this mission. Its §5 isolates a finite family of candidate assortments for each nest, despite the per-nest space-constrained problem being a knapsack problem. A small family matters because the paper's earlier Theorem 4 can then combine the families across nests while controlling expected revenue.

The paper contrasts this case with cardinality constraints. When every product consumes one unit, the per-nest optimization can be solved exactly by a short list of candidates. General space requirements turn it into a knapsack problem, so the paper gives quantitative approximation factors instead. The factor improves when no single product occupies much of a nest's capacity. These statements and their dependencies occur in §§5.1–5.2, pp. 19–22 of the manuscript.

Products, nests, and the parameterized problem

There is a finite set of nests $M$ and a nonempty finite product set $N=\{1,\ldots,n\}$ in each nest. In nest $i$, product $j$ has preference weight $v_{ij}>0$, real revenue $r_{ij}$, and space requirement $w_{ij}>0$. The nest's capacity is $c_i$, and each product fits by itself: $w_{ij}\le c_i$. An assortment $S_i\subseteq N$ is feasible when its total space requirement is at most $c_i$. The empty assortment is feasible and gives zero revenue. The full nested logit model has a no-purchase preference weight $v_0$ and a dissimilarity parameter $\gamma_i\in(0,1]$ for each nest; these parameters are relevant to the cross-nest expected revenue, but the local problem of this mission uses only one nest's product data.

For an assortment $S_i$, write $V_i(S_i)=\sum_{j\in S_i}v_{ij}$ and $R_i(S_i)=\sum_{j\in S_i}v_{ij}r_{ij}/V_i(S_i)$, with $R_i(\varnothing)=0$. The paper's parameterized local problem, problem (7), maximizes $V_i(S_i)(R_i(S_i)-u)$ over feasible assortments for each $u\ge0$. Since the within-nest no-purchase weight is zero, equation (8) gives its equivalent sum of product utilities:

$$V_i(S_i)(R_i(S_i)-u)=\sum_{j\in S_i}v_{ij}(r_{ij}-u).$$

Problem (10) is this objective written as a zero-one knapsack: each product decision is zero or one and $\sum_jw_{ij}x_{ij}\le c_i$. Its LP relaxation permits $0\le x_{ij}\le1$. At parameter $u$, the product's utility-to-space ratio is $f_{ij}(u)=v_{ij}(r_{ij}-u)/w_{ij}$. Rounding a relaxation solution down retains precisely the products with $x_{ij}=1$. The candidate family also contains each singleton assortment $\{j\}$.

Formalization targets

Theorem 6 asserts that a collection $\mathcal A_i$ of at most quadratic size includes a two-approximate solution to problem (7) for every $u\ge0$. Here an assortment $S$ is $\alpha$-approximate at $u$ if it is feasible and $\alpha V_i(S)(R_i(S)-u)$ is at least the objective of every feasible assortment. The $O(n^2)$ statement is pinned to the explicit bound $|\mathcal A_i|\le(n+1)^2$.

$$\forall u\ge0,\quad \exists S\in\mathcal A_i:\quad \forall T\in C_i,\quad V_i(T)(R_i(T)-u)\le 2V_i(S)(R_i(S)-u).$$

The §5.2 target keeps the same collection and adds the finer guarantee whenever each product is small relative to capacity. For every $\epsilon\in[0,1)$ such that $w_{ij}\le\epsilon c_i$ for all $j$, and for every $u\ge0$, some member of $\mathcal A_i$ satisfies

$$\forall T\in C_i,\quad V_i(T)(R_i(T)-u)\le\frac{1}{1-\epsilon}V_i(S)(R_i(S)-u).$$

The two members need not be the same, but the finite family is fixed before $u$ and $\epsilon$ are chosen. Together the claims yield the paper's factor $\min\{2,1/(1-\epsilon)\}$. The main goal formalizes both parts; Theorem 6 and the paper's intermediate statements are milestones.

What the guarantees supply

The local result converts infinitely many parameter values into a finite search domain. Theorem 4 of the same paper says that if each nest has candidates containing an $\alpha$-approximate local solution for every $u\ge0$, then some cross-nest combination obtains at least the optimal expected revenue divided by $\alpha$. Theorem 2 relates the best combination of candidates to a linear program. Thus the finite collection in this mission supplies the local ingredient needed for the paper's global factor two, or the smaller factor under the product-size condition. These consequences are stated in the paragraphs immediately following Theorem 6 and the §5.2 conclusion.

The paper already proves these mathematical results. This mission asks for machine-checked proofs of its specific knapsack relaxation, rounding inequality, and approximation statements. It also creates reusable finite-knapsack definitions and explicit interfaces between the paper's local objective and the published nested logit model. The goal and milestones here remain open Lean statements until solvers provide proofs; compiling a statement with sorry checks its syntax and types, not its mathematical validity.

Where the argument is delicate

The parameter $u$ ranges over a continuum, yet one family of bounded size must work for all of it. Different values of $u$ change the objective coefficients and may change which products belong in an LP optimum. At ties or sign changes, the optimum need not be unique, so a statement about a particular chosen solution requires care. A second difficulty is the fractional LP coordinate: its value can exceed the rounded set's objective, and the refined factor uses a comparison between its utility and the space already occupied. The displayed chain in §5.2 contains quotients that can have zero denominators; the formal milestone states its endpoint inequality directly. A fractional product with zero utility need not force capacity to be filled, which is why the capacity-consumption milestone states positive utility explicitly.

Formalization scope

The existing NestedLogitVariants.LP.Model supplies the nested logit instance and its $V_i$ and $R_i$ functions. A general finite continuous-knapsack definition is separate from the paper-specific assortment data. Products use Fin n, nests use a finite type, and assortments use finite sets. The empty finite set represents $\bar 0$. The model's within-nest no-purchase weight is fixed to zero, as in the manuscript's main local formulation. Revenues remain arbitrary real numbers; there is no assumption that they are nonnegative or sorted. The capacity and product space requirements are real numbers, with $w_{ij}>0$ and $w_{ij}\le c_i$. Positive preference weights and nonempty $N$ are explicit. No condition on $\gamma_i$ or $v_0$ is needed for this local problem (7).

The candidate family is a finite set of rounded LP optima and all singletons. Its size is bounded before $u$ and $\epsilon$ are quantified. Each approximation compares against feasible integer assortments using problem (7), including the empty assortment. The LP optimum itself is never substituted for the integer comparator. General unequal space requirements remain in scope. Contributions that formalize the parametric LP behavior, its one-fractional-coordinate optimum, and the paper's two rounding guarantees fit this mission.

Selected references

• Guillermo Gallego and Huseyin Topaloglu, Constrained Assortment Optimization for the Nested Logit Model, Management Science 60(10), 2014, DOI 10.1287/mnsc.2014.1931. Authors' manuscript, September 11, 2013, especially pp. 7–8 and 19–22.

Motivation

A constraint satisfaction problem (CSP) asks whether variables can be assigned values from a finite domain so that every constraint, drawn from a fixed list of allowed relations, is satisfied. A promise CSP (PCSP) relaxes the question: given two templates $\mathbf A$ and $\mathbf B$ with a homomorphism $\mathbf A\to\mathbf B$, distinguish instances satisfiable in $\mathbf A$ from instances not even satisfiable in the weaker $\mathbf B$. Approximate graph colouring (colour a graph with more colours than its chromatic number) is the standard example. For CSPs, the resolution of the Feder–Vardi dichotomy conjecture by Bulatov and Zhuk (FOCS 2017) ties tractability to the existence of polymorphisms satisfying non-trivial identities; for PCSPs no such dichotomy is known, and the question of which polymorphism families yield algorithms is open in general.

A polymorphism of a PCSP is a function $f:A^L\to B$ mapping tuples of rows satisfying the strict constraints to columns satisfying the weak ones. Brakensiek, Guruswami, Wrochna and Živný (arXiv:1907.04383v3, SIAM J. Comput. 2020) give a single algorithm, BLP+Affine, that decides every PCSP with infinitely many symmetric polymorphisms, and extend it to block-symmetric polymorphisms. As a corollary the same algorithm solves all tractable Boolean CSPs of Schaefer's dichotomy (2-SAT, Horn-SAT and its dual, linear equations mod 2).

Timeline, as recorded in the paper's introduction:

• 2012: Kun, O'Donnell, Tamaki, Yoshida and Zhou (ITCS 2012): with symmetric polymorphisms of all arities, the Basic LP alone decides the CSP; with only some arities (e.g. odd majorities) it does not.
• 2017: Austrin, Guruswami and Håstad classify $(2+\epsilon)$-SAT and introduce polymorphisms for PCSPs (SIAM J. Comput. 46(5), 2017).
• 2018–2019: Brakensiek and Guruswami study PCSPs through polymorphisms; their SODA 2019 algorithm (arXiv:1807.05194) solves the search version for PCSPs with structured symmetric polymorphisms (threshold, threshold-periodic, regional), combining an LP over $\mathbb Z[\sqrt2]$ with an affine relaxation over a finite ring.
• 2019: Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970) show that the identities satisfied by polymorphisms, captured by minion homomorphisms, determine the complexity of a PCSP.
• 2019–2020: the present paper. Theorem 2 needs only that $f$ be symmetric, with no structure beyond that; Theorem 3 handles any number of blocks; Theorem 4 characterizes exactly the PCSPs that BLP+Affine solves.

Setting

A signature $\tau$ is a set of symbols $R$ with arities $\mathrm{ar}(R)$. A relational structure $\mathbf A$ on a finite domain $A$ gives, for each $R$, a relation $R^{\mathbf A}\subseteq A^{\mathrm{ar}(R)}$. A homomorphism $\mathbf A\to\mathbf B$ is a map $\sigma:A\to B$ sending every tuple of $R^{\mathbf A}$, componentwise, into $R^{\mathbf B}$; $(\mathbf A,\mathbf B)$ is a promise template when one exists.

An instance $X$ has variables $x_1,\dots,x_n$ and constraints $c_j=(R_j,\bar x_j)$, $j\in[m]$, where $\bar x_j$ is a tuple of $\mathrm{ar}(R_j)$ variables. $X$ is satisfiable in $\mathbf A$ if some assignment sends every $\bar x_j$ into $R_j^{\mathbf A}$.

A polymorphism of $(\mathbf A,\mathbf B)$ of arity $L$ is $f:A^L\to B$ such that for every $R$ and every $L\times\mathrm{ar}(R)$ matrix whose rows lie in $R^{\mathbf A}$, applying $f$ to each column gives a tuple in $R^{\mathbf B}$. It is symmetric if it is invariant under all permutations of its $L$ arguments.

The Basic LP $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$ has rational unknowns $w_i(a)\ge0$, a distribution on $A$ for each variable, and $p_j(y)\ge0$, a distribution on $R_j^{\mathbf A}$ for each constraint, linked by the marginal conditions $\sum_{y:\,y_k=a}p_j(y)=w_i(a)$ when $x_i$ is the $k$-th variable of $\bar x_j$. The affine relaxation $\mathrm{Aff}_{\mathbb Z}(X,\mathbf A)$ is the same system of equations in integer unknowns $r_i(a)$, $q_j(y)$, with no sign constraints.

The BLP+Affine algorithm (Figure 1) finds a relative interior point $(w,p)$ of $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$, rejecting if there is none; restricts the affine system to $\mathrm{Aff}'_{\mathbb Z}(X,\mathbf A)$ by forcing $r_i(a)=0$ wherever $w_i(a)=0$ and $q_j(y)=0$ wherever $p_j(y)=0$; and accepts if and only if the restricted system has an integer solution. It correctly solves $\mathrm{PCSP\text{-}Decision}(\mathbf A,\mathbf B)$ (Definition 1) if it accepts every instance satisfiable in $\mathbf A$ and rejects every instance unsatisfiable in $\mathbf B$.

Formalization targets

Goal: Theorem 2 (p. 6)

$$\Bigl(\forall N\ \exists L\ge N\ \exists f:A^L\to B \text{ symmetric polymorphism of } (\mathbf A,\mathbf B)\Bigr)\ \Longrightarrow\ \text{BLP+Affine correctly solves } \mathrm{PCSP\text{-}Decision}(\mathbf A,\mathbf B).$$

The hypothesis is a property of the template alone; the conclusion quantifies over all instances.

Milestones, in attack order

1. Footnote 1 (p. 5): a feasible $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$ has a solution of maximal support.
2. Completeness (p. 6): an instance satisfiable in $\mathbf A$ is accepted.
3. Rounding of variables (pp. 6–7): $W_i(a)=u\ell w_i(a)+v r_i(a)$ are non-negative integers with $\sum_a W_i(a)=L$, for $L=u\ell+v\ge M\ell^2$, $0\le v<\ell$.
4. Rounding of constraints (p. 7): $P_j(y)=u\ell p_j(y)+v q_j(y)$ are non-negative integers with $\sum_y P_j(y)=L$.
5. Eq. (9) (p. 7): $W_i(a)=\sum_{y:\,y|i=a}P_j(y)$.
6. Satisfying assignment (p. 7): $X_i:=f(a,\dots,a\ [W_i(a)\text{ times}])$ satisfies $X$ in $\mathbf B$.

Companion: Theorem 3 (p. 8)

The same conclusion when $\mathrm{Pol}(\mathbf A,\mathbf B)$ contains block-symmetric polymorphisms of arbitrarily large width: $[L]$ is split into blocks, each of size at least $N$, within which $f$ is invariant.

Significance

Theorem 2 gives one algorithm that decides every PCSP with an infinite family of symmetric polymorphisms, without knowing or evaluating the polymorphisms; it subsumes the BLP-then-AIP algorithm of Brakensiek and Guruswami for Boolean templates and applies over any finite domain. Theorem 3 extends this to block-symmetric families, which covers nearly all known tractable Boolean PCSPs, including 1-in-3-SAT versus NAE-SAT, whose alternating threshold polymorphisms are block-symmetric but not symmetric.

The results are proved in the paper. No machine-checked formalization of PCSPs, polymorphisms or the Basic LP is known to exist; Mathlib has no theory of constraint satisfaction. This mission produces a formal model of promise templates, instances, polymorphisms, the two relaxations and the algorithm's acceptance condition, together with a formal proof of the correctness theorem. The same model is the starting point for the characterization theorem (Theorem 4) treated in the companion mission.

Difficulty

Completeness is routine. Soundness is the substance: from a rational LP solution and an integer solution of the refined affine system one must produce an actual assignment in $\mathbf B$, using a polymorphism whose arity is chosen only after the instance is known. The natural first idea, clearing denominators of the LP solution and feeding the resulting multiplicities to a polymorphism, needs a polymorphism of exactly the arity the denominators dictate; with polymorphisms of only some arities it fails, and the paper's introduction notes that the LP alone does not suffice there. An integer affine solution, on the other hand, may have negative entries, which are not multiplicities. The paper stresses that the affine system must be the one refined by the support of a relative interior point: an arbitrary solution of the unrefined lattice gives no control on where the negative entries sit. In the formalization, the counting step (the columns of the matrix built from the constraint multiplicities have the variable multiplicities) and the passage from equal multiplicities to equal values of a symmetric function require explicit combinatorics on finite tuples, and the existence of a maximal-support LP solution requires an averaging argument over the finite set of coordinates.

Formalization scope

All declarations are in the namespace PCSPBLPAff.Symmetric. Conventions:

• Domains are Lean types with Fintype and DecidableEq; variables are Fin n, constraints Fin m, and a constraint's scope is a function Fin (ar R_j) → Fin n, possibly repeating variables.
• Arities are any natural numbers (the page asks for positive arities; every statement remains true for arity 0).
• The LP is over $\mathbb Q$ and the affine system over $\mathbb Z$. The weights $p_j$, $q_j$ are total functions on $A^{\mathrm{ar}(R_j)}$ required to vanish off $R_j^{\mathbf A}$.
• The marginal conditions (5) and (8) are imposed per position of the scope.
• The relative interior point is encoded by its only property the algorithm uses (footnote 1): a solution whose support contains the support of every solution. Acceptance requires such a solution and an affine solution vanishing outside its support.
• A block-symmetric function of width at least $N$ has at least one block, each block of size at least $N$.
• The polynomial-time claims of the paper, and the Remark on $\mathbb Z[\sqrt2]$, are out of scope: the algorithm is formalized by its acceptance condition.

The acceptance condition must not be replaced by "the LP is feasible and $\mathrm{Aff}_{\mathbb Z}(X,\mathbf A)$ has a solution", nor by an affine solution vanishing outside the support of an arbitrary LP solution; the first is a different algorithm and the second bypasses footnote 1.

Contributions welcome: proofs of the milestones, in particular the combinatorial lemma that a symmetric function takes the same value on tuples with the same multiplicities, and the averaging argument for maximal-support solutions; the block-wise version for Theorem 3.

Selected references

• J. Brakensiek, V. Guruswami, M. Wrochna, S. Živný, The Power of the Combined Basic Linear Programming and Affine Relaxation for Promise Constraint Satisfaction Problems, SIAM J. Comput. 49(6), 2020; arXiv:1907.04383v3. https://arxiv.org/abs/1907.04383v3
• J. Brakensiek, V. Guruswami, An Algorithmic Blend of LPs and Ring Equations for Promise CSPs, SODA 2019. https://arxiv.org/abs/1807.05194
• J. Brakensiek, V. Guruswami, Promise Constraint Satisfaction: Structure Theory and a Symmetric Boolean Dichotomy, SODA 2018. https://arxiv.org/abs/1704.01937
• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic Approach to Promise Constraint Satisfaction, J. ACM 68(4), 2021. https://arxiv.org/abs/1811.00970

Motivation

An assortment planner chooses which products to offer to arriving customers. When products are grouped into nests, a customer's choice of nest depends on all the assortments offered at once. A planner may nevertheless be able to generate only a short list of promising assortments for each nest. The remaining task is to choose one assortment from each list so that their combined expected revenue is as large as possible. Testing every combination requires a number of evaluations equal to the product of the list sizes. Gallego and Topaloglu show that the choice can instead be described through a linear program whose number of constraints grows with the sum of those sizes; this is Theorem 2 of their 2014 paper, in the authors' September 11, 2013 manuscript, pp. 10–12.

This mission isolates that selection result. Later parts of the paper address how to construct useful candidate lists under cardinality, space, and pricing constraints. Here the candidates are already given, and the question is which combination earns the most. The result matters whenever the candidate lists are much smaller than the space of all assortments: it makes the last step of those algorithms an exact optimization over the candidates, without enumerating their Cartesian product.

Setting

Let $M$ be a finite set of nests and $N$ a finite set of products available in each nest. An assortment $S_i\subseteq N$ is the set offered in nest $i$. Product $j$ in nest $i$ has preference weight $v_{ij}>0$ and revenue $r_{ij}\in\mathbb R$. The empty assortment is allowed. The main model has no within-nest no-purchase option, so its total offered weight is $V_i(S_i)=\sum_{j\in S_i}v_{ij}$. The conditional revenue in nest $i$ is $R_i(S_i)=\sum_{j\in S_i}v_{ij}r_{ij}/V_i(S_i)$, with $R_i(\varnothing)=0$ under the paper's $0/0=0$ convention.

The weight of no purchase outside the nests is $v_0>0$. Each nest has a dissimilarity parameter $\gamma_i\in(0,1]$. Its attraction weight is $V_i(S_i)^{\gamma_i}$. The expected revenue of a combined assortment $S=(S_i)_{i\in M}$ is

$$\Pi(S)=\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}}.$$

For each nest, $A_i$ is a finite nonempty collection of candidate assortments. The paper obtains these from a feasible set $C_i$, which may impose a cardinality or space constraint; Theorem 2 compares only combinations drawn from the supplied candidates. Equation (2) defines a real scalar $\widehat z$ through the maximum, over $A_i$ separately, of $V_i(S_i)^{\gamma_i}(R_i(S_i)-z)$. Problem (3) selects a maximizing candidate $\widehat S_i$ in each nest at that scalar. Linear program (4) has decision variables $(z,y_i)_{i\in M}$, minimizes $z$, and imposes $v_0z\ge\sum_i y_i$ and $y_i\ge V_i(S_i)^{\gamma_i}(R_i(S_i)-z)$ for every $i$ and every $S_i\in A_i$.

Formalization targets

The goal is the exact candidate-selection claim of Theorem 2. If $(\widehat z,\widehat y)$ minimizes $z$ among all feasible pairs of program (4), and every $\widehat S_i$ solves problem (3) at $\widehat z$, then

$$\Pi(S_1,\ldots,S_m)\le\Pi(\widehat S_1,\ldots,\widehat S_m) \qquad\text{for every }S_i\in A_i.$$

The milestones record three statements from pp. 11–12: equation (2) has a unique real root; the balance equation and its inequality form characterize the expected revenue of a fixed assortment; and Lemma 1 identifies the root as the best revenue attainable from candidate combinations while showing that local maximizers attain it. They separate the paper's numerical characterization of the best candidate revenue from its LP formulation. The target does not prescribe how the candidate lists were generated or claim that the selected combination is best among assortments outside those lists.

Significance

The theorem gives an exact, compact choice rule for assembling nestwise candidates. If the lists contain useful assortments under the original constraints, their best combination can be selected through program (4). The rest of the paper establishes candidate-generation and approximation results under particular constraint families; the stitching theorem supplies the common final selection step for those results. A larger candidate list may improve the obtainable revenue, but its Cartesian product need not be searched explicitly. The authors' manuscript, p. 12, states that program (4) has $1+m$ variables and $1+\sum_i|T_i|$ constraints when the candidates are indexed by $T_i$.

Formalizing the theorem yields a reusable statement about the interaction of a fractional revenue objective, independent nestwise candidate families, and a shared scalar LP. The published Prove2Me definition NestedLogitVariants.LP.Model already supplies the instance, $V_i$, $R_i$, $\Pi$, and the feasibility and optimality predicates for program (4). Its previously proved lp4_opt_binding concerns an equality at an LP optimum under ordered, nonnegative revenues; it does not contain Theorem 2's maximality claim under this paper's revenue assumptions. The four statements in this mission are draft targets awaiting machine-checked proofs.

Difficulty

Optimizing a candidate independently in every nest at an arbitrary value of $z$ does not generally optimize the combined revenue: the revenue denominator couples all nests. Likewise, an LP-feasible value need not be its minimum, and using such a value in problem (3) does not establish the theorem. The substantive assertion is that choosing the local maximizers at the optimal LP value solves the combined selection problem. The unique-root statement also needs care at empty assortments, where a nest contributes zero attraction and the conditional revenue uses the paper's $0/0$ convention.

Formalization scope

Nests are represented by any finite type, and products by Fin n, indexed $0,\ldots,n-1$ rather than the paper's $1,\ldots,n$. A Boolean offer vector is represented by Finset (Fin n); $\overline 0$ is the empty finset. Each $A_i$ is a finite set of such assortments. There is no single-nest or $\gamma_i=1$ specialization, and no substitution of all possible assortments for the supplied candidates. The LP assumption is its full minimum objective property, not merely feasibility. The imported LP4Optimal predicate uses a set of candidates, supplied by coercing each finite $A_i$ to a set.

The source's main model is selected from the imported general instance by setting $v_{i0}=0$. In the paper's later extension, $V_i(S_i)=v_{i0}\mathbf1(S_i\ne\overline0)+\sum_jv_{ij}S_{ij}$; this is different from the imported unmodified $v_{i0}+\sum_jv_{ij}S_{ij}$ when $S_i=\overline0$, so the extension is outside this mission. Positive $v_0$ and product weights are stated explicitly to keep the probability denominator positive and to match the model's preference interpretation. Revenues remain arbitrary real numbers: neither an order nor nonnegativity is assumed. The dissimilarities satisfy the paper's $(0,1]$ range. The paper states candidate feasibility $A_i^t\in C_i$; this mission's claim holds for arbitrary candidate collections because no step compares against $C_i$. The definitions of revenue and LP feasibility are imported, so useful contributions include proofs of the balance characterization, the root result, Lemma 1, and the final LP statement.

Selected references

• Guillermo Gallego and Huseyin Topaloglu, Constrained Assortment Optimization for the Nested Logit Model, Management Science, 2014. DOI: 10.1287/mnsc.2014.1931; authors' manuscript, September 11, 2013, pp. 7–12.
• James Davis, Guillermo Gallego, and Huseyin Topaloglu, Assortment Optimization under Variants of the Nested Logit Model, Operations Research, 2014. DOI: 10.1287/opre.2014.1256. The published Prove2Me model definition used here comes from this line of work.

Motivation

In two-echelon distribution goods travel from a central depot to intermediate facilities, called satellites, on large first-level vehicles, and from the satellites to customers on smaller second-level vehicles. City logistics schemes that keep heavy trucks out of urban centres are the standard example. The two-echelon capacitated vehicle routing problem (2E-CVRP) asks for the cheapest set of routes on both levels that serves every customer while respecting vehicle, fleet and satellite capacities.

Exact methods for problems of this kind are branch-and-bound or enumeration schemes whose speed depends on the quality of the lower bounds they use. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) built their exact algorithm on a Lagrangean-type relaxation $RF$ of a set-partitioning formulation $F$, rather than on the LP relaxation $LF$ of that formulation. Their Theorem 2 is the justification for that design choice: the best bound $RF$ can deliver is never weaker than $z(LF)$, and can be strictly stronger. This mission formalizes that comparison.

Setting

An instance has a depot $0$, satellites $N_S$ and customers $N_C$, a symmetric travel cost $d_{uv}$ (in which the fixed vehicle costs $U_1, U_2$ have already been folded into the depot–satellite and satellite–customer entries), positive integer demands $q_i$, capacities $Q_1 > Q_2 > 0$ for first- and second-level vehicles, a bound $m^1$ on first-level vehicles, $m_k$ second-level vehicles at satellite $k$, a global bound $m^2 \le \sum_k m_k$ on second-level vehicles, a capacity $B_k$ and a unit handling cost $H_k$ for each satellite.

A first-level route $r \in \mathcal M$ leaves the depot, visits a set $R_r$ of satellites and returns; its cost $g_r$ is the cost of that closed walk. A second-level route $l \in \mathcal R_k$ leaves satellite $k$, visits a set $R_{kl}$ of customers and returns; its load is $w_{kl} = \sum_{i \in R_{kl}} q_i \le Q_2$, $a_{ikl}$ counts its visits to customer $i$, and its cost $c_{kl}$ is its closed-walk cost plus $H_k w_{kl}$.

Formulation $F$ uses binaries $x_{kl}$ (route $l$ of satellite $k$ is used), binaries $y_r$, and nonnegative integers $q_{kr}$ (quantity route $r$ delivers to satellite $k \in R_r$). It minimizes $\sum c_{kl}x_{kl} + \sum g_r y_r$ subject to: each customer is covered exactly once (2); at most $m_k$ routes at satellite $k$ (3) and $m^2$ overall (4); the load delivered from satellite $k$ is at most $B_k$ (5); at most $m^1$ first-level routes (6); what first-level routes bring to satellite $k$ equals what its second-level routes carry (7); and $\sum_{k \in R_r} q_{kr} \le Q_1 y_r$ (8).

The LP relaxation $LF$ replaces the integrality of $x, y, q$ by $0 \le x, y \le 1$, $q \ge 0$. Its value is $z(LF)$, equal to $+\infty$ when $LF$ is infeasible.

The relaxation $RF(\beta, \lambda, \mu)$ relaxes (2)–(4) with penalties $\lambda \in \mathbb{R}^{N_C}$, $\mu_k \le 0$ and $\mu_0 \le 0$, and replaces the second-level routes by marginal routing costs $\beta_{ik}$ that must satisfy, for every route $l \in \mathcal R_k$,

$$\sum_{i} a_{ikl}\beta_{ik} \le c_{kl} - \sum_i a_{ikl}\lambda_i - \mu_k - \mu_0. \tag{12}$$

Its variables are binaries $\xi_{ik}$ (customer $i$ is supplied from satellite $k$), $y_r$ and $q_{kr}$; it minimizes

$$\sum_{k,i}\beta_{ik}\xi_{ik} + \sum_r g_r y_r + \sum_i \lambda_i + \sum_k m_k\mu_k + m^2\mu_0$$

subject to single assignment of each customer, flow balance $\sum_{r \in \mathcal M_k} q_{kr} = \sum_i q_i\xi_{ik}$, satellite capacity $\sum_i q_i \xi_{ik} \le B_k$, and (6), (8). A choice $(\beta,\lambda,\mu,\mu_0)$ with $\mu, \mu_0 \le 0$ and (12) is admissible.

Formalization targets

Goal: Theorem 2

$$\max_{\beta,\lambda,\mu}\, z(RF(\beta,\lambda,\mu)) \ \ge\ z(LF), \quad\text{and the inequality can be strict.}$$

Formally: (1) for every instance and route families whose $LF$ is feasible, some admissible $(\beta,\lambda,\mu,\mu_0)$ satisfies $z(LF) \le z(RF(\beta,\lambda,\mu))$; (2) some instance, route families and admissible choice give $z(LF) < z(RF(\beta,\lambda,\mu)) < +\infty$.

Milestones

• §3, remark on $LF$: if every $g_r > 0$, every optimal $LF$ solution has $y_r = (\sum_{k \in R_r} q_{kr})/Q_1$.
• Theorem 2, first clause: the bound, for every instance with $LF$ feasible.
• Theorem 2, second clause: the strict instance.

Significance

Theorem 2 places the relaxation $RF$ in the hierarchy of bounds for the 2E-CVRP. The remark on $LF$ explains its weakness: in the LP relaxation each first-level route is paid for only in proportion to the load it carries, so $z(LF)$ degrades as first-level routing costs grow. $RF$ keeps $y_r$ binary and therefore pays the full cost of every first-level route used, while the second-level routing is priced through $\beta$. The theorem guarantees that optimizing over penalties never loses against the LP bound, which is what makes the bounds LD1 and the further relaxation $\overline{RF}$ of the paper worth computing.

The paper's proof is in its electronic companion and is not reproduced in the article. A formal proof makes the comparison checkable, and fixes the exact conditions under which it holds: the remark on $LF$ needs positive first-level route costs, and the "max" in Theorem 2 is attained only when $LF$ is feasible. Neither part is formalized elsewhere. Linear programming strong duality is available on the platform as LinearOptimization.lp_strong_duality (Bertsimas and Tsitsiklis, Theorem 4.4, Proved); a related but different statement is LinearOptimization.lagrangean_dual_eq_lp_over_hull (Theorem 11.4 there), which concerns the Lagrangean dual of a generic integer program rather than $RF$.

Difficulty

$RF$ is not the Lagrangean dual of $F$ in the textbook sense: it changes the variables (customer-to-satellite assignments $\xi$ instead of routes $x$), keeps the assignment constraints, and couples the multipliers through the inequalities (12). So the general fact that a Lagrangean dual is at least the LP bound does not apply directly; one must construct, from the data of $LF$, an admissible $\beta$ that is compatible with the flow-balance and capacity constraints of $RF$. For the strict clause, the instance must satisfy every structural requirement of the model (positive demands, $Q_2 < Q_1$, route loads at most $Q_2$, $m^2 \le \sum_k m_k$), and $RF$ must be feasible, so that the gap is a genuine gap between finite bounds.

Formalization scope

Satellites and customers are Fin ns and Fin nc (0-based). The travel cost is an arbitrary symmetric real matrix; the triangle inequality is not assumed. Demands are positive integers. Route families $\mathcal M$, $\mathcal R$ are arbitrary finite families of nonempty elementary routes (repetitions allowed), with costs computed from $d$ along the closed walk, so the statements cover the paper's families of all routes as a special case. Binary variables are Bool, integer quantities ℕ, $LF$ variables real. Optimal values are infima over the feasible set in EReal, $+\infty$ for an infeasible problem; there is no junk value $0$.

Part 1 of the goal assumes $LF$ feasible: when $LF$ is infeasible the printed relation would read "$\sup = +\infty$", which is not attained by any single choice of penalties. Part 2 requires $z(RF) < +\infty$, which rules out the trivial witness of an instance with $RF$ infeasible; admissibility includes $\mu, \mu_0 \le 0$, without which the supremum is $+\infty$ for trivial reasons.

The definitions (instance, route systems, $F$, $LF$, (12), $RF$) are shared in shape with the two companion missions of this series and are intended for consolidation. Proofs of the bound will need finite-dimensional LP duality; contributions that connect $LF$ to the platform's general-form LP and its strong duality theorem are welcome.

Selected references

• R. Baldacci, A. Mingozzi, R. Roberti, R. Wolfler Calvo, An Exact Algorithm for the Two-Echelon Capacitated Vehicle Routing Problem, Operations Research 61(2), 298–314, 2013. https://doi.org/10.1287/opre.1120.1153
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 4.4, strong duality; Theorem 11.4, Lagrangean duality).

Motivation

Search engines sell advertising space query by query. Each advertiser states a bid for each keyword and a daily budget; queries arrive one at a time, and each must be assigned to an advertiser immediately, without knowledge of the queries still to come. The revenue-maximizing assignment of the day can only be computed offline. The adwords problem asks how close an online rule can get to it. It generalizes online bipartite matching, for which Karp, Vazirani and Vazirani (KVV 1990) showed that randomized ranking attains ratio $1-1/e$, and $b$-matching, for which Kalyanasundaram and Pruhs (KP 2000) showed that the deterministic BALANCE algorithm attains $1-1/e$ as the budget grows.

Mehta, Saberi, Vazirani and Vazirani (J. ACM 2007) gave a deterministic algorithm for arbitrary bids that weighs each bid by a function of the fraction of budget already spent, and proved that it is $(1-1/e)$-competitive when bids are small compared to budgets. The algorithm and its tradeoff function became the reference point for the online budgeted-allocation literature, including the primal-dual analysis of Buchbinder, Jain and Naor (ESA 2007).

Setting

There are $N$ bidders, each with budget $1$, and a sequence of $M$ queries $q_1,\dots,q_M$. Bidder $b$ bids $c_{b,t}\ge0$ for the query at position $t$. An allocation $\sigma$ assigns each query to at most one bidder. Bidder $b$'s spend before position $t$ is $\min(1,\sum_{s<t,\,\sigma(s)=b}c_{b,s})$, and $b$ is alive while its spend is below $1$. The revenue of $\sigma$ is $\mathrm{rev}(\sigma)=\sum_b\min(1,\sum_{t:\sigma(t)=b}c_{b,t})$.

Fix an integer $k$ and split each budget into $k$ equal slabs; a spent fraction $s\in((j-1)/k,j/k]$ lies in slab $j$, and $s=0$ in slab $1$. Given a tradeoff function $\psi$ on slabs, the discrete tradeoff algorithm assigns each arriving query to an alive bidder maximizing

$$c_{b,t}\,\psi(\mathrm{slab}(b)),$$

ties broken arbitrarily. Every allocation produced this way, for any tie-breaking, is a run.

The analysis uses the factor-revealing LP $L$: maximize $\sum_{i=1}^{k-1}\frac{k-i}{k}x_i$ subject to $\sum_{j=1}^{i}(1+\frac{i-j}{k})x_j\le\frac ikN$ and $x\ge0$, written $\max c\cdot x$, $Ax\le b$, $x\ge0$, and its dual $D$. Its optimal dual solution is $y^*_i=\frac1k(1-\frac1k)^{k-i-1}$, and Theorem 8's tradeoff function is

$$\psi_k(i)=\sum_{j=i}^{k-1}y^*_j .$$

Formalization targets

Goal: Theorem 8 (p. 12)

For every $\delta>0$ there is $k_0$ such that for every $k\ge k_0$ there is $\eta>0$ such that, for every instance with bids in $[0,\eta]$, every run $\sigma$ of the algorithm with $\psi_k$, and every allocation $\tau$,

$$\mathrm{rev}(\sigma)\ \ge\ \Bigl(1-\frac1e-\delta\Bigr)\mathrm{rev}(\tau).$$

The goal fixes no rate in $k$ or $\eta$: it asserts only that the ratio tends to $1-1/e$.

Milestones

1. Proof of Lemma 3 (pp. 8–9): $x^*_i=\frac Nk(1-\frac1k)^{i-1}$ and $y^*$ are optimal for $L$ and $D$, with value $N(1-1/k)^k$.
2. Lemma 3 (p. 8): the value of $L$ and $D$ tends to $N/e$.
3. Lemma 4 (p. 10): for every nonnegative $a$ and $l=Aa$, $y^*$ minimizes $l\cdot y$ over the constraints of $D$.
4. Lemma 5 (p. 10): $l=b+\Delta$ under the relation $\beta_i=N/k-(\alpha_1+\dots+\alpha_{i-1})/k$.
5. Lemma 6 (p. 11): $\mathrm{OPT}(q)\psi(\mathrm{type}(q))\le\mathrm{ALG}(q)\psi(\mathrm{slab}(q))$ when $1\le\mathrm{type}(q)\le k-1$.
6. Lemma 7 (p. 11): $\sum_{i=1}^{k-1}\psi(i)(\alpha_i-\beta_i)\le N/k$, for a monotonically decreasing nonnegative $\psi$ with $\psi(k)=0$ (such as $\psi_k$).

Significance

Theorem 8 gives an online algorithm for budgeted allocation with arbitrary bids whose revenue is within a factor $1-1/e$ of the offline optimum, the best possible ratio even for randomized algorithms (Theorem 9 of the same paper, the second mission of this series). It reduces to BALANCE when all bids are equal, and its tradeoff function $1-e^{x-1}$ in the limit is the function used in later work on online budgeted allocation and display-ad allocation.

The result is proved in the paper; none of it is formalized. The work here is to formalize the proof in a version that holds for actual runs. The paper's argument makes two simplifications with "negligible error": bidders of type $j$ spend exactly $j/k$ of their budget, and the offline optimum exhausts every budget. A formal proof must carry the bid size through the slab boundaries and compare with an arbitrary offline allocation. The LP lemmas (Lemmas 3–5) are self-contained statements about one triangular linear program and are reusable for factor-revealing analyses of BALANCE.

Difficulty

The milestones are short: Lemmas 3–5 are finite linear algebra with geometric sums, Lemma 6 is one application of the assignment rule plus monotonicity of spend, and Lemma 7 regroups finite sums. The difficulty is in Theorem 8. The paper's proof chains Lemmas 4, 5 and 7 through the LP $L(\pi,\psi)$, whose right-hand side is computed from the numbers $\alpha_j$ of bidders of each type under the assumption that a bidder of type $j$ spends exactly $j/k$. In an actual run this identity fails: a single bid can straddle a slab boundary, and types are intervals, not points. So the chain does not compose literally, and the natural first attempt, instantiating Lemma 5 with the run's quantities, does not apply. The slab-wise inequalities that do hold, with an error of order $k\eta$, have to replace the equalities, and the comparison with an offline allocation that does not exhaust budgets has to be made through capped revenues.

Formalization scope

Bidders are Fin N and query positions Fin M, zero-based; slabs and LP coordinates keep the paper's 1-based ranges, with vectors as functions $\mathbb N\to\mathbb R$ read on $1\le i\le k-1$. Budgets are $1$ (the paper's standing simplification of §2). Bids are real and nonnegative.

A run is a predicate on the whole allocation: at position $t$, if some bidder is alive the query goes to an alive maximizer of bid $\times\,\psi(\text{slab})$, where spends are computed from earlier positions only; the query is unassigned only when all budgets are exhausted. Every tie-breaking rule gives a run, and the goal holds for all of them. $\mathrm{ALG}(q)$ is the full bid of the chosen bidder; revenue is capped at the budget.

Conventions the statements commit to:

• $\psi_k$ is the defining sum of Theorem 8. The closed form printed beside it, $1-(1-1/k)^{k-i+1}$, is off by one in the exponent; the sum equals $1-(1-1/k)^{k-i}$ and vanishes at slab $k$.
• "As $k\to\infty$" is $\forall\delta\,\exists k_0\,\forall k\ge k_0$; "bids small compared to budgets" is a bound $\eta$ chosen after $k$, never depending on the instance.
• The comparator is every allocation $\tau$, not an optimum that exhausts all budgets; the paper says the proof extends without that assumption (§4, §6 item 2). Only the lower bound on the ratio is stated.
• Lemma 4 quantifies over every nonnegative vector $a$, through which alone the instance and $\psi$ enter $D(\pi,\psi)$. Lemma 5 takes the paper's relation for $\beta_i$ as a hypothesis. Lemma 7 defines $\alpha_i,\beta_i$ as the query sums of its proof, and adds $\psi(k)=0$ in place of the paper's bound on the slab-$k$ term, which rests on its exact-spend simplification.

Trivializing formalizations are ruled out: a run cannot leave a query unassigned while a bidder has budget, so the empty allocation is not a run; no hypothesis of the form "bidders of type $j$ spend exactly $j/k$" or "the optimum exhausts every budget" is imposed, since either would make the goal vacuous on most instances.

All definitions are local to the namespace AdWordsMSVV.Tradeoff. Related platform items analyse a different algorithm: BJNAdAuctions.Basic.* and OnlinePrimalDual.AdAuctions.* formalize the Buchbinder–Jain–Naor primal-dual algorithm, which updates a covering variable multiplicatively and has ratio $(1-1/c)(1-R_{\max})$; they are not reused. Proofs of any milestone, and lemmas carrying the bid-size error through slab boundaries, are welcome.

Selected references

• A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized on-line matching, J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321
• B. Kalyanasundaram, K. Pruhs, An optimal deterministic algorithm for online b-matching, Theoretical Computer Science 233, 2000. https://doi.org/10.1016/S0304-3975(99)00140-1
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
• N. Buchbinder, K. Jain, J. Naor, Online primal-dual algorithms for maximizing ad-auctions revenue, ESA 2007. https://doi.org/10.1007/978-3-540-75520-3_24

Motivation

Network revenue management decides, over a finite selling horizon, which products to offer to arriving customers when the products share limited resources: seats on flight legs, hotel room-nights, rental capacity. The exact dynamic program is intractable for realistic networks, so practice relies on heuristics built from a deterministic linear program (DLP), the fluid relaxation that replaces random demand by its mean. Its value is an upper bound on the revenue of every policy, and the quality of a heuristic is measured by its revenue loss against it.

For the fluid-based heuristics, the loss grows with the size of the system: a static policy derived from one DLP solution loses order $\sqrt{k}$ when capacities and demand rates are both scaled by $k$ (Gallego and van Ryzin, 1997; Talluri and van Ryzin, 1998). Re-solving the DLP during the horizon is common practice, but for a long time it was unclear whether re-solving helps asymptotically; Cooper (2002) showed that naive re-solving can even hurt. Jasin and Kumar (Math. Oper. Res. 37(2), 2012, doi:10.1287/moor.1120.0537) proved that a re-solving heuristic with probabilistic allocation control (PAC) has a loss bounded by a constant independent of $k$, in a model that also covers customer choice through random resource consumption. Later work (Bumpensanti and Wang, 2020, arXiv:1802.06192) removed the nondegeneracy assumption with a different re-solving rule.

Setting

The horizon is $[0,1]$. Customer types $q$ arrive as independent Poisson processes of rates $\lambda_q \ge 0$. Each of the $n$ offers $j$ belongs to one type $q(j)$; $P_{q,j} = 1$ iff $q = q(j)$, and $S_q = \{j : q(j) = q\}$. Presenting offer $j$ consumes a random vector $A^j \ge 0$ of the $m$ resources, i.i.d. across presentations, and earns revenue $r_j(A^j)$, with $r_j(0) = 0$; $A^j = 0$ models a customer who buys nothing. Resource $i$ starts with capacity $C_i$, and $\xi_j$ bounds every $A_{ij}$. Write $\bar A = \mathbb E[A]$ and $\bar r_j = \mathbb E[r_j(A^j)]$. The DLP is

$$\mathrm{DLP}[C,\lambda]:\quad \max\ \bar r^\top x\quad\text{s.t.}\quad \bar A x \le C,\ Px \le \lambda,\ x \ge 0.$$

Assumption 2.1 requires $\mathrm{DLP}[C,\lambda]$ to be nondegenerate with a unique optimal solution $Y$; Assumption 2.2 requires that every optimum $z$ of the LP without capacity constraints violates $\bar A z \le C$.

PAC re-solves at times $0 = t_0 < t_1 < \dots < t_M < 1$. At $t_\ell$ it solves $\mathrm{DLP}[C(t_\ell), (1-t_\ell)\lambda]$ with the remaining capacity, obtaining $Y(t_\ell)$; until $t_{\ell+1}$ it picks offer $j \in S_q$ for an arriving type-$q$ customer with probability $Y_j(t_\ell)/((1-t_\ell)\lambda_q)$ and presents it only if the remaining capacity is at least $\xi_j$ on every resource. In the $k$-th system capacities are $kC$ and rates $k\lambda$; $V^k_{\mathrm{DLP}}$ is the DLP value and $R^k_{\mathrm{PAC}}$ the revenue of PAC. Mid-point PAC re-solves at $t_l = 1 - 2^{-l}$, $l = 1,\dots,M^k$, with $M^k$ the smallest integer such that $2^{-M^k} \le 1/k$: about $\log_2 k$ re-solves.

Formalization targets

Goal: Theorem 5.2

There is $\rho > 0$, independent of $k$, such that mid-point PAC satisfies

$$V^k_{\mathrm{DLP}} - \mathbb E[R^k_{\mathrm{PAC}}] \le \rho \quad\text{for all } k \ge 1.$$

The goal fixes no constant: it asserts only that the loss is bounded uniformly in $k$.

Milestones

• Observations B.1 and B.2: the fractional part $J_y$ of $Y$ is nonempty, and the augmented matrix $W = [\bar A_{B,y}; P_{B_2,y}]$ is square and invertible.
• App. B.2: the perturbed point $Y_\Delta = Y - H\Delta_B$ is the unique optimum of $\mathrm{DLP}[C-\Delta,\lambda]$ under explicit feasibility conditions.
• Lemma C.4: the window deviation of the consumption has a sub-Gaussian exponential moment, $\mathbb E[e^{r\tilde\Delta_i}] \le e^{k\varphi(t-s)r^2}$ for $|r\xi_{\max}| \le 1$.
• Theorem 5.3, the general bound for any schedule:

$$V^k_{\mathrm{DLP}} - \mathbb E[R^k_{\mathrm{PAC}}] \le \rho + \hat\rho k\int_0^1 \min\{1, \rho' F(k,t)\}\,dt.$$

• App. C.6: for mid-point re-solving, $G(k,t) \le 4(1-t)$ before the last re-solve.
• Further consequences: Theorem 5.1 (periodic PAC, loss $\le \rho + \hat\rho\sqrt{kh}$) and Corollary 5.1 (any schedule, loss $\le \rho + \hat\rho\sqrt k$).

Significance

The result shows that $O(\log k)$ re-solves suffice for a loss that does not grow with the size of the system, against an upper bound that is valid for every policy; so PAC is within a constant of the optimal policy, and the DLP bound, the optimal value and PAC are asymptotically equivalent to order $O(1)$. Theorem 5.3 makes the trade-off between re-solving frequency and loss explicit for any schedule, and Corollary 5.1 guarantees that re-solving in this form never worsens the static $O(\sqrt k)$ bound.

The result is proved on paper. No part of it is formalized: the mission produces a machine-checked model of a Poisson network with random consumption and a re-solving policy, a statement of LP perturbation theory for nondegenerate programs, and compound-Poisson moment bounds, each reusable for other re-solving and fluid-approximation results in revenue management.

Difficulty

The obvious argument compares PAC with its fluid path and bounds the deviation of the remaining capacity by a martingale estimate over the whole horizon. That gives only $O(\sqrt k)$: deviations late in the horizon cannot be corrected. A constant bound needs re-solving to correct earlier deviations, which in turn needs the re-solved DLP solution to depend linearly and stably on the capacity deviation (the perturbation analysis of App. B) and a hitting-time estimate for when that linear regime fails. The capacity check and the coupling between the re-solved solutions and the random consumption make the process non-Markovian in the obvious state variables.

Formalization scope

Types are Fin NT, offers Fin n, resources Fin m. The model is a structure holding $q(j)$, $\lambda$, $C$, the consumption laws $D_j$ (measures on $\mathbb R^m$), $\xi$ and the revenue functions. Standing readings (IsValid): $\lambda \ge 0$ and $C \ge 0$; each $D_j$ is a probability measure with $0 \le A_{ij} \le \xi_j$ almost surely (the page has $\xi_j \ge A_{ij}$ on p. 317 and $A_{ij} < \xi_j$ on p. 327; the weaker one is used); revenue functions are measurable, vanish at $0$, and are nonnegative and bounded by a common constant (implicit on the page). $\bar r_j = \mathbb E[r_j(A^j)]$ is a reading fixed by App. A.1.

$\mathbb E[R^k_{\mathrm{PAC}}]$ is a backward recursion over the windows between re-solves. Each window holds a Poisson$(k\Lambda\ell)$ number of arrivals with i.i.d. types (superposition and marking), and the expected value is computed arrival by arrival with the capacity check on every resource. PAC is quantified over every DLP selector that returns an optimal solution and is measurable in the capacity, since the page leaves ties open after time 0. All constants are chosen after the instance and before $k$, the selector, the schedule, $v$ and $h$. Nondegeneracy follows Bertsimas–Tsitsiklis: every basic feasible solution has exactly $n$ active constraints.

Disclosed deviations from the page:

• Theorem 5.3 adds integrability of $v$ in $t$ (stated in Lemma C.1) and writes $v \le 1/\xi_{\max}$ as $v\,\xi_{\max} \le 1$.
• The C.6 bound $G(k,t) \le 4(1-t)$ is stated for $t < t_{M^k}$; the page's "for all $t \in [0,1]$" is false after the last re-solve.
• Theorem 5.1's constants are chosen before $h$, which is what (6) requires.
• The goal is stated as printed, although the printed proof uses $v = 1/\xi_{\max}$, admissible only when $\xi_{\max} \ge 1$. Measuring every resource in a common smaller unit multiplies $A$, $C$ and $\xi$ by the same factor and changes neither $V^k_{\mathrm{DLP}}$ nor $\mathbb E[R^k_{\mathrm{PAC}}]$, so this assumption costs no generality.

A formalization in which PAC does not check capacity, or stops checking after a hitting time, earns exactly $V_{\mathrm{DLP}}$ and would make the goal trivial; the model here applies the check at every arrival. A constant chosen after $k$ would also be trivial, since the loss is at most $k\sum_q\lambda_q$ times the revenue bound.

The source is the published Math. Oper. Res. version; printed page = PDF page + 311. Sample-path lemmas (B.2–B.4, C.1–C.3) are not stated. Contributions are welcome on the LP perturbation lemma, the compound-Poisson moment bound and the measurability of the PAC recursion, each of which stands alone.

Selected references

• S. Jasin, S. Kumar, A Re-Solving Heuristic with Bounded Revenue Loss for Network Revenue Management with Customer Choice, Mathematics of Operations Research 37(2):313–345, 2012. https://doi.org/10.1287/moor.1120.0537
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1):24–41, 1997. https://doi.org/10.1287/opre.45.1.24
• K. Talluri, G. van Ryzin, An Analysis of Bid-Price Controls for Network Revenue Management, Management Science 44(11):1577–1593, 1998. https://doi.org/10.1287/mnsc.44.11.1577
• W. L. Cooper, Asymptotic Behavior of an Allocation Policy for Revenue Management, Operations Research 50(4):720–727, 2002. https://doi.org/10.1287/opre.50.4.720.2861
• P. Bumpensanti, H. Wang, A Re-Solving Heuristic with Uniformly Bounded Loss for Network Revenue Management, Management Science 66(7), 2020. https://arxiv.org/abs/1802.06192
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997.

Motivation

Multistage stochastic linear programs model sequential decisions under uncertainty: capacity and reservoir planning, hydro-thermal scheduling, inventory and asset–liability management. When the data process is stagewise independent, the problem decomposes by dynamic programming into one linear program per stage, coupled through expected cost-to-go functions. These functions are convex and piecewise linear, and the stochastic dual dynamic programming (SDDP) method of Pereira and Pinto (1991) approximates them from below by cutting planes. SDDP is the standard solution method in the long-term planning of hydro-dominated power systems, and its convergence theory determines what the bounds it reports actually mean.

Shapiro's paper (Optimization Online 2009/12/2509; European J. Oper. Res. 209(1), 2011, doi:10.1016/j.ejor.2010.08.007) analyses SDDP applied to a sample average approximation (SAA) of the true problem, with all of the data $(c_t, A_t, B_t, b_t)$ random. Its convergence result, Proposition 3.1, asserts finite convergence with probability one when the forward scenarios are subsampled independently. A related almost-sure finite convergence theorem for a different algorithm (DOASA, with randomness only in the right-hand sides and cut sharing across outcomes) is due to Philpott and Guan (2008); it is posed as a separate mission on this platform and is not restated here.

Setting

There are $T\ge 2$ stages. The decision $x_t\in\mathbb R^{n_t}$ satisfies $x_t\ge 0$ and, at the first stage, $A_1x_1=b_1$ with deterministic data $(c_1,A_1,b_1)$. For $t=2,\dots,T$ the data are replaced by a sample $\tilde\xi_t^j=(\tilde c_{tj},\tilde A_{tj},\tilde B_{tj},\tilde b_{tj})$, $j=1,\dots,N_t$, each with probability $1/N_t$, independently across stages, and the stage-$t$ constraint is $\tilde B_{tj}x_{t-1}+\tilde A_{tj}x_t=\tilde b_{tj}$. The SAA cost-to-go functions are defined backwards from $\widetilde{\mathcal Q}_{T+1}\equiv 0$:

$$\widetilde Q_{tj}(x_{t-1})=\inf_{x_t\ge0}\big\{\tilde c_{tj}^\top x_t+\widetilde{\mathcal Q}_{t+1}(x_t):\tilde B_{tj}x_{t-1}+\tilde A_{tj}x_t=\tilde b_{tj}\big\},\qquad \widetilde{\mathcal Q}_t=\frac1{N_t}\sum_{j=1}^{N_t}\widetilde Q_{tj}.$$

A scenario is a choice $(j_2,\dots,j_T)$; there are $N=\prod_t N_t$ of them, each of probability $1/N$. A policy $\bar x_t=\bar x_t(\tilde\xi_{[t]})$ depends only on the outcomes up to stage $t$; it is optimal for the SAA problem if it is feasible on every scenario and its expected cost $\frac1N\sum_{\text{scenarios}}\sum_t\tilde c_t^\top\bar x_t$ is minimal.

SDDP keeps, for each stage, a finite set of cuts $\alpha+\beta^\top x$ whose maximum $\mathfrak Q_{t+1}$ lies below $\widetilde{\mathcal Q}_{t+1}$. An iteration has a forward step: $M$ scenarios are sampled, and along each of them the decisions $\bar x_t$ solve the stage problems with $\mathfrak Q_{t+1}$ in place of $\widetilde{\mathcal Q}_{t+1}$, (3.13)–(3.14). It also has a backward step: from $t=T-1$ down to $1$, at each trial point $\bar x_t$ the stage-$(t+1)$ problems with the current cuts are solved for all $N_{t+1}$ outcomes, and the cut (3.17) $\ell(x)=\underline{\widetilde{\mathcal Q}}_{t+1}(\bar x_t)+\tilde g^\top(x-\bar x_t)$ is added, where $\tilde g$ averages $-\tilde B^\top\pi$ over basic optimal (extreme-point) dual solutions $\pi$.

Formalization targets

Goal: Proposition 3.1

Suppose the forward scenarios are drawn independently and uniformly from the SAA scenarios, (A1) holds ((3.13) and (3.14) have finite optimal values for every scenario at every iteration), and the backward steps use basic optimal dual solutions. Then

$$P\Big(\exists K\ \forall k\ge K:\ \text{the forward policy defined by }\mathfrak Q^k_2,\dots,\mathfrak Q^k_{T}\text{ is optimal for the SAA problem}\Big)=1 .$$

The goal fixes no iteration count, no rate and no number of forward scenarios $M\ge1$.

Milestones, in attack order

1. Attainment: an LP of the form (3.13)/(3.14) with finite optimal value has an optimal solution.
2. Cut validity: every cut lies below $\widetilde{\mathcal Q}_{t+1}$ on reachable decisions, and $\underline{\widetilde Q}_{tj}\le\widetilde Q_{tj}$.
3. Lower bound: the optimal value $\underline\vartheta_k$ of (3.13) is at most the SAA optimal value.
4. Finitely many cutting planes (3.17) for a fixed next-stage cut set, uniformly in the trial point.
5. Finitely many realizations of the $\mathfrak Q_t$ and of first-stage solutions; along each run the cut sets are eventually constant.
6. A policy is optimal for the SAA problem if and only if it satisfies the dynamic programming conditions (3.18) on every scenario.
7. With probability one every SAA scenario is drawn at infinitely many iterations.

Significance

The result separates SDDP's sampling from its convergence: on a finite scenario tree, independent subsampling of forward paths suffices for the method to stop at an optimal policy, without ever enumerating the tree. It explains why the lower bound $\underline\vartheta_k$ eventually equals the SAA optimal value, which is what makes the gap-based stopping rules of the paper (§3, Remarks 4–6) meaningful. The paper's closing remark stresses that without independence of the forward scenarios there is no guarantee of convergence.

The proposition is proved in the paper. No machine-checked proof of it, or of any SDDP convergence theorem, exists to our knowledge. Formalizing it requires a precise account of what the method is: which dual solutions, which forward solutions, which order of updates. Several of these points are left implicit on the page.

Difficulty

Finiteness of the cut universe (milestones 4–5) is a statement about extreme points of dual polyhedra whose dimension grows with the cut sets of the next stage, so it must be organized stage by stage from $T$ down. The central difficulty is the last step of the argument. Once the approximations have stopped changing, one must show that the stable cuts are exact where the forward policy goes, so that the forward policy satisfies (3.18). The obvious argument, "if (3.18) fails at the last stage where it fails, the next cut there increases $\mathfrak Q$", does not work as printed: (3.18) holding at later stages does not by itself make the next-stage approximation exact at the trial point. Closing this step is where the conventions on forward solutions and on sampling listed below become essential.

Formalization scope

The Lean development is in the namespace ShapiroSDDP.Convergence. Stages are numbered $1,\dots,T$; the data of stage $t+1$ are stored under index $t$ (the coupling matrix is indexed by the decision it multiplies); V t is $\widetilde{\mathcal Q}_{t+1}$, with V t ≡ 0 for $t\ge T$. Cost-to-go values are real infima, used only on reachable decisions. The explicit readings are:

• cost-to-go functions finite valued on reachable decisions (the paper: everywhere; weaker);
• initial cut sets: a parameter, nonempty and valid on reachable decisions, with $\{(0,0)\}$ at stage $T$;
• forward solutions from a deterministic oracle that reads the cut set and returns an optimal solution whenever one exists; the goal holds for every such oracle;
• basic optimal duals: extreme points of the dual feasible region, chosen arbitrarily; the goal holds for every run;
• (A1) as a hypothesis on the run; $M\ge1$ forward scenarios per iteration, i.i.d. uniform (independence via iIndepFun);
• forward step before backward step within an iteration, with cuts at that iteration's trial points.

Optimality of a policy is defined by expected cost, never by (3.18), so that milestone 6 is not definitional. Sampling is stated as i.i.d. uniform draws, not as "every scenario recurs", which is milestone 7. All of $c,A,B,b$ depend on the outcome. If some $\tilde A_{tj}$ lacks full row rank, no basic dual solution exists and no run exists; a sorry-free witness instance shows that all hypotheses of the goal can hold together.

Useful infrastructure: LP weak and strong duality (LinearOptimization.lp_weak_duality, LinearOptimization.lp_strong_duality exist on the platform in their own encoding), finiteness of extreme points of polyhedra, attainment for polyhedral objectives, and the second Borel–Cantelli lemma (ProbabilityTheory.measure_limsup_eq_one). Proofs of any milestone, and reusable lemmas on LPs with cut epigraphs, are welcome.

Selected references

• A. Shapiro, Analysis of Stochastic Dual Dynamic Programming Method, Optimization Online preprint 2009/12/2509; European Journal of Operational Research 209(1):63–72, 2011. https://optimization-online.org/2009/12/2509/ · https://doi.org/10.1016/j.ejor.2010.08.007
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52:359–375, 1991. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Operations Research Letters 36(4):450–455, 2008. https://doi.org/10.1016/j.orl.2008.01.013
• J. E. Kelley, The cutting-plane method for solving convex programs, J. SIAM 8(4):703–712, 1960. https://doi.org/10.1137/0108053
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751