Operations Research

Motivation

A linear multistage stochastic program chooses decisions over $T$ stages while a random vector is revealed one piece at a time; each decision may depend only on what has been observed so far. Such programs model production planning, capacity expansion, hydro scheduling and portfolio problems. Computing their optimal value exactly is intractable in general: Shapiro and Nemirovski argue that even medium-accuracy solutions are out of reach when the number of stages grows (Shapiro–Nemirovski 2005), and already the one-stage problem is #P-hard (Dyer–Stougie 2006, Theorem 3.2, as cited by the paper).

Linear decision rules restrict every decision to be an affine function of the observations. Introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried into stochastic programming by Shapiro and Nemirovski and by Chen, Sim, Sun and Zhang (2008), they turn the problem into a finite one whose optimal value is an upper bound. Kuhn, Wiesemann and Georghiou (Optimization Online 2009/02/2218; Math. Program. 130, 2011) apply the same restriction to the dual problem, which yields a lower bound. They show that, for polyhedral supports, both bounds are values of explicit linear programs. This mission formalizes the multistage version of that statement, Theorem 3 of the preprint.

Setting

Stages are $t \in \mathbb T = \{1,\dots,T\}$. The uncertainty is $\xi = (\xi_1,\dots,\xi_T) \in \mathbb R^k$ with $\xi_t \in \mathbb R^{k_t}$ and $k = \sum_t k_t$; by convention $k_1 = 1$ and $\xi_1 = 1$. The history at stage $t$ is $\xi^t = (\xi_1,\dots,\xi_t) \in \mathbb R^{k^t}$, $k^t = \sum_{s\le t} k_s$, and the truncation operator $P_t = [\,I\ \ 0\,] \in \mathbb R^{k^t\times k}$ maps $\xi$ to $\xi^t$. The law $\mathbb P$ of $\xi$ has support $\Xi = \{\xi : W\xi \ge h\}$, a nonempty bounded polyhedron spanning $\mathbb R^k$, whose first two constraints encode $\xi_1 = 1$. $\mathbb E_t$ denotes conditional expectation given $\xi^t$, and $M = \mathbb E(\xi\xi^\top)$ is the second-order moment matrix.

A stage-$t$ decision is a square-integrable Borel function $x_t$ of $\xi^t$ (written $x_t \in \mathcal L^2_{k^t,n_t}$). The program $\mathcal{MSP}$ minimizes

$$\mathbb E\Big(\sum_{t=1}^T c_t(\xi^t)^\top x_t(\xi^t)\Big) \quad\text{subject to}\quad \mathbb E_t\Big(\sum_{s=1}^T A_{ts}x_s(\xi^s)\Big) \le b_t(\xi^t)\ \ \mathbb P\text{-a.s.},\ t\in\mathbb T,$$

with deterministic matrices $A_{ts}$, $c_t(\xi^t) = C_tP_t\xi$ and $b_t(\xi^t) = B_tP_t\xi$. The linear conditional mean assumption requires $\mathbb E_t(\xi) = M_tP_t\xi$ almost surely for some $M_t \in \mathbb R^{k\times k^t}$; it holds, for example, for stagewise independent data.

The primal approximation $\mathcal{MSP}^u$ sets $x_t(\xi^t) = X_tP_t\xi$ and slacks $s_t(\xi^t) = S_tP_t\xi$. The dual approximation $\mathcal{MSP}^l$ keeps general rules $x_t, s_t$ but imposes the slack equations only in the weak form $\mathbb E([\sum_s A_{ts}x_s + s_t - b_t][P_t\xi]^\top) = 0$. The linear programs (4.2) and (4.6) are written in the matrices $X_t$, multipliers $\Lambda_t$ and slack matrices $S_t$, with $N_t = MP_t^\top(P_tMP_t^\top)^{-1}$.

Formalization targets

Goal: Theorem 3 (p. 22)

Under the standing assumptions, the linear conditional mean assumption, and strict feasibility of $\mathcal{MSP}$,

$$\mathrm{val}(\mathcal{MSP}^u) = \mathrm{val}(4.2) \qquad\text{and, if } k \ge 2 \text{ or } \hat W \ne 0,\qquad \mathrm{val}(\mathcal{MSP}^l) = \mathrm{val}(4.6),$$

as extended-real optimal values. Both equalities are part of the goal.

Milestones

1. Lemma 2 (p. 20): for every $x_t \in \mathcal L^2_{k^t,n_t}$ there is a unique $X_t$ with $X_tP_tM = \mathbb E(x_t(\xi^t)\xi^\top)$, and likewise for slacks.
2. Lemma 3 (p. 21): a moment condition $S_tP_tM = \mathbb E(s(\cdot)\xi^\top)$ with $s \ge 0$ can be met by a non-anticipative slack $s_t(\xi^t)$ iff it can be met by a slack depending on the full $\xi$.
3. §4, (4.7) (p. 21): through (4.3), the equality constraints of $\mathcal{MSP}^l$ are equivalent to $\sum_s A_{ts}X_sP_sN_tP_t + S_tP_t = B_tP_t$.

Significance

The theorem makes both linear-decision-rule bounds on a multistage stochastic program computable by linear programming, with size polynomial in $k$, $l$, $\sum_t m_t$ and $\sum_t n_t$ and hence typically linear in the number of stages. The gap between the two values measures the suboptimality of the primal linear rule. These results underlie later work on piecewise-linear and lifted decision rules and on multistage robust and distributionally robust optimization.

The preprint omits the proof of Theorem 3 ("it widely parallels the argumentation in Section 2"), so a formal proof has to supply the multistage details: the conditional-expectation bookkeeping, the truncation operators and the transfer of the one-stage cone description to non-anticipative slacks. No part of this paper has been machine-checked before; the companion mission of this series formalizes the one-stage Theorem 1.

Difficulty

The obvious route repeats the one-stage argument stage by stage, and it breaks at the slack constraints of $\mathcal{MSP}^l$. A slack $s_t$ must be a function of $\xi^t$ alone, while the one-stage cone characterization of moment vectors $\mathbb E(s(\xi)\xi)$ concerns functions of the full $\xi$; Lemma 3 bridges them only through the linear conditional mean assumption and conditional expectations. A second difficulty is the closure gap between that cone and its polyhedral outer description: the equality of $\mathrm{val}(\mathcal{MSP}^l)$ and $\mathrm{val}(4.6)$ relies on strict feasibility, and a proof that ignores it is wrong. On the primal side, the passage from almost sure constraints to identities of matrices needs both that every point of $\Xi$ is charged by $\mathbb P$ and that $\Xi$ spans $\mathbb R^k$.

Formalization scope

Vectors are functions Fin d → ℝ; stage $t$ is the Fin T index $t-1$ and coordinate $1$ is index 0. The history dimension is kbar kk t, the truncation is the restriction to the first $k^t$ coordinates, and $P_t$ is also given as a $0/1$ matrix. $\mathbb E_t$ is Mathlib's condExp with respect to the σ-algebra generated by $P_t$. "$\Xi$ is the support of $\mathbb P$" means: $\Xi$ closed, $\mathbb P(\Xi^c) = 0$, and every ball around a point of $\Xi$ has positive mass. Decision rules are Borel functions of the history whose composition with $P_t$ is in $L^2(\mathbb P)$. Optimal values are infima in EReal ($+\infty$ if infeasible, $-\infty$ if unbounded), and "equivalent" means equal optimal values. The matrices $M_t$ are data, with the conditional-mean identity as a hypothesis.

