Optimization

Motivation

In city logistics, goods often cannot be carried by large trucks all the way to the final customers. A common design routes the goods through intermediate depots, called satellites: large first-level vehicles carry freight from a central depot to the satellites, and small second-level vehicles deliver it from the satellites to the customers. The two-echelon capacitated vehicle routing problem (2E-CVRP) asks for the cheapest such two-level distribution plan. It contains the capacitated vehicle routing problem as a special case (a single satellite), and the location-routing problem can be reduced to it.

Exact methods for problems of this kind rest on lower bounds: a branch-and-bound or enumeration scheme can discard a partial solution only when it has a certified bound above the best known cost. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) built an exact algorithm for the 2E-CVRP on a chain of relaxations of a set-partitioning formulation $F$. Its first link is a Lagrangean relaxation $RF$ and a further relaxation $\overline{RF}$, a multiple-choice knapsack problem solved by dynamic programming. Its optimal value, maximised over the penalties, gives the lower bound $\mathrm{LD1}$ that drives the rest of the method. This mission formalizes the statements that make $\mathrm{LD1}$ a valid bound.

Setting

An instance has a depot $0$, satellites $N_S$ and customers $N_C$, a symmetric cost matrix $d_{ij}$ (with the vehicle fixed costs already added to the depot–satellite and satellite–customer entries), positive integer demands $q_i$ with total $q_{\mathrm{tot}}$, $m^1$ first-level vehicles of capacity $Q_1$, $m_k$ second-level vehicles of capacity $Q_2 < Q_1$ at satellite $k$, a global limit $m^2$ on second-level vehicles, satellite capacities $B_k$ and handling costs $H_k$ per unit.

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 this closed walk. A second-level route $l \in \mathcal R_k$ is a simple cycle from satellite $k$ through a set of customers of total demand $w_{kl} \le Q_2$; its cost $c_{kl}$ is the cost of the cycle plus $H_k w_{kl}$. In formulation $F$, binary variables $x_{kl}$ and $y_r$ select the routes and integers $q_{kr}$ give the amount that route $r$ delivers to satellite $k$. The constraints require that every customer is served exactly once (2), that the vehicle limits $m_k$, $m^2$, $m^1$ hold (3), (4), (6), that satellite capacities hold (5), that each satellite receives what its routes deliver (7), and that first-level capacities hold (8).

Relaxation $RF$ removes (2)–(4) with penalties $\lambda_i \in \mathbb R$, $\mu_k \le 0$, $\mu_0 \le 0$, and replaces the second-level routes by marginal costs $\beta_{ik}$ of serving customer $i$ from satellite $k$, subject to

$$\sum_{i} a_{ikl}\beta_{ik} \le c_{kl} - \sum_i a_{ikl}\lambda_i - \mu_k - \mu_0 \qquad (l \in \mathcal R_k), \qquad (12)$$

where $a_{ikl}$ counts the visits of route $l$ to customer $i$. Its variables are an assignment $\xi_{ik}$ of customers to satellites and the first-level variables $y_r$, $q_{kr}$.

Relaxation $\overline{RF}$ chooses for every first-level route $r$ at most one load $w$ in the interval $W_r = [w^{\min}, w_r^{\max}]$ of integers, so that the loads add up to $q_{\mathrm{tot}}$. A route with load $w$ costs $g_r + \phi_{rw}$, where $\phi_{rw}$ is the optimum of a continuous knapsack problem that serves demand $w$ at the cheapest marginal costs $\min_{k \in R_r}\beta_{ik}$. Both objectives carry the constant $\sum_i \lambda_i + \sum_k m_k\mu_k + m^2\mu_0$.

Formalization targets

Goal: LD1 is a valid lower bound (Eq. (23))

For every $\beta$ satisfying (12), every $\lambda$, every $\mu \le 0$, $\mu_0 \le 0$, and every feasible solution of $F$ with cost $\mathrm{cost}_F$,

$$z(\overline{RF}(\beta,\lambda,\mu)) \le \mathrm{cost}_F, \qquad\text{equivalently}\qquad \mathrm{LD1} = \max_{\beta,\lambda,\mu} z(\overline{RF}(\beta,\lambda,\mu)) \le z(F).$$

Milestones

