Linear Optimization

Motivation

Multistage stochastic integer programs model sequential decisions under uncertainty in which some decisions are discrete: unit commitment in power systems, capacity expansion, production planning with setups. Their linear (continuous) counterparts are routinely solved by nested decomposition methods such as stochastic dual dynamic programming (SDDP; Pereira and Pinto, 1991), which approximate each node's expected cost-to-go function from below by a maximum of linear cuts. With integer variables the cost-to-go functions are no longer convex, and cuts from linear programming duality are in general not exact at the points where they are generated.

Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) restrict the state variables passed between stages to be binary and introduce a local copy $z_n$ of the parent's state at every node. Dualizing only the copy constraint $z_n = x_{a(n)}$ gives a class of cuts, the Lagrangian cuts, which the authors call "one of the major results of the paper" (p. 478). Their Theorem 3 shows that these cuts are valid (they never overestimate the true value function) and tight (they reproduce the current approximate value at the binary state where they are generated). Together with finiteness, these are the sufficient conditions of the paper's Definition 2 under which SND and SDDiP find an optimal solution in finitely many iterations with probability one (Theorem 2 of the paper, the subject of a companion mission).

Setting

Fix a node $n$ of the scenario tree and an iteration $i$ of the algorithm. The node has:

• a nodal constraint set $X_n \subseteq \mathbb R^d \times \mathbb R^d \times \mathbb R^\ell$ of triples $(z_n, x_n, y_n)$, where $x_n$ is the node's state, $y_n$ its local variables and $z_n$ the local copy of the parent's state. By assumption (A1) $X_n$ is nonempty, compact and mixed integer polyhedral: the points of a polyhedron $\{w : Aw \ge b\}$ with some coordinates integer;
• a linear objective $f_n(x_n, y_n) = c^\top x_n + e^\top y_n$;
• children $m \in \mathcal C(n)$ with conditional probabilities $q_{nm} \ge 0$, a lower bound $L_n$, and the children's cut coefficients $(v^\ell_m, \pi^\ell_m)$ for $\ell = 1, \dots, i$.

The approximate expected cost-to-go (3.2) is

$$\psi^{i+1}_n(x) = \min\Big\{\theta : \theta \ge L_n,\ \theta \ge \sum_{m} q_{nm}\big(v^\ell_m + (\pi^\ell_m)^\top x\big),\ \ell = 1,\dots,i\Big\},$$

and the updated forward problem (3.1) at a parent state $\hat x$ has value

$$\underline Q^i_n(\hat x, \psi^{i+1}_n) = \min\{ f_n(x,y) + \psi^{i+1}_n(x) : (z,x,y) \in X_n,\ z = \hat x,\ x \in \{0,1\}^d\}.$$

Let $X'_n = \{(z,x,y) \in X_n : x \in \{0,1\}^d,\ z \in [0,1]^d\}$ and let $X''_n$ add a variable $\theta \ge L_n$ that dominates every aggregated cut. The Lagrangian function and Lagrangian dual (4.3)–(4.4) are

$$\mathcal L^i_n(\pi) = \min_{(z,x,y,\theta)\in X''_n} f_n(x,y) + \theta - \pi^\top z, \qquad (R^i_n):\ \max_{\pi\in\mathbb R^d}\ \mathcal L^i_n(\pi) + \pi^\top \hat x .$$

An optimal $\hat\pi$ and $\hat v = \mathcal L^i_n(\hat\pi)$ define the Lagrangian cut $\theta \ge \hat v + \hat\pi^\top x_{a(n)}$. Given true value functions $Q_m$ of the children and $\mathcal Q_n = \sum_m q_{nm} Q_m$, the true nodal value (2.3) is $Q_n(x_a) = \min\{f_n(x,y) + \mathcal Q_n(x) : (z,x,y) \in X_n,\ z = x_a,\ x \in \{0,1\}^d\}$.

Formalization targets

Goal: Theorem 3 at one node

For binary $\hat x \in \{0,1\}^d$ and $\hat\pi$ optimal for $(R^i_n)$:

$$\hat v + \hat\pi^\top \hat x = \underline Q^i_n(\hat x, \psi^{i+1}_n) \qquad \text{(tightness, (3.5))},$$

and, if the children's cuts are valid for $Q_m$ on $\{0,1\}^d$ and $\mathcal Q_n \ge L_n$ there,

$$Q_n(x_a) \ge \hat v + \hat\pi^\top x_a \quad \text{for all } x_a \in \{0,1\}^d \qquad \text{(validity, (3.4))}.$$

The paper's statement for the whole collection of cuts of an iteration follows by applying this at every sampled node from the last stage backwards, exactly as its proof does by induction.

Milestones

1. (4.5): $\hat v + \hat\pi^\top\hat x = \min\{f_n + \theta : (z,x,y,\theta) \in \mathrm{conv}(X''_n),\ z = \hat x\}$, for any parent state at which $(R^i_n)$ has an optimal solution.
2. Binary face: for binary $\hat x$, $\mathrm{conv}(X''_n) \cap \{z = \hat x\} = \mathrm{conv}(X''_n \cap \{z = \hat x\})$.
3. Tightness (display after (4.5)).
4. Validity, base case: at a last-stage node, $Q_n(x_a) \ge \mathcal L^i_n(\pi) + \pi^\top x_a$.
5. Validity, induction step ((4.6) and the display after it).

Significance

Tightness at binary states is what separates Lagrangian cuts from the cuts of continuous relaxations or of a direct Lagrangian relaxation of the constraints coupling stages: the paper's Example 2 shows a direct relaxation whose cut is not tight even at a binary state, and Example 1 shows that with a non-binary state the duality gap is positive. With valid, tight and finite cuts, SND and SDDiP become exact algorithms for multistage stochastic integer programs with binary states, and through binarization they approximate problems with general mixed-integer states.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires a Lean statement of Geoffrion's theorem for this nodal problem (Lagrangian duality equals optimization over the convex hull of a mixed integer set), which is of independent use for integer programming, and the binary-face fact for sets inside the unit cube.

Difficulty

