Operations Research

Motivation

Car dealers, electronics retailers and office suppliers sell products whose prices and features are set upstream by manufacturers, and bundle each product with a service of their own: maintenance, repairs or a warranty. The dealer's short-term problem is then purely combinatorial. Which products should be carried, and which of them should come with a long rather than a short service? Longer service makes a product more attractive to consumers but costs the dealer more per unit sold, and the cost per unit of service time depends on the product's quality.

Wang, Ke and Cui (SSRN 3766191, accepted at Manufacturing & Service Operations Management) study price, quality and service decisions under multinomial logit (MNL) and nested logit demand. Section 5.2 of the paper treats the dealer's problem and shows that its solution has a two-threshold structure. This mission formalizes that result, Theorem 5, together with the steps of its proof in the Online Supplement.

The single-service version of the question is classical: under MNL demand with fixed prices, the profit-maximizing assortment consists of the products with the highest margins, a revenue-ordered (here: markup-ordered) assortment (Talluri & van Ryzin 2004). Theorem 5 extends this to two service options per product, where the choice is between three actions for each product (not offered, short service, long service) and the margin of each action differs.

Setting

There are products $\mathcal N=\{1,\dots,N\}$. Product $i$ has a fixed price $p_i$ and quality $q_i$, a quality sensitivity $\alpha_i$, a service utility per unit time $s_i$, a unit production cost $c_iq_i^2$, and a service cost per unit time $a_i-b_iq_i$. Two service durations are available: a short one $t_s$ and a long one $t_l$.

The dealer chooses two disjoint sets $S_l,S_s\subseteq\mathcal N$: products in $S_l$ are offered with service duration $t_l$, products in $S_s$ with $t_s$, and the others are not offered. A product $i$ offered with duration $t$ has attraction $\exp(\alpha_iq_i-p_i+ts_i)$ and markup $p_i-c_iq_i^2-t(a_i-b_iq_i)$. Under MNL demand with an outside option, product $i\in S_l$ is bought with probability

$$d_i(\mathbf p,\mathbf q;S_l,S_s)=\frac{\exp(\alpha_iq_i-p_i+t_ls_i)}{1+\sum_{j\in S_l}\exp(\alpha_jq_j-p_j+t_ls_j)+\sum_{j\in S_s}\exp(\alpha_jq_j-p_j+t_ss_j)},$$

and similarly with $t_s$ for $i\in S_s$ (eq. (12)). The dealer's expected profit, with market size one, is

$$\Pi^s(\mathbf p,\mathbf q;S_l,S_s)=\sum_{i\in S_l}\big[p_i-c_iq_i^2-t_l(a_i-b_iq_i)\big]d_i+\sum_{i\in S_s}\big[p_i-c_iq_i^2-t_s(a_i-b_iq_i)\big]d_i ,$$

and problem (13) is to maximize $\Pi^s$ over disjoint pairs $(S_l,S_s)$.

Two orderings of products appear in the answer. The short-service markup is $z_i=p_i-c_iq_i^2-t_s(a_i-b_iq_i)$. The adjusted markup is

$$x_i=(p_i-c_iq_i^2)-A_i\,(a_i-b_iq_i),\qquad A_i=\frac{t_l\exp(t_ls_i)-t_s\exp(t_ss_i)}{\exp(t_ls_i)-\exp(t_ss_i)} .$$

A markup-ordered assortment is a set of the products with the highest values of $z_i$; an adjusted markup-ordered set is a set of the products with the highest values of $x_i$.

Formalization targets

Goal: Theorem 5

Assume $t_s<t_l$, $s_i>0$ and $a_i-b_iq_i\ge0$ for all $i$. There are thresholds $\theta,\theta'$ such that, with $S_{i^*}=\{i:z_i\ge\theta\}$ and $S_{j^\natural}=\{i:x_i\ge\theta'\}$,

$$S_{j^\natural}\subseteq S_{i^*}\quad\text{and}\quad \Pi^s(\mathbf p,\mathbf q;S_l,S_s)\le\Pi^s\big(\mathbf p,\mathbf q;S_{j^\natural},\,S_{i^*}\setminus S_{j^\natural}\big)\ \text{ for all disjoint }(S_l,S_s).$$

Part (a) of the paper (a markup-ordered assortment is an optimal offer set) and part (b) (long service on an adjusted markup-ordered subset of it, short service on the rest) are one statement about the same $S_{i^*}$.

Milestones from the proof (Online Supplement p. 8)