Three conventions are fixed where the page is silent or misprinted. Strict feasibility of $\mathcal{MSP}$, not defined in §4, is the analogue of (2.9) for the standard form (4.1): slacks at least $\varepsilon > 0$ almost surely. The equality constraint of $\mathcal{MSP}^l$ is printed with $s_t - b_t$ inside $\sum_s$; the formalization follows (4.7), where the sum covers only $A_{ts}x_s$. The sign condition in (4.5c) is printed as $\tilde s_t(\xi^t) \ge 0$ for a function of $\xi$, and is read as $\tilde s_t(\xi) \ge 0$. The theorem's last sentence (polynomial size, efficient solvability) is informal and not formalized. One hypothesis is added: the goal's second equality assumes $k \ge 2$ or that some row of $\hat W$ (the rows of $W$ below (2.1b)) is nonzero (the first equality is stated without it). For $k = 1$ the support is the single point $\{1\}$, and if $W$ has no nonzero row beyond (2.1b) the cone of Proposition 3 is all of $\mathbb R$; the printed second equality then fails (a strictly feasible one-stage instance has $\mathrm{val}(\mathcal{MSP}^l) = 0$ while (4.6) is unbounded below). The added hypothesis excludes exactly this case.

Expectations are Bochner integrals, which vanish on non-integrable functions; under the standing assumptions $\xi$ is bounded almost surely, so all integrands involving square-integrable rules are integrable and no constraint is satisfied vacuously. Matrix.inv returns $0$ on singular matrices, but $P_tMP_t^\top$ is positive definite under the standing assumptions. The linear conditional mean hypothesis cannot be dropped from Lemmas 2 and 3: without it $X_t$ need not exist.

A complete development needs the support and moment facts of §2 ($M \succ 0$, almost sure constraints extend to $\Xi$), Farkas-type duality for the polyhedron $\Xi$, the tower property of conditional expectation, and the cone results of Propositions 3 and 4 of the preprint. These are reusable across the series. Proofs of the milestones, or of these supporting facts as separate lemmas, are welcome.

Selected references

• D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Optimization Online preprint 2009/02/2218, 2009; Math. Program. 130:177–209, 2011. https://optimization-online.org/2009/02/2218/ ; https://doi.org/10.1007/s10107-009-0331-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99:351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
• A. Shapiro, A. Nemirovski, On complexity of stochastic programming problems, in Continuous Optimization, Springer, 2005. https://doi.org/10.1007/0-387-26771-9_4
• X. Chen, M. Sim, P. Sun, J. Zhang, A linear decision-based approximation approach to stochastic programming, Oper. Res. 56(2):344–357, 2008. https://doi.org/10.1287/opre.1070.0441
• M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Math. Program. 106:423–432, 2006. https://doi.org/10.1007/s10107-005-0597-0

Motivation

Scheduling jobs whose processing times are not known in advance is a basic problem of production planning, project management and computing systems. In the stochastic machine scheduling model only the distribution of each processing time is known beforehand; the actual duration of a job is revealed when the job completes. A solution is then not a schedule but a scheduling policy, which decides at every point in time what to start next on the basis of what has been observed so far.

For precedence-constrained problems, constant-factor guarantees for policies were long unavailable. Möhring, Schulz and Uetz (J. ACM 1999) introduced LP relaxations with load inequalities for stochastic scheduling and obtained the first constant-factor policies for independent jobs. In the deterministic setting, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 2001) gave a list scheduling algorithm with deliberate idle times for $\mathrm P\,|\,r_j,\mathit{prec}\,|\sum w_jC_j$. Skutella and Uetz (SIAM J. Comput. 2005) combined the two and gave the first constant-factor approximation for stochastic scheduling with precedence constraints and release dates. This mission formalizes that result.

Setting

A finite set $V$ of jobs is to be scheduled on $m\ge1$ identical parallel machines, nonpreemptively. Precedence constraints are the arcs $A$ of an acyclic digraph: an arc $(i,j)$ requires $j$ to start no earlier than $i$ completes, and $i$ is a predecessor of $j$ if a directed path leads from $i$ to $j$. Job $j$ has a release date $r_j\ge0$, before which it must not start, and a weight $w_j\ge0$. Following §2 of the paper, release dates are assumed to respect the precedence constraints (Assumption 2.1: $r_i\le r_j$ whenever $i$ is a predecessor of $j$).

The processing time of job $j$ is a random variable $P_j\ge0$ with finite mean $\mathrm E[P_j]$; the $P_j$ are stochastically independent. For a realization $p$ of the processing times, a feasible schedule assigns start times $S_j\ge r_j$ such that $S_i+p_i\le S_j$ for every arc and at most $m$ jobs are in process at any time. A policy $\Pi$ maps realizations to feasible schedules; it is nonanticipatory if what it has started by time $t$ depends only on what has been observed by $t$. The completion time of $j$ under $\Pi$ is $C^\Pi_j(P)=S^\Pi_j(P)+P_j$.

The coefficient of variation is $\mathrm{CV}[P_j]=\sqrt{\mathrm{Var}[P_j]}/\mathrm E[P_j]$; the mission assumes $\mathrm{CV}[P_j]\le\sqrt\Delta$ for all $j$ and some $\Delta\ge0$. With $\mu_j=\mathrm E[P_j]$, the set function

$$f(W)=\frac1{2m}\Big(\big(\textstyle\sum_{j\in W}\mu_j\big)^2+\sum_{j\in W}\mu_j^2\Big)-\frac{(m-1)(\Delta-1)}{2m}\sum_{j\in W}\mu_j^2$$

defines the LP relaxation: minimize $\sum_jw_jC^{\mathrm{LP}}_j$ subject to $\sum_{j\in W}\mu_jC^{\mathrm{LP}}_j\ge f(W)$ for all $W\subseteq V$, $C^{\mathrm{LP}}_j\ge C^{\mathrm{LP}}_i+\mu_j$ for $(i,j)\in A$, and $C^{\mathrm{LP}}_j\ge\mu_j$.

Algorithm CMNS takes a priority list $L$ and a parameter $\beta$. Whenever a machine is idle and the first job of the residual list (the jobs not yet scheduled) is available, it is scheduled. Otherwise the first available job $j$ of the residual list is deliberately delayed; idle machines accumulate deliberate idle time charged to $j$, and once $j$ has been charged $\beta\,\mathrm E[P_j]$ it is scheduled out of order. The critical chain of a job $j$ is traced backwards through critical predecessors (those completing last, after $r_j$); its length is $\ell_j(p)$.

Formalization targets

Goal: Theorem 4.1

If $C^{\mathrm{LP}}$ is an optimal LP solution, $L$ orders the jobs by nondecreasing $C^{\mathrm{LP}}_j$ and $\beta>0$, then for every feasible nonanticipatory policy $\Pi$

$$\mathrm E\Big[\sum_jw_jC^{\mathrm{CMNS}}_j(P)\Big]\le(1+\beta)\Big(1+\frac1\beta+\max\Big\{1,\frac{m-1}m\Delta\Big\}\Big)\,\mathrm E\Big[\sum_jw_jC^\Pi_j(P)\Big].$$

Milestones

1. Observation 2.4: each job is charged at most $\beta\,\mathrm E[P_j]$; idle time while $j$ waits is charged to jobs before $j$; no deliberate idle time is uncharged.
2. Lemma 2.5: the per-realization bound $C_j(p)\le\frac{m-1}m\ell_j(p)+\frac1mr_j+\frac1m\big(\sum_{i\in B_j}(p_i+\beta\mathrm E[P_i])+\sum_{i\in O_j(p)}p_i\big)$.
3. Lemma 2.6: $\mathrm E[\sum_{i\in O_j(P)}P_i]=\mathrm E[\sum_{i\in O_j(P)}\mathrm E[P_i]]$.
4. Lemma 2.7: $\frac1m\mathrm E[\sum_{i\in O_j(P)}\mathrm E[P_i]]\le\frac1\beta\mathrm E[\ell_j(P)]$.
5. Theorem 2.8: $\mathrm E[C_j(P)]\le\big(\frac{m-1}m+\frac1\beta\big)\mathrm E[\ell_j(P)]+\frac{1+\beta}m\sum_{i\in B_j}\mathrm E[P_i]+\frac1mr_j$.
6. Theorem 3.1: the load inequalities $\sum_{j\in W}\mathrm E[P_j]\mathrm E[C^\Pi_j(P)]\ge f(W)$.
7. §3: expected completion times of any policy are LP-feasible, so the LP optimum is a lower bound.
8. Lemma 3.3: $\frac1m\sum_{k\le j}\mathrm E[P_k]\le\big(1+\max\{1,\frac{m-1}m\Delta\}\big)C^{\mathrm{LP}}_j$ along the LP order.
9. §4: $\ell_j(p)\le C_j(p)$ in any feasible schedule, so $\mathrm E[\ell_j(P)]$ is a lower bound for every policy.

