Linear Optimization

Motivation

Two-stage adjustable robust optimization models decisions taken in two steps around an uncertain demand: a first-stage decision is fixed now, the demand is revealed, and a second-stage (recourse) decision reacts to it. The objective is the worst-case total cost over a set of possible demands. Computing the optimal adjustable solution is intractable in general, and even for a single budget constraint it cannot be approximated within $\Omega(\log n/\log\log n)$ under a standard complexity assumption (Feige, Jain, Mahdian, Mirrokni, IPCO 2007), where $n$ is the number of decision variables.

Affine policies, in which the recourse is restricted to an affine function of the revealed demand (Ben-Tal et al. 2004), are computable by one linear program and are widely used in practice. The question is how much they lose in the worst case.

Uncertainty sets in applications are rarely a single budget: demand is usually grouped (by region, product family or time period) with a separate budget per group. When the groups are disjoint the set is a Cartesian product of budget sets, a class studied by Gupta et al. and by Feige et al. in the robust covering literature.

Timeline. Bertsimas and Goyal (2012) proved that affine policies are within $O(\sqrt m)$ of the adjustable optimum for general uncertainty sets and that this is tight for some sets. El Housni and Goyal (arXiv:1807.00163, 2018; Mathematics of Operations Research 2021) proved $O(\log n/\log\log n)$ for a single budget set (Theorem 3.1, the first mission of this series) and $O(\log^2 n/\log\log n)$ for disjoint constrained budgeted sets (Theorem 4.1, the goal of this mission).

Setting

Let $A\in\mathbb R^{m\times n}$, a non-negative recourse matrix $B\in\mathbb R^{m\times n}_+$, costs $c,d\in\mathbb R^n_+$ and a polyhedral set $\mathcal X\subseteq\mathbb R^n$ be given. For an uncertainty set $\mathcal U\subseteq\mathbb R^m$ of right-hand sides, problem (1.1) is

$$z_{AR}(\mathcal U)=\min_{x\in\mathcal X}\ c^Tx+\max_{h\in\mathcal U}\ \min_{y(h)\ge0}\big\{d^Ty(h)\ :\ Ax+By(h)\ge h\big\}.$$

A first-stage $x$ and a recourse rule $y(\cdot)$ form a feasible solution when $x\in\mathcal X$ and $y(h)\ge0$, $Ax+By(h)\ge h$ for every $h\in\mathcal U$. The affine problem (2.1) restricts the rule to $y(h)=Ph+q$ (still requiring $Ph+q\ge0$ on $\mathcal U$); its value is $z_{Aff}(\mathcal U)\ge z_{AR}(\mathcal U)$.

Let $S_1,\dots,S_L$ be a partition of $[m]$ and $w_{\ell i}\in[0,1]$ weights. The disjoint constrained budgeted set (4.1) is

$$\mathcal U=\Big\{h\in[0,1]^m\ :\ \sum_{i\in S_\ell}w_{\ell i}h_i\le1\ \ \forall\ell\in[L]\Big\}.$$

With $L=1$ it is the budget of uncertainty set of the first mission.

The fractional covering value (3.2) of a requirement $h$ is $z(h)=\min_{y\ge0}\{d^Ty: By\ge h\}$. In an online fractional covering problem the rows to be covered arrive in batches and a solution may only be increased; an online algorithm $\mathcal A$ is $\rho$-competitive when its cost on every sequence is at most $\rho$ times the offline optimum $\Theta$. Throughout, $\log$ is the natural logarithm and $\beta=8\log n/\log\log n$.

Formalization targets

Goal: Theorem 4.1

$$z_{Aff}(\mathcal U)=O\Big(\frac{\log^2n}{\log\log n}\Big)\cdot z_{AR}(\mathcal U)$$

for every instance with $\mathcal U$ a disjoint constrained budgeted set: there are $C>0$ and $N$ such that $z_{Aff}\le C\frac{\log^2n}{\log\log n}z_{AR}$ for all $n\ge N$, all $m$, every number $L$ of blocks and all data. The constant is unfixed, and the bound must not depend on $L$.

