Linear Optimization

Motivation

In the secretary problem $n$ candidates arrive one at a time in uniformly random order; at each arrival the decision maker sees only how the current candidate compares with the earlier ones and must accept or reject irrevocably, aiming to accept the best candidate overall. Dütting, Lattanzi, Paes Leme and Vassilvitskii, Secretaries with Advice (arXiv:2011.06726), study a family of variants in which each candidate also carries a signal about its quality, and show that for many of them the optimal stopping rule is the solution of a finite factor-revealing linear program whose dual can be solved greedily by backward induction.

One of their main examples is the secretary problem with samples: before the $n$ candidates arrive, $k$ further elements of the same random order are revealed as a sample, and a candidate's signal is the number of sample elements smaller than it. This model interpolates between the classical problem ($k=0$, optimal success probability tending to $1/e$) and, as $k\to\infty$, the full-information problem of Gilbert and Mosteller (1966). The paper's Theorem 17 gives the optimal dual solution of this LP in closed form.

Setting

Fix natural numbers $n\ge 1$ (secretaries) and $k\ge 0$ (samples). Rounds are $i=1,\dots,n$; signals are $s\in\{0,1,\dots,k\}$. The dual LP of §5 has the coefficients

$$a(i,s)=\frac{1}{k+1}\prod_{t=1}^{n-1}\frac{s+t}{k+t+1},\qquad c(j,s',i,s)=\frac{1}{s'+1}\prod_{t=1}^{i-1}\frac{s+t}{s'+t+1}\ \ (s'\ge s),$$