The validity half is weak duality and is short. The difficulty is in tightness. Step (4.5) is a strong duality statement for a nonconvex set: it needs that the convex hull of $X''_n$ is a polyhedron, which follows only because $X_n$ is compact and mixed integer polyhedral (so $X'_n$ is a finite union of polytopes), and then linear programming duality with attainment over that polyhedron. Neither the polyhedrality of convex hulls of finite unions of polytopes with a common recession direction nor finite-dimensional LP strong duality in the needed form is readily available in Mathlib. A tempting shortcut, Lagrangian duality from convex analysis with a Slater point, does not apply: a binary $\hat x$ lies on the boundary of the projection of $\mathrm{conv}(X''_n)$ onto $z$, so the constraint qualification fails and polyhedrality is genuinely needed.

Formalization scope

States, copies and multipliers are vectors in $\mathbb R^d$ (Fin d → ℝ); a state is binary when each coordinate is $0$ or $1$. Points of $X''_n$ are tuples (z, x, y, θ). Assumption (A1) is three fields of the node structure (nonempty, compact, mixed integer polyhedral after concatenating coordinates). Cuts are indexed by Fin i and children by Fin nC; probabilities are only required to be nonnegative. A last-stage node is nC = 0 with L = 0. The constraint $z \in [0,1]^d$ (2.1c) is kept in $X'_n$ and folded into $X_n$ in (2.3) and (3.1), as in the paper.

Readings of informal words:

• "min" in $\psi^{i+1}_n$, $\mathcal L^i_n$, $\underline Q^i_n$, $Q_n$: the definitions use sInf of the set of objective values, and every theorem states the minimum as an attained least element (IsLeast) or as a lower bound over all feasible points, so no junk value of sInf on an empty or unbounded set is used. The hypothesis $X''_n \ne \emptyset$ makes $\mathcal L^i_n$ a genuine minimum.
• "$\hat\pi$ optimal for (4.3)": maximizes $\pi \mapsto \mathcal L^i_n(\pi) + \pi^\top\hat x$ over all of $\mathbb R^d$.
• "the cuts are valid": $Q_n(x_a) \ge \hat v + \hat\pi^\top x_a$ is stated as a lower bound over every feasible point of (2.3), which is the paper's convention $Q_n = +\infty$ on infeasible states.
• The induction hypothesis of the validity proof is made explicit: all children's cuts $\ell = 1,\dots,i$ are valid, and $\mathcal Q_n \ge L_n$ on binary states.
• Tightness is stated with $\psi^{i+1}_n$; the proof's last line writes $\psi^i_n$, a misprint.

A trivializing formalization is ruled out: $\underline Q^i_n$ is the primal value of the forward problem (3.1) with $\psi^{i+1}_n$ from (3.2) and is never defined through the dual, and validity is required at every binary $x_a$, not only at $\hat x$.

A complete development needs: polyhedrality of convex hulls of bounded mixed integer sets, LP strong duality with attainment (or Geoffrion's theorem directly), Carathéodory-type reasoning in product spaces, and the fact that a binary point which is a positive convex combination of points of $[0,1]^d$ equals each of them. The first two are reusable well beyond this mission. Proofs of individual milestones are welcome independently; the validity milestones are accessible first.

Selected references

• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Math. Program. 175 (2019) 461–502. https://doi.org/10.1007/s10107-018-1249-5
• A. M. Geoffrion, Lagrangean relaxation for integer programming, Math. Program. Study 2 (1974) 82–114. https://doi.org/10.1007/BFb0120690
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895

Motivation

Multistage stochastic linear programs model decisions taken over time under uncertainty: reservoir releases in hydro-thermal scheduling, production and inventory plans, capacity expansion. Their standard solution method, stochastic dual dynamic programming (SDDP, Pereira and Pinto 1991), approximates each stage's cost-to-go function from below by cutting planes. This gives a lower bound on the optimal value and a candidate policy, but no guaranteed upper bound: in the risk-neutral case the policy's expected cost is estimated by Monte Carlo simulation.

Planners who are averse to risk replace the expectation in each stage by a coherent risk measure (Artzner, Delbaen, Eber and Heath 1999), nested stage by stage so that the resulting dynamic risk measure is time consistent (Ruszczyński and Shapiro 2006). Under such a nested objective, simulation no longer estimates the cost of a policy: the nested risk of a policy is not an average over sampled scenarios. Philpott, de Matos and Finardi (2013) address this by an inner approximation of the cost-to-go functions from above, built from convex combinations of finitely many points with known upper bounds. Their Proposition 5 shows that the optimal value $y$ of the resulting first-stage problem bounds the nested risk-adjusted cost of the policy defined by the inner approximation. This gives a deterministic upper bound that complements the SDDP lower bound, and they apply it to the Brazilian hydro-thermal system.

Setting

There are $T\ge2$ stages. The decision at stage $t$ is $x_t\in\mathbb R^n$; $A_t,E_t$ are $m\times n$ matrices and $c_t\in\mathbb R^n$. Stage 1 is deterministic: $A_1x_1=b_1$. For $t\ge2$ a random outcome $\omega_t$ ranges over a finite set $\Omega_t$, independently of earlier stages, and enters through the right-hand side $b_t(\omega_t)$. The feasible set of stage $t$ given the previous decision $x_{t-1}$ is

$$\mathcal X_t(\omega_t)=\{x_t\ge0:\ A_tx_t=b_t(\omega_t)-E_tx_{t-1}\}.$$

A coherent risk measure $\rho$ maps random costs $Z:\Omega\to\mathbb R$ to $\mathbb R$ and is subadditive, monotone ($Z_1\le Z_2\Rightarrow\rho(Z_1)\le\rho(Z_2)$), positively homogeneous and translation equivariant ($\rho(\lambda+Z)=\lambda+\rho(Z)$). Larger is worse: these are costs. Each stage $t\ge2$ carries a one-step coherent risk measure $\rho_t$ on random costs over $\Omega_t$. It is extended to costs in $\mathbb R\cup\{+\infty\}$ by $\bar\rho_t(Z)=+\infty$ whenever some outcome has infinite cost.

For $s=2,\dots,T$ fix points $x^1_{s-1},\dots,x^{J_{s-1}}_{s-1}$ and numbers $q^1_s,\dots,q^{J_{s-1}}_s$. The inner approximation is the lower boundary of the convex hull of the pairs $(x^j_{s-1},q^j_s)$:

$$\hat{\mathcal Q}_s(x)=\min\Big\{\sum_j\lambda^jq^j_s:\ \sum_j\lambda^jx^j_{s-1}=x,\ \lambda\ge0,\ \sum_j\lambda^j=1\Big\},$$

which is $+\infty$ off the convex hull of the points, with $\hat{\mathcal Q}_{T+1}\equiv0$. The policy's stage problem (13) and the first-stage problem (8) are

$$q_t(x_{t-1},\omega_t)=\min_{x_t\in\mathcal X_t(\omega_t)}c_t^\top x_t+\hat{\mathcal Q}_{t+1}(x_t),\qquad y=\min_{A_1x_1=b_1}c_1^\top x_1+\hat{\mathcal Q}_2(x_1).$$

The numbers $q^j_s$ are upper bounds when $q^j_s\ge\bar\rho_s\big(q_s(x^j_{s-1},\omega_s)\big)$ for all $s$ and $j$. A policy defined by the inner approximation, $\hat\pi$, takes at each state $x_{t-1}$ and outcome $\omega_t$ an action $\hat x_t(x_{t-1},\omega_t)$ solving (13), and a first-stage action $\hat x_1$ solving (8). The actual risk-adjusted cost of $\hat\pi$ over stages $t,\dots,T$ is

$$\hat v_t(x_{t-1},\omega_t)=c_t^\top\hat x_t+\bar\rho_{t+1}\big(\hat v_{t+1}(\hat x_t,\omega_{t+1})\big),$$

with no future term at $t=T$. The nested risk-adjusted cost of the policy is $v(\hat\pi)=c_1^\top\hat x_1+\bar\rho_2(\hat v_2(\hat x_1,\omega_2))$.

Formalization targets

Goal: Proposition 5

$$v(\hat\pi)\ \le\ y.$$

The bound holds for every $T\ge2$, every family of coherent $\rho_t$, every choice of points satisfying the upper-bound property, and every minimizing selection $\hat\pi$.

Milestones

1. The convexity display of §2: subadditivity and positive homogeneity imply $\rho(\alpha Z_1+(1-\alpha)Z_2)\le\alpha\rho(Z_1)+(1-\alpha)\rho(Z_2)$.
2. $\hat{\mathcal Q}_s$ is the lower boundary of the convex hull $\mathcal H$ of the pairs $(x^j_{s-1},q^j_s)$ (its epigraph is $\mathcal H$ plus the vertical half-line), hence convex with $\hat{\mathcal Q}_s(x^j_{s-1})\le q^j_s$, and every convex function bounded by the $q^j_s$ at the points lies below $\hat{\mathcal Q}_s$.
3. $q_t(\cdot,\omega_t)$ is convex in $x_{t-1}$.
4. The interpolation bound $\bar\rho_t\big(q_t(x_{t-1},\omega_t)\big)\le\hat{\mathcal Q}_t(x_{t-1})$.
5. The induction claim $\bar\rho_t\big(\hat v_t(x_{t-1},\omega_t)\big)\le\hat{\mathcal Q}_t(x_{t-1})$ for $t=2,\dots,T$ and every $x_{t-1}$.

Companions

Proposition 3, the risk-neutral case $\rho_t=\mathbb E$. Proposition 4, the subgradient rule $\sum_mp_m\tilde\zeta_mg(\tilde x,\omega_m)\in\partial_x\rho(Z(x,\omega))$ for $\rho$ given by its dual representation. The existence of a policy $\hat\pi$, which shows that the hypotheses of the goal can be met.

Significance

Proposition 5 makes the inner approximation a certificate. Any policy computed by minimizing against $\hat{\mathcal Q}_{t+1}$ has nested risk-adjusted cost at most $y$, a number obtained by solving one linear program. Together with the lower bound $z$ from outer approximation it brackets the risk-adjusted optimal value. The gap $y-z$ then measures the quality of a risk-averse SDDP policy without simulation, which the nested objective does not allow. The bound covers every coherent nesting used in practice, such as mixtures of expectation and CVaR.

The results are proved in the paper. None of them is machine-checked. A formalization adds a precise account of the infinite values the paper does not discuss: infeasible stages, points outside the convex hull, and the extension of $\rho_t$ to $+\infty$. It also pins down the exact form of the upper-bound hypothesis the induction needs.

Difficulty

The obvious reading of the hypothesis on p. 16, "$q^j_{t+1}$ is an upper bound on $\rho_{t+1}(Q_{t+1}(x^j_t,\omega_{t+1}))$" with the true value function $Q_{t+1}$, does not support the induction. The policy $\hat\pi$ does not act optimally, so its cost can exceed the true value, and the inductive step compares $\hat v_t$ with the policy's own stage value $q_t$, not with $Q_t$. The hypothesis that works bounds the risk-adjusted optimal value of the policy's stage problem (13) at the points, which is what the paper's Upper Bound Computation actually computes.

The second difficulty is infinite values, which the paper never discusses. A risk measure is defined on real random costs, yet stage problems can be infeasible, $\hat{\mathcal Q}_s$ is $+\infty$ off a convex hull, and a convex combination may put zero weight on a point whose bound is $+\infty$. Every inequality of the paper has to be re-read in $\mathbb R\cup\{+\infty\}$, and the extended-real arithmetic must not silently produce a value the paper does not intend.

Formalization scope

Vectors are Fin n → ℝ, all stages share $n$ and $m$, and costs that may be infinite are EReal. Minima are EReal infima, $+\infty$ on an empty set. Attainment of a minimum is never built into a definition: the policy is a selection with a minimizing property, required at every state where the stage problem is feasible. Stages are natural numbers. Points and bounds are indexed by the stage $s$ of the function $\hat{\mathcal Q}_s$ they define, so pts s j is $x^j_{s-1}$ and qv s j is $q^j_s$. Stagewise independence is built in: $\omega_t$ ranges over $\Omega_t$ whatever happened before.

Standing assumptions made explicit in the statements:

• $T\ge2$;
• $\rho_t$ coherent for $t=2,\dots,T$ (all four axioms, though the proof uses only monotonicity and convexity);
• the terminal convention $\rho_{T+1}(Q_{T+1})=0$, so $\hat{\mathcal Q}_{T+1}\equiv0$;
• (8) without the constraint $x_1\ge0$, as printed;
• the upper-bound hypothesis in the form above.

The risk measures $\rho_t$ act on real random costs and are extended by $\bar\rho_t(Z)=+\infty$ when some outcome has infinite cost. In Proposition 4, $\rho$ is given by its dual representation (10); the representation theorem itself is not part of the mission. The existence statement adds solvability of $A_1x_1=b_1$ and boundedness below of the last-stage program, without which (8) or the last stage has no solution.

The goal is not to be trivialized. Its hypotheses mention neither $\hat v_t$ nor the induction claim; the policy must minimize at every feasible state, not only along visited states; and the statement is for general $T$ and general coherent $\rho_t$, not the expectation. The bound is trivially true when $y=+\infty$ and is informative when $\hat x_1$ lies in the convex hull of the stage-1 points.

A complete development needs:

• convexity of extended-real linear-programming value functions in their right-hand side;
• convexity of the convex-hull function $\hat{\mathcal Q}$;
• finite Jensen-type inequalities for monotone convex risk measures;
• linear-programming attainment, for the existence companion.

The first two are reusable for any SDDP-type development. Proofs of the milestones in any order are welcome.

Selected references

• A. B. Philpott, V. L. de Matos, E. Finardi, On Solving Multistage Stochastic Programs with Coherent Risk Measures, Operations Research 61(4), 2013. https://doi.org/10.1287/opre.2013.1175
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent Measures of Risk, Mathematical Finance 9(3), 1999. https://doi.org/10.1111/1467-9965.00068
• A. Ruszczyński, A. Shapiro, Conditional Risk Mappings, Mathematics of Operations Research 31(3), 2006. https://doi.org/10.1287/moor.1060.0204
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52, 1991. https://doi.org/10.1007/BF01582895
• A. Shapiro, Analysis of stochastic dual dynamic programming method, European Journal of Operational Research 209(1), 2011. https://doi.org/10.1016/j.ejor.2010.08.007

Motivation

Strategic open pit mine planning decides which parts of an ore body are excavated, when, and where each block of material is sent. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) model the problem as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), generalising the formulation of Bienstock and Zuckerberg (2010). Its integer versions have large integrality gaps on production scheduling instances, so the authors derive several families of cutting planes. This mission concerns the first family, the extraction cuts of §5.1: early start cuts, diamond cuts, and clique and lifted clique cuts. They exploit only the mining capacity of each period and the precedence structure, and they are valid both under full integrality and under the partial integrality used in commercial mine planning software.