1. (EC.11). For disjoint $(S_l,S_s)$, $r=\Pi^s(S_l,S_s)$ if and only if $r=\sum_{i\in S_l}h^l_i(r)+\sum_{i\in S_s}h^s_i(r)$, where $h^l_i(r)=[y_i-r]\exp(\alpha_iq_i-p_i+t_ls_i)$, $h^s_i(r)=[z_i-r]\exp(\alpha_iq_i-p_i+t_ss_i)$ and $y_i=p_i-c_iq_i^2-t_l(a_i-b_iq_i)$.
2. The fixed point. $H(r)=\max_{S_l,S_s}\{\sum_{S_l}h^l_i(r)+\sum_{S_s}h^s_i(r)\}=\sum_i\max\{h^l_i(r),h^s_i(r),0\}$; $H$ is non-increasing; $r=H(r)$ has a unique root $r^*$, and $r^*$ is the optimal value of (13).
3. Breakpoints. $x_i,y_i,z_i$ are the roots of $h^l_i=h^s_i$, $h^l_i=0$, $h^s_i=0$, and $x_i\le y_i\le z_i$.
4. Piecewise form. $h_i=h^l_i$ on $r\le x_i$, $h^s_i$ on $x_i<r\le z_i$, $0$ on $r>z_i$.
5. Level sets at $r^*$. $S_l=\{x_i\ge r^*\}$ and $S_s=\{z_i\ge r^*\}\setminus S_l$ is an optimal pair with profit $r^*$.

Significance

Problem (13) has $3^N$ feasible pairs. Theorem 5 reduces the search to at most $O(N^2)$ pairs indexed by two thresholds, and it says which products deserve the long service: those with the highest adjusted margin $x_i$, which charges each unit of service cost at the rate $A_i>t_l$ rather than at $t_l$. The paper's managerial reading is that high-margin products go with long service, as with retailers that attach longer warranties to expensive items.

The result is proved in the paper; none of it is machine-checked. A formal proof gives a verified two-service extension of the MNL revenue-ordered assortment theorem, and the fixed-point reduction (milestones 1 and 2) is a reusable device for MNL assortment problems with several options per product.

Difficulty

The profit is a ratio of sums, so exchanging one product's service changes every choice probability, and pairwise exchange arguments do not directly compare assortments. The naive idea of ranking products by a single margin fails: the long-service margin $y_i$ and the short-service margin $z_i$ order products differently, and the long service also raises the product's attraction. Neither ordering alone decides which products get long service. The adjusted markup $x_i$ is the breakpoint at which long and short service become equally profitable, and the three breakpoints $x_i\le y_i\le z_i$ must line up for the threshold structure to hold. This ordering uses $a_i-b_iq_i\ge0$: with a negative service cost the long service can be optimal for a product whose adjusted markup is below that of a product left unserved, and part (b) fails.

Formalization scope