Milestones (the paper's proof, in order)

1. Lemma 3.3 (structural result), restated from the first mission: if covering each row $i\in\mathcal J$ costs more than $4\gamma\frac{\log n}{\log\log n}w_i$ while every scenario $\mathcal W\subseteq\mathcal J$ with $\sum_{\mathcal W}w_i\le1$ costs at most $\gamma$, then $z(\mathcal J)\le4\gamma\frac{\log n}{\log\log n}$ (for $n$ large).
2. Lemma 4.1 — for a greedy scenario $a_1,\dots,a_L$ chosen by Algorithm 1, the online cost $\nu_L$ is at most $\rho\cdot\mathrm{OPT}$.
3. Lemma 4.2 — the affine solution (4.7), a linear part on the thresholded components plus a static part, is feasible.
4. Lemma 4.3 — the linear part costs at most $\beta\rho\cdot\mathrm{OPT}$ for every $h\in\mathcal U$.
5. Lemma 4.4 — the static part costs at most $(1+2\rho+\beta\rho)\cdot\mathrm{OPT}$.

With $\rho=O(\log n)$, Lemmas 4.3 and 4.4 give the goal.

Significance

The result. For disjoint budgets the bound is within a $\log n$ factor of the hardness bound for a single budget, and it does not depend on the number of groups $L$. It shows that affine policies stay near-optimal beyond the single-budget case, for a class that models grouped demand. The paper notes that it is open whether the extra $\log n$ factor is necessary. Gupta et al. give an $O(\log n)$-approximation for a special case with 0/1 matrices and equal weights, but their algorithm is not an affine policy.

Formalizing it. The theorem is proved on paper; no machine-checked proof is known. The formal development makes explicit what the paper uses about the online covering algorithm (monotone, covering, competitive), handles the "without loss of generality" relabelling of the blocks in the greedy scenario, and records two gaps in the proof of Lemma 4.4 (zero weights, and a zero increment $\nu_\ell-\nu_{\ell-1}$, for which Lemma 3.3 is stated with $\gamma>0$).

Difficulty

The thresholds that split cheap from expensive components cannot use the single quantity $\mathrm{OPT}$ as in the single-budget case: a scenario may activate one budget in every block at once, and summing per-block bounds gives a factor $L$. That is the $O(L\log n/\log\log n)$ bound of the paper's Section 5. Removing the dependence on $L$ requires per-block thresholds that add up to $O(\log n)\cdot\mathrm{OPT}$, and the paper obtains them from the increments of an online covering algorithm along a greedily chosen worst sequence of scenarios. A proof of the goal therefore needs an $O(\log n)$-competitive online fractional covering algorithm, Buchbinder and Naor's Theorem 4.1, posed on this platform as BNCovPack.Covering.theorem_4_1 (b57de23d-5953-424f-a729-5a018aa74b37, open). That theorem requires positive costs, so zero-cost columns, which this paper allows, need separate handling. The static part also needs Lemma 3.3, the core of the first mission.

Formalization scope

• Data. Vectors are functions on Fin m, Fin n with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ; Lean indices and blocks are 0-based. First stage and recourse share the dimension $n$, as on p. 1. The partition is S : Fin L → Finset (Fin m), pairwise disjoint and covering Fin m (empty blocks allowed).
• Values. $z_{AR}$, $z_{Aff}$, $z(h)$, $\Theta$ and $z_{Sta}$ are infima in the extended reals, $+\infty$ when infeasible. A formalization with real infima (equal to $0$ on infeasible problems) or without $Ph+q\ge0$ would trivialize the goal and is excluded, as is a constant $C$ that depends on the instance or on $L$.
• Standing assumptions of p. 1: $B\ge0$, $c,d\ge0$, $\mathcal X$ polyhedral, $w_{\ell i}\in[0,1]$, $S$ a partition. "$\mathcal U\subseteq[0,1]^m$ compact convex with $e_i\in\mathcal U$" holds for the set (4.1) and is not added.
• Added hypotheses and corrections. (i) $c^Tx\ge0$ for $x\in\mathcal X$: Theorem 4.1 is false without it (already for $L=1$), and it holds whenever $\mathcal X\subseteq\mathbb R^n_+$. (ii) $n\ge3$ where $\beta\ge0$ is needed, and a threshold $N_0$ in Lemma 3.3, which as printed fails at $n=2$. (iii) Covering solutions $v_i$ are required only for $i\in\mathcal I$.
• The online algorithm is an abstract structure OnlineCover with ratio $\rho$: starting at $0$, non-negative, monotone, covering every revealed coverable row, and $\rho$-competitive on disjoint batches. The milestones hold for every such algorithm, with the paper's $O(\log n)$ written as $\rho$. The goal does not mention the algorithm. Algorithm 1 is a predicate on a run (a bijection of blocks and the chosen scenarios) with its maximality clause, so ties are arbitrary.
• Thresholds are in multiplied form $\alpha_iz(e_i)\le w\beta(\nu_\ell-\nu_{\ell-1})$; no division by a weight that may be $0$.
• Infrastructure. Lemma 3.3 is shared with the first mission and needs LP duality and randomized rounding. Buchbinder–Naor's theorem, or any $O(\log n)$-competitive online fractional covering algorithm, is needed for the goal. Proofs of any milestone are welcome.

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

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.00163
• N. Buchbinder, J. Naor, Online primal-dual algorithms for covering and packing, Mathematics of Operations Research 34(2), 2009. https://doi.org/10.1287/moor.1080.0363
• 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
• U. Feige, K. Jain, M. Mahdian, V. Mirrokni, Robust combinatorial optimization with exponential scenarios, IPCO 2007, LNCS 4513.
• 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

Motivation

Two-stage adjustable robust optimization models decisions taken in two steps around an uncertain demand: a first-stage decision is fixed now, the demand is revealed, and a second-stage (recourse) decision reacts to it. The objective is the worst-case total cost over a set of possible demands. The model covers set cover, capacity planning and network design under uncertain demand (Bertsimas, Goyal 2012; Gupta, Nagarajan, Ravi 2014). Computing the optimal adjustable solution is intractable in general: Feige, Jain, Mahdian and Mirrokni (2007) showed that, for the budget of uncertainty sets below, the problem cannot be approximated within a factor better than $\Omega(\log n/\log\log n)$ under a standard complexity assumption, where $n$ is the number of decision variables.

Affine policies, in which the recourse is restricted to an affine function of the revealed demand (Ben-Tal et al. 2004), are computable by a single linear program and perform well empirically. The question is how much they can lose in the worst case.

Timeline. Bertsimas and Goyal (2012) proved that affine policies are within $O(\sqrt m)$ of the adjustable optimum for general uncertainty sets ($m$ = number of uncertain parameters) and that this is tight for some sets. El Housni and Goyal (arXiv:1807.00163, 2018; Mathematics of Operations Research 2021) proved that for budget of uncertainty sets the factor is $O(\log n/\log\log n)$, matching the hardness bound. That result is the goal of this mission.

Setting

Let $A\in\mathbb R^{m\times n}$, a non-negative recourse matrix $B\in\mathbb R^{m\times n}_+$, costs $c,d\in\mathbb R^n_+$ and a polyhedral set $\mathcal X\subseteq\mathbb R^n$ be given. For an uncertainty set $\mathcal U\subseteq\mathbb R^m$ of right-hand sides, problem (1.1) is

$$z_{AR}(\mathcal U)=\min_{x\in\mathcal X}\ c^Tx+\max_{h\in\mathcal U}\ \min_{y(h)\ge0}\big\{d^Ty(h)\ :\ Ax+By(h)\ge h\big\}.$$

A first-stage $x$ and a recourse rule $y(\cdot)$ form a feasible solution when $x\in\mathcal X$ and $y(h)\ge0$, $Ax+By(h)\ge h$ for every $h\in\mathcal U$. The affine problem (2.1) restricts the rule to $y(h)=Ph+q$ with $P\in\mathbb R^{n\times m}$, $q\in\mathbb R^n$ (still requiring $Ph+q\ge0$ on $\mathcal U$); its value is $z_{Aff}(\mathcal U)\ge z_{AR}(\mathcal U)$.

The budget of uncertainty set (1.2) with weights $w_i\in[0,1]$ is

$$\mathcal U=\Big\{h\in[0,1]^m\ :\ \sum_{i=1}^mw_ih_i\le1\Big\}.$$

The fractional covering value (3.2) of a requirement $h$ is $z(h)=\min_{y\ge0}\{d^Ty: By\ge h\}$, and $z(\mathcal W)=z(\mathbb 1(\mathcal W))$ for $\mathcal W\subseteq[m]$. Throughout, $\log$ is the natural logarithm and $\beta=4\log n/\log\log n$.

Formalization targets

Goal: Theorem 3.1

$$z_{Aff}(\mathcal U)=O\Big(\frac{\log n}{\log\log n}\Big)\cdot z_{AR}(\mathcal U)$$

for every instance with $\mathcal U$ a budget of uncertainty set: there are $C>0$ and $N$ such that $z_{Aff}\le C\frac{\log n}{\log\log n}z_{AR}$ for all $n\ge N$, all $m$ and all data. The constant is left unfixed, so the goal survives any improvement of the constant.

Milestones (the paper's proof, in order)

1. Lemma 3.1 — the explicit affine solution (3.5), a linear part $y_{Lin}(h)=\sum_{i\in\mathcal I}\alpha_ih_iv_i$ plus a static part from (3.4), is feasible.
2. Lemma 3.2 — the linear part costs at most $\beta\cdot\mathrm{OPT}$ for every $h\in\mathcal U$.
3. Lemmas B.1, B.2 — two Chernoff bounds for weighted sums of independent Bernoulli variables.
4. Claims 3.1–3.3 — rescaling of the covering problem, and two probability bounds for a randomized rounding of a dual (packing) solution.
5. Lemma 3.3 (structural result) — if covering each single row $i\in\mathcal J$ costs more than $4\gamma\frac{\log n}{\log\log n}w_i$, while every scenario $\mathcal W\subseteq\mathcal J$ with $\sum_{\mathcal W}w_i\le1$ costs at most $\gamma$, then $z(\mathcal J)\le4\gamma\frac{\log n}{\log\log n}$.
6. Lemma 3.4 — the static part costs $O(\beta)\cdot\mathrm{OPT}$.

Significance

The result. The bound shows that affine policies are an optimal approximation for this class, up to a constant factor: no polynomial-time algorithm can beat them by more than a constant in the worst case (under the hardness assumption). It improves the earlier $O(\sqrt m)$ bound for budget sets exponentially, and it is the base case from which the paper derives bounds for intersections of budget constraints (Sections 4–5). Lemma 3.3 is a statement about fractional covering problems alone; it generalizes a set-cover result of Gupta, Nagarajan and Ravi (2014) to arbitrary non-negative matrices and weights, and improves its bound from $O(\log n)$ to $O(\log n/\log\log n)$.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of the structural lemma is known. A formal development would also settle the paper's slips: Claim 3.2's $1-O(1/n)$ does not follow from its proof (stated here in the explicit form the proof gives), Lemma B.2's strict inequality fails when $\mu=0$, and Lemma 3.3 needs $n$ large.

Difficulty

Feasibility and the cost of the linear part follow directly from the construction. The difficulty is the static part, that is, Lemma 3.3. The obvious argument covers $\mathcal J$ by a union of cheap scenarios, and it fails: each scenario covers rows of total weight at most $1$, there can be many disjoint scenarios, and adding up their costs gives a bound proportional to $\sum_{i\in\mathcal J}w_i$, which may be as large as $m$. The lemma asserts a bound that depends on $n$ alone, at the rate $\log n/\log\log n$ of the hardness result. Any argument therefore has to exploit condition 1 (every single row is expensive) together with condition 2 across all $2^{|\mathcal J|}$ scenarios at once. As printed, the lemma holds only for $n$ large; for $n=2$ it is false.

Formalization scope

• Data. Vectors are functions on Fin m, Fin n with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ; Lean index $i$ is the paper's $i+1$. First stage and recourse share the same dimension $n$, as on p. 1.
• Values. $z_{AR}$, $z_{Aff}$, $z(h)$ and the static value $z_{Sta}$ are infima in the extended reals, $+\infty$ when infeasible. The recourse is a function of $h$, which gives the same value as the paper's inner minimum. A formalization with real infima (equal to $0$ on infeasible problems) or without $Ph+q\ge0$ would trivialize the goal and is excluded.
• Standing assumptions of p. 1: $B\ge0$, $c,d\ge0$, $\mathcal X$ polyhedral, $w_i\in[0,1]$. The assumption "$\mathcal U\subseteq[0,1]^m$ compact convex with $e_i\in\mathcal U$" holds for the budget set and is not added.
• Added hypotheses and corrections. (i) $c^Tx\ge0$ for $x\in\mathcal X$: Theorem 3.1 is false without it, and it holds whenever $\mathcal X\subseteq\mathbb R^n_+$. (ii) $n\ge3$ where $\beta>0$ is needed, and a threshold $N_0$ in Lemma 3.3. (iii) Lemma B.2 in non-strict form. (iv) Claim 3.2 with the explicit bound $1-n\,e^\delta/(1+\delta)^{1+\delta}$, $\delta=\eta/2-2$. (v) Covering solutions $v_i$ are required only for $i\in\mathcal I$.
• Quantifiers. In the goal and in Lemmas 3.3, 3.4 the constants $C$, $N$, $N_0$ are chosen before $m$ and the instance; a constant allowed to depend on the instance would make the goal trivial.
• Randomness is finite: independent Bernoulli selection with probabilities and expectations as finite sums, reusing the published definition SpectralSparsify.Sampling.BernoulliSubset. No measure theory is needed.
• Infrastructure. LP strong duality (LinearOptimization.lp_strong_duality, proved on the platform) is a tool for Lemma 3.3. The Chernoff bounds and the structural lemma are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3.3, are welcome.

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

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.00163
• 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
• U. Feige, K. Jain, M. Mahdian, V. Mirrokni, Robust combinatorial optimization with exponential scenarios, IPCO 2007, LNCS 4513 (cited as [19] in the source).
• A. Gupta, V. Nagarajan, R. Ravi, Thresholded covering algorithms for robust and max–min optimization, Mathematical Programming 146(1–2), 2014 (cited as [21] in the source).
• 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
• P. Raghavan, Probabilistic construction of deterministic algorithms: approximating packing integer programs, FOCS 1986 (cited as [26] in the source).

Motivation

Designing a revenue-maximizing auction for several items is hard once buyers have budgets. Myerson's optimal auction (Myerson 1981) solves the single-item problem without budgets, under a known prior on the buyers' values. With several items, correlated values or budget constraints, no comparable characterization is known, and the Bayesian formulation requires a prior the seller rarely has.

Bandi and Bertsimas (2014) replace the prior by an uncertainty set: a set $\mathcal U$ of valuation matrices that the seller considers possible. The seller then maximizes worst-case revenue over $\mathcal U$, subject to incentive compatibility, budget feasibility and individual rationality. This is the approach of robust optimization (Ben-Tal and Nemirovski 1998; Bertsimas and Sim 2004) applied to mechanism design. The paper's central object is a mechanism built from linear optimization problems, the robust optimal mechanism ROM. It looks like a Vickrey–Clarke–Groves mechanism with reservation prices that depend on both the buyer and the item.

Setting

There are $n$ buyers $\mathcal N=\{1,\dots,n\}$ and $m$ divisible items $\mathcal M=\{1,\dots,m\}$. A valuation vector is an $n\times m$ real matrix $\mathbf v=(v_{ij})$, with $v_{ij}$ buyer $i$'s value for one unit of item $j$. The uncertainty set $\mathcal U$ is a set of such matrices, and $B_1,\dots,B_n$ are public budgets. Writing $(\mathbf u_i,\mathbf v_{-i})$ for $\mathbf v$ with row $i$ replaced by $\mathbf u_i$, a mechanism assigns to each bid vector $\mathbf v\in\mathcal U$ an allocation $x^{\mathbf v}\ge 0$ and payments $p^{\mathbf v}$. It is feasible for the robust auction LP (5) if, for all $\mathbf v\in\mathcal U$ and $i\in\mathcal N$:

• (7) $\sum_i x^{\mathbf v}_{ij}\le 1$ for every item $j$;
• (8) $\sum_j v_{ij}x^{(\mathbf u_i,\mathbf v_{-i})}_{ij}-p^{(\mathbf u_i,\mathbf v_{-i})}_i\le\sum_j v_{ij}x^{\mathbf v}_{ij}-p^{\mathbf v}_i$ whenever $(\mathbf u_i,\mathbf v_{-i})\in\mathcal U$ (incentive compatibility);
• (9) $p^{\mathbf v}_i\le B_i$ (budget feasibility);
• (10) $p^{\mathbf v}_i\le\sum_j v_{ij}x^{\mathbf v}_{ij}$ (individual rationality).

ROM has two stages. ROM.a runs before any bid. It picks a valuation $\mathbf z\in\mathcal U$ and a nominal allocation $\mathbf x^*$ solving the robust optimization problem (12). For each buyer it picks a minimizer $\tilde{\mathbf u}^i\in\mathcal U$ of $\sum_j x^*_{ij}u_{ij}$ (14), and an optimal solution $(\xi^*,\eta^*,\theta^*)$ of a linear program (13). It then sets reservation prices $r^*_{ij}=\xi^*_j+\eta^*_iz_{ij}+\theta^*_iz_{ij}$ (15). ROM.b runs on the bids $\mathbf v$:

• it maximizes $\sum_{i,j}y_{ij}(v_{ij}-r^*_{ij})$ over a polyhedron $\mathcal P$ (16), (18), and for each buyer $k$ the same objective without buyer $k$ over a polyhedron $\mathcal Q_k$ (17), (19);
• it allocates $a^{\mathbf v}=\mathbf x^*+\mathbf y^{\mathbf v}$ (20) and charges VCG-type payments $p^{\mathbf v}$ (21).

The Lean development uses the same names: ROMData for the chosen optimizers, IsROMa, IsROM, rStar, PSet, QSet, alloc, pay, and IsFeasibleMechanism for (7)–(10).

Formalization targets

Goal: ROM is feasible for (5)

For every uncertainty set of nonnegative valuation matrices, every nonnegative budget vector and every choice of optimal solutions of (12), (13), (14), (16), (17):

$$(a,p)\ \text{satisfies (7)},\ a\ge 0,\ \text{(8)},\ \text{(9)},\ \text{(10) on } \mathcal U.$$

This is the feasibility half of the paper's Theorem 1; its proof (p. 1025) says "the feasibility follows from Propositions 3–5".

Milestones

• Proposition 2 (p. 1020): the relations (22)–(27) among $\mathbf z,\mathbf x^*,\xi^*,\eta^*,\theta^*,r^*$, among them $x^*_{ij}r^*_{ij}=x^*_{ij}z_{ij}$ and $\sum_jx^*_{ij}r^*_{ij}\le B_i$.
• Proposition 3 (p. 1021): ROM satisfies (8).
• Proposition 4 (p. 1022): ROM satisfies (9).
• Proposition 5 (p. 1023): ROM satisfies (10).

Significance

The result shows that a mechanism specified by the paper's optimization problems is incentive compatible, budget feasible and individually rational over an arbitrary uncertainty set. No distributional assumption is made, and multiple items and budgets are allowed. Proposition 2 also records the identity between the total reserved revenue and the optimal value of the auxiliary program (13).

Status. The paper's main claim, Theorem 1, says that ROM is optimal for (5), i.e. that it maximizes worst-case revenue. That claim is false as printed, and so is Proposition 6 (the worst case of ROM is attained at $\mathbf z$). Small counterexamples refute both:

• with one buyer, one item, $\mathcal U=\{1,2\}$ and a large budget, some choice of optimal dual solution in (13) makes ROM's worst-case revenue $0$, while a posted price of $1$ earns $1$;
• with two buyers, one item and $\mathcal U=\{(1,2),(2,1)\}$, full surplus extraction earns $2$, while ROM earns at most $1$ for every choice of optimizers.

The feasibility half is true, and this mission formalizes exactly that half. No result of this paper is on Prove2Me yet, and no machine-checked proof of it is known.

Difficulty

The difficulty lies in the definitions and in how many problems interlock, not in any single deep step. ROM is defined through five optimization problems, none with a unique solution. The payments (21) of a buyer depend on the optimizer chosen in (17), which may differ between a truthful and a deviating bid vector. Incentive compatibility must therefore rest on properties of optimal values, not of particular optimizers. The robust constraints of (12) and (18) range over the whole of $\mathcal U$, which may be infinite. Relating $\mathbf x^*$ to the multipliers of (13) requires replacing the robust constraint by a finite one before linear programming duality applies. Budget feasibility requires comparing two polyhedra whose budget rows differ by a term involving $\theta^*$ and $\tilde{\mathbf u}^i$. Neighbouring statements in the same section (Theorem 1, Proposition 6) are false, so no step can be taken on the paper's word.

Formalization scope

Buyers are Fin n and items Fin m. A valuation matrix is Fin n → Fin m → ℝ, the uncertainty set an arbitrary Set of them, and $(\mathbf u_i,\mathbf v_{-i})$ is Function.update v i u_i. Every optimizer is a field of ROMData. IsROMa/IsROM assert optimality for exactly the page's problems, built from the same $\mathbf z$, $\mathbf x^*$, $\theta^*$, $\tilde{\mathbf u}^i$. Every statement holds for every such choice, never for one canonical selection. Allocation and payments are $0$ for bids outside $\mathcal U$ (step 1 of ROM.b); constraints (7)–(10) are imposed only on $\mathcal U$.

Committed conventions and additions to the page:

• Nonnegative valuations ($u_{ij}\ge 0$ for $\mathbf u\in\mathcal U$) and nonnegative budgets are standing assumptions the paper uses without stating. The proof of Proposition 5 invokes "$\tilde u_{kj}$ ... nonnegative", and (12) is infeasible for negative budgets. Both are explicit hypotheses.
• No finiteness, boundedness or convexity of $\mathcal U$ is assumed. Existence of the optimizers is part of the hypothesis IsROM, and its satisfiability has been checked on a one-buyer, one-item instance.
• Payments may be negative; no $p\ge 0$ is imposed, as (5) has none.
• In $\mathcal Q_k$ row $k$ is only nonnegative; it enters neither constraint nor objective.
• Printed slip corrected: in (18) the term $\sum_jx^*_{kj}\theta^*_i\tilde u^i_j$ has an unbound $k$ and is read as $\sum_jx^*_{ij}\theta^*_i\tilde u^i_j$, matching (13) and (34).
• The paper's optimality claims (Theorem 1, Proposition 6), the objective (5)–(6) and the dual (11) are deliberately not part of the mission.

A trivializing formalization is ruled out: the optimizers are not fixed to degenerate values (such as $\theta^*=0$ or a canonical $\mathbf y$), constraint (8) ranges over all deviations that stay in $\mathcal U$ with the true values multiplying both allocations, and the hypotheses are jointly satisfiable.

A complete development needs finite-dimensional LP duality and complementary slackness (for Proposition 2), and finite-sum manipulation over Fin n with one index removed. LP duality lemmas in matrix form are reusable well beyond this mission. Contributions are welcome on any milestone, and on general LP duality statements stated in a form that applies directly to (33)–(34).

Selected references

• S. Bandi, D. Bertsimas, Optimal Design for Multi-Item Auctions: A Robust Optimization Approach, Mathematics of Operations Research 39(4):1012–1038, 2014. https://doi.org/10.1287/moor.2014.0645
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1):58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• A. Ben-Tal, A. Nemirovski, Robust Convex Optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1):35–53, 2004. https://doi.org/10.1287/opre.1030.0065