Clique inequalities for precedence-constrained knapsack problems go back to Boyd (1993); early start cuts to Gaupp (2008, doctoral dissertation, Colorado School of Mines); the diamond cuts resemble cuts of Zhu, Bard and Yu (2006) for multimode project scheduling. The paper's contribution is their extension to the multi-period clustered model and to partial integrality.

All page references are journal pages of the published Operations Research article.

Setting

An instance has finite sets $\mathcal B$ of blocks, $\mathcal D$ of destinations and $\mathcal C$ of clusters, the latter a partition of $\mathcal B$, and periods $\mathcal T=\{1,\dots,T\}$. Block $b$ lies in cluster $c(b)$ and has weight $q_b\ge 0$. A precedence relation $b_1\prec b_2$ on blocks induces one on clusters ($c_1\prec c_2$ if some block of $c_1$ precedes some block of $c_2$), assumed to be a strict partial order. The arc set $\mathcal A$ is its transitive reduction: $(c,c')\in\mathcal A$ when $c'$ is an immediate predecessor of $c$. The closure is $cl(c)=\{c\}\cup\{c':c'\prec c\}$, the reverse closure $rcl(c)=\{c\}\cup\{c':c\prec c'\}$, and for a set $S$ of clusters $q(S)=\sum_{c\in S}\sum_{b\in c}q_b$, with $q_c=q(\{c\})$.

Variables $x_{c,t}$ give the fraction of cluster $c$ extracted in period $t$ and $y_{b,d,t}$ the fraction of block $b$ sent to destination $d$ in period $t$. The constraints (2)–(7) of p. 1427 are

$$x_{c(b),t}=\sum_{d}y_{b,d,t},\qquad \sum_{t}x_{c,t}\le 1,\qquad \sum_{t'\le t}x_{c,t'}\le\sum_{t'\le t}x_{c',t'}\ \ ((c,c')\in\mathcal A),\qquad Gy\le g,\qquad y\ge 0,$$