1. Theorem 1. $z(RF(\beta,\lambda,\mu)) \le \mathrm{cost}_F$ under the same hypotheses.
2. Theorem 3, corrected. $z(\overline{RF}(\beta,\lambda,\mu))$ is at most the objective of every feasible $RF$ solution whose satellite loads satisfy $\sum_i q_i\xi_{ik} \le m_kQ_2$.
3. Reduced-cost elimination with $\overline{RF}$ (§3.2): a feasible solution of cost below $z(\mathrm{UB})$ uses no route with $\tilde c_{kl} \ge z(\mathrm{UB}) - z(\overline{RF})$, where $\tilde c_{kl} = c_{kl} - \sum_i a_{ikl}(\beta_{ik}+\lambda_i) - \mu_k - \mu_0$.
4. Corollary 1: the same elimination with $z(RF)$.
5. Theorem 4: for any enlarged family $\hat{\mathcal R}_k \supseteq \mathcal R_k$ of not necessarily elementary routes, $\beta_{ik} = q_i \min_{l \in \hat{\mathcal R}_{ik}} \frac{c_{kl} - \sum_{i'} a_{i'kl}\lambda_{i'} - \mu_k - \mu_0}{\sum_{i'} a_{i'kl}q_{i'}}$ solves (12).

Significance

The bound $\mathrm{LD1}$ is the first lower bound of the paper's exact method. The configuration enumeration of its §5 and the reduced-cost elimination of second-level routes both use it as a certificate: a configuration or a route is discarded only when this bound shows that no cheaper solution contains it. If the bound were invalid, the method could discard the optimum. Theorem 4 provides, at every step of the paper's subgradient procedure, a $\beta$ to which the bound applies.

The paper's proofs are in an electronic companion. As printed, Theorem 3 ($z(\overline{RF}) \le z(RF)$) is false: $RF$ does not limit a satellite's load by its fleet capacity $m_kQ_2$, whereas the loads of $\overline{RF}$ are capped by it. A small instance with one satellite and two unit-demand customers, $Q_2 = 1$ and $m_1 = 1$ has $z(RF)$ finite and $z(\overline{RF}) = +\infty$. The bound (23) is nevertheless true, because the $RF$ solutions that come from feasible solutions of $F$ respect the fleets. A machine-checked version pins down exactly which hypotheses the chain needs, including the positivity of demands, without which (23) fails. None of these results has been formalized before.

Difficulty

Theorems 1, 4 and Corollary 1 are bookkeeping with sums over routes, customers and satellites. The substantive step is the corrected Theorem 3. A solution of $RF$ assigns whole customers to satellites, while $\overline{RF}$ sees each first-level route only through its total load and a continuous knapsack. The two descriptions have to be related, and that relation must respect every side condition of $\overline{RF}$: the knapsack bounds $0 \le z_i \le 1$, the load window $W_r$ (whose lower end $w^{\min}$ depends on the vehicle count $m^1$) and the fleet cap $\sum_{k \in R_r} m_kQ_2$. The obvious route, comparing the optimal values $z(RF)$ and $z(\overline{RF})$ directly as the paper states, does not work: the inequality between them is false, and the fleet condition is what has to be carried from $F$.

Formalization scope

Satellites are Fin ns, customers Fin nc (0-based). Demands are positive integers; capacities, fleet sizes and loads are natural numbers, and costs are real. Binary variables are Bool and integer variables ℕ. The route families $\mathcal M$ and $\mathcal R$ are arbitrary finite families of routes (nonempty, no repeated vertex, second-level loads at most $Q_2$), not necessarily all routes as in the paper; every statement holds in this generality. Route costs are computed along the closed walk, so $(0,k,0)$ costs $2d_{0k}$. The triangle inequality is not assumed. Optimal values $z(RF)$, $z(\overline{RF})$ and $\phi_{rw}$ are infima in EReal, equal to $+\infty$ on infeasible problems, and comparisons with an upper bound are written with $+$ instead of $-$. Where the paper writes "optimal solution of cost below $z(\mathrm{UB})$", the statements cover every feasible solution below any real $z(\mathrm{UB})$.

The formalization cannot be trivialized: every optimal value is an infimum over the feasible set of the paper's own problem, so it equals $+\infty$, not $0$, when that set is empty. The hypotheses of each theorem are satisfiable, which is checked on explicit small instances. The definitions of the instance, $F$, $RF$ and $\overline{RF}$ are written in the shape shared by the other missions of this series. Proofs of any milestone and reusable lemmas on finite sums over route families 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
• R. Baldacci, A. Mingozzi, R. Roberti, New Route Relaxation and Pricing Strategies for the Vehicle Routing Problem, Operations Research 59(5), 1269–1283, 2011 (ng-routes). https://doi.org/10.1287/opre.1110.0975
• G. Perboli, R. Tadei, D. Vigo, The Two-Echelon Capacitated Vehicle Routing Problem: Models and Math-Based Heuristics, Transportation Science 45(3), 364–380, 2011. https://doi.org/10.1287/trsc.1110.0368

Motivation