Significance

The theorem gives a policy with a performance guarantee independent of the number of jobs for $\mathrm P\,|\,r_j,\mathit{prec}\,|\,\mathrm E[\sum w_jC_j]$, using only the expected processing times and a bound on their coefficients of variation. For NBUE distributions ($\Delta=1$) and $\beta=1/\sqrt2$ it yields $3+2\sqrt2\approx5.83$, matching the deterministic guarantee of Chekuri et al. The analysis separates cleanly into an algorithmic half (Theorem 2.8, valid for arbitrary distributions) and a polyhedral half (load inequalities and Lemma 3.3), both reused for the in-forest results of the same paper and in later work on stochastic scheduling.

The result is proved in the paper; it has no machine-checked proof. Formalizing it produces a precise definition of nonanticipatory policies and of a list scheduling algorithm with deliberate idle times in continuous time, a formal proof of the Möhring–Schulz–Uetz load inequalities, and a verified approximation guarantee for a stochastic scheduling policy.

Difficulty

Lemma 2.6 is the step where the stochastic setting departs from the deterministic one: the set $O_j(P)$ of out-of-order jobs is random and correlated with the schedule, and the identity holds only because the decision to start a job out of order is taken before its processing time is revealed. Making this rigorous requires a formal notion of nonanticipation and an independence argument over a random set. On the algorithmic side, the bookkeeping of deliberate idle time, which accumulates at a rate equal to the number of idle machines, must be made precise at instants where several jobs start, including jobs of length zero. The load inequalities compare every nonanticipatory policy at once and involve second moments of the processing times, so they cannot be checked policy by policy.

Formalization scope

Jobs form a finite type; arcs are a relation whose transitive closure is irreflexive; machine capacity is the counting condition "at most $m$ jobs in process", with half-open processing intervals. Processing times may be zero. The CV bound is encoded as finite second moments, positive means and $\mathrm{Var}[P_j]\le\Delta\,\mathrm E[P_j]^2$.

Algorithm CMNS is characterized by its rules: a decision order nondecreasing in time, the scheduling rule at each decision, and the condition that after the decisions at any time nothing remains to be done. A CMNS policy is a map $\sigma$ with this property for every realization. Nonanticipation and measurability of $\sigma$, which the paper asserts without proof (p. 795; §5), are hypotheses. Critical chains use a fixed tie-breaking order.

Standing assumptions and added hypotheses: independence, Assumption 2.1, $r_j\ge0$, $w_j\ge0$ and finite means appear in every statement where they are used. $\beta>0$ is assumed wherever $1/\beta$ appears (Lemma 2.7, Theorem 2.8), where the page allows $\beta\ge0$ with $1/0=\infty$. Lemma 2.6 assumes that $L$ is a linear extension, as in the surrounding Lemma 2.5 and Theorem 2.8; with zero processing times it fails otherwise. Comparator policies have integrable completion times and, like $\sigma$, are measurable for the law of $P$, which §5's requirement that every policy be universally measurable implies.

The goal is not trivialized: comparators range over every feasible nonanticipatory policy, not over list policies or the algorithm itself; $C^{\mathrm{LP}}$ is optimal over all $W\subseteq V$, not merely feasible; and the expected cost of CMNS is asserted to be finite, so neither side can collapse to a default integral value.

Contributions welcome: proofs of any milestone, in particular Theorem 3.1 and Lemma 3.3, which are reusable for the companion in-forest mission, and a proof that the CMNS rules determine a unique, nonanticipatory, measurable policy.

Selected references

• M. Skutella, M. Uetz, Stochastic machine scheduling with precedence constraints, SIAM J. Comput. 34(4) (2005) 788–802. https://doi.org/10.1137/S0097539702415007
• R. H. Möhring, A. S. Schulz, M. Uetz, Approximation in stochastic scheduling: the power of LP-based priority policies, J. ACM 46(6) (1999) 924–942. https://doi.org/10.1145/331524.331530
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31(1) (2001) 146–166. https://doi.org/10.1137/S0097539797327180
• R. H. Möhring, F. J. Radermacher, G. Weiss, Stochastic scheduling problems I: General strategies, Z. Oper. Res. 28 (1984) 193–260. https://doi.org/10.1007/BF01919323

Motivation

Linear stochastic programs with recourse model decisions that are taken after an uncertain parameter $\xi$ has been observed: the decision is a decision rule $x(\xi)$, a function of the data. Computing the optimal value exactly is intractable in general. Dyer and Stougie showed that already two-stage linear stochastic programs are #P-hard (Math. Program. 2006), and the same holds for the one-stage problem $\mathcal{SP}$ below even when $\mathbb P$ is uniform on a cube.

A widely used remedy restricts decision rules to be linear in $\xi$. Ben-Tal, Goryashko, Guslitzer and Nemirovski introduced this restriction in robust optimization (Math. Program. 2004); Shapiro and Nemirovski (2005) and Chen, Sim, Sun and Zhang (Oper. Res. 2008) carried it into stochastic programming. The restriction yields an upper bound, but on its own it says nothing about how much optimality is lost. Kuhn, Wiesemann and Georghiou (Optimization Online 2009/02/2218; published in Math. Program. 2011) also apply the linear restriction to the dual multipliers. This gives a lower bound, so the gap between the two computable bounds estimates the approximation error. This mission formalizes the paper's model result for the case of fixed recourse and polyhedral support (§2, Theorem 1).

Setting

Uncertainty is a probability measure $\mathbb P$ on $(\mathbb R^k, \mathfrak B(\mathbb R^k))$. The support $\Xi$ of $\mathbb P$ is the smallest closed set of probability one. A decision rule is an element of $\mathcal L^2_{k,n}$, the Borel measurable, square-integrable functions $\mathbb R^k \to \mathbb R^n$. Inequalities between vectors and matrices are componentwise.

The data are a fixed recourse matrix $A \in \mathbb R^{m\times n}$, matrices $C \in \mathbb R^{n\times k}$ and $B \in \mathbb R^{m\times k}$ giving the costs $c(\xi) = C\xi$ and right-hand sides $b(\xi) = B\xi$, and $W \in \mathbb R^{l\times k}$, $h \in \mathbb R^l$. The stochastic program is

$$\mathcal{SP}:\quad \min_{x \in \mathcal L^2_{k,n}} \ \mathbb E\big(c(\xi)^\top x(\xi)\big) \quad\text{s.t.}\quad Ax(\xi) \le b(\xi)\ \ \mathbb P\text{-a.s.}$$

The standing assumptions of §2 are:

• the support is the nonempty bounded polyhedron $\Xi = \{\xi : W\xi \ge h\}$ (2.1a);
• (2.1b) holds: the first two rows of $W$ are $e_1^\top$ and $-e_1^\top$, the remaining rows form $\widehat W$, and $h = (1,-1,0,\dots,0)$, so that $\xi_1 = 1$ on $\Xi$;
• $\Xi$ spans $\mathbb R^k$.