together with an integrality condition: full integrality (10) $x_{c,t}\in\{0,1\}$ defines the PCPSP-F, and partial integrality (11), "$\sum_{t'\le t}x_{c,t'}>0$ implies $\sum_{t'\le t}x_{c',t'}=1$ for $(c,c')\in\mathcal A$", defines the PCPSP-P. The general rows $Gy\le g$ include the mining capacity rows (8), $\sum_b\sum_d q_b\,y_{b,d,t}\le U_t$.

The cuts are written in the cumulative variables $w_{c,t}=\sum_{t'=1}^{t}x_{c,t'}$ (17), and with $Q_t=\sum_{t'=1}^{t}U_{t'}$. Two clusters $c_1,c_2$, neither preceding the other, are f-incompatible in time $t$ if $q(cl(\{c_1,c_2\}))>Q_t$, and p-incompatible if $q(cl(\{c_1,c_2\})\setminus\{c_1,c_2\})>Q_t$.

Formalization targets

Goal: Theorem 4 (clique and lifted clique cuts), p. 1433

For a set $\{c_1,\dots,c_k\}$ of clusters and $t\in\mathcal T$, the clique inequality

$$\sum_{i=1}^{k}w_{c_i,t}\le 1\tag{23}$$

is valid for the PCPSP-F if the $c_i$ are pairwise f-incompatible, and for the PCPSP-P if they are pairwise p-incompatible. If moreover $c\prec c_i$ for every $i$, the lifted inequality $\sum_{i=1}^{k}w_{c_i,t}\le w_{c,t}$ is valid under the same conditions. The goal is the conjunction of these four validity claims.

Milestones

• (18)–(20), p. 1432: $w_{c,t}\le w_{c,t+1}$, $w_{c,t}\le w_{c',t}$ for $(c,c')\in\mathcal A$, and $\sum_c q_c\,w_{c,t}\le Q_t$ at every feasible point satisfying (8).
• (21), p. 1432: under full integrality, $w_{c,t}\in\{0,1\}$. Its partial counterpart (22), "$w_{c,t}>0$ implies $w_{c',t}=1$ for $(c,c')\in\mathcal A$", is condition (11) verbatim in this formalization, which writes (11) in cumulative form, so it has no item of its own.
• Theorem 2 (early start cuts), p. 1432: if $q(cl(c))>Q_t$, then $w_{c,t}=0$ is valid for the PCPSP-F, and if $q_c>0$, $w_{c,t}\le (Q_t-q(cl(c)\setminus\{c\}))^+/q_c$ is valid for the PCPSP-P.
• Theorem 3 (diamond cuts), p. 1433: for $t_1\le t_2$ and $c_1\prec c_2$, $w_{c_2,t_2}\le w_{c_1,t_1}$ is valid for the PCPSP-F if $q(cl(c_2)\cap rcl(c_1))>Q_{t_1,t_2}=\sum_{t'=t_1}^{t_2}U_{t'}$, and for the PCPSP-P if $q((cl(c_2)\cap rcl(c_1))\setminus\{c_1,c_2\})>Q_{t_1,t_2}$.

Significance

Each of these inequalities cuts off fractional points of the linear relaxation while keeping every integer (or partially integer) schedule, and early start cuts can fix variables to zero before the solve. The paper motivates them by the large integrality gaps it observes on production scheduling instances (§5, p. 1432) and evaluates them, with its production cuts, in the computational study of §8. Because they use only the precedence order and the mining capacity, the extraction cuts apply to any multi-period precedence-constrained knapsack structure, beyond mining.

The results are proved in the paper, by short contradiction arguments. None of them has a machine-checked proof. Formalizing them yields a reusable model of the PCPSP-C with its two integrality regimes, and a checked account of exactly which rows of the formulation each cut relies on: in particular that validity needs the capacity rows (8) and the integrality condition, and fails for the LP relaxation.

Difficulty

The arguments rely on facts the paper uses in one line. Under partial integrality, $w_{c,t}>0$ forces $w_{c',t}=1$ for every predecessor $c'$ of $c$, not only for the immediate ones of $\mathcal A$; this requires chaining condition (11) along covering arcs of a finite strict order, and showing that every precedence is a chain of immediate ones. The counting step needs $x\ge 0$, which is not a constraint of the formulation but follows from $x_{c(b),t}=\sum_d y_{b,d,t}$, $y\ge 0$ and the nonemptiness of clusters. The diamond cut further splits the capacity $Q_{t_1,t_2}$ between periods and uses monotonicity of $w$ in time. A natural first attempt, arguing directly from the closure of $\prec$, does not apply: the formulation constrains only the arcs of $\mathcal A$.

Formalization scope

Blocks, destinations and clusters are finite types; periods are Fin T, index $t$ standing for period $t+1$. An instance carries the block-to-cluster map, the block precedence, values, discount rate, weights, capacities and $m$ side rows $Gy\le g$. Cluster precedence is derived from block precedence; $\mathcal A$ is its covering relation, and constraints (4) and (11) range over $\mathcal A$ only. The closure of a pair, which the page does not define, is $cl(c_1)\cup cl(c_2)$. Incompatibility includes incomparability of the two clusters, as on the page; "pairwise" ranges over distinct members of a finite set, which may be empty or a singleton.

The standing assumptions of §2.1 are hypotheses of every statement: clusters cover $\mathcal B$ (so each is nonempty), $\prec$ is a strict partial order on clusters, $r>0$, and $q_b\ge 0$. A cut "valid for the PCPSP-F (PCPSP-P)" is stated as: at every point feasible for the formulation with full (partial) integrality whose mining capacity rows (8) hold, the inequality holds. The capacity rows enter as an explicit hypothesis because the paper assumes they are among the rows of $Gy\le g$; without them every cut is false. Validity is never asserted for the LP relaxation, where the cuts do not hold, so the integrality condition cannot be dropped. In Theorem 2 the division by $q_c$ is guarded by $q_c>0$, as on the page.

The development needs only finite sums, finite sets and orders from Mathlib. Contributions are welcome on the chaining lemma for covering relations of finite strict orders and on the nonnegativity and monotonicity of $w$, which every milestone shares.

Selected references

• O. Rivera Letelier, D. Espinoza, M. Goycoolea, E. Moreno, G. Muñoz, Production Scheduling for Strategic Open Pit Mine Planning: A Mixed-Integer Programming Approach, Operations Research 68(5):1425–1444, 2020. https://doi.org/10.1287/opre.2019.1965
• D. Bienstock, M. Zuckerberg, Solving LP Relaxations of Large-Scale Precedence Constrained Problems, Proc. 14th Conf. Integer Programming and Combinatorial Optimization (IPCO), 2010, pp. 1–14.
• E. A. Boyd, Polyhedral results for the precedence-constrained knapsack problem, Discrete Applied Mathematics 41(3):185–201, 1993.
• G. Zhu, J. F. Bard, G. Yu, A Branch-and-Cut Procedure for the Multimode Resource-Constrained Project-Scheduling Problem, INFORMS Journal on Computing 18(3):377–390, 2006.

Motivation

Strategic open pit mine planning decides which parts of an ore body are excavated, in which period, and where each block of material is sent: to a processing plant, a stockpile or a waste dump. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) state the problem as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), which extends the formulation of Bienstock and Zuckerberg (IPCO 2010) to clusters of blocks that are extracted together. The integer versions of this program have large integrality gaps on production scheduling instances (§5, p. 1432), so the authors derive problem-specific cutting planes. This mission concerns the variable-right-hand-side (VRHS) production cuts of §5.2. They combine the precedence order of the clusters with the capacity of a single destination: if a solution sends many blocks to a capacitated destination, the predecessors of those blocks must be fully extracted.