Many problems in signal processing, statistics and machine learning ask for a minimizer of a smooth loss among vectors with few nonzero entries: compressed sensing with a nonlinear measurement model, sparse regression with a non-quadratic loss, sparse phase retrieval. The common abstraction is the sparsity constrained problem

$$(\mathrm P)\qquad \min\ f(x)\quad\text{s.t.}\quad \|x\|_0\le s,$$

where $f$ is continuously differentiable but not necessarily convex. The constraint set is a finite union of linear subspaces, so (P) is nonconvex and in general NP-hard, and the classical optimality theory (KKT conditions, convex duality) gives no usable characterization of its solutions.

Beck and Eldar (SIAM J. Optim. 2013, arXiv:1203.4580) replaced that missing theory with a hierarchy of necessary optimality conditions of increasing strength, and matched each condition with an algorithm whose limit points satisfy it. This mission formalizes the comparison between the two strongest conditions of that hierarchy: coordinate-wise minimality and $L_2(f)$-stationarity.

Setting

Vectors live in $\mathbb R^n$ with the Euclidean norm. For $x\in\mathbb R^n$:

• the $\ell_0$ norm $\|x\|_0$ is the number of nonzero components of $x$;
• the support is $I_1(x)=\{i: x_i\ne0\}$, and $I_0(x)=\{i: x_i=0\}$ is its complement;
• $C_s=\{x:\|x\|_0\le s\}$ is the feasible set of (P), for an integer $0<s<n$;
• $M_s(x)$ is the $s$-th largest of $|x_1|,\dots,|x_n|$, counted with multiplicity, so that $M_s(x)=0$ exactly when $\|x\|_0<s$.

The objective $f:\mathbb R^n\to\mathbb R$ is continuously differentiable and bounded below (Assumption 1). Assumption 2 asks that $\nabla f$ be Lipschitz with some constant $L(f)$.

The local Lipschitz condition (2.15) with constant $L_2$ asks that for every pair $i\ne j$, every $x$ and every $d$ supported in $\{i,j\}$,

$$\big\|\nabla_{i,j}f(x)-\nabla_{i,j}f(x+d)\big\|\le L_2\|d\|,$$

where $\nabla_{i,j}f(x)=(\nabla_if(x),\nabla_jf(x))$. The paper's local Lipschitz constant $L_2(f)=\max_{i\ne j}L_{i,j}(f)$ satisfies it, and $L_2(f)\le L(f)$, often by a large factor.

A point $x^*\in C_s$ is a basic feasible (BF) vector (Definition 2.1) if $\nabla f(x^*)=0$ when $\|x^*\|_0<s$, and $\nabla_if(x^*)=0$ on $I_1(x^*)$ when $\|x^*\|_0=s$.

A point $x^*\in C_s$ is a coordinate-wise (CW) minimum (Definition 2.4) if either $\|x^*\|_0<s$ and $f(x^*)\le f(x^*+te_i)$ for every $i$ and every $t\in\mathbb R$ (Case I), or $\|x^*\|_0=s$ and

$$f(x^*)\le f(x^*-x^*_ie_i+te_j)\qquad\text{for every } i\in I_1(x^*),\ j\in\{1,\dots,n\},\ t\in\mathbb R$$

(Case II): no swap of a support coordinate for any coordinate, with any value, decreases $f$.

Formalization targets

Goal: Theorem 2.4

Every CW-minimum $x^*$ of (P) satisfies

$$|\nabla_i f(x^*)|\ \begin{cases}\le L_2(f)\,M_s(x^*), & i\in I_0(x^*),\\ =0, & i\in I_1(x^*),\end{cases}$$

that is, $x^*$ is an $L_2(f)$-stationary point. The constant $L_2(f)$ multiplies $M_s(x^*)$ exactly.

Milestones

1. Lemma 2.5. Every CW-minimum is a BF vector.
2. Lemma 2.6 (Local Descent Lemma). Under (2.15), for every $d$ with at most two nonzero components,

$$f(x+d)\le f(x)+\nabla f(x)^Td+\frac{L_2(f)}{2}\|d\|^2 .$$

3. (2.18). At a CW-minimum with $\|x^*\|_0=s$, for $i\in I_0(x^*)$, an index $m$ with $|x^*_m|=M_s(x^*)$ and $\sigma=\operatorname{sgn}(x^*_m\nabla_if(x^*))$,

$$f(x^*-x^*_me_m-\sigma x^*_me_i)\le f(x^*)-\sigma x^*_m\nabla_if(x^*)+L_2(f)(x^*_m)^2 .$$

Significance