The second-order moment matrix is $M = \mathbb E(\xi\xi^\top)$. $\mathcal{SP}$ is strictly feasible (2.9) if some $\bar x \in \mathcal L^2_{k,n}$, $\bar s \in \mathcal L^2_{k,m}$ and $\varepsilon > 0$ satisfy $A\bar x(\xi) + \bar s(\xi) = b(\xi)$ and $\bar s(\xi) \ge \varepsilon e$ almost surely.

The two approximations are as follows.

• Primal linear decision rules, $\mathcal{SP}^u$: minimize $\operatorname{Tr}(MC^\top X)$ over $X \in \mathbb R^{n\times k}$, $S \in \mathbb R^{m\times k}$ with $AX\xi + S\xi = B\xi$ and $S\xi \ge 0$ almost surely.
• Dual linear decision rules, $\mathcal{SP}^l$: minimize $\mathbb E(c(\xi)^\top x(\xi))$ over $x \in \mathcal L^2_{k,n}$, $s \in \mathcal L^2_{k,m}$ with $\mathbb E\big([Ax(\xi)+s(\xi)-b(\xi)]\xi^\top\big) = 0$ and $s \ge 0$ almost surely.

Formalization targets

Goal: Theorem 1 (p. 10)

Under the standing assumptions, $\widehat W \ne 0$ (see Formalization scope) and strict feasibility,

$$\operatorname{val}\mathcal{SP}^u = \operatorname{val}(2.3) \quad\text{and}\quad \operatorname{val}\mathcal{SP}^l = \operatorname{val}(2.8),$$

where (2.3) and (2.8) are the linear programs

$$(2.3)\quad \min_{X,\Lambda}\ \operatorname{Tr}(MC^\top X)\ \text{ s.t. }\ AX + \Lambda W = B,\ \Lambda h \ge 0,\ \Lambda \ge 0,$$ $$(2.8)\quad \min_{X,S}\ \operatorname{Tr}(MC^\top X)\ \text{ s.t. }\ AX + S = B,\ (W - he_1^\top)MS^\top \ge 0.$$

Milestones, in the order the proof uses them

1. §2.2 (p. 5). The almost-sure constraints of $\mathcal{SP}^u$ hold on all of $\Xi$, and $AX\xi + S\xi = B\xi$ a.s. is equivalent to $AX + S = B$.
2. Proposition 1 (p. 5). If $\Xi$ is nonempty, then $z^\top\xi \ge 0$ on $\Xi$ if and only if $z = W^\top\lambda$ for some $\lambda \ge 0$ with $h^\top\lambda \ge 0$.
3. Proposition 2 (p. 7). $M$ is positive definite and invertible.
4. §2.4 (p. 7). $\operatorname{val}\mathcal{SP}^l$ equals the optimal value of the moment problem (2.6).
5. Proposition 3 (p. 7). If $\widehat W \ne 0$, then $\emptyset \ne \operatorname{int}\mathcal K \subseteq \mathcal K_{\mathbb P} \subseteq \mathcal K$, for the polyhedral cone $\mathcal K = \{z : (W-he_1^\top)z \ge 0\}$ and the moment cone $\mathcal K_{\mathbb P} = \{\mathbb E(s(\xi)\xi) : s \in \mathcal L^2_{k,1},\ s \ge 0\}$.
6. Proposition 4 (p. 9). Under strict feasibility and $\widehat W \ne 0$, (2.6) and (2.8) have the same optimal value.

Significance

Because $\mathcal{SP}^u \ge \mathcal{SP} \ge \mathcal{SP}^l$, Theorem 1 brackets the value of an intractable stochastic program between two explicit linear programs. The sizes of these programs are polynomial in $k, l, m, n$. They depend on $\mathbb P$ only through its support and its second-order moment matrix. The difference $\operatorname{val}(2.3) - \operatorname{val}(2.8)$ is therefore a computable certificate of how much the linear-decision-rule restriction can lose. Sections 3 and 4 of the paper extend the same scheme to random recourse (semidefinite programs) and to multistage problems; they are the subjects of the companion missions 2 and 3.

The theorem is proved in the paper. As far as a search of the platform shows, none of the statements above has a machine-checked proof. A formal proof would check the measure-theoretic steps that the paper passes over quickly. These are the passage from "almost surely" to "on the support", the density argument behind $\operatorname{int}\mathcal K \subseteq \mathcal K_{\mathbb P}$, and the approximation argument of Proposition 4. A formal proof would also produce reusable results on robust counterparts of polyhedral constraints and on moment cones.

Difficulty

The primal half is robust-optimization duality. Its only delicate point is that almost-sure constraints become constraints on all of $\Xi$, which uses the fact that every point of the support is charged. The dual half is harder. The constraint "$SM$ has rows in $\mathcal K_{\mathbb P}$" is a family of moment problems over nonnegative square-integrable densities, and $\mathcal K_{\mathbb P}$ is in general not closed. Replacing it by the polyhedral cone $\mathcal K$ is exact only up to the boundary, and it is strict feasibility that removes the boundary effect. Without strict feasibility the optimal values of (2.6) and (2.8) are only known to bracket each other. The proof of Proposition 3 also needs a description of the closed cone generated by $\Xi$, and this description uses (2.1b).

Formalization scope

Vectors in $\mathbb R^k$ are Fin k → ℝ and matrices are Matrix (Fin m) (Fin k) ℝ. The paper's 1-based indices are 0-based in Lean, so $e_1$ is index 0 and the rows of (2.1b) are rows 0 and 1. The data form a structure Setting, and the standing assumptions form one predicate Standing. The support is encoded by three conditions on $\Xi$: it is closed, $\mathbb P(\Xi^c) = 0$, and every ball centred in $\Xi$ has positive mass. This is equivalent to "smallest closed set of probability one"; $\mathbb P(\Xi) = 1$ alone would not be enough. Decision rules are measurable functions with MemLp x 2 P. Expectations of vector- and matrix-valued quantities are written entrywise as Bochner integrals. Under the standing assumptions $\xi$ is bounded almost surely, so every integrand involved is integrable and no integral defaults to $0$.

"Equivalent" means equal optimal values. Each optimal value is the infimum of the objective over the feasible set in EReal: $+\infty$ if the problem is infeasible and $-\infty$ if it is unbounded below. A one-sided inequality between the values, or the bare statement that the problems are linear programs, is not Theorem 1 and does not close the goal. Strict feasibility is a hypothesis of both equalities, as printed. Proposition 1 is stated for any $W, h$ with a nonempty polyhedron, since nonemptiness is the only property of $\Xi$ it uses. Proposition 3, Proposition 4 and Theorem 1 carry one hypothesis the paper does not state, $\widehat W \ne 0$ (some row of $W$ below the first two is nonzero). The printed statements are false without it: for $k = 1$, $W = (1,-1)^\top$, $h = (1,-1)^\top$, $\mathbb P = \delta_1$ every assumption holds, $W - he_1^\top = 0$, so $\mathcal K = \mathbb R$ while $\mathcal K_{\mathbb P} = [0,\infty)$, and (2.8) loses the sign constraint $S \ge 0$ that (2.6) keeps. Under the standing assumptions the hypothesis is automatic whenever $k \ge 2$. Theorem 1's closing sentence ("the sizes of these linear programs are polynomial … efficiently solvable") is informal and is not formalized.

A complete development needs strong LP duality or Farkas' lemma for inequality systems, the support of a measure in $\mathbb R^k$, density of $L^2$-densities in nonnegative measures, and basic facts on interiors of polyhedral cones. The Farkas lemma is on the platform (LinearOptimization.farkas_lemma). Proofs of the milestones are welcome independently. Proposition 1 and Proposition 3 are reusable outside this paper.

Selected references