Motivation

Many nonconvex optimization problems in binary variables have a polynomial objective or polynomial constraints. The standard way to bring them into the reach of linear and mixed-integer programming solvers is to introduce one new variable per monomial and to study the convex hull of the resulting set of feasible 0/1 vectors, the multilinear polytope. Strong linear descriptions of this polytope translate directly into tighter relaxations in global solvers such as BARON, which is where the inequalities of this mission were tested (Del Pia and Khajavirad 2021, §2.5).

The multilinear polytope of a general hypergraph has no compact description, so the question is for which hypergraphs a given family of inequalities is enough. The quadratic case is classical: the Boolean quadric polytope of a graph (Padberg 1989) is described by its standard linearization exactly when the graph is a forest, and the odd-cycle inequalities are the first facets that appear on a cycle. For higher-degree monomials, Del Pia and Khajavirad showed in 2018 that their flower relaxation is exact if and only if the hypergraph is γ-acyclic. The 2021 paper introduces the stronger running intersection relaxation and asks the same question for it. This mission formalizes the necessary condition the paper proves: the relaxation cannot be exact unless the hypergraph is β-acyclic.

Setting

A hypergraph $G=(V,E)$ is a finite node set $V$ with a set $E$ of subsets of $V$ of size at least two (no loops, no parallel edges). Its multilinear set is