The VRHS cuts are introduced first on a one-period, two-destination set, the mode-knapsack set MK (§5.2.1), and then generalised to the full multi-period clustered model (§5.2.2). Disaggregated formulations with destination choices go back to Boland et al. (Comput. Oper. Res. 2009); cutting planes for the precedence-constrained knapsack structure of open pit scheduling were studied by Bley et al. (Comput. Oper. Res. 2010).

All page references are journal pages of the published Operations Research article.

Setting

An instance has finite sets $\mathcal B$ of blocks, $\mathcal D$ of destinations and $\mathcal C$ of clusters, the latter a partition of $\mathcal B$, and periods $\mathcal T=\{1,\dots,T\}$. Block $b$ lies in cluster $c(b)$ and has weight $q_b\ge 0$. A precedence relation $b_1\prec b_2$ on blocks induces one on clusters ($c_1\prec c_2$ if some block of $c_1$ precedes some block of $c_2$), assumed to be a strict partial order. The arc set $\mathcal A$ is its transitive reduction: $(c,c')\in\mathcal A$ when $c'$ is an immediate predecessor of $c$. The reverse closure of a cluster is $rcl(c)=\{c\}\cup\{c':c\prec c'\}$, the cluster and everything that requires it; for a set $S$ of clusters, $q(S)=\sum_{c\in S}\sum_{b\in c}q_b$.

Variables $x_{c,t}$ give the fraction of cluster $c$ extracted in period $t$, and $y_{b,d,t}$ the fraction of block $b$ sent to destination $d$ in period $t$. The constraints (2)–(7) of p. 1427 are

$$x_{c(b),t}=\sum_{d}y_{b,d,t},\qquad \sum_{t}x_{c,t}\le 1,\qquad \sum_{t'\le t}x_{c,t'}\le\sum_{t'\le t}x_{c',t'}\ \ ((c,c')\in\mathcal A),\qquad Gy\le g,\qquad y\ge 0,$$

together with an integrality condition: full integrality (10), $x_{c,t}\in\{0,1\}$, defines the PCPSP-F, and partial integrality (11), "$\sum_{t'\le t}x_{c,t'}>0$ implies $\sum_{t'\le t}x_{c',t'}=1$ for $(c,c')\in\mathcal A$", defines the PCPSP-P. The general rows $Gy\le g$ include the destination capacity rows (9), $\sum_b q_b\,y_{b,d,t}\le U^d_t$. The cuts use the cumulative variables $w_{c,t}=\sum_{t'=1}^{t}x_{c,t'}$ (17).

The mode-knapsack set MK (p. 1433) fixes a DAG $G=(\mathcal B,\mathcal A)$, weights $q_b>0$ and a capacity $U>0$, and consists of the vectors $(x,y^P,y^W)$ with

$$\sum_b q_b y^P_b\le U,\qquad y^P_b+y^W_b=x_b,\qquad x_b\le 1,\qquad x_b>0\Rightarrow x_{b'}=1\ ((b,b')\in\mathcal A),\qquad y^P,y^W\ge 0.$$

Formalization targets

Goal: Theorem 7 (VRHS cuts), p. 1434

Fix $d\in\mathcal D$, $t\in\mathcal T$ and clusters $c_1\prec c_2\prec\dots\prec c_n$ with $q(rcl(c_1)\setminus rcl(c_n))<U^d_t<q(rcl(c_1))$. Let $\Delta_k=rcl(c_k)\setminus rcl(c_{k+1})$, $\delta_k=q(\Delta_k)$ for $k<n$, and $\Delta_n=rcl(c_n)$, $\delta_n=U^d_t-q(rcl(c_1)\setminus rcl(c_n))$. For constants $0\le\alpha_b\le 1$ ($b\in c_n$), the inequality

$$\sum_{k=1}^{n-1}\sum_{c\in\Delta_k}\sum_{b\in c}q_b y_{b,d,t}+\sum_{b\in c_n}\alpha_b q_b y_{b,d,t}+\sum_{c\in rcl(c_n)\setminus\{c_n\}}\sum_{b\in c}q_b y_{b,d,t}\le\sum_{k=1}^{n}\delta_k w_{c_k,t}\tag{32}$$

is valid for the PCPSP-F, and, when $\sum_{b\in c_n}\alpha_b q_b\le U^d_t-q(rcl(c_1)\setminus rcl(c_n))$ (33), for the PCPSP-P. The goal is the conjunction of the two validity claims.

Milestones