• D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Optimization Online 2009/02/2218 (2009); Math. Program. 130 (2011) 177–209. https://doi.org/10.1007/s10107-009-0331-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999) 1–13. https://doi.org/10.1016/S0167-6377(99)00016-4
• X. Chen, M. Sim, P. Sun, J. Zhang, A linear decision-based approximation approach to stochastic programming, Oper. Res. 56 (2008) 344–357. https://doi.org/10.1287/opre.1070.0441
• M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Math. Program. 106 (2006) 423–432. https://doi.org/10.1007/s10107-005-0597-0
• A. Shapiro, A. Nemirovski, On complexity of stochastic programming problems, in Continuous Optimization, Springer (2005) 111–144. https://doi.org/10.1007/0-387-26771-9_4

Motivation

Risk measures quantify the danger of an uncertain cost $X$ by a single number. The axiomatic theory of coherent and convex risk measures (Artzner, Delbaen, Eber and Heath, Coherent measures of risk, 1999; Föllmer and Schied, Convex measures of risk and trading constraints, 2002) is static: the risk is evaluated once, with no information beyond what is known at time zero. Multistage stochastic optimization and dynamic risk management need risk evaluated conditionally: at time 1 part of the uncertainty has been resolved, and the risk of a time-2 cost should be a function of what is known at time 1.

Ruszczyński and Shapiro, in Conditional risk mappings (preprint of February 21, 2004; journal version Mathematics of Operations Research 31(3), 2006), extend their earlier static theory (Optimization of convex risk functions, Math. Oper. Res. 31(3), 2006) to this conditional setting. They define conditional risk mappings by three axioms, derive a pointwise conjugate duality, and show that positively homogeneous conditional risk mappings are, under regularity conditions, suprema of countably many conditional expectations. The last result explains the word conditional: the conditional expectation is the prototype, and every positively homogeneous conditional risk mapping is a worst case over a countable family of them.

Setting

Let $\Omega$ be a set with $\sigma$-algebras $\mathcal F_1\subset\mathcal F_2$; $\mathcal F_1$ is the information available when risk is evaluated. Let $\mathcal X_2$ be a real vector space of $\mathcal F_2$-measurable functions $X:\Omega\to\mathbb R$, and $\mathcal X_1\subset\mathcal X_2$ a subspace of $\mathcal F_1$-measurable ones. Let $\mathcal Y_2$ be a real vector space of finite signed measures on $(\Omega,\mathcal F_2)$ with $\int|X|\,d|\mu|<\infty$, and pair them by

$$\langle\mu,X\rangle=\int_\Omega X\,d\mu .$$

Both spaces carry locally convex topologies that are compatible with this pairing: the continuous linear functionals on each space are exactly the pairings with elements of the other. Two standing conditions hold throughout: (C) if $\mu\in\mathcal Y_2$ is not a nonnegative measure, some nonnegative $X\in\mathcal X_2$ has $\langle\mu,X\rangle<0$; (C′) $\mathbb 1_B\in\mathcal X_1$ for every $B\in\mathcal F_1$.

A conditional risk mapping is a map $\rho:\mathcal X_2\to\mathcal X_1$ with, writing $\rho_\omega(X)=[\rho(X)](\omega)$:

• (A1) convexity: $\rho_\omega(tX+(1-t)Y)\le t\rho_\omega(X)+(1-t)\rho_\omega(Y)$ for $t\in[0,1]$;
• (A2) monotonicity: $Y(\omega')\ge X(\omega')$ for all $\omega'$ implies $\rho_\omega(Y)\ge\rho_\omega(X)$;
• (A3) translation equivariance: $\rho(X+Y)=\rho(X)+Y$ for every $Y\in\mathcal X_1$.

Costs are minimised: smaller $X$ is better. All inequalities hold at every $\omega\in\Omega$, not almost surely. $\rho$ is positively homogeneous if $\rho(tX)=t\rho(X)$ for $t>0$, and lower semicontinuous if each $\rho_\omega$ is.

The conjugate is $\rho^*(\mu,\omega)=\sup_{X}\{\langle\mu,X\rangle-\rho_\omega(X)\}\in\overline{\mathbb R}$ and the risk envelope is $\mathcal A(\omega)=\{\mu:\rho^*(\mu,\omega)<\infty\}$. $\mathcal P_{\mathcal Y_2}$ denotes the probability measures in $\mathcal Y_2$, and $\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)$ those $\nu$ with $\nu(B)=\mathbb 1_B(\omega)$ for all $B\in\mathcal F_1$. A map $\omega\mapsto\mu_\omega$ is weakly* $\mathcal F_1$-measurable if every $\omega\mapsto\langle\mu_\omega,X\rangle$ is $\mathcal F_1$-measurable. For such a selection of $\mathcal A$, the operator $[\mathbb Q_\mu(\nu)](A)=\int\mu_\omega(A)\,d\nu(\omega)$ acts on $\mathcal Y_2$. Assumption (K): $\mathcal P_{\mathcal Y_2}$ is compact, and every such $\mathbb Q_\mu$ maps $\mathcal P_{\mathcal Y_2}$ into itself with a closed graph. Finally, $\mu(\cdot)$ is the conditional probability of $\nu$ given $\mathcal F_1$ if each $\omega\mapsto\mu_\omega(A)$ is $\mathcal F_1$-measurable and $\int_S\mu_\omega(A)\,d\nu=\nu(A\cap S)$ for $S\in\mathcal F_1$, $A\in\mathcal F_2$; then $\mathbb E_\nu[X|\mathcal F_1](\omega)=\langle\mu_\omega,X\rangle$.

Formalization targets

Goal: Theorem 2 (p. 11)

If $\mathcal X_2$ is separable, (K) holds and $\rho$ is a positively homogeneous, lower semicontinuous conditional risk mapping, then there are probability measures $\nu^i\in\mathcal P_{\mathcal Y_2}$, $i\in\mathbb N$, with

$$\rho_\omega(X)=\sup_{i\in\mathbb N}\mathbb E_{\nu^i}[X|\mathcal F_1](\omega)\qquad\text{for all }X\in\mathcal X_2,\ \omega\in\Omega,$$

each conditional expectation being the integral against a weakly* $\mathcal F_1$-measurable conditional probability of $\nu^i$.

Milestones

1. $\operatorname{dom}\rho^*(\cdot,\omega)\subseteq\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)$ (proof of Theorem 1, pp. 5–6).
2. Theorem 1 (p. 5): $\rho_\omega(X)=\sup_{\mu\in\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)}\{\langle\mu,X\rangle-\rho^*(\mu,\omega)\}$, and its converse.
3. (3.8) (p. 6): for positively homogeneous $\rho$, $\rho^*(\cdot,\omega)$ is the indicator of a closed convex $\mathcal A(\omega)$ and $\rho_\omega(X)=\sup_{\mu\in\mathcal A(\omega)}\langle\mu,X\rangle$.
4. Lemma 1 (p. 11): for separable $\mathcal X_2$, countably many weakly* measurable selections of $\mathcal A$ suffice.
5. Under (K), each $\mathbb Q_\mu$ has a fixed point in $\mathcal P_{\mathcal Y_2}$ (p. 10).
6. Proposition 3 (p. 9): a fixed point $\bar\nu$ of $\mathbb Q_\mu$ has $\mu$ as its conditional probability given $\mathcal F_1$.

Corollary 1 (p. 10, singleton envelopes give a conditional expectation) and Proposition 2 (p. 7, $\rho(YX)=Y\rho(X)$ for nonnegative $\mathcal F_1$-step functions $Y$) are included as further statements.

Significance

Theorem 2 identifies the positively homogeneous conditional risk mappings with suprema of conditional expectations. It is the conditional analogue of the representation of a coherent risk measure as a worst-case expectation over a set of probability measures. It shows that the axioms (A1)–(A3), stated at every $\omega$, are the right abstraction of "conditional": nothing beyond conditional expectations and a supremum is needed to generate them. Theorem 1, the pointwise duality on which it rests, is what makes conditional risk mappings usable in multistage problems. Its envelope form (3.8) is what the paper's composition results and dynamic programming equations in §5–§7 manipulate.