$$\mathcal S_G=\Big\{z\in\{0,1\}^{V+E}: z_e=\prod_{v\in e}z_v\ \ \forall e\in E\Big\},$$

and the multilinear polytope is $\mathrm{MP}_G=\operatorname{conv}\mathcal S_G$. The standard linearization is

$$\mathrm{MP}^{\mathrm{LP}}_G=\Big\{z: z_v\le 1\ \forall v;\ z_e\ge 0,\ z_e\ge\sum_{v\in e}z_v-|e|+1\ \forall e;\ z_e\le z_v\ \forall e,\ v\in e\Big\}.$$

An ordering $p_1,\dots,p_m$ of a multiset of sets is a running intersection ordering if each $p_k$, $k\ge2$, meets the union of its predecessors inside a single predecessor $p_j$; it induces $N(p_1)=\emptyset$ and $N(p_k)=p_k\cap\bigcup_{i<k}p_i$. A running intersection inequality has a center $e_0\in E$, neighbors $e_k$ ($k\in K$) meeting $e_0$ such that $\tilde E=\{e_0\cap e_k\}$ admits a running intersection ordering, and nodes $u_k\in N(e_0\cap e_k)$ when these sets are nonempty:

$$-\sum_{k:\,N(e_0\cap e_k)\ne\emptyset}z_{u_k}+\sum_{v\in e_0\setminus\bigcup_k e_k}z_v+\sum_{k\in K}z_{e_k}-z_{e_0}\le\omega-1,$$

with $\omega$ the number of connected components of $(e_0,\tilde E)$. The running intersection relaxation $\mathrm{MP}^{\mathrm{RI}}_G$ is $\mathrm{MP}^{\mathrm{LP}}_G$ together with all these inequalities.

A β-cycle of length $t\ge3$ is a sequence $v_1,e_1,\dots,v_t,e_t,v_1$ of distinct nodes and distinct edges in which each $v_i$ lies in $e_{i-1}$ and $e_i$ and in no other $e_j$; $G$ is β-acyclic if it has none. For $W\subseteq V$ the subhypergraph $G_W$ has node set $W$ and edges $\{e\cap W: |e\cap W|\ge2\}$.

Formalization targets

Goal: Proposition 5

$$G\ \text{not β-acyclic}\ \Longrightarrow\ \mathrm{MP}_G\subsetneq\mathrm{MP}^{\mathrm{RI}}_G .$$

The milestones follow the paper's proof, in order:

1. $\mathrm{MP}_G\subseteq\mathrm{MP}^{\mathrm{LP}}_G$ (p. 1014) and validity of every running intersection inequality (Proposition 1), giving $\mathrm{MP}_G\subseteq\mathrm{MP}^{\mathrm{RI}}_G$.
2. Lemma 3: β-cycles of $G_{V'}$ lift to β-cycles of $G$ of the same length.
3. Lemma 5: $\mathrm{MP}_{G_{\bar V}}=\mathrm{proj}_{G_{\bar V}}(\mathrm{MP}_G\cap L_{\bar V})$, with $L_{\bar V}=\{z: z_v=1\ \forall v\notin\bar V\}$.
4. Lemma 6: $\mathrm{MP}^{\mathrm{RI}}_{G_{\bar V}}\subseteq\mathrm{proj}_{G_{\bar V}}(\mathrm{MP}^{\mathrm{RI}}_G\cap L_{\bar V})$.
5. The reduction: strictness for $G_W$ implies strictness for $G$.
6. For a shortest β-cycle $C$, $G_{V(C)}$ is a chordless cycle, possibly enclosed by the edge $V(C)$.
7. Strictness for a chordless cycle.
8. Strictness for a chordless cycle enclosed by the edge $V(C)$.

Significance

The result is one half of the paper's picture of when the running intersection relaxation is exact. Proposition 5 shows β-acyclicity is necessary; Theorem 3 of the paper shows that kite-free β-acyclicity is sufficient; Example 2 shows β-acyclicity alone is not. Combined with the 2018 characterization of the flower relaxation by γ-acyclicity, it places the running intersection relaxation strictly between two acyclicity notions and tells a solver designer that on hypergraphs with β-cycles some other family of cuts (for instance odd-cycle-type inequalities lifted from Padberg's) is unavoidable.

The intermediate results are reusable on their own. Lemma 5 is a general statement that multilinear polytopes of induced subhypergraphs are projections of faces, and Lemma 3 with the shortest-cycle structure step is pure hypergraph combinatorics.