Optimality conditions for (P) matter because no efficient algorithm finds a global minimizer; what algorithms can guarantee is a limit point satisfying some necessary condition, and the strength of that condition is the guarantee. The paper's hierarchy runs: optimal $\Rightarrow$ CW-minimum $\Rightarrow$ $L_2(f)$-stationary $\Rightarrow$ $L$-stationary for $L\ge L(f)$ $\Rightarrow$ BF vector. Theorem 2.4 is the step that ties the coordinate-wise notion, which needs no Lipschitz constant to state, to the stationarity notion behind iterative hard thresholding. Combined with "every optimal solution is a CW-minimum", it shows that every optimal solution of (P) is $L_2(f)$-stationary, with the local constant instead of $L(f)$. It is the reason the greedy and partial sparse-simplex methods of the same paper, whose limit points are CW-minima or $L_2(f)$-stationary, are at least as strong as iterative hard thresholding.

The result is proved on paper. To our knowledge none of these notions (BF vectors, CW-minima, the local Lipschitz constant, the local descent lemma) has a machine-checked formalization. The mission produces a formal statement of the hierarchy's central step together with reusable definitions of the sparse-optimization objects, which the companion missions on the same paper (iterative hard thresholding, the greedy and partial sparse-simplex methods) state their results against.

Difficulty

The local descent lemma has no proof in the paper ("it is not difficult to see"). The global descent lemma integrates the gradient along the segment $[x,x+d]$ and applies the global Lipschitz bound; the local version must instead observe that along a direction supported on two coordinates only the two corresponding gradient components enter, and that the restricted Lipschitz bound (2.15) controls exactly those. Formally this requires the integral form of the mean value theorem for $C^1$ functions on a Euclidean space, together with the bookkeeping that $x+\tau d$ stays in the class of perturbations allowed by (2.15).

In Theorem 2.4 the natural first attempt, perturbing a single zero coordinate $i$ and comparing with $f(x^*)$, fails when $\|x^*\|_0=s$: the perturbed point has $s+1$ nonzeros and is infeasible, and Case II of the definition only compares $x^*$ with points obtained by swapping a support coordinate out. The bound on $|\nabla_if(x^*)|$ must therefore be extracted from swaps alone, and the degenerate case $\nabla_if(x^*)=0$ breaks the printed identity $\|x^*_me_m+\sigma x^*_me_i\|^2=2(x^*_m)^2$ in the paper's chain (2.18).

Formalization scope

All statements are in the namespace SparseNLO.CWOpt and work on EuclideanSpace ℝ (Fin n); indices run over Fin n, so $0,\dots,n-1$ instead of $1,\dots,n$. The gradient is Mathlib's gradient, $te_i$ is EuclideanSpace.single i t, and $f$ is ContDiff ℝ 1. Assumption 1 is carried as a hypothesis on every statement, as the paper's standing assumption; Assumption 2 is carried wherever the page states it, with a free constant $L_f$.

$M_s(x)$ is the entry at position $s-1$ of the list of $|x_i|$ sorted in nonincreasing order; the hypotheses $0<s<n$ of (P) make it meaningful. The local Lipschitz constant is not computed as a maximum: $L_2$ is any real constant satisfying (2.15), with "at most two nonzero components" read as "supported in some $\{i,j\}$, $i\neq j$" (the reading of Example 2.1). Every statement therefore holds for every valid $L_2$, in particular for $L_2(f)$. The minima in (2.11)–(2.12) are written as "$f(x^*)\le$ every value", which is equivalent. The goal states the displayed condition (2.16); its identification with Definition 2.3's $L$-stationarity goes through Lemma 2.2, which belongs to a companion mission.

A trivializing formalization is ruled out: the CW-minimum predicate requires feasibility in $C_s$ and is satisfiable (for $n=2$, $s=1$, $f(x)=(x_1-1)^2+x_2^2$, the point $(1,0)$ is a CW-minimum), $M_s$ is the $s$-th largest absolute value, and $L_2$ is constrained by (2.15) rather than left free.

Contributions welcome: proofs of Lemma 2.6 (reusable for any coordinate-descent analysis on two coordinates), Lemma 2.5, (2.18) and the goal; general lemmas on $M_s$ (it is attained by some coordinate, and it vanishes exactly when $\|x\|_0<s$).

Theorem numbers and pages follow source.pdf, the arXiv version arXiv:1203.4580v1, not the SIAM typesetting.

Selected references

• A. Beck, Y. C. Eldar, Sparsity Constrained Nonlinear Optimization: Optimality Conditions and Algorithms, SIAM Journal on Optimization 23(3), 2013. https://doi.org/10.1137/120869778 — arXiv:1203.4580v1 (2012), https://arxiv.org/abs/1203.4580
• T. Blumensath, M. E. Davies, Iterative Hard Thresholding for Compressed Sensing, Applied and Computational Harmonic Analysis 27(3), 2009. https://doi.org/10.1016/j.acha.2009.04.002