The results are proved in the paper, partly by reference: the duality of Theorem 1 by applying the authors' earlier unconditional theorem "verbatim" at each $\omega$, Lemma 1 through a measurable-selection theorem, and Theorem 2 through Kakutani's fixed-point theorem. None of them is formalized. A formalization would check these deferred steps. In particular the passage, in the proof of Lemma 1, from a dense subset of $\mathcal X_2$ to all of $\mathcal X_2$ uses only lower semicontinuity of $\rho_\omega$, and whether that suffices in every separable paired space is open to scrutiny.

Difficulty

Theorem 1 needs the Fenchel–Moreau theorem in a general locally convex space, paired through integrals against signed measures. Mathlib's convex duality is mostly finite-dimensional or normed, and the extended-real bookkeeping of conjugates is delicate. The main obstacle is Lemma 1. The envelope $\mathcal A(\omega)$ can be uncountable, and choosing countably many selections that are simultaneously measurable in $\omega$ and exhaust the supremum for every $X$ requires a measurable-selection theorem for multifunctions with values in $\mathcal Y_2$, a space that need not be metrizable. The obvious argument fixes a dense sequence $X_n$, picks $\varepsilon$-optimal measures for each $X_n$, and passes to general $X$ by semicontinuity. As written, that last step appears to need more than the proof supplies: approximation of $\langle\mu,X\rangle$ by $\langle\mu,X_n\rangle$ uniformly over the chosen $\mu$ needs more than lower semicontinuity of $\rho_\omega$. The fixed-point step needs a Kakutani-type theorem in a locally convex space, which Mathlib does not provide.

Formalization scope

$\mathcal X_2$ and $\mathcal Y_2$ are abstract real vector spaces with their own topologies (instances of IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ), realised by injective linear maps into $\Omega\to\mathbb R$ and into Mathlib's SignedMeasure Ω. They are not subspaces of $\Omega\to\mathbb R$ with the pointwise topology. The ambient MeasurableSpace Ω is $\mathcal F_2$; $\mathcal F_1\le\mathcal F_2$ is a structure field. The pairing is $\int X\,d\mu^+-\int X\,d\mu^-$, and integrability against $|\mu|$ is a field, so no integral takes a junk value. Compatibility includes continuity of both pairings as well as the representation of continuous functionals. The paper's space $\mathcal Y_1$ is not modelled; no statement uses it.

Committed conventions:

• every statement holds at every $\omega$; there are no a.e. classes;
• the conjugate and the supremum in (3.6) are in EReal;
• suprema of real numbers ((3.8), (4.7), (4.9)) are least upper bounds (IsLUB), never sSup on $\mathbb R$;
• (K) is taken in its closed-graph form and quantifies over every weakly* measurable selection;
• separability is that of the topology of $\mathcal X_2$.

Two hypotheses are added where the page relies on them implicitly. $\Omega$ is nonempty in the goal, Corollary 1 and the fixed-point milestone. $\mathbb 1_A\in\mathcal X_2$ for every $A\in\mathcal F_2$ is assumed in the goal, Proposition 3 and Corollary 1, because the paper derives measurability of $\omega\mapsto\mu_\omega(A)$ from weak* measurability.

The goal cannot be satisfied by an almost-everywhere version of a conditional expectation chosen separately for each $X$, which would allow $\rho$ itself as a "version". Each $\mathbb E_{\nu^i}[\cdot|\mathcal F_1]$ is integration against one kernel $\kappa^i$ that is a conditional probability of $\nu^i$. The goal mentions no selection, fixed point or Kakutani; $\mathbb Q_\mu$ appears only inside (K).

Contributions are welcome on all of the following:

• Fenchel–Moreau duality for paired locally convex spaces;
• measurable selections of weakly* measurable multifunctions;
• a Kakutani–Fan–Glicksberg or Schauder–Tychonoff fixed-point theorem.

All three are reusable beyond this mission.

Selected references

• A. Ruszczyński, A. Shapiro, Conditional risk mappings, preprint dated February 21, 2004; Mathematics of Operations Research 31(3):544–561, 2006. https://doi.org/10.1287/moor.1060.0204
• A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
• P. Billingsley, Probability and Measure, 3rd ed., Wiley, 1995 (conditional probability, pp. 430–431).

Motivation

Mathematical programs with complementarity constraints (MPCCs, also called MPECs) model optimization problems in which some constraints say that, for every index $i$, at least one of two nonnegative quantities $G_i(x)$, $H_i(x)$ must vanish. They arise in bilevel optimization, Stackelberg games, the design of equilibria in traffic and electricity markets, and contact problems in mechanics (Luo, Pang, Ralph 1996). Standard nonlinear-programming algorithms do not apply directly: at every feasible point of an MPEC the Mangasarian–Fromovitz constraint qualification fails, so the classical convergence theory of SQP or interior-point methods gives no guarantees.

Relaxation methods replace the MPEC by a sequence of better-behaved nonlinear programs $R(t_k)$ with a parameter $t_k \downarrow 0$, solve each one approximately, and study the limits of the computed points. The question every relaxation method has to answer is what kind of stationary point such limits are, and under which constraint qualification.

Timeline of the result formalized here:

• 2001: Scholtes introduces the global relaxation $G_iH_i \le t$ and proves that limits are C-stationary under MPEC-LICQ (SIAM J. Optim. 11).
• 2009: Kadrani, Dussault and Benchakroun propose a relaxation whose feasible set is the union of two shifted orthants (below), and prove that limits are M-stationary under MPEC-LICQ (SIAM J. Optim. 20).
• 2010–2013: Hoheisel, Kanzow and Schwartz compare five relaxation schemes; for the Kadrani et al. scheme they replace MPEC-LICQ by the much weaker MPEC-CPLD (Theorem 3.5 of the Würzburg preprint, published in Math. Program. 137).

Setting

The MPEC (1) on $\mathbb R^n$ is

$$\min f(x)\ \text{ s.t. }\ g_i(x)\le 0\ (i\le m),\ h_i(x)=0\ (i\le p),\ G_i(x)\ge 0,\ H_i(x)\ge 0,\ G_i(x)H_i(x)=0\ (i\le l),$$

with continuously differentiable data. At a feasible $x^*$ the index sets are $I_g=\{i\mid g_i(x^*)=0\}$, $I_{0+}=\{i\mid G_i(x^*)=0<H_i(x^*)\}$, $I_{00}=\{i\mid G_i(x^*)=0=H_i(x^*)\}$ (the biactive set) and $I_{+0}=\{i\mid G_i(x^*)>0=H_i(x^*)\}$.

A feasible $x^*$ is weakly stationary if there are multipliers $\lambda\ge 0$ with $\lambda_ig_i(x^*)=0$, $\mu$, $\gamma$, $\nu$ such that

$$\nabla f(x^*)+\sum_i\lambda_i\nabla g_i(x^*)+\sum_i\mu_i\nabla h_i(x^*)-\sum_i\gamma_i\nabla G_i(x^*)-\sum_i\nu_i\nabla H_i(x^*)=0,$$

with $\gamma_i=0$ on $I_{+0}$ and $\nu_i=0$ on $I_{0+}$. It is M-stationary if the same multipliers satisfy, for every $i\in I_{00}$, either $\gamma_i>0$ and $\nu_i>0$, or $\gamma_i\nu_i=0$.

The tightened program TNLP$(x^*)$ replaces the complementarity constraints by $G_i=0\le H_i$ on $I_{0+}$, $G_i\ge 0=H_i$ on $I_{+0}$ and $G_i=H_i=0$ on $I_{00}$. CPLD (constant positive linear dependence) for a nonlinear program says: whenever a set of active-constraint gradients is positive-linearly dependent at $x^*$ (a nontrivial vanishing combination with nonnegative coefficients on the inequalities), the same gradients stay linearly dependent on a neighbourhood of $x^*$. MPEC-CPLD is CPLD for TNLP$(x^*)$.