• Products are Fin N (0-based); $N=0$ is allowed. All parameters $\alpha,a,b,c,s,p,q$ are arbitrary real vectors and $t_s,t_l$ real numbers; prices and qualities are fixed data, not decisions.
• The outside option is the constant $1$ in the denominator. The MNL formula is the definition; its derivation from Gumbel utilities is cited, not formalized.
• Decisions are pairs of Finset (Fin N) with Disjoint Sl Ss; optimality is a global inequality against every disjoint pair.
• "Markup-ordered" and "adjusted markup-ordered" are upper level sets $\{i: z_i\ge\theta\}$, $\{i:x_i\ge\theta'\}$ with real thresholds. Each is a prefix of every decreasing relabelling, so no tie-break is fixed; the empty and the full set are allowed.
• The model's standing assumptions are explicit hypotheses wherever they are used: $t_s<t_l$ (shortest and longest duration), $s_i>0$ (service utility) and $a_i-b_iq_i\ge0$ (service cost). The first two make $A_i$ well defined; $A_i$ is a total Lean function that returns $0$ when its denominator vanishes, a value no statement relies on. No sign is imposed on $b_i$ or $c_i$.
• Trivializing formalizations are ruled out: the statement has two service levels (a single level would be the Talluri–van Ryzin theorem), uses level sets rather than a fixed relabelling with strict orders, ties the long-service set to the same offered set in (a) and (b) instead of using independent existentials, and states the three hypotheses rather than leaving them implicit.
• Definitions: the MNL choice probabilities and profit (12)–(13), and the auxiliary functions $h^l_i,h^s_i,h_i,H$, $A_i$, $x_i$. Proofs of the milestones need only finite sums, max and elementary real analysis. Proofs of any milestone, and alternative routes to Theorem 5, are welcome.

Selected references

• Ruxian Wang, Chenxu Ke, Shiliang Cui, Product Price, Quality and Service Decisions under Consumer Choice Models, Manufacturing & Service Operations Management, 2022 (accepted manuscript, SSRN 3766191). https://ssrn.com/abstract=3766191 — DOI of the published version: https://doi.org/10.1287/msom.2020.0947
• Kalyan Talluri, Garrett van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• Daniel McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in Frontiers in Econometrics, Academic Press, 1974.

Motivation

A firm that sells durable products with an attached service (a warranty, a maintenance plan, a support contract) chooses three things for each product: its price, its quality, and how long the service lasts. Wang, Ke and Cui (SSRN 3766191, Manufacturing & Service Operations Management, 2022) study this joint decision when consumers choose among the products according to a discrete choice model. Under the multinomial logit (MNL) model they show that every product's optimal service duration is either the shortest or the longest available, so that the products split into a short-service group and a long-service group.

That conclusion suggests a different model of the consumer. In business procurement, and more generally when the buyer first decides how long a product will be used, the consumer plausibly chooses a service duration first and a product second. The two-stage nested logit (NL) model (Ben-Akiva 1973; McFadden 1980) captures exactly this: the two service groups become nests, and products within a nest are closer substitutes than products in different nests. Section 4 of the paper asks whether the MNL structure of optimal qualities and prices survives in this model. This mission formalizes its answer, Theorem 4.

Price optimization under the nested logit model has a substantial literature. For prices alone, the optimal prices within a nest share one markup and the problem reduces to a one-dimensional fixed point (Li & Huh 2011; Gallego & Wang 2014). Theorem 4 adds quality as a decision, with production cost quadratic in quality and service cost depending on quality.

Setting

There are two nests $x\in\{s,l\}$. Nest $x$ contains $m_x$ products $i=1,\dots,m_x$, and every product of nest $x$ is sold with the same fixed service duration $t_x$. Product $i$ of nest $x$ has parameters $\alpha_{xi}$ (quality sensitivity), $a_{xi}$ (base service cost per unit time), $b_{xi}$ (marginal effect of quality on service cost), $c_{xi}>0$ (production-cost coefficient) and $s_{xi}$ (service utility per unit time). The firm chooses a price $p_{xi}$ and a quality $q_{xi}$ for every product.

The total attractiveness of nest $x$ is $e_x=\sum_{i=1}^{m_x}\exp(\alpha_{xi}q_{xi}-p_{xi}+t_xs_{xi})$. With upper-level scale parameter $\mu_1\ge 1$ (the nest coefficient is $1/\mu_1$; the lower-level scale is normalized to $1$), a consumer chooses nest $x$ with probability

$$d_x(\mathbf p,\mathbf q)=\frac{e_x^{1/\mu_1}}{1+e_s^{1/\mu_1}+e_l^{1/\mu_1}},$$

buys nothing with the remaining probability, and, having chosen nest $x$, picks product $i$ with probability $d_{i|x}=\exp(\alpha_{xi}q_{xi}-p_{xi}+t_xs_{xi})/e_x$. The probability of buying product $i$ of nest $x$ is $d_{xi}=d_x\,d_{i|x}$. The markup of a product is its price minus production cost $c_{xi}q_{xi}^2$ minus service cost $t_x(a_{xi}-b_{xi}q_{xi})$, and the firm's expected profit (market size one) is

$$\Pi_M(\mathbf p,\mathbf q)=\sum_{x\in\{s,l\}}\sum_{i=1}^{m_x}\bigl[p_{xi}-c_{xi}q_{xi}^2-t_x(a_{xi}-b_{xi}q_{xi})\bigr]\,d_{xi}(\mathbf p,\mathbf q).$$

The firm maximizes $\Pi_M$ over all real price and quality vectors. When $\mu_1=1$ the model is the MNL model.

Formalization targets

Goal: Theorem 4

Let $q^\dagger_{xi}=(\alpha_{xi}+t_xb_{xi})/(2c_{xi})$. The equation

$$r=\sum_{x\in\{s,l\}}\mu_1\Bigl(\sum_{i=1}^{m_x}\exp\bigl(\alpha_{xi}q^\dagger_{xi}-c_{xi}q^{\dagger2}_{xi}-t_x(a_{xi}-b_{xi}q^\dagger_{xi})+t_xs_{xi}-r-\mu_1\bigr)\Bigr)^{1/\mu_1}$$

has a unique real solution $r^\dagger$. With $p^\dagger_{xi}=\mu_1+r^\dagger+c_{xi}q^{\dagger2}_{xi}+t_x(a_{xi}-b_{xi}q^\dagger_{xi})$,

$$\Pi_M(\mathbf p,\mathbf q)\le\Pi_M(\mathbf p^\dagger,\mathbf q^\dagger)=r^\dagger\quad\text{for all }(\mathbf p,\mathbf q),$$

and $(\mathbf p^\dagger,\mathbf q^\dagger)$ is the only maximizer.

Milestones

The milestones follow the paper's proof in the Online Supplement:

1. (EC.5): at an optimal price vector, every product $i$ of nest $x$ has markup $1+r/\mu_1+(1-1/\mu_1)r_x$, where $r$ is the profit and $r_x$ the nest's average markup; so markups are constant within a nest.
2. (EC.6): with a common markup $\rho_x$ per nest, the profit is $\sum_x\rho_x d_x(\boldsymbol\rho,\mathbf q)$; at the optimal markups, $\rho_x-\mu_1=r$ for each nonempty nest.
3. (EC.7): for every $r$, the right-hand side above, as a function of $\mathbf q$, is maximized exactly at $\mathbf q^\dagger$.
4. (EC.8): that right-hand side is strictly decreasing in $r$, so the fixed-point equation has exactly one root.

Significance

The result. Theorem 4 has two consequences. First, each product's optimal quality depends only on its own parameters and its nest's service duration, not on any other product, although all products are substitutes. At this quality, the marginal production and service cost of quality equals the consumer's marginal utility from it. Second, every product in both nests carries the same markup, $\mu_1+r^\dagger$: the optimal profit plus the reciprocal of the nest coefficient. A pricing problem with $m_s+m_l$ prices reduces to finding the root of a single monotone function. Proposition 7 of the paper uses these closed forms to compare consumer surplus with and without quality control under the NL model.

Formalizing it. The paper's proof writes down first-order conditions and assumes an optimum exists. The goal here is global optimality and uniqueness over all real prices and qualities, which the paper does not prove. A complete formalization needs the existence of the maximizer or a direct upper bound, together with the first-order identities. The related platform item DLevelNestedLogit.Pricing.stationary_point_iff (Li et al. 2015) characterizes stationary points of the price-only revenue in a $d$-level nested logit model. It has no costs and no quality, and it is not used here. No result of this mission has a machine-checked proof yet.

Difficulty

The profit $\Pi_M$ is not concave in prices (under the nested logit model, concavity is known only after a change of variables to market shares, Li & Huh 2011), so a first-order condition does not by itself certify a global maximum. The paper's argument shows only that any optimum satisfies the stated formulas. For a global result, the critical points must be shown to coincide with the maximizers, and the profit must be bounded above by $r^\dagger$ everywhere, including at decisions where markups differ across products of a nest or are negative. The two reductions, to nest markups and then to the scalar $r$, are only valid at the optimum and have to be carried out with that in mind. The exponent $1/\mu_1\le 1$ makes $e_x^{1/\mu_1}$ concave rather than linear in the nest attractiveness. This is the step where the MNL argument does not transfer verbatim.

Formalization scope

• Nests are a two-element type Nest (s, l). Products of nest $x$ are Fin (m x), 0-based. Nests may be empty: an empty nest has $e_x=0$, $0^{1/\mu_1}=0$, and contributes nothing.
• The outside option is the "$1+$" in the denominator of $d_x$, not a nest.
• Durations $t_s,t_l$ are fixed data, not decisions, with no order assumed between them. The nests are fixed.
• Prices and qualities range over all of $\mathbb R$. The model's normalization $q\ge 0$ is not imposed, as in the paper's own formula.
• Standing hypotheses: $\mu_1\ge 1$ (general; $\mu_1=1$ is allowed but is not the only case) and $c_{xi}>0$. No sign is imposed on $\alpha,a,b,s$.
• Powers are Real.rpow of nonnegative sums of exponentials.
• "Optimal" means a global maximizer over all real vectors. The milestones that the paper derives from first-order conditions are stated as properties of a global maximizer.
• The price formula $p^\dagger$ takes $r$ as an argument, and the theorem must identify $r=r^\dagger$.

The following versions are trivializing and are excluded: $\mu_1=1$ only (the MNL case), a single nest, first-order conditions in place of global optimality, fixed qualities, or an optimum defined by the paper's formula.

The definitions (Model, MarkupProblem, Optimum) are self-contained and can be reused for other nested logit pricing results. Contributions are welcome on each milestone, on a sorry-free derivative of $\Pi_M$ in $p_{xi}$, and on an existence result for the maximizer.

Selected references

• Y. Wang, J. Ke, S. Cui, Product Price, Quality and Service Decisions under Consumer Choice Models, Manufacturing & Service Operations Management, 2022 (accepted manuscript, SSRN 3766191). https://ssrn.com/abstract=3766191 — DOI https://doi.org/10.1287/msom.2020.0947
• M. Ben-Akiva, Structure of Passenger Travel Demand Models, PhD thesis, Massachusetts Institute of Technology, 1973 (no stable link; cited as in the source's bibliography).
• D. McFadden, Econometric Models for Probabilistic Choice Among Products, Journal of Business 53(3), S13–S29, 1980. https://doi.org/10.1086/296093
• H. Li, W. T. Huh, Pricing Multiple Products with the Multinomial Logit and Nested Logit Models: Concavity and Implications, Manufacturing & Service Operations Management 13(4), 549–564, 2011. https://doi.org/10.1287/msom.1110.0344
• G. Gallego, R. Wang, Price Optimization and Competition for Multi-Products under the Nested Logit Model with Product-Differentiated Price Coefficients, Operations Research 62(2), 450–461, 2014 (cited as in the source's bibliography; link not verified in this session).

Motivation

Quadratically constrained quadratic programs (QCQPs) minimize a quadratic function subject to quadratic inequality and equality constraints. They model facility location, pooling, max-cut, trust-region steps and robust optimization problems, and every $\{0,1\}$ integer program can be written as one; in general they are NP-hard. The standard tractable approach is the Shor semidefinite relaxation, which lifts $x$ to the matrix $xx^\top$ and relaxes the rank-one condition to positive semidefiniteness. A recurring question is when this relaxation loses nothing: when its optimal value equals that of the QCQP (SDP tightness), and, more strongly, when its projected epigraph equals the convex hull of the QCQP's epigraph (convex hull exactness). The second property also describes the convex hull of the nonconvex feasible set's epigraph, which is useful in branch-and-bound and cutting-plane methods.

Timeline. The S-lemma (Yakubovich, 1971) gives SDP tightness for one inequality constraint, and Fujie and Kojima (1997) recorded the dual description of the SDP value used below. For the trust-region subproblem and its generalization, convex hull descriptions of the epigraph were given by Ho-Nguyen and Kılınç-Karzan (2017) and by Wang and Kılınç-Karzan (arXiv:1907.08843, 2019). Beck (2007) and Beck, Drori and Teboulle (2012) gave SDP tightness results for quadratic matrix programs. Wang and Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs (arXiv:1911.09195v3, Math. Program. 2021), introduced a general framework based on the faces of a dual set $\Gamma$ and proved convex hull and tightness results for polyhedral $\Gamma$ and for QCQPs with large quadratic eigenvalue multiplicity. This mission formalizes the paper's first convex hull theorem (Theorem 1, p. 13) and the framework it rests on.

Setting

Fix $N$ variables and $m\ge1$ constraints, the first $m_I$ inequalities and the remaining $m_E=m-m_I$ equalities. Each function is

$$q_i(x)=x^\top A_ix+2b_i^\top x+c_i,\qquad A_i\in\mathbb S^N,\ b_i\in\mathbb R^N,\ c_i\in\mathbb R,\quad i=0,\dots,m.$$

The QCQP (1) is $\mathrm{Opt}=\inf\{q_0(x): q_i(x)\le0\ (i\le m_I),\ q_i(x)=0\ (i>m_I)\}$, and its epigraph is $\mathcal D=\{(x,t): x\text{ feasible},\ q_0(x)\le2t\}$.

With $Q_i=\begin{pmatrix}c_i&b_i^\top\\ b_i&A_i\end{pmatrix}$ and $Y=\begin{pmatrix}1&x^\top\\ x&X\end{pmatrix}$, the SDP relaxation (3) minimizes $\langle Q_0,Y\rangle$ over $X\in\mathbb S^N$ with $Y\succeq0$ and the constraints $\langle Q_i,Y\rangle\le0$ or $=0$; its value is $\mathrm{Opt}_{\mathrm{SDP}}$ and its projected epigraph is $\mathcal D_{\mathrm{SDP}}=\{(x,t):\exists X,\ (x,X)\text{ feasible},\ \langle Q_0,Y\rangle\le2t\}$ (4). Always $\mathrm{conv}(\mathcal D)\subseteq\mathcal D_{\mathrm{SDP}}$ and $\mathrm{Opt}\ge\mathrm{Opt}_{\mathrm{SDP}}$.

For $\gamma\in\mathbb R^m$ let $A(\gamma)=A_0+\sum_i\gamma_iA_i$, and similarly $b(\gamma)$, $c(\gamma)$ and the Lagrangian $q(\gamma,x)=q_0(x)+\sum_i\gamma_iq_i(x)$. The dual object is

$$\Gamma=\{\gamma\in\mathbb R^m:\ A(\gamma)\succeq0,\ \gamma_i\ge0\ \text{for } i\le m_I\}.$$

Assumption 1: the QCQP is feasible and some $\gamma^*$ with $\gamma^*_i\ge0$ for $i\le m_I$ has $A(\gamma^*)\succ0$. Assumption 3: $\Gamma$ is polyhedral. For $\hat x\in\mathbb R^N$, $\mathcal F(\hat x)=\arg\max_{\gamma\in\Gamma}q(\gamma,\hat x)$. A face $\mathcal F$ of $\Gamma$ is definite if some $\gamma\in\mathcal F$ has $A(\gamma)\succ0$ and semidefinite otherwise, with shared zero eigenspace $\mathcal V(\mathcal F)=\{v: A(\gamma)v=0\ \forall\gamma\in\mathcal F\}$. Finally $\operatorname{aff\,dim}$ denotes affine dimension.

Formalization targets

Goal: Theorem 1 (p. 13)

Under Assumptions 1 and 3, if every semidefinite face $\mathcal F$ of $\Gamma$ satisfies $\dim\mathcal V(\mathcal F)\ge\operatorname{aff\,dim}\{b(\gamma):\gamma\in\mathcal F\}+1$, then

$$\mathrm{conv}(\mathcal D)=\mathcal D_{\mathrm{SDP}}\qquad\text{and}\qquad\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}.$$

Milestones

1. Lemma 1 (p. 7): under Assumption 1, $\mathcal D_{\mathrm{SDP}}=\{(x,t):\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t\}$ and $\mathrm{Opt}_{\mathrm{SDP}}=\min_x\sup_{\gamma\in\Gamma}q(\gamma,x)$.
2. Lemma 2 (p. 9): a semidefinite face has a unit vector in $\mathcal V(\mathcal F)$.
3. Lemma 3 (p. 9): under Assumptions 1 and 2, a point of $\mathcal D_{\mathrm{SDP}}$ with definite $\mathcal F(\hat x)$ lies in $\mathcal D$.
4. Observation 1 (p. 10): under Assumption 1, a face of affine dimension $m$ is definite.
5. Lemma 4 (p. 10): under Assumptions 1, 2 and the decomposition condition (7), the two conclusions of Theorem 1 hold.
6. Lemma 8 (p. 13): under Assumption 3, $\Gamma=\Gamma_e+\mathrm{cone}(\Gamma_r)$ with polytopes $\Gamma_e,\Gamma_r$, and $\mathcal F(\hat x)=\mathcal F_e(\hat x)+\mathrm{cone}(\mathcal F_r(\hat x))$ when the supremum is finite.
7. Lemma 7 (p. 13): under the hypotheses of Theorem 1, condition (7) holds.

Companions

Lemma 6 (p. 11: $\dim\mathcal V(\mathcal F)\ge k$ for the quadratic eigenvalue multiplicity $k$), Theorem 2 (p. 15: the hypothesis of Theorem 1 with $k$ in place of $\dim\mathcal V(\mathcal F)$), and Corollaries 1–4 (pp. 16–18: convex quadratic programs, one constraint, $b_i=0$, scalar quadratic forms with $m\le N$).

Significance

The result. Theorem 1 gives a checkable sufficient condition, stated on the faces of a polyhedral dual set, under which the Shor relaxation is exact in the strongest sense: it describes $\mathrm{conv}(\mathcal D)$, so the SDP value equals the QCQP value and, by Remark 7, $\mathrm{conv}(\mathcal D)$ is second-order cone representable. Through Lemma 6 it becomes Theorem 2, the symmetry condition $k\ge\operatorname{aff\,dim}\{b(\gamma)\}+1$; its corollaries recover the convex hull results for the trust-region subproblem and its generalization and give new ones for simultaneously diagonalizable and "Swiss cheese" problems. The sharpness of the bound is shown in §4.3 of the paper.

Formalizing it. The theorem is proved in the paper; nothing in it is machine-checked. A formal proof needs strong conic duality for the SDP in Lemma 1, the Minkowski–Weyl decomposition in Lemma 8, and the face-by-face decomposition argument of Lemma 7. These pieces are shared with the paper's SDP tightness result (Theorem 3), which uses Lemmas 1–3 and 8 again.

Difficulty

The obvious attempt is to take $(\hat x,\hat t)\in\mathcal D_{\mathrm{SDP}}$, recover a rank-one solution of the SDP, and read off a point of $\mathcal D$. This fails because an optimal $Y$ need not have rank one, and a rank-reduction step can leave the feasible set of a nonconvex constraint. The paper instead moves $(\hat x,\hat t)$ along a direction $v$ in the shared zero eigenspace of the face $\mathcal F(\hat x)$, and must show that both endpoints of the move stay in $\mathcal D_{\mathrm{SDP}}$ while the face strictly grows in affine dimension. Controlling the endpoints needs finiteness of the relevant family of quadratic functions, which is where polyhedrality enters; without it (§4.3) the argument and the theorem fail. Lemma 1 also needs a strong duality theorem for semidefinite programs with a minimax step, neither of which is elementary in Lean.

Formalization scope

The Lean development lives in the namespace QCQPTightness.ConvHull. A QCQP is a structure with symmetric $A_0, A_i$, vectors $b_0,b_i$, scalars $c_0,c_i$ and a count $m_I\le m$; constraints are indexed by Fin m, constraint $i$ being an inequality exactly when $i<m_I$. Conventions:

• $\mathrm{Opt}$ and $\mathrm{Opt}_{\mathrm{SDP}}$ are infima in EReal, never real infima; points of $\mathbb R^{N+1}$ are pairs $(x,t)$, and $\mathrm{conv}$ is convexHull ℝ.
• Faces of $\Gamma$ are nonempty convex extreme subsets; the page's convention $\operatorname{aff\,dim}\emptyset=-1$ makes the empty face irrelevant, while Lean's affine dimension of $\emptyset$ would be $0$.
• "$\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t$" is written $\forall\gamma\in\Gamma,\ q(\gamma,x)\le2t$; "a convex combination of points with property $P$" is membership in the convex hull of the set of such points; the unit sphere is $v^\top v=1$.
• The goal carries exactly the paper's hypotheses plus its standing assumption $m\ge1$ (p. 1); Assumption 2 is not assumed because Assumption 3 implies it.
• Lemma 8 is printed with "$\mathcal F_r(\hat x)$ is the face of $\Gamma_e$"; it is formalized with $\Gamma_r$, as the proof and Lemma 7 use it.

A trivializing formalization would assume condition (7), the decomposition of Lemma 8, or any property of $\mathcal F(\hat x)$ in the goal; the goal assumes none of these, and the dimension hypothesis is satisfiable with semidefinite faces present (for $q_0=-x^2$, $q_1=x^2-1$, the face $\{\gamma_1=1\}$ is semidefinite with $\dim\mathcal V=1$).

Infrastructure needed: SDP strong duality (the platform has ConvexOptimization.sdp_strong_duality), the Minkowski–Weyl theorem for polyhedra, faces of convex sets and affine dimension. Proofs of any milestone, of the companions, and reusable lemmas about faces of spectrahedra are welcome.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Math. Program. (2021); arXiv:1911.09195v3. https://arxiv.org/abs/1911.09195 , https://doi.org/10.1007/s10107-020-01589-9
• T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, J. Global Optim. 10 (1997) 367–380. https://doi.org/10.1023/A:1008282830093
• A. Beck, Quadratic matrix programming, SIAM J. Optim. 17 (2007) 1224–1238. https://doi.org/10.1137/05064816X
• N. Ho-Nguyen, F. Kılınç-Karzan, A second-order cone based approach for solving the trust-region subproblem and its variants, SIAM J. Optim. 27 (2017) 1485–1512. https://doi.org/10.1137/16M1065197
• A. L. Wang, F. Kılınç-Karzan, The generalized trust region subproblem: solution complexity and convex hull results, arXiv:1907.08843 (2019). https://arxiv.org/abs/1907.08843
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007) 371–418. https://doi.org/10.1137/S003614450444614X

Motivation

In online matching with multiple prices, a firm sells $n$ items with limited inventories to customers who arrive one at a time; each item can be offered at any price from its own finite price set, and the firm must commit to an offer without knowing future customers. Ma and Simchi-Levi (arXiv:1905.04770, Oper. Res. 2020) show that the best possible competitive ratio (worst-case ratio of the online revenue to the offline LP optimum) for a price set $\mathcal P$ is an explicit number $F(\mathcal P) = 1 - e^{-\alpha^{(1)}}$, computed from $\mathcal P$ alone.

Two tight ratios were known before. For a single item sold over a price set, Ball and Queyranne (Oper. Res. 2009) found the tight ratio $\sigma^{(1)}$. For many items with one price each, the tight ratio is $1 - 1/e$ (Karp, Vazirani and Vazirani 1990; Mehta, Saberi, Vazirani and Vazirani 2007). For a single item whose price ranges over a continuum $[r^{(1)}, r^{(m)}]$, Ball and Queyranne give $1/(1 + \ln(r^{(m)}/r^{(1)}))$. A reader meeting $F(\mathcal P)$ for the first time asks how it compares with these. Proposition 2 of the paper answers that question with strict inequalities, and this mission formalizes it.

Setting

A price set consists of $m$ prices

$$0 < r^{(1)} < r^{(2)} < \dots < r^{(m)},$$

with the convention $r^{(0)} := 0$. Write $s_j = r^{(j-1)}/r^{(j)} \in (0,1)$ for $j = 2, \dots, m$.

The booking limits $\alpha^{(1)}, \dots, \alpha^{(m)}$ are positive numbers with $\sum_j \alpha^{(j)} = 1$ satisfying

$$1 - e^{-\alpha^{(1)}} = \frac{1 - e^{-\alpha^{(j)}}}{1 - s_j}, \qquad j = 2, \dots, m. \qquad (7)$$

The Ball–Queyranne limits $\sigma^{(1)}, \dots, \sigma^{(m)}$ are positive numbers with $\sum_j \sigma^{(j)} = 1$ satisfying

$$\sigma^{(1)} = \frac{\sigma^{(j)}}{1 - s_j}, \qquad j = 2, \dots, m. \qquad (8)$$

Both systems have exactly one solution (Proposition 1). The paper's ratios are $F(\mathcal P) = 1 - e^{-\alpha^{(1)}}$ and $G(\mathcal P) = \sigma^{(1)}$ (Definition 2). Finally, for $m \ge 2$ let $\alpha$ be the unique real root of

$$1 - e^{-\alpha} = \frac{1 - \alpha}{\ln(r^{(m)}/r^{(1)})};$$

$1 - e^{-\alpha}$ is the paper's competitive ratio when every item may be priced anywhere in $[r^{(1)}, r^{(m)}]$ (App. E.1).

In Lean the prices are r : ℕ → ℝ read at $1, \dots, m$, and IsPriceSet m r, IsBookingLimits m r α, IsBQLimits m r σ are the predicates above.

Formalization targets

Goal: Proposition 2 (p. 17)

For $m \ge 2$,

$$\Bigl(1 - \frac1e\Bigr)\sigma^{(1)} < 1 - e^{-\sigma^{(1)}} < 1 - e^{-\alpha^{(1)}}, \qquad (11)$$ $$\frac{1}{1 + \ln(r^{(m)}/r^{(1)})} < \sigma^{(1)}, \qquad (12)$$ $$1 - e^{-\alpha} < 1 - e^{-\alpha^{(1)}}. \qquad (13)$$

Milestones

1. Proposition 1 (p. 13): existence and uniqueness of the solutions of (7) and of (8).
2. Explicit $\sigma$ (App. A, p. 38): $\sigma^{(j)} = (1 - r^{(j-1)}/r^{(j)})\bigl(1 + \sum_{j'=2}^m (1 - s_{j'})\bigr)^{-1}$.
3. Monotonicity (App. A, p. 38): $x \mapsto x/(1 - e^{-x})$ (with its limit value $1$ at $x = 0$) is strictly increasing on $[0, 1]$.
4. (33) (App. A, p. 39): $\alpha^{(1)}$ is the unique solution of $x + \sum_{j=2}^m -\ln\bigl(1 - (1 - e^{-x})(1 - s_j)\bigr) = 1$.
5. (34) (App. A, p. 39): the root $\alpha$ is the unique solution of $x + \sum_{j=2}^m (1 - e^{-x})\ln(r^{(j)}/r^{(j-1)}) = 1$, and it lies in $(0,1)$.
6. Ranges of $F$ and $G$ (p. 14): $1 - e^{-1/m} \le F(\mathcal P) \le 1 - e^{-1}$ and $1/m \le G(\mathcal P) \le 1$.
7. Two prices, (4) (p. 7): for $\mathcal P = \{r, \xi r\}$, $F(\mathcal P) = 1 - \bigl(\sqrt{1 + 4\xi(\xi-1)/e} - 1\bigr)/(2(\xi - 1))$.