Motivation

Genetic algorithms with local search ("memetic" or hybrid genetic algorithms) are among the most effective heuristics for vehicle routing. Their recurring weakness is premature convergence: selection and local improvement both favour good individuals, so the population fills with near-copies of a few solutions and the search stalls. Vidal, Crainic, Gendreau, Lahrichi and Rei addressed this in their hybrid genetic search with adaptive diversity control (HGSADC) for multi-depot and periodic vehicle routing (CIRRELT-2010-34, 2010; journal version Operations Research 60(3), 2012). Instead of judging an individual by its cost alone, HGSADC ranks it by a Biased Fitness that mixes its cost rank with its rank in contribution to population diversity, and it uses that score to decide which individuals survive.

Trading cost for diversity raises an obvious worry: a very good but unoriginal solution could be discarded. The paper answers it with its only stated result, an elitism property (Section 4.6, an unnumbered Proposition with a three-sentence proof): the best individuals by cost are never discarded, as long as they are not clones. The HGSADC framework has since become the basis of state-of-the-art codes for many routing variants, and this guarantee is the one formal statement on which its population management rests.

Setting

HGSADC keeps two subpopulations (feasible and infeasible) and manages each separately. Everything below concerns one subpopulation; no routing object is involved.

A population is a finite set $P$ of individuals, with $\mathit{nbIndiv} = |P|$. Each individual $I$ has a penalized cost $c(I)\in\mathbb R$, its fitness (lower is better); a distance $\delta(I_1,I_2)$ to every other individual; and a diversity contribution $\Delta_P(I)$, which in the paper is the mean distance from $I$ to its $n_{close}$ nearest neighbours in $P$ (higher is better).

The normalized ranks of $I$ relative to the current population are