The result is proved in the paper. No part of it, nor the multilinear polytope, nor the Boolean quadric polytope, is formalized in Lean or Mathlib as far as a search of the platform showed. Lemma 6 is stated in the paper without proof, and the two strictness cases are justified there by "it can be checked" and by a citation of Padberg; a formal proof closes these gaps.

Difficulty

The obvious argument exhibits a point of $\mathrm{MP}^{\mathrm{RI}}_G\setminus\mathrm{MP}_G$ directly from a β-cycle of $G$. This fails because a β-cycle of $G$ is surrounded by arbitrary other edges, which contribute running intersection inequalities that can cut off any candidate point. The paper's route is to pass to the subhypergraph induced by the cycle's nodes, and that step requires two facts with real content: the projection lemmas (Lemma 6 is an inclusion between relaxations defined by different families of inequalities), and the structure of $G_{V(C)}$, which holds only for a shortest β-cycle. A long β-cycle can have chords in $G_{V(C)}$.

Strictness on the two small families requires a point, or an inequality, separating $\mathrm{MP}$ from $\mathrm{MP}^{\mathrm{RI}}$. That means controlling every running intersection inequality of the cycle, over all centers, neighbor sets, orderings and choices of $u_k$, and also checking that the separating inequality is valid for $\mathrm{MP}$.

Formalization scope

Lean conventions:

• Nodes are elements of a finite type α with decidable equality. Hypergraphs carry their node set and their edge set as Finsets, with every edge of size at least two.
• Points of $\mathbb R^{V+E}$ are functions α ⊕ Finset α → ℝ, and every polytope of $G$ is pinned to zero off $G$'s own coordinates, so polytopes of different hypergraphs, and the projection $\mathrm{proj}_{G_{\bar V}}$, live in one space.
• $\mathrm{MP}^{\mathrm{LP}}_G$ is exactly (8), with no row $z_v\ge0$.
• $\mathrm{MP}^{\mathrm{RI}}_G$ quantifies over all centers, all sets of distinct neighbors other than $e_0$, all running intersection orderings and all choices of $u_k$.
• $\omega$ is the number of connected components of the 2-section graph on $e_0$.
• Orderings and cycles are 0-indexed.
• The projection takes the choice $e'(f)$ of an edge of $G$ with trace $f$ as an argument, and Lemmas 5 and 6 hold for every choice.
• The strict inclusion $\subset$ of the paper is Lean's ⊂ ($\subseteq$ and $\ne$).

There is one disclosed addition. Lemma 6 and the reduction step assume that $G_{\bar V}$ has no isolated node. Without it both statements are false: since (8) has no lower bound on $z_v$, a node isolated in $G_{\bar V}$ is unbounded below in $\mathrm{MP}^{\mathrm{RI}}_{G_{\bar V}}$. The paper uses them only for $\bar V=V(C)$, where the hypothesis holds. The goal itself carries no added hypothesis.

A trivializing formalization is ruled out. A relaxation missing some running intersection inequalities (a fixed ordering, a fixed $u_k$, a fixed neighbor set) would make strictness easier, and an empty or mis-pinned relaxation would make the inclusion false. The definitions here take the full family.

A complete development needs:

• convex hulls of finite point sets and separation of a point from them;
• connected components of the 2-section graph;
• running intersection orderings;
• the combinatorics of β-cycles.

The β-cycle and subhypergraph material and Lemma 5 are reusable beyond this mission. Contributions are welcome on any milestone, on alternative proofs of the two strictness cases (for instance by an explicit fractional point), and on a proof of Lemma 6.

Selected references

• A. Del Pia and A. Khajavirad, The running intersection relaxation of the multilinear polytope, Mathematics of Operations Research 46(3):1008–1037, 2021. https://doi.org/10.1287/moor.2021.1121
• A. Del Pia and A. Khajavirad, A polyhedral study of binary polynomial programs, Mathematics of Operations Research 42(2):389–410, 2017. https://doi.org/10.1287/moor.2016.0804
• A. Del Pia and A. Khajavirad, The multilinear polytope for acyclic hypergraphs, SIAM Journal on Optimization 28(2):1049–1076, 2018. https://doi.org/10.1137/16M1095998
• M. Padberg, The Boolean quadric polytope: some characteristics, facets and relatives, Mathematical Programming 45:139–172, 1989. https://doi.org/10.1007/BF01589101
• C. Beeri, R. Fagin, D. Maier and M. Yannakakis, On the desirability of acyclic database schemes, Journal of the ACM 30(3):479–513, 1983. https://doi.org/10.1145/2402.322389

Motivation

Binary polynomial optimization asks to minimize a polynomial over $\{0,1\}^n$. The standard way to attack it with linear programming is to introduce one variable $z_e$ for every monomial $\prod_{v\in e} z_v$ and to work with the convex hull of the resulting set of binary points. This convex hull, the multilinear polytope, is the object behind the cutting planes that global solvers such as BARON add at every node of a branch-and-bound tree, and in general its facets are as hard to describe as the original problem is to solve. The useful theory is therefore structural: which hypergraphs of monomials give multilinear polytopes with an explicit, combinatorial description.

A line of work by Del Pia and Khajavirad answers this for increasingly general classes of acyclic hypergraphs: Berge-acyclic and γ-acyclic hypergraphs via flower inequalities (SIAM J. Optim. 2018), sufficient conditions for decomposing multilinear sets (Math. Program. 2018), and, in the paper this mission formalizes (Math. Oper. Res. 2021), the running intersection inequalities, a generalization of flower inequalities that does not need γ-acyclicity. The paper reports that adding these cuts reduces BARON's root-node relaxation gap by more than 95% on most of 35 computer-vision instances.

Setting

A hypergraph $G=(V,E)$ has a finite node set $V$ and a set $E$ of subsets of $V$, each with at least two nodes. Points live in $\mathbb R^{V+E}$, one coordinate per node and per edge. The multilinear set and multilinear polytope are

$$\mathcal S_G=\Big\{z\in\{0,1\}^{V+E}: z_e=\prod_{v\in e}z_v\ \forall e\in E\Big\},\qquad \mathrm{MP}_G=\operatorname{conv}\mathcal S_G .$$

The standard linearization $\mathrm{MP}^{\mathrm{LP}}_G$ replaces each equation $z_e=\prod_{v\in e}z_v$ by its convex hull over the unit cube: $z_v\le 1$, $z_e\ge 0$, $z_e\ge\sum_{v\in e}z_v-|e|+1$ and $z_e\le z_v$ for $v\in e$.

An ordering $p_1,\dots,p_m$ of a family of sets is a running intersection ordering if each $p_k$ meets the union of its predecessors inside a single predecessor $p_j$; write $N(p_k)=p_k\cap\bigcup_{i<k}p_i$ and $N(p_1)=\emptyset$. Given a center edge $e_0$ and neighbor edges $e_k$, $k\in K$, meeting $e_0$ such that the sets $e_0\cap e_k$ admit a running intersection ordering, and nodes $u_k\in N(e_0\cap e_k)$ wherever this set is nonempty, the running intersection inequality is

$$-\sum_{k:\,N(e_0\cap e_k)\neq\emptyset}z_{u_k}+\sum_{v\in e_0\setminus\bigcup_k e_k}z_v+\sum_{k\in K}z_{e_k}-z_{e_0}\le\omega-1,$$

with $\omega$ the number of connected components of the hypergraph on $e_0$ with edges $e_0\cap e_k$. The running intersection relaxation $\mathrm{MP}^{\mathrm{RI}}_G$ is $\mathrm{MP}^{\mathrm{LP}}_G$ together with all these inequalities.

A β-cycle is a cyclic sequence of $t\ge 3$ distinct nodes and distinct edges $v_1,e_1,\dots,v_t,e_t$ in which $v_i$ lies in $e_{i-1}$ and $e_i$ and in no other edge of the cycle; $G$ is β-acyclic if it has none. A kite is three edges $e_0,e_1,e_2$ with $|e_0\cap e_1\cap e_2|\ge 2$, $(e_0\cap e_1)\setminus e_2\ne\emptyset$ and $(e_0\cap e_2)\setminus e_1\ne\emptyset$; $G$ is kite-free if it has none. $G$ is two-laminar if any two distinct edges sharing at least two nodes are strictly nested.

Formalization targets

Goal: Theorem 3 (p. 1023)

For every kite-free β-acyclic hypergraph $G$ without isolated nodes,