Significance

The result. Inequality (11) shows that the multi-item, multi-price ratio is not obtained by multiplying the single-item ratio $\sigma^{(1)}$ by the single-price penalty $1 - 1/e$: the true ratio is strictly larger, so neither the ratio nor the algorithms of the paper can be assembled from the two classical cases. Inequalities (12) and (13) quantify the value of a discrete price menu: restricting the continuum $[r^{(1)}, r^{(m)}]$ to finitely many prices strictly raises the tight ratio, both for one item (Ball–Queyranne) and for many items (this paper). The ranges of $F$ and $G$ bound the guarantees in terms of the number of prices alone, and the two-price formula (4) is the explicit instance used throughout the paper's introduction.

Formalizing it. All results here are proved in the paper (App. A); none has a machine-checked proof that we know of. The mission produces a checked theory of the booking-limit systems (7) and (8), which the paper's three main theorems (the competitive ratios of Multi-price Balance and Multi-price Ranking, and the matching upper bound) all rest on, and checked proofs of the comparisons. The booking-limit predicates are the same in the companion missions of this series and are intended to be shared after consolidation.

Difficulty

The statements are elementary, but (7) is a nonlinear system: eliminating $\alpha^{(2)}, \dots, \alpha^{(m)}$ leaves a polynomial equation of degree $m$ in $e^{-\alpha^{(1)}}$, with no closed form for $m \ge 3$. So $\alpha^{(1)}$ cannot be computed and compared directly; every inequality has to be derived from properties of the defining equations. The root $\alpha$ of (13) is likewise defined only implicitly (via the Lambert $W$ function). The naive approach of comparing the two systems equation by equation does not give (11)'s second inequality, because (7) and (8) relate each limit to the first one through different functions and the two families are tied together only by their common normalization $\sum_j = 1$. In Lean the main friction is bookkeeping: sums over $\{2, \dots, m\}$, natural-number index arithmetic $j - 1$, and the uniqueness arguments, which require strict monotonicity of the functions in (33) and (34).