The relaxation of Kadrani et al. is, for $t>0$,

$$R^{KDB}(t):\quad\min f(x)\ \text{ s.t. }\ g(x)\le 0,\ h(x)=0,\ G_i(x)\ge -t,\ H_i(x)\ge -t,\ (G_i(x)-t)(H_i(x)-t)\le 0.$$

A stationary point of $R^{KDB}(t)$ is a feasible point with KKT multipliers.

Formalization targets

Goal: Theorem 3.5

$$t_k\downarrow 0,\quad x^k \text{ stationary for } R^{KDB}(t_k),\quad x^k\to x^*,\quad \text{MPEC-CPLD at } x^*\ \Longrightarrow\ x^* \text{ is M-stationary for (1)}.$$

Milestones, in proof order

1. MPEC-CPLD written out in terms of the MPEC data (§2.2, display (3)).
2. The KKT conditions of $R^{KDB}(t_k)$ recast with $\eta^{G,k}_i=-\gamma^k_i(H_i(x^k)-t_k)$, $\eta^{H,k}_i=-\gamma^k_i(G_i(x^k)-t_k)$: identity (11), disjointness (13), signs (14).
3. Eventual support inclusions (12) into $I_{00}\cup I_{0+}$ and $I_{00}\cup I_{+0}$.
4. Reduction to linearly independent gradients (15).
5. Boundedness of the multiplier sequence under MPEC-CPLD.
6. Weak stationarity of the limit $x^*$.

Significance

Local minimizers of an MPEC are M-stationary under weak constraint qualifications, whereas strong stationarity needs stronger ones such as MPEC-LICQ; a C-stationary point, the kind of limit the Scholtes relaxation delivers, may still admit first-order descent directions. Theorem 3.5 shows that the Kadrani et al. relaxation reaches M-stationary limits under a constraint qualification that is implied by MPEC-LICQ and MPEC-MFCQ and that holds, for instance, whenever all constraint functions are affine. It separates this scheme from the Scholtes and Steffensen–Ulbrich relaxations in the comparison of the paper.

The theorem is proved in the paper. As far as is known, no part of MPEC theory (constraint qualifications for MPECs, the stationarity hierarchy, relaxation schemes) has a machine-checked proof in Lean or Mathlib. This mission produces a formal account of the stationarity notions of Definition 2.3, of CPLD and MPEC-CPLD, and a complete formal proof of the convergence result, including the standard constraints $g$, $h$ that the paper's proof skips for brevity.

Difficulty

The obvious argument passes to the limit in the KKT conditions of $R^{KDB}(t_k)$. This fails because the multipliers need not be bounded: unlike under MPEC-LICQ or MPEC-MFCQ, MPEC-CPLD does not by itself bound KKT multipliers, and the KKT points of the relaxed programs need not satisfy any constraint qualification themselves (Example 3.6 of the paper). The second difficulty is the biactive set $I_{00}$: the product constraint contributes multipliers $\eta^{G,k}$, $\eta^{H,k}$ to both $\nabla G_i$ and $\nabla H_i$, with signs that are not fixed a priori, so a naive limit of the multipliers only gives C-stationarity-type information, or none at all.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and gradients are Mathlib's gradient; indices are 0-based (Fin m, Fin p, Fin l), and $m,p,l$ may be zero. Explicit choices fixed by the formalization:

• The standing assumption of p. 1 (all data $C^1$) is a hypothesis P.IsC1 of every analytic statement.
• "$\{t_k\}\downarrow 0$" is $t_k>0$, $t$ nonincreasing, $t_k\to 0$.
• "Stationary point" of an NLP means feasible with KKT multipliers (p. 5).
• Gradient sets are indexed families; linear (in)dependence is LinearIndependent ℝ of a family indexed by a disjoint union of subtypes, so repeated gradients count as dependent.
• In positive-linear dependence (Definition 2.1), "not all of them being zero" refers to all coefficients; the sign constraint is on the inequality part only.
• "Linearly dependent for all $x\in N(x^*)$" is ∀ᶠ y in 𝓝 x*.
• Definition 2.3 is used with its two misprints corrected ($\mu_i\nabla h_i(x^*)$; $\lambda_ig_i(x^*)=0$ for $i\le m$); weak and M-stationarity include feasibility of $x^*$, which the goal derives rather than assumes.
• TNLP$(x^*)$ has exactly the constraints the paper lists (subtype index sets, no padding with zero constraints).
• The standard constraints $g$, $h$, skipped in the paper's proof, are kept in every statement; displays (12) and (15) are extended by their $g$, $h$ parts.

Two trivializing readings are ruled out. M-stationarity uses one multiplier tuple for both the weak-stationarity equation and the condition on $I_{00}$; separate multipliers would make the sign condition vacuous. MPEC-CPLD demands linear dependence on a whole neighbourhood of $x^*$, not only at $x^*$; the pointwise version is a different hypothesis.

A complete development needs the gradient calculus of products and compositions on EuclideanSpace, a Carathéodory-type lemma (a conic combination can be reduced to one over linearly independent vectors with the same signs), and compactness of bounded sequences in finite dimensions. The Carathéodory lemma and the CPLD/positive-linear-dependence layer are reusable for any constraint-qualification argument in nonlinear programming. Proofs of individual milestones, and of the lemma behind (15), are welcome independently of the goal.

Selected references

• T. Hoheisel, C. Kanzow, A. Schwartz, Theoretical and numerical comparison of relaxation methods for mathematical programs with complementarity constraints, Preprint 299, Institute of Mathematics, University of Würzburg, 2010; Mathematical Programming 137 (2013) 257–288. https://doi.org/10.1007/s10107-011-0488-5
• A. Kadrani, J.-P. Dussault, A. Benchakroun, A new regularization scheme for mathematical programs with complementarity constraints, SIAM Journal on Optimization 20 (2009) 78–103. https://doi.org/10.1137/070705490
• S. Scholtes, Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM Journal on Optimization 11 (2001) 918–936. https://doi.org/10.1137/S1052623499361233
• S. Steffensen, M. Ulbrich, A new relaxation scheme for mathematical programs with equilibrium constraints, SIAM Journal on Optimization 20 (2010) 2504–2539. https://doi.org/10.1137/090748883
• Z.-Q. Luo, J.-S. Pang, D. Ralph, Mathematical Programs with Equilibrium Constraints, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511983658

Motivation

The dial-a-ride problem (DARP) asks for minimum-cost vehicle routes that carry users from individual pick-up points to individual drop-off points, subject to vehicle capacities, time windows, route durations and a bound on each user's ride time. It models door-to-door transport for elderly and disabled people, shared taxis and on-demand microtransit. Cordeau (Oper. Res. 54(3), 2006) gave a mixed-integer formulation of the DARP and the first branch-and-cut algorithm for it, and reported that instances with up to 30 users can be solved to optimality in reasonable time. The algorithm's strength comes from families of valid inequalities: linear constraints satisfied by every feasible route plan that cut off fractional points of the linear relaxation. Several of these families were adapted from the precedence-constrained asymmetric TSP (Balas, Fischetti and Pulleyblank 1995; Grötschel and Padberg 1985) and from the pick-up and delivery problem (Ruland and Rodin 1997); others, notably the generalized order-matching inequalities, were new in this paper.

Setting

Let $n$ be the number of users. Nodes are $N = \{0, 1, \dots, 2n+1\}$ with pick-up nodes $P = \{1,\dots,n\}$, drop-off nodes $D = \{n+1,\dots,2n\}$, origin depot $0$ and destination depot $2n+1$; user $i$ travels from node $i$ to node $n+i$. An instance fixes, for each node $i$, a load $q_i$, a service duration $d_i \ge 0$ and a time window $[e_i, l_i]$; for each pair of nodes a travel time $t_{ij}$; for each vehicle $k$ in a finite set $K$ a capacity $Q_k$ and a maximal route duration $T_k$; and a maximal ride time $L$. The standing conditions are $q_0 = q_{2n+1} = 0$, $q_i = -q_{n+i}$ for $i \in P$, and $d_0 = d_{2n+1} = 0$.