$$\mathrm{MP}_G=\mathrm{MP}^{\mathrm{RI}}_G .$$

Milestones

In attack order: validity of the inequalities (Proposition 1); heredity of β-acyclicity (Lemma 3); kite-free implies edge-induced subhypergraphs are two-laminar (Lemma 7); β-acyclicity as the running intersection property of every edge subset (Lemma 4); the explicit facet description of $\mathrm{MP}_G$ for two-laminar β-acyclic $G$ by system (20) (Proposition 6) and its consequence $\mathrm{MP}_G=\mathrm{MP}^{\mathrm{RI}}_G$ there (Corollary 3); the decomposition theorem for multilinear sets (Theorem 1); and five steps of the inductive proof of Theorem 3 in §5.3: $G_\omega$ is kite-free β-acyclic with one maximal edge fewer, the inductive step $\mathrm{MP}_{G^+}=\mathrm{MP}^{\mathrm{RI}}_{G^+}$, Claim 14 on partial hypergraphs, the projection $\mathrm{MP}_G=\mathrm{proj}\,\mathrm{MP}_{G^+}$, and the Fourier–Motzkin step $\mathrm{MP}^{\mathrm{RI}}_G\subseteq\mathrm{proj}\,\mathrm{MP}^{\mathrm{RI}}_{G^+}$.

Companions

Theorem 2 (p. 1022), the polynomial-size extended formulation $\mathrm{MP}_{G^+}=\bigcap_{i}\mathrm{MP}_{G^+_i}$ over the maximal edges, and the form (19) taken by running intersection inequalities in kite-free β-acyclic hypergraphs.

Significance

Theorem 3 gives a description of the multilinear polytope in the original space, by inequalities defined combinatorially from the hypergraph, for a class that strictly contains the γ-acyclic hypergraphs covered by flower inequalities. With Theorem 2 it implies that linear optimization and separation over $\mathrm{MP}_G$ are polynomial for kite-free β-acyclic hypergraphs, and that separation can be done without the ellipsoid method. The paper also shows (Proposition 5, a separate mission of this series) that β-acyclicity is necessary for $\mathrm{MP}_G=\mathrm{MP}^{\mathrm{RI}}_G$, so the characterization sits close to the boundary of what such relaxations can achieve.

All results of this mission are proved in the paper; none is machine-checked. A complete development would be the first formal treatment of hypergraph acyclicity degrees and of multilinear polytopes, and would include a formal Fourier–Motzkin elimination argument on a structured polytope.

Difficulty

The inclusion $\mathrm{MP}_G\subseteq\mathrm{MP}^{\mathrm{RI}}_G$ is a validity check. The reverse inclusion is the content. A direct argument through integrality fails: for two-laminar β-acyclic hypergraphs, facets have general integer coefficients, so total unimodularity and balancedness arguments used for laminar hypergraphs do not apply. The decomposition step is also harder than in earlier work: the shared part of the two pieces may be an edge whose nodes are only partly covered by edges of one side, so a point cannot be written by pairing one vertex of each side. Finally, the induction lifts to $G^+$, which has an extra variable, and the projection back must be shown to produce only running intersection inequalities, which requires recognizing every Fourier–Motzkin combination as one.

Formalization scope

Nodes form a type α with Fintype and DecidableEq; a point is a function z : α ⊕ Finset α → ℝ, and every polytope of a hypergraph vanishes off that hypergraph's coordinates, so that polytopes of different hypergraphs, lifts and projections are literal sets in one space. Hypergraphs have no loops or parallel edges, as the paper assumes. Orderings are lists, 0-based. The relaxation quantifies over every center, every neighbor set, every running intersection ordering and every choice of the nodes $u_k$; the number of components counts isolated nodes and ignores loops. The standard linearization has no row $z_v\ge 0$, exactly as printed.

One hypothesis is added to the paper: no isolated nodes, on Theorem 3, Corollary 3, Theorem 2 and the inductive step. It is necessary: for $V=\{a,b,c\}$, $E=\{\{a,b\}\}$ the point with $z_c=-1$ and all other coordinates $0$ lies in $\mathrm{MP}^{\mathrm{RI}}_G$ but not in $\mathrm{MP}_G$. No other result carries it.

A trivializing formalization is ruled out by construction: restricting the relaxation to one fixed ordering or choice of $u_k$ would make the goal false rather than easy, and the goal is an equality of sets, not an inclusion.

A complete development needs: convex hulls of finite sets of 0/1 points, hypergraph connectivity, β-acyclicity and the running intersection property (Lemma 4 is a classical database-theory theorem of Beeri, Fagin, Maier and Yannakakis), and Fourier–Motzkin elimination. The hypergraph acyclicity layer is reusable beyond this mission, including by the two other missions of this series. Proofs of any milestone, and of reusable lemmas on hypergraph acyclicity, are welcome.

Selected references

• A. Del Pia, A. Khajavirad, The running intersection relaxation of the multilinear polytope, Math. Oper. Res. 46(3):1008–1037, 2021. https://doi.org/10.1287/moor.2021.1121
• A. Del Pia, A. Khajavirad, The multilinear polytope for acyclic hypergraphs, SIAM J. Optim. 28(2):1049–1076, 2018. https://doi.org/10.1137/16M1095998
• A. Del Pia, A. Khajavirad, On decomposability of multilinear sets, Math. Program. 170(2):387–415, 2018. https://doi.org/10.1007/s10107-017-1158-y
• C. Beeri, R. Fagin, D. Maier, M. Yannakakis, On the desirability of acyclic database schemes, J. ACM 30(3):479–513, 1983. https://doi.org/10.1145/2402.322389
• R. Fagin, Degrees of acyclicity for hypergraphs and relational database schemes, J. ACM 30(3):514–550, 1983. https://doi.org/10.1145/2402.322390

Motivation

Binary polynomial optimization asks for the maximum of a polynomial over $\{0,1\}^n$. Linearizing each monomial $\prod_{v\in e}z_v$ by a new variable $z_e$ turns the problem into a linear program over the convex hull of a set of 0/1 points, the multilinear polytope of the hypergraph whose edges are the monomials. Global solvers such as BARON build polyhedral relaxations of this polytope at every node of their branch-and-bound trees, so valid inequalities that are as strong as possible, that is, facet-defining, translate directly into smaller root gaps.

Del Pia and Khajavirad introduced running intersection inequalities in The running intersection relaxation of the multilinear polytope (Math. Oper. Res. 46 (2021) 1008–1037, doi:10.1287/moor.2021.1121). They generalize the flower inequalities of the same authors (SIAM J. Optim. 2018), which are facet-defining when the support hypergraph is $\gamma$-acyclic, to support hypergraphs that are not. This mission formalizes the paper's sufficient condition for a running intersection inequality to define a facet (§2.4, Proposition 4) together with the structural results it rests on.

Timeline. Crama (1993) studied the standard linearization; Del Pia and Khajavirad (2017, Math. Oper. Res.) proved that the multilinear polytope is full dimensional and gave lifting theorems for facets; flower inequalities followed in 2018; running intersection inequalities and the facet conditions formalized here appeared in 2021.

Setting

A hypergraph $G=(V,E)$ has a finite node set $V$ and a set $E$ of subsets of $V$ of cardinality at least two. Its multilinear set is

$$\mathcal S_G=\Big\{z\in\{0,1\}^{V+E}:\ z_e=\prod_{v\in e}z_v\ \ \forall e\in E\Big\},$$

and its multilinear polytope is $\mathrm{MP}_G=\operatorname{conv}\mathcal S_G$.

A multiset $F$ of sets has the running intersection property if its elements can be ordered $p_1,\dots,p_m$ so that each $p_k\cap(p_1\cup\dots\cup p_{k-1})$, $k\ge 2$, is contained in a single earlier $p_j$. Such an ordering defines $N(p_1)=\emptyset$ and $N(p_k)=p_k\cap\bigcup_{i<k}p_i$. A leaf of $F$ is an element that comes last in some such ordering.

Fix an edge $e_0$ (the center) and edges $e_k$, $k\in K$, adjacent to $e_0$ (the neighbors), such that the multiset $\tilde E=\{e_0\cap e_k:k\in K\}$ has the running intersection property. Choose an ordering of $\tilde E$, and for each $k$ with $N(e_0\cap e_k)\neq\emptyset$ a node $u_k\in N(e_0\cap e_k)$. The running intersection inequality is