with $c(j,s',i,s)=0$ for $s'<s$, and reads

$$\min\sum_{i}\sum_{s}u(i,s)\quad\text{s.t.}\quad u(i,s)+\sum_{j>i}\sum_{s'\ge s}u(j,s')\,c(j,s',i,s)\ge a(i,s),\quad u(i,s)\ge 0 .$$

The greedy solution (equation (8) of the paper) sets $u(n,s)=a(n,s)$ and, going backwards,

$$u(i,s)=\max\Bigl\{0,\ a(i,s)-\sum_{j>i}\sum_{s'}u(j,s')\,c(j,s',i,s)\Bigr\}\qquad(i<n).$$

The un-clipped recursion $v(i,s)$ is the same backward induction with the $\max\{0,\cdot\}$ removed. In Lean, the generic recursion (8) is greedyDual (and unclippedDual) over an arbitrary finite signal type, and the samples instance is samplesGreedy n k i s (resp. samplesUnclipped) with s : Fin (k + 1). Products $\prod_{t=a}^{b}$ with $b<a$ equal $1$.

Formalization targets

Goal: Theorem 17

For every $1\le i\le n$ and $0\le s\le k$: $u(n,s)=a(n,s)$, and for $i<n$

$$u(i,s)=\max\left\{0,\frac{1}{k+1}\prod_{t=1}^{i-1}\frac{s+t}{k+t+1}\left(\prod_{t=i}^{n-1}\frac{s+t}{k+t+1}-\frac{\sum_{j=1}^{n-i}\binom{n-i}{j}\frac1j\prod_{\ell=1}^{j}(k-s+\ell)\prod_{\ell=1}^{n-i-j}(s+i-1+\ell)}{\prod_{t=i}^{n-1}(k+t+1)}\right)\right\}.$$

Milestones (the steps of the paper's proof)

1. Reduction (p. 17): if $v(i',\cdot)$ has the closed form for all $i'>i$, then $v(i,s)=a(n,s)-\frac{1}{k+1}\prod_{t=1}^{n-1}\frac{1}{k+t+1}\prod_{t=1}^{i-1}(s+t)\sum_{s'=s}^{k}T(i,s')$, with $T(i,s')$ an explicit double sum.
2. Two forms of $T$ (pp. 17–18): the double sum collapses to $\sum_{j=1}^{n-i-1}(n-i)\binom{n-i-1}{j}\frac{1}{j(j+1)}\prod_{\ell\le j}(k-s'+\ell)\prod_{t=i+1}^{n-j-1}(s'+t)$.
3. Key identity (p. 18): $\sum_{s'=s}^{k}T(i,s')=\sum_{j=1}^{n-i}\binom{n-i}{j}\frac1j\prod_{\ell=1}^{j}(k-s+\ell)\prod_{t=i}^{n-j-1}(s+t)$.
4. Base case $s=k$ (p. 18) and 5. inductive step $s+1\to s$ (Appendix B, pp. 26–28) of the key identity.
5. Un-clipped closed form (pp. 17–19): $v(i,s)$ equals the expression inside the max, for all $1\le i\le n$.

Significance

Theorem 16 of the paper shows that the greedy dual solution is optimal and that the optimal policy for secretaries with samples is a threshold policy in the signal: accept a best-so-far candidate in round $i$ iff its signal is large enough. Theorem 17 makes this solution explicit, so the optimal thresholds can be read off from the sign of a closed-form expression rather than computed by running the backward recursion, and it is the discrete precursor of the paper's Corollary 18, which recovers the Gilbert–Mosteller full-information thresholds in the limit $k\to\infty$.

The identities are proved in the paper by explicit manipulation of finite sums and products of binomials. No machine-checked version exists. A formal proof checks the long index computations of the proof and of Appendix B, and closes a gap: the paper proves the identity for the un-clipped recursion only ("for the proof we can ignore the $\max\{0,\cdot\}$") and does not argue why the clipped greedy solution has the same form. The goal as stated here, with the maximum, is the statement the paper asserts.

Difficulty

The identities are rational-function identities in $s$, $k$ and the round indices, with sums whose ranges depend on the summation variables and products whose ranges may be empty. The natural first idea, induction on $n-i$ directly on the formula, requires the key identity for $\sum_{s'=s}^{k}T(i,s')$, a double sum over $s'$ and $j$ of products of rising factorials; the paper handles it by a second backward induction over $s$, and both the base case and the step re-index sums with shifted bounds and boundary terms such as $(n-i-1)!$ and $\frac{1}{n-i}\prod_{\ell=1}^{n-i}(k-s+\ell)$.

The passage from the un-clipped to the clipped recursion is a separate difficulty: once $u(j,s')$ is clipped to $0$ at a later round, the sums used at earlier rounds differ from those of the un-clipped recursion, and the closed form survives only because the clipped entries do not affect the relevant sums. That argument is not in the paper.

Formalization scope

• Rounds are natural numbers $1\le i\le n$ (1-based, as printed); signals are Fin (k + 1) in the recursion and naturals $s\le k$ in the formulas. All arithmetic is in $\mathbb R$; naturals are cast before $k-s$, and the natural differences $n-i$, $n-i-j$, $n-j-1$ appear only where the ranges keep them non-truncated.
• Products and sums are over Finset.Icc a b, empty when $b<a$, matching the paper's convention.
• The recursion is defined by well-founded recursion on $n-i$ and sums over all later rounds $j\in\{i+1,\dots,n\}$ and all signals; $c=0$ for $s'<s$ encodes the paper's $\sum_{s'\ge s}$.
• The goal keeps the $\max\{0,\cdot\}$. Stating instead the identity for the un-clipped recursion would be a different (weaker-content) theorem; it is milestone 6.
• No probability model appears: the coefficients are taken as given by their formulas on p. 15. Their probabilistic derivation, the optimality of the greedy solution (Theorem 16), the running time of the LP algorithm, the "natural interpretation" paragraph, Corollary 18 and the plots are out of scope.
• The generic recursion greedyDual is reusable for any instance of the paper's factor-revealing LP (the binary-classifier model of §6 included). General lemmas about sums of rising factorials (ascPochhammer) and binomial re-indexing developed for the milestones are welcome contributions.

Selected references

• P. Dütting, S. Lattanzi, R. Paes Leme, S. Vassilvitskii, Secretaries with Advice, arXiv:2011.06726v1, 2020; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2011.06726
• J. P. Gilbert, F. Mosteller, Recognizing the Maximum of a Sequence, Journal of the American Statistical Association 61(313), 1966. https://doi.org/10.1080/01621459.1966.10502008
• T. S. Ferguson, Who Solved the Secretary Problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

Why the sign of the recourse matrix matters

A two-stage adjustable robust linear program chooses a first-stage decision $x$ before an uncertain right-hand side $h$ is revealed, and a second-stage (recourse) decision $y(h)$ afterwards, minimising the worst case over an uncertainty set $\mathcal U$ of the total cost. Computing the optimal value $z_{AR}(\mathcal U)$ is hard in general (Feige et al., 2007), and the standard tractable restriction is to affine policies $y(h)=Ph+q$ (Ben-Tal et al., 2004), whose optimal value $z_{Aff}(\mathcal U)$ is computed by a single linear program.

El Housni and Goyal (arXiv:1807.00163v2) show that, when the recourse matrix $B$ is non-negative and $\mathcal U$ is a budget of uncertainty set, $z_{Aff}$ is within a factor $O(\log n/\log\log n)$ of $z_{AR}$. Their Section 7 asks whether the non-negativity of $B$ is needed, and answers with a family of two-stage lot-sizing instances whose recourse matrix is a network matrix with entries in $\{-1,0,1\}$. On this family the adjustable problem has value $0$ while every affine policy costs at least $m/2-1$. Lot-sizing and transportation recourse are among the most common uses of two-stage robust optimisation (see Bertsimas and de Ruiter, 2016), so the instance is a natural one, not an artefact.

Lower bounds on the gap between affine and adjustable policies were known before (Bertsimas and Goyal, 2012); the point of the present family is that the adjustable value is exactly $0$, so the ratio $z_{Aff}/z_{AR}$ is infinite and the difference $z_{Aff}-z_{AR}$ grows linearly in $m$.

Setting

The lot-sizing problem (7.1). There are $m$ nodes. Node $i$ stores inventory $x_i$ at cost $c_i$ per unit, up to a capacity $K_i$, and faces an uncertain demand $h_i$. After $h$ is revealed, inventory may be shipped from node $i$ to node $j$ in amount $y_{ij}(h)\ge0$ at cost $d_{ij}$ per unit. A solution $(x,y)$ is feasible when $0\le x_i\le K_i$ and, for every $h\in\mathcal U$,

$$x_i+\sum_{j}y_{ji}(h)-\sum_j y_{ij}(h)\ \ge\ h_i\qquad(i\in[m]).$$

The objective is the first-stage cost $\sum_ic_ix_i$ plus the worst case over $h\in\mathcal U$ of the transportation cost $\sum_{ij}d_{ij}y_{ij}(h)$. The optimum over all rules $h\mapsto y(h)$ is $z_{AR}(\mathcal U)$, and the optimum over affine rules $y(h)=Ph+q$ (one row of $P$ per arc, one column per node) is $z_{Aff}(\mathcal U)$.

The family (7.2). Let $m=2k$, and split the nodes into $J_1$ and $J_2$ with $|J_1|=|J_2|=k$. Set $c_i=0$ on $J_1$ and $c_i=1$ on $J_2$, $K_i=1$ everywhere, $d_{ij}=0$ for $i\in J_1$, $j\in J_2$, and $d_{ij}=\infty$ otherwise. The uncertainty set is

$$\mathcal U=\Big\{h\in[0,1]^m\ \Big|\ \sum_{i=1}^m h_i\le m/2\Big\}.$$

Inventory can thus move only from $J_1$ to $J_2$, at no cost; stocking $J_1$ is free and stocking $J_2$ costs one per unit.

In the Lean development the general problem is the structure LotSizing N E (nodes N, usable arcs E with tail src, head tgt, distances d), with the predicate Feasible, the cost cost, and the sets adjustableValues, affineValues of objective values. The family is lotSizingFamily k, on nodes Fin k ⊕ Fin k and arcs Fin k × Fin k.

Formalization targets

Goal: Lemma 7.1

For every $k\ge1$,

$$z_{AR}(\mathcal U)=0\qquad\text{and}\qquad z_{Aff}(\mathcal U)=\frac m2-1=k-1,$$

each stated as IsLeast of the corresponding set of objective values, which asserts that the value is attained and is the minimum. The unboundedness of the gap, $z_{Aff}-z_{AR}=k-1\to\infty$, is immediate.

Milestones (Appendix D, in proof order)

1. The first-stage decision $x=\mathbb 1_{J_1}$ admits a second-stage policy with cost $0$ in every scenario (p. 35).
2. (D.3), for $k\ge2$: every feasible affine solution has $x_i=1$ on $J_1$, and its flow on arc $(i,j)$ depends on $h_i$ only, with $P_{(i,j),i}+q_{ij}=0$ (p. 36).
3. For $k\ge2$, every feasible affine solution satisfies $x_j+q_{\ell j}\ge1$ for $\ell\in J_1$, $j\in J_2$ (pp. 36–37).
4. Every feasible affine solution has $\sum_{j\in J_2}x_j\ge m/2-1$, hence $z_{Aff}\ge m/2-1$ (p. 37).
5. The explicit affine solution $x=\mathbb 1-e_m$, $y_{im}(h)=1-h_i$, is feasible and costs $m/2-1$ (p. 37).

Significance

The result. The approximation guarantees of the paper ($O(\log n/\log\log n)$ for budget sets, $O(\log^2 n/\log\log n)$ for disjoint constrained budgets) assume $B\ge0$. Lemma 7.1 shows that this assumption is not a convenience of the proof: with a network recourse matrix no bound on $z_{Aff}/z_{AR}$ of any form holds, even for a budget set and a bipartite network. Any extension of the guarantees to transportation or flow recourse must therefore change the policy class or add structure, which is the open direction the paper states after the lemma.

Formalizing it. The lemma is proved in the paper; it has not been machine-checked. The mission produces a reusable definition of the two-stage robust lot-sizing problem with arc-based recourse, the precise instance family, and checked versions of the five steps of Appendix D. Two of those steps hold only for $m\ge4$ and one is printed with its indices swapped (see the scope section); the formal statements make those boundaries explicit.

Difficulty

The adjustable half is a transportation argument, and the affine upper bound is a direct verification of one explicit solution. The substance is the affine lower bound, which must hold for every feasible affine solution, not for a particular one. Comparing an affine policy with the adjustable optimum on a few extreme scenarios gives nothing: on any single scenario an affine policy can match the adjustable cost. What fails for affine policies is simultaneous feasibility over the whole of $\mathcal U$, and the lower bound has to extract a cost from that requirement alone. It is also sensitive to the size of the instance: two of the intermediate steps of Appendix D are false for $m=2$, so a formal proof has to treat small $m$ separately.

Formalization scope

• Model. Vectors are functions on finite types with the componentwise order; indices are 0-based. The second stage is a rule $y:\mathbb R^N\to\mathbb R^E$, which gives the same values as choosing $y(h)$ separately per scenario. The epigraph variable $z$ of (7.1) appears through the sets of objective values $t$ with $\sum_ic_ix_i+\sum_a d_a y_a(h)\le t$ for all $h\in\mathcal U$.
• Infinite distances. Arcs with $d_{ij}=\infty$ are omitted rather than given an extended-real cost: a finite-cost solution never uses them, so no optimal value changes, and App. D itself works with the reduced constraints (D.1)–(D.2) and with a matrix $P$ having "one row per edge". The kept arcs $J_1\times J_2$ have $d=0$, and the cost keeps the term $\sum_a d_a y_a(h)$ so that (7.1) is visible.
• Values as IsLeast. No real infimum is used, so "$z=0$" cannot hold on an empty feasible set; feasibility includes $0\le x\le K$, $Ph+q\ge0$ on all of $\mathcal U$, and the coverage constraint at every node, including the outflow constraint (D.2) at $J_1$.
• Sizes. The paper's "$m$ even" is $m=2k$. The goal assumes $k\ge1$; at $k=0$ the affine value would be $0\ne-1$.
• Corrections, disclosed in the items. (i) The paper builds the zero-cost adjustable policy only at extreme points of $\mathcal U$; the milestone quantifies over all of $\mathcal U$, as feasibility requires. (ii) (D.3) and the bound $x_j+q_{\ell j}\ge1$ are false for $m=2$ (explicit counterexamples are in the items' notes) and carry the hypothesis $k\ge2$. (iii) "for any $j\in J_1$ and for any $\ell\in J_2$" on p. 37 has the indices swapped and is stated with $\ell\in J_1$, $j\in J_2$.
• Not formalized. That (7.1) has a network recourse matrix with entries in $\{-1,0,1\}$ is descriptive and is not stated; total unimodularity is not needed.
• Reusable parts. LotSizing (any node set, any arc set, any uncertainty set) can host other two-stage lot-sizing and transportation results. Proofs of any milestone, and alternative arguments for the affine lower bound, are welcome.

The source is arXiv:1807.00163v2; its printed page numbers equal the PDF's.

Selected references

• O. El Housni, V. Goyal, On the Optimality of Affine Policies for Budgeted Uncertainty Sets, arXiv:1807.00163v2, 2019 (Mathematics of Operations Research 46(2), 2021). https://arxiv.org/abs/1807.00163v2
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99(2), 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134(2), 2012. https://doi.org/10.1007/s10107-011-0444-4
• D. Bertsimas, F. de Ruiter, Duality in two-stage adaptive linear optimization: Faster computation and stronger bounds, INFORMS Journal on Computing 28(3), 2016. https://doi.org/10.1287/ijoc.2016.0689
• U. Feige, K. Jain, M. Mahdian, V. Mirrokni, Robust combinatorial optimization with exponential scenarios, IPCO 2007. https://doi.org/10.1007/978-3-540-72792-7_33

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