• (29)–(30), p. 1434: under either integrality condition, $w_{c,t}<1$ implies $y_{b,d,t}=0$ for every block of a cluster in $rcl(c)\setminus\{c\}$, and $y_{b,d,t}\le w_{c(b),t}$. The third condition (31) of the page is the capacity row (9) itself.
• (35), p. 1435: $\sum_{c\in\Delta_k}\sum_{b\in c}q_b y_{b,d,t}\le\delta_k w_{c_k,t}$ for $k=1,\dots,n-1$.
• (36), p. 1435: under (33), $\sum_{b\in c_n}\alpha_b q_b y_{b,d,t}\le\delta_n w_{c_n,t}$.
• Theorem 5, p. 1434: in MK, every block $b$ with $q_b\le U$ gives the valid inequality $\sum_{b'\in rcl(b)}q_{b'}y^P_{b'}\le U x_b$.

Significance

A valid inequality removes fractional points of the linear relaxation while keeping every feasible schedule. The VRHS cuts are among the production cuts that the paper evaluates in its computational study (§8), alongside the extraction cuts and the hourglass cuts. Their right-hand side is not a constant but a combination of extraction variables along a chain, which is what lets them couple the destination capacity with the precedence order; the paper's Theorem 5 shows the mechanism on MK, Theorem 7 in the full model. The partial integrality regime, under which the second half of Theorem 7 holds, is the one used by commercial mine planning software (p. 1427).

The results are proved in the paper by case analysis on the first index $k$ with $w_{c_k,t}<1$. None of them has a machine-checked proof. Formalizing them makes explicit which rows of the formulation each cut uses (the destination capacity (9) and the integrality condition), and what role the coefficient condition (33) plays in the partially integral case.

Difficulty

The proof uses that $\Delta_1,\dots,\Delta_{n-1}$ partition $rcl(c_1)\setminus rcl(c_n)$ and are disjoint from $rcl(c_n)$, which requires $rcl(c_{k+1})\subseteq rcl(c_k)$ along the chain. It uses that $w_{c,t}\le w_{c_k,t}$ for every $c\in rcl(c_k)$, and that $w_{c,t}<1$ forces all strict successors of $c$ to be unextracted; both chain the constraints (4) and (11) along covering arcs of a finite strict order, since the formulation constrains only the arcs of $\mathcal A$, not all of $\prec$. A natural first attempt, arguing directly from $\prec$, therefore does not apply. The counting step needs $x\ge 0$, which is not a constraint of the formulation but follows from $x_{c(b),t}=\sum_d y_{b,d,t}$, $y\ge 0$ and the nonemptiness of clusters. In the partial integrality case a fractional $w_{c_n,t}$ is possible, and the bound on the $c_n$ term must come from (33) rather than from integrality.

Formalization scope

Blocks, destinations and clusters are finite types; periods are Fin T, index $t$ standing for period $t+1$. An instance carries the block-to-cluster map, the block precedence, values, discount rate, weights, capacities and $m$ side rows $Gy\le g$. Cluster precedence is derived from block precedence; $\mathcal A$ is its covering relation, and constraints (4) and (11) range over $\mathcal A$ only. The chain $c_1,\dots,c_n$ is a function on $\mathbb N$ read at $1,\dots,n$ with $n\ge 1$, and condition 1 of Theorem 7 is stated for consecutive pairs. In (32), $y$ is taken at the single period $t$ and $w$ is cumulative.

The standing assumptions of §2.1 are hypotheses of every PCPSP-C statement: clusters cover $\mathcal B$ (so each is nonempty), $\prec$ is a strict partial order on clusters, $r>0$, and $q_b\ge 0$. A cut "valid for the PCPSP-F (PCPSP-P)" is stated as: at every point feasible for the formulation with full (partial) integrality whose destination capacity rows (9) hold, the inequality holds. The capacity rows enter as an explicit hypothesis because the paper assumes they are among the rows of $Gy\le g$; without them the cut is false. Validity is never asserted for the LP relaxation, where (29) and (32) fail, so the integrality condition cannot be dropped. Conditions 2 and 3 of Theorem 7 are kept as on the page, although the proof does not use condition 3. In MK, the DAG property, $q>0$ and $U>0$ are hypotheses; an arc $(b,b')$ means that extracting $b$ forces $b'$, and $rcl(b)$ collects $b$ and the blocks from which $b$ is reachable.

The development needs only finite sums, finite sets and orders from Mathlib. Contributions are welcome on the chaining lemma for covering relations of finite strict orders, on the nonnegativity and monotonicity of $w$, and on the partition $\{\Delta_k\}$ of $rcl(c_1)\setminus rcl(c_n)$, which the goal and the milestones share.

Selected references

• O. Rivera Letelier, D. Espinoza, M. Goycoolea, E. Moreno, G. Muñoz, Production Scheduling for Strategic Open Pit Mine Planning: A Mixed-Integer Programming Approach, Operations Research 68(5):1425–1444, 2020. https://doi.org/10.1287/opre.2019.1965
• D. Bienstock, M. Zuckerberg, Solving LP Relaxations of Large-Scale Precedence Constrained Problems, Proc. 14th IPCO, LNCS 6080, 1–14, 2010. https://doi.org/10.1007/978-3-642-13036-6_1
• N. Boland, I. Dumitrescu, G. Froyland, A. M. Gleixner, LP-based disaggregation approaches to solving the open pit mining production scheduling problem with block processing selectivity, Computers & Operations Research 36(4):1064–1089, 2009. https://doi.org/10.1016/j.cor.2007.12.006
• A. Bley, N. Boland, C. Fricke, G. Froyland, A strengthened formulation and cutting planes for the open pit mine production scheduling problem, Computers & Operations Research 37(9):1641–1647, 2010. https://doi.org/10.1016/j.cor.2009.12.008

Motivation

In many planning problems the decision changes the uncertainty it faces. Opening a facility raises the demand observed near it; a maintenance decision changes the failure distribution of a component; a price shifts the demand law. Decision-dependent uncertainty of this kind breaks the standard assumption of stochastic programming that the probability distribution is fixed in advance. When the distribution is in addition only partly known, the natural model is distributionally robust: the decision maker optimizes against the worst distribution in an ambiguity set whose shape itself depends on the decision.

X. Yu and S. Shen (arXiv:2002.12518v3, 2020; published in Mathematical Programming) study the multistage version of this model with binary state variables, and show that under three families of moment-based ambiguity sets each stage of the dynamic program can be rewritten as a single minimization, which can then be solved by stochastic dual dynamic integer programming (SDDiP). This mission formalizes the first family, Type 1, in which every moment is bounded above and below by decision-dependent functions.

Timeline. Two-stage decision-dependent DRO with moment bounds was reformulated by F. Luo and S. Mehrotra (Distributionally robust optimization with decision dependent ambiguity sets, Optimization Letters, 2020, arXiv:1806.09215), Theorem 3.1. SDDiP for multistage stochastic integer programs is due to J. Zou, S. Ahmed and X. A. Sun (Stochastic dual dynamic integer programming, Math. Program. 175(1–2):461–502, 2019, doi:10.1007/s10107-018-1249-5). Yu and Shen (2020) combine the two in the multistage setting, for Type 1 (moment bounds), Type 2 (mean and covariance) and Type 3 (Delage–Ye type) sets.

Setting

Fix one stage $t$ of the dynamic program. The state $x\in\{0,1\}^I$ links stage $t$ to stage $t+1$, and the stage variable $y\in\mathbb R^{I\times J}$ is used only at stage $t$. The pairs $(x,y)$ allowed at stage $t$ form the stage feasible set $S=X_t(x_{t-1},\xi_t)$, and $g(x,y)$ is the stage cost.

The random vector of stage $t+1$ takes one of $K$ values $\xi^1,\dots,\xi^K\in\mathbb R^J$, the same for every decision (Assumption 3). What depends on the decision is the probability vector $p\in\mathbb R^K$ on these points. $Q_{t+1}(x,\xi^k)$ is the value of the next stage when the state is $x$ and scenario $k$ occurs.

Moment functions. For nonnegative integers $k_{sj}$, the moment functions are $f_s(\xi)=\prod_{j=1}^J\xi_j^{k_{sj}}$, $s=1,\dots,m$, collected into $f=(f_1,\dots,f_m)$.

Type 1 ambiguity set. For decision-dependent bounds $l(x),u(x)\in\mathbb R^m$ and $\underline p(x),\bar p(x)\in\mathbb R^K$,

$$\mathcal P^{D_1}_{t+1}(x)=\Big\{p\in\mathbb R^K_+\ :\ \underline p(x)\le p\le\bar p(x),\ \ l(x)\le\sum_{k=1}^Kp_kf(\xi^k)\le u(x)\Big\}.$$

Normalization $\sum_kp_k=1$ is obtained by choosing one moment function $f_1\equiv1$ with $l_1=u_1=1$.

Stage Bellman equation. The stage value is

$$Q_t(x_{t-1},\xi_t)=\min_{(x,y)\in S}\Big\{g(x,y)+\max_{p\in\mathcal P^{D_1}_{t+1}(x)}\sum_{k=1}^Kp_k\,Q_{t+1}(x,\xi^k)\Big\}.\tag{2}$$

Formalization targets

Goal: Theorem 1 (p. 8)

If $\mathcal P^{D_1}_{t+1}(x)$ is nonempty for every feasible $x$, then (2) equals the joint minimization

$$\begin{aligned}\min_{\alpha,\beta,\underline\gamma,\bar\gamma,x,y}\ \ &g(x,y)-\alpha^{\mathsf T}l(x)+\beta^{\mathsf T}u(x)-\underline\gamma^{\mathsf T}\underline p(x)+\bar\gamma^{\mathsf T}\bar p(x)\\ \text{s.t.}\ \ &(-\alpha+\beta)^{\mathsf T}f(\xi^k)-\underline\gamma_k+\bar\gamma_k\ge Q_{t+1}(x,\xi^k),\quad k\in[K],\\ &(x,y)\in S,\qquad \alpha,\beta,\underline\gamma,\bar\gamma\ge0.\end{aligned}\tag{4}$$

In Lean, "equals" is the statement that for every real $q$, $q$ is the attained minimum of (2) if and only if it is the attained minimum of (4).

Milestones: the inner LP (C-17) (p. 36)

1. Weak duality. For a state $x$, every $p\in\mathcal P^{D_1}_{t+1}(x)$ and every dual point satisfying (4b) and (4d) at $x$, $\sum_kp_kQ_{t+1}(x,\xi^k)\le-\alpha^{\mathsf T}l(x)+\beta^{\mathsf T}u(x)-\underline\gamma^{\mathsf T}\underline p(x)+\bar\gamma^{\mathsf T}\bar p(x)$.
2. Strong duality. If $\mathcal P^{D_1}_{t+1}(x)\ne\emptyset$, some feasible $p$ and some dual point satisfying (4b) and (4d) have equal objective values.

Companion: (7) (p. 9)

With the $2J+1$ moment constraints of (5)–(6) (normalization, first and second moments of each coordinate around affine decision-dependent empirical moments $\mu_j(x)$, $S_j(x)$) and $\underline p=0$, $\bar p=1$, the stage value equals the joint program (7), whose objective (7a) has no $\gamma$-terms.

Significance

Theorem 1 removes the inner maximization from every stage of the multistage model. Without it, each stage is a min–max problem whose inner feasible set moves with the binary decision, and SDDiP's cut generation does not apply. After the reformulation, each stage is a single mixed-integer program whose only nonlinearities are products of a binary state with a continuous dual variable, which McCormick envelopes linearize exactly. The paper's facility-location experiments use exactly this route via (7).

The result is proved on paper by a one-line appeal to LP strong duality. No machine-checked version exists. The formal content this mission adds is the precise accounting of what the appeal needs: that the inner LP is bounded (from $0\le p\le\bar p(x)$), that its dual is attained, that the outer minimum transfers between the two formulations in both directions, and that the sign constraint $p\ge0$ is present. A Lean development also separates the parts that hold for arbitrary $S$ and $g$ from the paper's standing linearity and compactness assumptions.

The platform already has a general LP strong duality theorem, LinearOptimization.lp_strong_duality (Bertsimas–Tsitsiklis, Theorem 4.4, on a general-form LP structure; proved). It is a tool for the milestones, not a statement of this paper.

Difficulty

The inner problem is a finite LP, so the difficulty is not depth but bookkeeping that the paper leaves to the reader. Strong duality must be applied to an LP with four families of inequality rows plus sign constraints, with the moment rows written as sums of vectors. The obvious reading of (3) as printed — no $p\ge0$ — makes Theorem 1 false when $\underline p(x)$ has negative entries, because the free variable $p$ would force (4b) to be an equality. The equivalence of the two outer minima also needs care: (4) minimizes jointly over $(x,y)$ and the multipliers, so the attained minimum of (4) must be matched with a pair $(x,y)$ at which the inner maximum of (2) is attained, in both directions. For (7), the dual of (6) lacks the $\bar\gamma$-terms of (4), so (7) is not a literal instance of Theorem 1: the redundancy of $p\le1$ under $\sum_kp_k=1$, $p\ge0$ has to be used.

Formalization scope

All declarations live in the namespace DDMomentDRO.Type1. States are Fin I → ℝ, stage variables Fin I → Fin J → ℝ, scenarios Fin K → Fin J → ℝ, all indices $0$-based. The moment exponents are a matrix e : Fin m → Fin J → ℕ. $Q_{t+1}$ is an arbitrary real function of $(x,k)$: the theorems use nothing about the next stage, so the recursion is not formalized. The binary state is kept as a hypothesis on $S$; linearity of $g$ and compactness and polyhedrality of $S$ (p. 5) are dropped, a disclosed generalization. The ambiguity set includes $p\ge0$ (the proof's (C-17f)), which (3) as printed omits, and no normalization row is added. Minimum and maximum are IsLeast and IsGreatest of explicitly defined value sets, never sSup/sInf, so an empty ambiguity set or an unbounded inner problem cannot produce a junk value; nonemptiness of the ambiguity set at every feasible state is the theorem's hypothesis, as on the page. An empty stage set makes both sides of the equivalence false rather than vacuously true, so it does not trivialize the goal. The objective (7a) is transcribed term by term.

Contributions welcome: proofs of the two duality milestones (from the platform's LP duality or directly from Farkas' lemma in Mathlib), the transfer argument for Theorem 1, and the specialization (7).

Selected references

• X. Yu, S. Shen, Multistage distributionally robust mixed-integer programming with decision-dependent moment-based ambiguity sets, arXiv:2002.12518v3, 2020; Mathematical Programming, 2020. https://arxiv.org/abs/2002.12518
• F. Luo, S. Mehrotra, Distributionally robust optimization with decision dependent ambiguity sets, Optimization Letters, 2020. https://arxiv.org/abs/1806.09215
• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Mathematical Programming 175, 2019. https://doi.org/10.1007/s10107-018-1249-5
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 4.4.

Motivation

Many planning problems are solved in stages. A decision is taken, uncertainty is revealed, and the next decision reacts to it. Facility location, capacity expansion and network design all fit this pattern. In a growing class of such problems, the distribution of the uncertainty depends on the decision: opening a facility changes the demand it attracts, and a maintenance decision changes the failure rates that follow. Stochastic programs with decision-dependent uncertainty go back to Jonsbråten, Wets and Woodruff (1998) and Goel and Grossmann (2006).

When the distribution is not known exactly, distributionally robust optimization (DRO) optimizes against the worst distribution in an ambiguity set of plausible ones. Moment-based ambiguity sets, which are defined by constraints on the mean and covariance, are one of the standard choices (Delage and Ye, 2010). Luo and Mehrotra (2020) studied single-stage DRO in which such moment sets depend on the decision. Yu and Shen (2020) carry this into the multistage mixed-integer setting. Their goal is to rewrite each stage's min–max Bellman equation as one minimization, so that the stagewise decomposition algorithm SDDiP (Zou, Ahmed and Sun, 2019) applies.

This mission formalizes their reformulation for the Type 2 ambiguity set, which matches a decision-dependent mean and covariance exactly.

Setting

Fix a stage $t$. The decision at stage $t$ is a pair $(x_t,y_t)$: a binary state $x_t\in\{0,1\}^I$, passed to the next stage, and a stage variable $y_t\in\mathbb R^{I\times J}$. The pair must lie in a stage feasible set $S=X_t(x_{t-1},\xi_t)$ and costs $g_t(x_t,y_t)$.

The next-stage random vector $\xi_{t+1}\in\mathbb R^J$ takes one of finitely many values $\xi^1_{t+1},\dots,\xi^K_{t+1}$. This support is fixed (Assumption 3), and only the probabilities $p=(p_1,\dots,p_K)$ are uncertain. The value of being in state $x_t$ when scenario $k$ occurs is $Q^k_{t+1}=Q_{t+1}(x_t,\xi^k_{t+1})$.

The decision determines a mean $\mu(x_t)\in\mathbb R^J$ and a covariance matrix $\Sigma(x_t)\in\mathbb R^{J\times J}$. The Type 2 ambiguity set is the set of probability vectors that match them exactly:

$$\mathcal P^{D_2}_{t+1}(x_t)=\Big\{p\in\mathbb R^K_{\ge 0}:\ \sum_{k}p_k=1,\ \ \sum_k p_k\xi^k_{t+1}=\mu(x_t),\ \ \sum_k p_k(\xi^k_{t+1}-\mu(x_t))(\xi^k_{t+1}-\mu(x_t))^\top=\Sigma(x_t)\Big\}.$$

The Bellman equation (2) of stage $t$ is

$$Q_t(x_{t-1},\xi_t)=\min_{(x_t,y_t)\in S}\Big\{g_t(x_t,y_t)+\max_{p\in\mathcal P^{D_2}_{t+1}(x_t)}\sum_{k=1}^Kp_kQ^k_{t+1}\Big\}.$$

Throughout, $A\bullet B=\operatorname{trace}(A^\top B)$ is the Frobenius inner product.

Formalization targets

Goal: Theorem 2 (p. 11)

If $\mathcal P^{D_2}_{t+1}(x_t)$ is nonempty for every feasible $x_t$, then

$$\begin{aligned} Q_t(x_{t-1},\xi_t)=\min_{x_t,y_t,s,u,Y}\ & g_t(x_t,y_t)+s+u^\top\mu(x_t)+\Sigma(x_t)\bullet Y\\ \text{s.t. }\ & s+u^\top\xi^k_{t+1}+(\xi^k_{t+1}-\mu(x_t))(\xi^k_{t+1}-\mu(x_t))^\top\bullet Y\ge Q^k_{t+1}\quad\forall k,\\ & (x_t,y_t)\in S,\ s\in\mathbb R,\ u\in\mathbb R^J,\ Y\in\mathbb R^{J\times J}. \end{aligned}$$

The left side is a minimum exactly when the right side is, and the two values agree.

Milestones (proof of Theorem 2, p. 37)

1. Weak duality. For every $p\in\mathcal P^{D_2}_{t+1}(x)$ and every $(s,u,Y)$ satisfying the constraints above at $x$,

$$\sum_k p_kQ^k_{t+1}\le s+u^\top\mu(x)+\Sigma(x)\bullet Y.$$

2. Strong duality. If $\mathcal P^{D_2}_{t+1}(x)\neq\emptyset$, both sides are attained and the two optimal values are equal.

Significance

The theorem turns a min–max problem into a single minimization. Under the paper's affine model (12) for $\mu$ and $\Sigma$, and with McCormick envelopes for the products of binary states and continuous duals, that minimization becomes a mixed-integer linear program. SDDiP can then solve the multistage model stage by stage, with valid cuts. The Type 2 set is the paper's middle case. It captures correlations between the components of $\xi_{t+1}$, which the separate moment bounds of the Type 1 set (Theorem 1) cannot, and it still has an LP dual. The Type 3 set of Theorem 3 instead leads to a semidefinite program.

The result is proved in the paper: Appendix C gives a short argument by linear-programming duality. It has not been formalized. A formal proof pins down details the printed proof leaves implicit:

• the nonnegativity constraint, which (10) omits;
• that the dual matrix $Y$ is unrestricted;
• that both optima are attained.

It also yields a reusable, machine-checked instance of LP duality for moment-matching problems on a finite support.

Difficulty

There are two steps. The first is linear-programming strong duality for the inner problem in matrix-valued form. Its constraints are a scalar equation, a vector equation in $\mathbb R^J$ and a matrix equation in $\mathbb R^{J\times J}$, so the dual variables are a scalar, a vector and a matrix, paired through dot and Frobenius products. Turning this into a standard-form LP to which a library duality theorem applies takes bookkeeping. The second step is the exchange of the outer minimum with the dual minimum. Here attainment matters: the inner maximum must be attained at every feasible $x_t$, and the stated equality must hold both when the outer minimum exists and when it does not. Weak duality alone gives only one inequality. The naive argument "dualize and combine" also hides the fact that, without $p\ge0$, the dual constraints would have to be equalities.

Formalization scope

• Indices and types. States are Fin I → ℝ, stage variables are Fin I → Fin J → ℝ, the support is ξ : Fin K → Fin J → ℝ, and the next-stage values are an arbitrary function Qn x k. The theorem uses nothing about the recursion that defines $Q_{t+1}$. The covariance map is named Sig.
• Minima and maxima. These are least and greatest elements of value sets (IsLeast, IsGreatest), never sInf/sSup. The goal states that $q$ is the least stage value if and only if $q$ is the least value of (11). An empty stage set, or an empty ambiguity set, cannot make the statement hold by default values. The ambiguity set is never empty at a feasible state, because that is the theorem's hypothesis, and an empty stage set makes both sides false.
• Hypotheses added or dropped.
  • The ambiguity set includes $p\ge0$. This is (C-18e) of the paper's proof; (10) as printed omits it.
  • $Y$ is a free real matrix.
  • The standing assumptions that $g_t$ is linear and $S$ is a nonempty compact mixed-integer polyhedron are not imposed, since the theorem holds for every $S$ and $g_t$. The binary state is kept as a hypothesis.
  • No symmetry or definiteness is assumed of $\Sigma(x)$.
  • The affine forms (12) are not imposed; they are used only afterwards, for the MILP.
• Infrastructure. Finite-dimensional LP duality with equality constraints and a nonnegative variable, transported to vector and matrix constraints. Statements of LP strong duality already exist on the platform and may be used as tools. Contributions welcome: a proof of each milestone, a general "finite-support moment-matching duality" lemma, and the attainment argument.

Selected references

• X. Yu, S. Shen, Multistage distributionally robust mixed-integer programming with decision-dependent moment-based ambiguity sets, arXiv:2002.12518v3, 2020; Mathematical Programming. https://arxiv.org/abs/2002.12518
• E. Delage, Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• F. Luo, S. Mehrotra, Distributionally robust optimization with decision dependent ambiguity sets, Optimization Letters, 2020. https://arxiv.org/abs/1806.09215
• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Mathematical Programming 175(1–2):461–502, 2019. https://doi.org/10.1007/s10107-018-1249-5
• V. Goel, I. E. Grossmann, A class of stochastic programs with decision dependent uncertainty, Mathematical Programming 108(2–3):355–394, 2006. https://doi.org/10.1007/s10107-005-0658-4
• T. W. Jonsbråten, R. J.-B. Wets, D. L. Woodruff, A class of stochastic programs with decision dependent random elements, Annals of Operations Research 82:83–106, 1998. https://doi.org/10.1023/A:1018943626786