Formalization scope

Conventions: prices are r : ℕ → ℝ, 1-based, with price r 0 = 0 for $r^{(0)}$; sums over $j = 2, \dots, m$ are over Finset.Icc 2 m. The booking limits are not constructed by Classical.choose: every statement takes functions α, σ together with the hypotheses IsBookingLimits m r α / IsBQLimits m r σ (equations (7)/(8), positivity on $1, \dots, m$, sum $1$). Proposition 1 shows these hypotheses pin down the paper's values on $1, \dots, m$, so no statement is about an arbitrary $\alpha$; a sanity file exhibits solutions for $m = 1$ and for the price set $\{1, 2\}$, so the hypotheses are satisfiable. Standing assumptions are those of the paper: $m \ge 1$ throughout and $m \ge 2$ in Proposition 2, (33), (34), as printed. The constant $1 - 1/e$ is written $1 - e^{-1}$.

Clause (13) is stated for every real root of $1 - e^{-a} = (1-a)/\ln(r^{(m)}/r^{(1)})$; milestone 5 proves that exactly one root exists, so the clause is neither vacuous nor weaker than the printed "the unique solution". The monotonicity of $x/(1 - e^{-x})$ is posed on the printed $[0,1]$ with the value at $0$ set explicitly to the limit $1$, since Lean's $0/0 = 0$ would otherwise give a junk value there.

Everything needed is in Mathlib (Real.exp, Real.log, Real.sqrt, finite sums). Contributions are welcome on any milestone; the monotonicity lemma and Proposition 1 are reusable by the other missions of this series. The paper's proofs are in its Appendix A (pp. 38–39).

Selected references

• W. Ma, D. Simchi-Levi, Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-dependent Competitive Ratios, arXiv:1905.04770v1, 2019; Operations Research 68(6), 2020. https://arxiv.org/abs/1905.04770, https://doi.org/10.1287/opre.2019.1957
• M. O. Ball, M. Queyranne, Toward Robust Revenue Management: Competitive Analysis of Online Booking, Operations Research 57(4), 2009. https://doi.org/10.1287/opre.1080.0654
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, STOC 1990. https://doi.org/10.1145/100216.100262
• A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and Generalized Online Matching, Journal of the ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321

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