$$-\sum_{k\in K:\,N(e_0\cap e_k)\neq\emptyset} z_{u_k}+\sum_{v\in e_0\setminus\bigcup_{k}e_k} z_v+\sum_{k\in K}z_{e_k}-z_{e_0}\ \le\ \omega-1,$$

where $\omega$ is the number of connected components of the hypergraph $\tilde G=(e_0,\tilde E)$. Its support hypergraph $G$ has node set $e_0\cup\bigcup_k e_k$ and edge set $\{e_0\}\cup\{e_k:k\in K\}$. An inequality defines a facet of $\mathrm{MP}_G$ if it is valid and the face it cuts out is nonempty of dimension $\dim\mathrm{MP}_G-1$.

Formalization targets

Goal: Proposition 4 (p. 1016)

Assume

1. $|e_0\cap e_k|\ge 2$ for every $k\in K$;
2. for every $K'\subseteq K$ with $e_0\cap\bigcap_{k\in K'}e_k\neq\emptyset$: $\ e_0\cap\big(e_i\setminus\bigcup_{k\in K'\setminus\{i\}}e_k\big)\neq\emptyset$ for all $i\in K'$;
3. each nonempty $N(e_0\cap e_k)$ meets $U=\{u_k: N(e_0\cap e_k)\neq\emptyset\}$ in exactly one node.

Then the running intersection inequality defines a facet of $\mathrm{MP}_G$ for its support hypergraph $G$.

Milestones

Lemma 1 (p. 1011, leaves and reorderings), Lemma 2 (p. 1011, components $=n_0+|\{e:N(e)=\emptyset\}|$), Proposition 1 (p. 1012, validity), and the full dimensionality of $\mathrm{MP}_G$ (cited on p. 1016 from [12]):

$$\dim\mathrm{MP}_G=|V|+|E|.$$

Companions

Corollary 2 (p. 1017): $|e_0\cap e_k|\ge 2$ and $|e_0\cap e_k\cap e_{k'}|\le 1$ for $k\neq k'$ suffice. Proposition 2 and Corollary 1 (pp. 1013–1014): the multiset $\{N(e)\}$, hence the system of inequalities, does not depend on the ordering. Proposition 3 (p. 1014): necessary conditions for a facet of the running intersection relaxation $\mathrm{MP}^{\mathrm{RI}}_G$.

Significance

Proposition 4 certifies a large family of facets of multilinear polytopes whose support hypergraphs contain cycles that flower inequalities cannot handle. Together with the lifting theorems of Del Pia and Khajavirad (2017), it yields sufficient conditions under which these inequalities define facets of the multilinear polytope of general hypergraphs (p. 1015); §2.5 of the paper reports that running intersection cuts reduce BARON's root-node relaxation gap on image-restoration instances. Proposition 3 and Example 1 show that condition 1 is necessary while conditions 2–3 are not, so the result is a sufficient condition and not a characterization.

The results are proved in the paper; none is formalized. A Lean development would provide the first machine-checked library for the running intersection property (orderings, leaves, the multiset of $N$-sets), the connected-component count of Lemma 2, and the multilinear polytope as a convex hull with an exact dimension count, all reusable for the companion missions on the tightness of $\mathrm{MP}^{\mathrm{RI}}_G$ for kite-free $\beta$-acyclic hypergraphs and its strictness otherwise.

Difficulty

Validity (Proposition 1) decomposes over the connected components of $\tilde G$; the facet claim does not, because a face of codimension one is a global object and the neighbors of different components, and the nodes $u_k$ shared between neighbors, interact in it. Conditions 2 and 3 are exactly where this interaction is controlled, and Example 1 of the paper shows that dropping condition 3 does not destroy facetness, so no simple equivalence is available to fall back on. Formally, three nontrivial ingredients have no Mathlib counterpart: the combinatorics of running intersection orderings (Lemma 1, Proposition 2), the count of connected components of a hypergraph with loops and parallel edges (Lemma 2), and the affine dimension of a convex hull of 0/1 points in a space indexed by nodes and edges.

Formalization scope

Nodes form a finite type α; every hypergraph's space $\mathbb R^{V+E}$ lives inside α ⊕ Finset α → ℝ, with the coordinates outside $V+E$ pinned to $0$ in the definition of $\mathcal S_G$, so $\dim\mathrm{MP}_G=|V|+|E|$ is meaningful. Orderings are lists indexed from $0$. The number of components is that of the 2-section graph on the node set. An inequality is given by its data: center, a set $K$ of distinct neighbors other than $e_0$, an ordering of $K$ whose traces form a running intersection ordering of $\tilde E$, and the choice $k\mapsto u_k$; the first sum runs over neighbors, so a node chosen for two neighbors has coefficient $-2$. "Defines a facet" requires a nonempty face and compares dimensions as $\dim F+1=\dim P$, so the empty face can never qualify and no truncated subtraction occurs. The facet statement is about $\mathrm{MP}_G$ for the support hypergraph only, not for a larger host hypergraph, which would require the lifting theorems. The reading $k\neq k'$ is used where the page's "for all $k,k'$" would otherwise be contradictory (Corollary 2, Proposition 3(i)); Lemma 2 is stated for lists of nonempty sets, which covers its use on $\tilde G$.

Contributions welcome: proofs of the milestones, a reusable library for the running intersection property and $\alpha$-acyclic hypergraphs, and the full-dimensionality proof.

Selected references

• A. Del Pia, A. Khajavirad, The running intersection relaxation of the multilinear polytope, Math. Oper. Res. 46(3):1008–1037, 2021. https://doi.org/10.1287/moor.2021.1121
• A. Del Pia, A. Khajavirad, A polyhedral study of binary polynomial programs, Math. Oper. Res. 42(2):389–410, 2017. https://doi.org/10.1287/moor.2016.0804
• A. Del Pia, A. Khajavirad, The multilinear polytope for acyclic hypergraphs, SIAM J. Optim. 28(2):1049–1076, 2018. https://doi.org/10.1137/16M1095998
• C. Beeri, R. Fagin, D. Maier, M. Yannakakis, On the desirability of acyclic database schemes, J. ACM 30(3):479–513, 1983. https://doi.org/10.1145/2402.322389
• Y. Crama, Concave extensions for nonlinear 0–1 maximization problems, Math. Programming 61:53–60, 1993. https://doi.org/10.1007/BF01582138

Motivation

Online matching models a platform that must commit resources to requests as they arrive, without knowing the future. In revenue management the resources are items in limited supply and the requests are customers, and the firm also chooses the price. Ma and Simchi-Levi (arXiv:1905.04770, Oper. Res. 2020, DOI 10.1287/opre.2019.1957) give algorithms whose worst-case guarantee depends on the set of prices each item can be sold at, and show that the guarantee is tight.

Timeline of the deterministic (matching) case:

• 1990. Karp, Vazirani and Vazirani introduce RANKING for unweighted online bipartite matching: each item gets a random rank, and each arriving customer takes the best-ranked available neighbour. Its competitive ratio is $1-1/e$, which is optimal.
• 2011. Aggarwal, Goel, Karande and Mehta extend RANKING to vertex-weighted matching, where each item has a single fixed price, with the same ratio $1-1/e$.
• 2013. Devanur, Jain and Kleinberg give a randomized primal–dual proof of these results with continuous seeds $W_i\sim U[0,1]$.
• 2019. Ma and Simchi-Levi allow each item a set of prices. Their Multi-price Ranking ranks items by a price-dependent value function, and it is $\min_iF(\mathcal P_i)$-competitive. $F(\mathcal P)$ depends only on the ratios of the prices; it equals $1-1/e$ for one price and lies in $[1-e^{-1/m},1-1/e]$ for $m$ prices (p. 14).

Setting

A firm sells $n$ items, one unit of each. Item $i$ has a price set $\mathcal P_i=\{r_i^{(1)}<\dots<r_i^{(m_i)}\}$ with $r_i^{(1)}>0$, and $r_i^{(0)}:=0$. Customers $t=1,\dots,T$ arrive one at a time. In the deterministic case, customer $t$ either would or would not buy item $i$ at price $j$: $p^{(j)}_{t,i}\in\{0,1\}$. Let $j_{t,i}$ be the largest $j$ with $p^{(j)}_{t,i}=1$, or $0$ if there is none. Assigning item $i$ to customer $t$ earns $r_i^{(j_{t,i})}$. An online algorithm sees $p_{t}$ only when customer $t$ arrives.

The benchmark is the LP (5): maximize $\sum_{t,i,j}p^{(j)}_{t,i}r_i^{(j)}x^{(j)}_{t,i}$ subject to $\sum_{t,j}p^{(j)}_{t,i}x^{(j)}_{t,i}\le k_i$, $\sum_{i,j}x^{(j)}_{t,i}\le1$ and $x\ge0$, with optimal value $\mathrm{OPT}$. Its dual (19) minimizes $\sum_ik_iy_i+\sum_tz_t$ subject to $p^{(j)}_{t,i}y_i+z_t\ge p^{(j)}_{t,i}r_i^{(j)}$ and $y,z\ge0$. An algorithm is $c$-competitive if $\mathbb E[\mathrm{ALG}]\ge c\cdot\mathrm{OPT}$ for every arrival sequence.

Booking limits. By Proposition 1 there are unique positive $\alpha^{(1)},\dots,\alpha^{(m)}$ that sum to $1$ and satisfy

$$1-e^{-\alpha^{(1)}}=\frac{1-e^{-\alpha^{(j)}}}{1-r^{(j-1)}/r^{(j)}}\quad (j=2,\dots,m).$$

Set $F(\mathcal P)=1-e^{-\alpha^{(1)}}$ and $L^{(j)}=\alpha^{(1)}+\dots+\alpha^{(j)}$. For $w\in[0,1]$ let $\ell(w)$ be the segment containing $w$. The value function is

$$\Phi_{\mathcal P}(w)=r^{(\ell-1)}+\bigl(r^{(\ell)}-r^{(\ell-1)}\bigr)\frac{e^{\,w-L^{(\ell-1)}}-1}{e^{\alpha^{(\ell)}}-1},\qquad \ell=\ell(w).$$

It increases continuously from $0$ to $r^{(m)}$ and equals $r^{(j)}$ at $L^{(j)}$.

Multi-price Ranking (Algorithm 2). Each item draws an independent seed $W_i\sim U[0,1]$. Customer $t$ is assigned an available item maximizing $r_i^{(j_{t,i})}-\Phi_{\mathcal P_i}(W_i)$, provided the maximum is strictly positive. Ties are broken arbitrarily. The analysis uses dual variables: when $i$ is assigned to $t$, $Z_t=r_i^{(j_{t,i})}-\Phi_{\mathcal P_i}(W_i)$ and $Y_i=\Phi'_{\mathcal P_i}(W_i)$; all other dual variables are $0$.

Formalization targets

Goal: Theorem 2 (p. 16)

For every setup in the deterministic case with $k_i=1$, every arrival sequence, every tie-breaking rule and every feasible $x$ of (5),

$$\min_iF(\mathcal P_i)\cdot\sum_{t,i,j}p^{(j)}_{t,i}r_i^{(j)}x^{(j)}_{t,i}\ \le\ \mathbb E_{W}\bigl[\mathrm{ALG}\bigr].$$

Milestones

1. Weak duality for (5)/(19) (p. 19).
2. Lemma 2 (p. 22): if item $i$ is assigned to customer $t$, then $(1-e^{-\alpha_i^{(1)}})(Y_i+Z_t)\le r_i^{(j_{t,i})}$.
3. Dominance claim (App. C, pp. 45–46): let $Z^{\mathrm{crit}}$ be the pseudorevenue at $t$ of the run without item $i$. If $W_i\in[0,W^{\mathrm{crit}})$, then item $i$ is matched by time $t$ in the run with item $i$.
4. Monotonicity claim (App. C, p. 46): $Z_t\ge Z^{\mathrm{crit}}$ for every value of $W_i$.
5. Lemma 3 (p. 22): $y_i=\mathbb E[Y_i]$, $z_t=\mathbb E[Z_t]$ is feasible for (19).

Significance

The theorem shows that one randomized rule achieves the optimal guarantee for every price set, and that the guarantee depends only on the price ratios. For one price, $F=1-1/e$ and the classical vertex-weighted result is recovered. With several prices the benchmark (5) is stronger, because the offline optimum may also choose prices, and the guarantee degrades gracefully: $F(\mathcal P)$ lies in $[1-e^{-1/m},1-1/e]$ and depends only on how far apart the prices are. Theorem 3 of the same paper shows that no online algorithm does better than $F(\mathcal P)$ when every item has price set $\mathcal P$, so the ratio is tight.

The results are proved in the paper, in §4 and App. C. As far as the platform's records show, they have not been formalized. A formalization adds three things on top of the paper. It machine-checks a randomized primal–dual argument whose expectations are integrals over $[0,1]^n$. It makes precise the measure-zero conventions the paper uses: ties in (23), and $\Phi'$ at segment borders. It also gives a Lean model of a ranking algorithm with continuous seeds that sees only the present customer, which could be reused for related online algorithms.

Difficulty

The pointwise part (Lemma 2) is a direct computation from the booking-limit identity (7). The difficulty is Lemma 3. The constraint for a pair $(t,i)$ needs $\mathbb E[Y_i+Z_t]\ge r_i^{(j_{t,i})}$, but on a single sample path $Y_i+Z_t$ can be far below this: item $i$ may be taken by an earlier customer, or customer $t$ may take another item. The bound only holds after conditioning on the other seeds and comparing two coupled runs, one with item $i$ and one without. That comparison needs an invariant that holds at every step: the set of items still available in the run with $i$ contains the set in the run without $i$. The invariant fails when ties are broken differently in the two runs, so the measure-zero set of ties must be handled explicitly. The conditional expectation of $Y_i$ is then an integral of $\Phi'$, which is discontinuous at the segment borders.

Formalization scope

• Indexing. Items are Fin n and customers Fin T, both 0-based. Prices are 1-based within an item, with pr r 0 = 0 for $r^{(0)}=0$. Data at indices outside $[1,m_i]$ are never read.
• Standing assumptions (p. 11), passed as hypotheses: every price set has $m_i\ge1$ and $0<r_i^{(1)}<\dots<r_i^{(m_i)}$; the booking limits are positive, sum to $1$ and satisfy (7) (IsBookingLimits, unique by Proposition 1); $p\in\{0,1\}$ on $[1,m_i]$; $k_i=1$. Weak duality is stated for any $p\in[0,1]$ and any inventories.
• Algorithm. The step at customer $t$ reads only $p_t$, the seeds and the set of available items. Tie-breaking is any rule returning a maximizer of (23), universally quantified. A run can start from a subset of the items, which gives the run "with item $i$ removed".
• Expectations are Lebesgue integrals over the product of $n$ uniform laws on $[0,1]$. No integrability hypothesis is added: the integrands are bounded, and measurable outside the null set of ties.
• Competitive ratio. It is stated multiplied out, for every feasible $x$ of (5), and needs $n\ge1$ for the minimum (with no items both sides are $0$). This rules out the trivializing readings $\mathbb E[\mathrm{ALG}]/\mathrm{OPT}$ with $x/0=0$, and an infimum over arrival sequences. The algorithm is fixed as Algorithm 2; it is not "any algorithm with a property".
• Added or changed hypotheses.
  • Lemma 2 is claimed for every seed vector in $[0,1]^n$, with $\Phi'$ the right derivative at a border. This implies the paper's "w.p.1".
  • The two claims assume no ties, the paper's "we ignore measure-zero events".
  • Dominance is written as $\Phi_{\mathcal P_i}(W_i)<r_i^{(j)}-Z^{\mathrm{crit}}$. This is equivalent to $W_i<W^{\mathrm{crit}}$ because $\Phi$ is a strictly increasing bijection $[0,L_i^{(j)}]\to[0,r_i^{(j)}]$.
• Infrastructure. A solver needs: monotonicity and continuity of $\Phi_{\mathcal P}$ and the integral $\int_0^{w}\Phi'=\Phi(w)$; measurability of the run in $W$; the fact that ties are null under the product of uniform laws; and conditioning via Fubini on $[0,1]^n$. These pieces are reusable for other randomized primal–dual analyses. The paper's proofs are in §4 (p. 23) and App. C (pp. 45–46). Proofs of any milestone, and lemmas on $\Phi_{\mathcal P}$, are welcome.

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
• 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
• G. Aggarwal, G. Goel, C. Karande, A. Mehta, Online vertex-weighted bipartite matching and single-bid budgeted allocations, SODA 2011. https://arxiv.org/abs/1007.1271
• N. R. Devanur, K. Jain, R. D. Kleinberg, Randomized primal-dual analysis of RANKING for online bipartite matching, SODA 2013. https://doi.org/10.1137/1.9781611973105.7