$$\mathit{fit}_P(I)=\frac{\#\{J\in P:\ c(J)<c(I)\}}{|P|-1},\qquad \mathit{dc}_P(I)=\frac{\#\{J\in P:\ \Delta_P(I)<\Delta_P(J)\}}{|P|-1},$$

so that the best individual has rank $0$ and the worst rank $1$. For an integer parameter $\mathit{nbElit}$, the Biased Fitness is (equation (7))

$$BF_P(I)=\mathit{fit}_P(I)+\Bigl(1-\frac{\mathit{nbElit}}{|P|-1}\Bigr)\times \mathit{dc}_P(I).$$

An individual $I$ is a clone in $P$ if some other $J\in P$ has $\delta(J,I)=0$ or $c(J)=c(I)$. With $\mathit{best}$ the current best solution, $X(P)$ is the set of individuals of $P$, other than $\mathit{best}$, that have a clone.

Survivor selection. When a subpopulation reaches $\mu+\lambda$ individuals, $\lambda$ of them are discarded one at a time: if $X\neq\emptyset$, an individual of maximum $BF$ in $X$ is removed; otherwise an individual of maximum $BF$ in the whole population. After each removal the distances, $X$, the ranks and $BF$ are recomputed on the remaining population. An individual is among the $\mathit{nbElit}$ best of $P$ in terms of fitness when fewer than $\mathit{nbElit}$ members of $P$ have strictly smaller cost.

Formalization targets

Goal: Section 4.6, Proposition

For every run of the survivor-selection procedure that removes $\lambda$ individuals from $P$ and ends at $P'$, with $\mathit{nbElit}+\lambda\le|P|$:

$$J\in P,\quad J\notin X(P),\quad \#\{K\in P: c(K)<c(J)\}<\mathit{nbElit}\ \Longrightarrow\ J\in P'.$$

Milestones: the three sentences of the proof (p. 17)

1. If $X(P)=\emptyset$, the individual $W$ with the worst fitness has $\mathit{fit}_P(W)=1$ and $BF_P(W)\ge 1$.
2. An individual $J$ among the $\mathit{nbElit}$ best has

$$BF_P(J)\le\frac{\mathit{nbElit}-1}{|P|-1}+1-\frac{\mathit{nbElit}}{|P|-1}<1.$$

3. One removal step does not remove an individual $J\notin X(P)$ among the $\mathit{nbElit}$ best.

Significance

The result. The Proposition explains what the parameter $\mathit{nbElit}$ means: it is the number of top individuals whose survival is guaranteed from one generation to the next, whatever their diversity contribution. It lets the algorithm designer push for diversity through $BF$ without risking the loss of the best solutions, and it is what makes the "removal zone" $BF\ge 1$ of the paper's Figure 4 a meaningful picture. The same Biased Fitness and survivor rule are reused in later HGS variants, so the guarantee transfers to them.

Formalizing it. The proof in the paper is three sentences long, but it leaves several things implicit: what happens with ties in cost or diversity, why "the" worst individual has rank exactly $1$, why the coefficient of $\mathit{dc}$ is nonnegative, and why the one-step argument survives $\lambda$ successive removals with everything recomputed. A machine-checked version settles each of these. To our knowledge no formalization of this or any other population-management guarantee for genetic algorithms exists.

Difficulty

The arithmetic of each step is elementary. The difficulty is in reading the statement correctly. "The individual with the worst fitness has rank 1" fails when costs tie; it holds only in the branch $X=\emptyset$, where equal costs are excluded because two individuals with equal cost are both clones and at most one of them is the best solution. The inequality $BF\ge 1$ needs $\mathit{nbElit}\le|P|-1$, which the Proposition does not state: it follows from the population sizes ($\mu+\lambda$ reduced to $\mu$, with $\mathit{nbElit}=el\times\mu$, $el\in[0,1]$, Table 1). Without it the Proposition is false: if $\mathit{nbElit}\ge|P|$ and $X=\emptyset$, some elite individual must be removed. Finally, the one-step argument must be iterated: the population, its ranks and $X$ change after each removal, and one must check that the hypotheses on $J$ persist.

Formalization scope

Individuals are elements of an arbitrary type $\alpha$ with decidable equality; populations are Finset α. Costs, distances and diversity contributions are real-valued, and $\Delta$ is an arbitrary function of (population, individual), which includes the paper's equation (5); the goal is therefore stated for every diversity measure. Explicit readings of loose phrases:

• "normalized ranks … where the best individual has rank 0 and the worst has rank 1": the number of strictly better individuals divided by $|P|-1$, in $\mathbb R$ (competition ranking; tied individuals share the better rank);
• "the nbElit best individuals … in terms of fitness": fewer than $\mathit{nbElit}$ members with strictly smaller cost;
• "Update the distance measures and X, and repeat": $X$, ranks and $BF$ are recomputed on the current population at each of the $\lambda$ steps;
• ties in "maximum Biased Fitness" are broken arbitrarily, and the goal quantifies over every run;
• the population-size condition $\mathit{nbElit}+\lambda\le|P|$ is an explicit hypothesis, taken from Section 4.6 and Table 1;
• the best solution $\mathit{best}$ is a parameter, not required to lie in $P$ (for the infeasible subpopulation it is the incumbent feasible solution); $J$ may itself be $\mathit{best}$.

A formalization that freezes the initial Biased Fitness, that takes the ranks as arbitrary functions into $[0,1]$, that states the existence of one good run, or whose size hypothesis cannot be met, would not be this Proposition. The supporting definition file contains the ranks, the Biased Fitness, clones, $X$, a removal step and a run of $\lambda$ steps; no further library is needed beyond Finset cardinalities. Proofs of the three milestones and of the goal are welcome, as is a formalization of the paper's Hamming distance (6) and diversity contribution (5) as an instance of $\Delta$.

Selected references

• T. Vidal, T. G. Crainic, M. Gendreau, N. Lahrichi, W. Rei, A Hybrid Genetic Algorithm for Multi-Depot and Periodic Vehicle Routing Problems, technical report CIRRELT-2010-34, July 2010. https://www.cirrelt.ca/documentstravail/cirrelt-2010-34.pdf (the version cited throughout; Section 4.6, pp. 16–17).
• T. Vidal, T. G. Crainic, M. Gendreau, N. Lahrichi, W. Rei, A Hybrid Genetic Algorithm for Multidepot and Periodic Vehicle Routing Problems, Operations Research 60(3):611–624, 2012. https://doi.org/10.1287/opre.1120.1048
• C. Prins, A simple and effective evolutionary algorithm for the vehicle routing problem, Computers & Operations Research 31(12):1985–2002, 2004. https://doi.org/10.1016/S0305-0548(03)00158-8
• K. Sörensen, M. Sevaux, MA|PM: memetic algorithms with population management, Computers & Operations Research 33(5):1214–1225, 2006. https://doi.org/10.1016/j.cor.2004.09.011

Motivation

Single-leg capacity allocation under customer choice is the basic dynamic problem of revenue management: a firm holds a fixed stock of a perishable resource (seats on a flight leg, rooms on a night), and in every period of a finite selling horizon it decides which products (fare classes) to offer to the arriving customer. Talluri and van Ryzin (Management Science, 2004) showed that under a multinomial logit (MNL) choice model with known parameters, the optimal assortment in every period is revenue-ordered and shrinks as capacity becomes scarcer ("nesting by fare order"), which is what justifies the protection levels and bid prices used in practice.

The MNL parameters are estimated from data and are never known exactly. Rusmevichientong and Topaloglu (Operations Research, 2012) study the robust version, in which an adversary picks the parameters of each period from an uncertainty set after seeing the offered assortment, following the robust Markov decision process framework of Iyengar (Mathematics of Operations Research, 2005). Their Section 4 shows that the structure of the known-parameter problem survives: the value function is concave in capacity, the optimal assortment is a revenue threshold set, and it grows with remaining capacity and, when uncertainty does not shrink, over time. This mission formalizes those results.

Setting

There are $n$ products $\mathcal A = \{1,\dots,n\}$ with revenues $r_1,\dots,r_n$. An MNL parameter vector is $v = (v_0, v_1, \dots, v_n) \in \mathbb R^{n+1}_{++}$; offered the assortment $S \subseteq \mathcal A$, a customer buys product $i \in S$ with probability

$$\phi_i(S,v) = \frac{v_i}{v_0 + \sum_{\ell\in S} v_\ell},$$

and nothing with probability $1 - \sum_{i\in S}\phi_i(S,v)$. The expected revenue is $f(S,v) = \sum_{i\in S} r_i \phi_i(S,v)$.

Static problem (Section 3). For a compact nonempty uncertainty set $\mathcal V \subseteq \mathbb R^{n+1}_{++}$,

$$Z^*(\mathcal V) = \max_{S\subseteq\mathcal A}\ \min_{v\in\mathcal V} f(S,v),$$

and $S^*(\mathcal V)$ is an optimal assortment of smallest cardinality.

Dynamic problem (Section 4). Periods $t = 1,\dots,T$ each bring one customer, whose parameter vector lies in a compact nonempty $\mathcal V_t \subseteq \mathbb R^{n+1}_{++}$. A purchase consumes one unit of capacity. The value function $J_t(x)$, the maximum worst-case revenue from period $t$ on with $x$ units of capacity, satisfies

$$J_t(x) = \max_{S_t\subseteq\mathcal A}\ \min_{v_t\in\mathcal V_t}\Big\{\sum_{i\in S_t}\phi_i(S_t,v_t)\big(r_i + J_{t+1}(x-1)\big) + \Big(1-\sum_{i\in S_t}\phi_i(S_t,v_t)\Big)J_{t+1}(x)\Big\}$$

for $x \ge 1$, with $J_t(0) = 0$ and $J_{T+1} \equiv 0$. The marginal value of capacity is $\Delta J_t(x) = J_t(x) - J_t(x-1)$, and $S^*_t(x)$ is a maximizer of the right-hand side of smallest cardinality.

Formalization targets

Goal: Theorem 4.3 (p. 17)

For every $1 \le t \le T$ and $x \ge 1$, and, in the second part, every $1 \le t \le T-1$ with $\mathcal V_t \subseteq \mathcal V_{t+1}$:

$$S^*_t(x) \subseteq S^*_t(x+1), \qquad \mathcal V_t \subseteq \mathcal V_{t+1} \implies S^*_t(x) \subseteq S^*_{t+1}(x).$$

Milestones

1. (Dynamic Robust), second line (p. 16): $J_t(x) = \max_{S}\min_{v\in\mathcal V_t}\sum_{i\in S}\phi_i(S,v)\,(r_i - \Delta J_{t+1}(x)) + J_{t+1}(x)$.
2. Proof of Theorem 4.2 (pp. 16–17): $S^*_t(x)$ is the static $S^*(\mathcal V_t)$ for revenues $r_i - \Delta J_{t+1}(x)$, and $J_t(x) - J_{t+1}(x)$ is the corresponding $Z^*(\mathcal V_t)$.
3. Theorem 3.2 (p. 7): $S^*(\mathcal V) = \{i : r_i > Z^*(\mathcal V)\}$.
4. Theorem 3.7 (p. 10): for $\delta \ge 0$, $S^*(\mathcal V)$ is contained in the robust assortment for revenues $r + \delta$.
5. Corollary 3.5 (p. 9): $\mathcal V \subseteq \mathcal V' \implies Z^*(\mathcal V') \le Z^*(\mathcal V)$ and $S^*(\mathcal V) \subseteq S^*(\mathcal V')$.
6. Theorem 4.1, first inequality (p. 16): $\Delta J_t(x+1) \le \Delta J_t(x)$.
7. Theorem 4.1, second inequality (p. 16): $\Delta J_{t+1}(x) \le \Delta J_t(x)$.
8. Theorem 4.2 (p. 16): $S^*_t(x) = \{i : r_i > J_t(x) - J_{t+1}(x-1)\}$.

Significance

The result. Theorems 4.1–4.3 say that robustness costs nothing structurally: the robust policy is still a nested threshold policy, so it can be implemented with the protection levels or bid-price controls already in use, and it can be computed by examining at most $n$ revenue-ordered assortments per state instead of $2^n$. Theorem 4.3 gives the operational content: with less inventory, offer fewer, higher-revenue products; nearer the end of the season (when the uncertainty sets are nested), offer more.

Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. A formalization produces a checked robust finite-horizon dynamic program over finite action sets with compact adversary sets, the reduction of each Bellman step to a static max–min problem with shifted revenues, and checked concavity and time-monotonicity arguments that are reusable for other single-resource problems. The known-parameter analogues for general regular choice models and for the Markov chain choice model are separate drafts on the platform (RevenueOrdered.Nesting.*, MarkovChainChoice.SingleResource.*); they have no uncertainty set and are not used here.

Difficulty

The obvious route to concavity, an induction on $t$ in which $J_t$ is a maximum of concave functions, fails: a maximum of concave functions is not concave, and here each candidate assortment is evaluated by a minimum over $\mathcal V_t$, and the worst-case parameter vector changes with the capacity level, so the known-parameter argument cannot be reused term by term. Any induction on $t$ also has to handle the boundary $x = 0$, where the Bellman equation does not apply and only $J_t(0) = 0$ is given. Every step involving a minimum must use that the minimum over a compact set is attained, and translating a minimum by a constant must be justified rather than assumed.

Formalization scope

• Representation. Products are Fin n (Lean index $i$ is product $i+1$). A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 $= v_0$. $f(S,v)$ is the published ChoiceCDLP.MNL.mnlObjective. Minima over uncertainty sets are real infima (sInf), equal to the attained minima under the standing hypotheses; maxima are Finset.sup' over all $2^n$ assortments.
• Standing assumptions. Every V t, $1 \le t \le T$, is compact, nonempty and contained in $\mathbb R^{n+1}_{++}$ (IsUncertaintySeq); the static results assume the same of V. The paper writes "$\mathcal V \subset \mathbb R^n_{++}$" in Theorem 3.2 and Corollary 3.5; this is read as $\mathbb R^{n+1}_{++}$, compact.
• Revenues are arbitrary reals. The paper orders $r_1 \ge \dots \ge r_n > 0$ "without loss of generality"; no proof uses it, and the dynamic reduction applies Theorem 3.2 to $r_i - \Delta J_{t+1}(x)$, which may be negative. Dropping it strengthens every statement.
• The value function is defined by the recursion. The max–min policy formulation (p. 15) and Iyengar's theorem that it satisfies the Bellman equation are not formalized. $J_t(x)$ is defined for every $x \in \mathbb N$; the initial capacity $C$ never enters the recursion, so the paper's $J_t$ on $\{0,\dots,C\}$ is the restriction.
• Capacity $x \ge 1$. Theorem 4.1 is printed "for any $x \in \{0,1,\dots,C\}$", which includes the undefined $\Delta J_t(0)$; Theorems 4.2 and 4.3 say "for any $x$", but $S^*_t(0)$ is not defined by the Bellman equation. All statements assume $x \ge 1$.
• Tie-break. $S^*(\mathcal V)$ and $S^*_t(x)$ are predicates ("$S$ is an optimal assortment of smallest cardinality"), not choice functions; Theorems 3.2 and 4.2 are stated as "↔ $S$ is the threshold set", which also asserts the threshold set is optimal. Without the tie-break Theorems 4.2 and 4.3 are false, since a product with revenue exactly at the threshold can be added.
• Ruled out. Defining $J$ as a maximum over revenue-ordered assortments, or through the threshold formula, would make Theorem 4.2 definitional; $J$ is defined with the minimum inside a maximum over all subsets.
• Restatements. Theorems 3.2, 3.7 and Corollary 3.5 restate, in RobustMNL.Dynamic, the companion mission on Section 3 of the same paper, identically up to namespace.
• Source. The source is the authors' manuscript of 20 September 2011 of the Operations Research 2012 article; its printed page numbers equal the PDF's.
• Welcome contributions. Lemmas on attained minima of continuous functions on compact sets of positive parameter vectors, the translation of a max–min by a constant, and the bound $\sum_{i\in S}\phi_i(S,v) \le 1$ are reusable across all three missions of this paper.

Selected references

• P. Rusmevichientong, H. Topaloglu, Robust Assortment Optimization in Revenue Management Under the Multinomial Logit Choice Model, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1063
• K. Talluri, 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
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2), 2005. https://doi.org/10.1287/moor.1040.0129