A feasible solution gives each vehicle $k$ a route $0 \to v_1 \to \dots \to v_r \to 2n+1$ through distinct nodes of $P \cup D$, start-of-service times $B^k_i$ and loads $Q^k_i$ such that every node of $P \cup D$ is visited by exactly one vehicle, $i$ and $n+i$ are on the same route with $i$ first, $B^k_j \ge B^k_i + d_i + t_{ij}$ and $Q^k_j \ge Q^k_i + q_j$ along each travelled arc, the ride time $B^k_{n+i} - (B^k_i + d_i)$ lies in $[t_{i,n+i}, L]$, the route lasts at most $T_k$, and the time windows and capacity bounds hold at every visited node. These are the constraints (2)–(14) of the paper's model.

The arc variables are $x^k_{ij} = 1$ when vehicle $k$ travels from $i$ to $j$, and $x_{ij} = \sum_{k \in K} x^k_{ij}$. For a node set $S$ write $\bar S = N \setminus S$, $x(S) = \sum_{i,j\in S} x_{ij}$, $x(\delta^+(S)) = \sum_{i\in S, j\in \bar S} x_{ij}$, $x(\delta^-(S)) = \sum_{i \in \bar S, j \in S} x_{ij}$, $\pi(S) = \{i \in P \mid n+i \in S\}$ and $\sigma(S) = \{n+i \in D \mid i \in S\}$. An inequality in $x$ is valid for the DARP when the aggregated arc variables of every feasible solution satisfy it.

Formalization targets

Goal: Proposition 5 (p. 578)

Let $i_1, \dots, i_m$ be distinct users and let $H, T_1, \dots, T_m \subseteq P \cup D$ satisfy $\{i_h, n+i_h\} \subseteq T_h$ and $H \cap T_h = \{i_h\}$. Then every feasible solution satisfies

$$x(H) + \sum_{h=1}^m x(T_h) \le |H| + \sum_{h=1}^m |T_h| - 2m. \tag{39}$$

The handle $H$ and the teeth $T_h$ are not required to be disjoint from one another beyond $H \cap T_h = \{i_h\}$, and $m$ is arbitrary.

Milestones (the steps of the proof of Proposition 5)

1. $x(S) \le |S| - 1$ for every nonempty $S \subseteq P \cup D$.
2. If $x(T) = |T| - 1$ for a set $T \ni i, n+i$, then a path of arcs with $x_{ab} = 1$ covers $T$ and does not finish at $i$.
3. With $\alpha$ the number of teeth for which $x(T_h) = |T_h| - 1$: $x(\delta^+(H)) \ge \alpha$.
4. $x(\delta^+(H)) = x(\delta^-(H))$ and $2x(H) + x(\delta^+(H)) + x(\delta^-(H)) = 2|H|$ for $H \subseteq P \cup D$.
5. $x(H) \le |H| - \alpha$.

Companion statements

The mission also states the other propositions of §4: the lifted subtour elimination inequalities (33) and (34) (Propositions 1 and 2), the predecessor inequality (30), the two liftings (36) and (37) of the generalized order constraint (Propositions 3 and 4), the redundancy of the strengthening (40) of (39) under (30) for fractional points (Proposition 6), and the infeasible path inequality (41) under the triangle inequality for travel times (Proposition 7).

Significance

Valid inequalities are what make branch-and-cut work: each family is added to the linear relaxation by a separation heuristic, and the paper's computational section reports how the bound improves as families are added. Validity is the one property the algorithm cannot check at run time, since a cut that removes a feasible route plan silently returns a suboptimal answer. Remark 2 of the paper observes that (39) is stronger than the TSP comb inequality on the same sets, and Proposition 6 shows that its natural strengthening adds nothing once the predecessor inequalities (30) are present, which tells an implementer which families to separate.

All propositions are proved in the paper, partly in an appendix; none is formalized. A machine-checked development would give a precise route-based model of the DARP that later DARP and pick-up and delivery papers can reuse, and certified validity of the cut families that branch-and-cut codes for these problems separate.

Difficulty

The proofs are short on paper but argue about the shape of routes: "there exists a path connecting all nodes in $T_h$", "this path cannot finish at node $i_h$ because of the precedence constraint". Turning a tight subtour count $x(T) = |T| - 1$ into a single covering path requires knowing that the arcs of a feasible solution inside a subset of $P \cup D$ form vertex-disjoint paths, which in turn rests on each node of $P \cup D$ having exactly one predecessor and one successor and on routes containing no cycles. The arithmetic step from $\alpha$ tight teeth to the bound on the handle needs the degree identities for every subset of $P \cup D$, and counting the arcs leaving $H$ needs the distinctness of the users $i_h$. Reasoning directly with the linear constraints (2)–(14) does not suffice: those constraints alone do not exclude cycles of zero duration.

Formalization scope

Nodes are natural numbers, so $n+i$ and $2n+1$ appear literally; $N$, $P$, $D$ and $P \cup D$ are Finset.range (2n+2), Icc 1 n, Icc (n+1) (2n) and Icc 1 (2n). All data and arc variables are real-valued, and every right-hand side is computed in $\mathbb R$. Feasible solutions are route-based: each vehicle has a duplicate-free list of nodes of $P \cup D$, and the constraints of the model are imposed along that list. Read literally, the program (1)–(14) admits closed cycles when $d_i + t_{ij} = 0$ around a cycle, on which every proposition fails, and imposes (11)–(13) also at nodes a vehicle does not visit; the route encoding follows the paper's verbal definition of the DARP and its proofs, which reason about routes. Precedence ($i$ before $n+i$) is a field of the solution, since with zero travel and service times the nonnegativity of ride times does not order the visits. The routing cost plays no role and is omitted. No positivity is assumed for travel or service times.

Added hypotheses, each necessary: sets $S$ in the subtour bound and in (30) are nonempty ($S = \emptyset$ gives $0 \le -1$); the users of Proposition 5 are distinct; the generalized order constraint (Propositions 3 and 4) has $m \ge 2$ (for $m = 1$ it is false); the ordered sets of Propositions 1 and 2 have $h \ge 3$ nodes, the standing assumption of the paragraph that introduces them; Proposition 7 has $p \ge 1$ and a path through distinct nodes. Proposition 6 is the only statement about fractional points: it assumes nonnegativity, no loops, (2), (3) and (30), and drops the remaining constraints of the relaxation, which makes it stronger.

The inequalities are stated for the arc variables of every feasible solution, not for an arbitrary $0$–$1$ vector satisfying a few degree constraints; a statement of the latter kind is a different and false theorem. Useful contributions include the path structure of the arcs of a feasible solution inside a subset of $P \cup D$, the degree identities, and the milestone proofs, which are reusable for the other propositions.

Selected references

• J.-F. Cordeau, A Branch-and-Cut Algorithm for the Dial-a-Ride Problem, Operations Research 54(3):573–586, 2006. https://doi.org/10.1287/opre.1060.0283
• E. Balas, M. Fischetti, W. R. Pulleyblank, The precedence-constrained asymmetric traveling salesman polytope, Mathematical Programming 68:241–265, 1995 (as cited in Cordeau 2006).
• M. Grötschel, M. W. Padberg, Polyhedral theory, in Lawler et al. (eds.), The Traveling Salesman Problem, Wiley, New York, 1985, pp. 251–305 (as cited in Cordeau 2006).
• K. S. Ruland, E. Y. Rodin, The pickup and delivery problem: Faces and branch-and-cut algorithm, Computers & Mathematics with Applications 33:1–13, 1997 (as cited in Cordeau 2006).