Operations Research

Motivation

In two-echelon distribution goods travel from a central depot to intermediate facilities, called satellites, on large first-level vehicles, and from the satellites to customers on smaller second-level vehicles. City logistics schemes that keep heavy trucks out of urban centres are the standard example. The two-echelon capacitated vehicle routing problem (2E-CVRP) asks for the cheapest set of routes on both levels that serves every customer while respecting vehicle, fleet and satellite capacities.

Exact methods for problems of this kind are branch-and-bound or enumeration schemes whose speed depends on the quality of the lower bounds they use. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) built their exact algorithm on a Lagrangean-type relaxation $RF$ of a set-partitioning formulation $F$, rather than on the LP relaxation $LF$ of that formulation. Their Theorem 2 is the justification for that design choice: the best bound $RF$ can deliver is never weaker than $z(LF)$, and can be strictly stronger. This mission formalizes that comparison.

Setting

An instance has a depot $0$, satellites $N_S$ and customers $N_C$, a symmetric travel cost $d_{uv}$ (in which the fixed vehicle costs $U_1, U_2$ have already been folded into the depot–satellite and satellite–customer entries), positive integer demands $q_i$, capacities $Q_1 > Q_2 > 0$ for first- and second-level vehicles, a bound $m^1$ on first-level vehicles, $m_k$ second-level vehicles at satellite $k$, a global bound $m^2 \le \sum_k m_k$ on second-level vehicles, a capacity $B_k$ and a unit handling cost $H_k$ for each satellite.

A first-level route $r \in \mathcal M$ leaves the depot, visits a set $R_r$ of satellites and returns; its cost $g_r$ is the cost of that closed walk. A second-level route $l \in \mathcal R_k$ leaves satellite $k$, visits a set $R_{kl}$ of customers and returns; its load is $w_{kl} = \sum_{i \in R_{kl}} q_i \le Q_2$, $a_{ikl}$ counts its visits to customer $i$, and its cost $c_{kl}$ is its closed-walk cost plus $H_k w_{kl}$.

Formulation $F$ uses binaries $x_{kl}$ (route $l$ of satellite $k$ is used), binaries $y_r$, and nonnegative integers $q_{kr}$ (quantity route $r$ delivers to satellite $k \in R_r$). It minimizes $\sum c_{kl}x_{kl} + \sum g_r y_r$ subject to: each customer is covered exactly once (2); at most $m_k$ routes at satellite $k$ (3) and $m^2$ overall (4); the load delivered from satellite $k$ is at most $B_k$ (5); at most $m^1$ first-level routes (6); what first-level routes bring to satellite $k$ equals what its second-level routes carry (7); and $\sum_{k \in R_r} q_{kr} \le Q_1 y_r$ (8).

The LP relaxation $LF$ replaces the integrality of $x, y, q$ by $0 \le x, y \le 1$, $q \ge 0$. Its value is $z(LF)$, equal to $+\infty$ when $LF$ is infeasible.

The relaxation $RF(\beta, \lambda, \mu)$ relaxes (2)–(4) with penalties $\lambda \in \mathbb{R}^{N_C}$, $\mu_k \le 0$ and $\mu_0 \le 0$, and replaces the second-level routes by marginal routing costs $\beta_{ik}$ that must satisfy, for every route $l \in \mathcal R_k$,

$$\sum_{i} a_{ikl}\beta_{ik} \le c_{kl} - \sum_i a_{ikl}\lambda_i - \mu_k - \mu_0. \tag{12}$$

Its variables are binaries $\xi_{ik}$ (customer $i$ is supplied from satellite $k$), $y_r$ and $q_{kr}$; it minimizes

$$\sum_{k,i}\beta_{ik}\xi_{ik} + \sum_r g_r y_r + \sum_i \lambda_i + \sum_k m_k\mu_k + m^2\mu_0$$

subject to single assignment of each customer, flow balance $\sum_{r \in \mathcal M_k} q_{kr} = \sum_i q_i\xi_{ik}$, satellite capacity $\sum_i q_i \xi_{ik} \le B_k$, and (6), (8). A choice $(\beta,\lambda,\mu,\mu_0)$ with $\mu, \mu_0 \le 0$ and (12) is admissible.

Formalization targets

Goal: Theorem 2

$$\max_{\beta,\lambda,\mu}\, z(RF(\beta,\lambda,\mu)) \ \ge\ z(LF), \quad\text{and the inequality can be strict.}$$

Formally: (1) for every instance and route families whose $LF$ is feasible, some admissible $(\beta,\lambda,\mu,\mu_0)$ satisfies $z(LF) \le z(RF(\beta,\lambda,\mu))$; (2) some instance, route families and admissible choice give $z(LF) < z(RF(\beta,\lambda,\mu)) < +\infty$.

Milestones

• §3, remark on $LF$: if every $g_r > 0$, every optimal $LF$ solution has $y_r = (\sum_{k \in R_r} q_{kr})/Q_1$.
• Theorem 2, first clause: the bound, for every instance with $LF$ feasible.
• Theorem 2, second clause: the strict instance.

Significance

Theorem 2 places the relaxation $RF$ in the hierarchy of bounds for the 2E-CVRP. The remark on $LF$ explains its weakness: in the LP relaxation each first-level route is paid for only in proportion to the load it carries, so $z(LF)$ degrades as first-level routing costs grow. $RF$ keeps $y_r$ binary and therefore pays the full cost of every first-level route used, while the second-level routing is priced through $\beta$. The theorem guarantees that optimizing over penalties never loses against the LP bound, which is what makes the bounds LD1 and the further relaxation $\overline{RF}$ of the paper worth computing.

The paper's proof is in its electronic companion and is not reproduced in the article. A formal proof makes the comparison checkable, and fixes the exact conditions under which it holds: the remark on $LF$ needs positive first-level route costs, and the "max" in Theorem 2 is attained only when $LF$ is feasible. Neither part is formalized elsewhere. Linear programming strong duality is available on the platform as LinearOptimization.lp_strong_duality (Bertsimas and Tsitsiklis, Theorem 4.4, Proved); a related but different statement is LinearOptimization.lagrangean_dual_eq_lp_over_hull (Theorem 11.4 there), which concerns the Lagrangean dual of a generic integer program rather than $RF$.

Difficulty

$RF$ is not the Lagrangean dual of $F$ in the textbook sense: it changes the variables (customer-to-satellite assignments $\xi$ instead of routes $x$), keeps the assignment constraints, and couples the multipliers through the inequalities (12). So the general fact that a Lagrangean dual is at least the LP bound does not apply directly; one must construct, from the data of $LF$, an admissible $\beta$ that is compatible with the flow-balance and capacity constraints of $RF$. For the strict clause, the instance must satisfy every structural requirement of the model (positive demands, $Q_2 < Q_1$, route loads at most $Q_2$, $m^2 \le \sum_k m_k$), and $RF$ must be feasible, so that the gap is a genuine gap between finite bounds.

Formalization scope

Satellites and customers are Fin ns and Fin nc (0-based). The travel cost is an arbitrary symmetric real matrix; the triangle inequality is not assumed. Demands are positive integers. Route families $\mathcal M$, $\mathcal R$ are arbitrary finite families of nonempty elementary routes (repetitions allowed), with costs computed from $d$ along the closed walk, so the statements cover the paper's families of all routes as a special case. Binary variables are Bool, integer quantities ℕ, $LF$ variables real. Optimal values are infima over the feasible set in EReal, $+\infty$ for an infeasible problem; there is no junk value $0$.

Part 1 of the goal assumes $LF$ feasible: when $LF$ is infeasible the printed relation would read "$\sup = +\infty$", which is not attained by any single choice of penalties. Part 2 requires $z(RF) < +\infty$, which rules out the trivial witness of an instance with $RF$ infeasible; admissibility includes $\mu, \mu_0 \le 0$, without which the supremum is $+\infty$ for trivial reasons.

The definitions (instance, route systems, $F$, $LF$, (12), $RF$) are shared in shape with the two companion missions of this series and are intended for consolidation. Proofs of the bound will need finite-dimensional LP duality; contributions that connect $LF$ to the platform's general-form LP and its strong duality theorem are welcome.

Selected references

• R. Baldacci, A. Mingozzi, R. Roberti, R. Wolfler Calvo, An Exact Algorithm for the Two-Echelon Capacitated Vehicle Routing Problem, Operations Research 61(2), 298–314, 2013. https://doi.org/10.1287/opre.1120.1153
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 4.4, strong duality; Theorem 11.4, Lagrangean duality).

Motivation

Coordinate descent methods update one block of variables at a time. They are the method of choice when the number of variables is so large that even one full gradient is too expensive, while a single partial derivative is cheap: support vector machines, $\ell_1$-regularized regression, and large sparse least-squares problems are the standard examples. Yu. Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012), doi:10.1137/100802001) gave the first global efficiency estimates for randomized coordinate descent, and these estimates started a large literature on random coordinate and block methods.

Many applications carry simple constraints on each block: bounds on each variable, a simplex or a ball per block. Section 4 of the paper shows that randomized coordinate descent handles such block-separable constraints at no loss: a projected block step, chosen uniformly at random, enjoys the same $O(n/k)$ expected rate as the unconstrained method, and a linear rate under strong convexity. This mission formalizes that result, Theorem 5.

Setting

The space $\mathbb R^N$ is split into $n\ge1$ blocks, $\mathbb R^N=\mathbb R^{n_1}\times\cdots\times\mathbb R^{n_n}$ with $N=\sum_in_i$ and every $n_i\ge1$. A point $x$ is the family of its blocks $x^{(i)}\in\mathbb R^{n_i}$, and $U_ih$ is the point whose $i$-th block is $h$ and whose other blocks are zero. Each block carries a Euclidean norm $\|h\|_{(i)}^2=\langle B_ih,h\rangle$ with $B_i\succ0$ (3.4).

The objective $f:\mathbb R^N\to\mathbb R$ is convex and differentiable, and its gradient is coordinate-wise Lipschitz (2.2): writing $f'_i(x)=U_i^T\nabla f(x)$ for the $i$-th block of the gradient, there are constants $L_i>0$ with

$$\|f'_i(x+U_ih)-f'_i(x)\|^*_{(i)}\le L_i\|h\|_{(i)}\quad\text{for all }x,\ i,\ h .$$

The weighted norm is $\|x\|_1^2=\sum_iL_i\|x^{(i)}\|_{(i)}^2$ (3.5). The function $f$ is strongly convex in $\|\cdot\|_1$ with constant $\sigma>0$ if $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\sigma2\|y-x\|_1^2$ for all $x,y$ (3.1).

The problem is (4.1), $\min_{x\in Q}f(x)$ with $Q=Q_1\times\cdots\times Q_n$ and each $Q_i\subseteq\mathbb R^{n_i}$ nonempty, closed and convex. Its optimal value is $f^*$, attained at an optimal solution $x_*\in Q$. The constrained coordinate update (4.2) is

$$u^{(i)}(x)=\arg\min_{u\in Q_i}\Big[\langle f'_i(x),u-x^{(i)}\rangle+\tfrac{L_i}2\|u-x^{(i)}\|_{(i)}^2\Big],\qquad V_i(x)=x+U_i\big(u^{(i)}(x)-x^{(i)}\big).$$

The uniform coordinate descent method UCDM$(x_0)$ (4.5) draws $i_k$ uniformly from $\{1,\dots,n\}$ and sets $x_{k+1}=V_{i_k}(x_k)$. Its expected objective is $\varphi_k=\mathbb E f(x_k)$, the expectation over $i_0,\dots,i_{k-1}$. The level-set radius $R_1(x_0)$ is the largest $\|\cdot\|_1$-distance between a feasible $x$ with $f(x)\le f(x_0)$ and an optimal solution.

Formalization targets

Goal: Theorem 5

For every $k\ge0$,

$$\varphi_k-f^*\le\frac n{n+k}\Big[\tfrac12R_1^2(x_0)+f(x_0)-f^*\Big],$$

and, if $f$ is strongly convex in $\|\cdot\|_1$ with constant $\sigma>0$,

$$\varphi_k-f^*\le\Big(1-\frac{2\sigma}{n(1+\sigma)}\Big)^k\Big(\tfrac12R_1^2(x_0)+f(x_0)-f^*\Big).\qquad(4.6)$$

Milestones

1. (4.3): the optimality condition $\langle f'_i(x)+L_iB_i(u^{(i)}(x)-x^{(i)}),u-u^{(i)}(x)\rangle\ge0$ for all $u\in Q_i$.
2. (4.4): for feasible $x$, $f(x)-f(V_i(x))\ge\frac{L_i}2\|u^{(i)}(x)-x^{(i)}\|_{(i)}^2$.
3. (4.7): with $r_k=\|x_k-x_*\|_1$, $\ \mathbb E_{i_k}\big(\frac12r_{k+1}^2+f(x_{k+1})-f^*\big)\le\frac12r_k^2+f(x_k)-f^*+\frac1n\langle\nabla f(x_k),x_*-x_k\rangle$.
4. Footnote 2: under (2.2), the strong convexity constant satisfies $\sigma\le1$.

Significance

The result. Theorem 5 shows that the cost of a constrained problem with separable constraints is, up to the projection onto each $Q_i$, the cost of the unconstrained one: $O(n/\epsilon)$ block steps for accuracy $\epsilon$, and $O\big(\frac n\sigma\log\frac1\epsilon\big)$ under strong convexity. The method needs no knowledge of $\sigma$; the same iteration attains whichever rate applies. The Lyapunov function $\frac12\|x-x_*\|_1^2+f(x)-f^*$ of (4.7) needs no level-set argument, so it applies wherever the projected step is cheap.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any rate for a randomized constrained coordinate method, appears in the Prove2Me catalogue or in Mathlib. The Prove2Me catalogue holds Bubeck's scalar, unconstrained random coordinate descent results (ConvexOptAlg.CoordDescent.*) and the deterministic Tseng–Yun coordinate gradient descent; neither covers a projected block step. A formalization produces the first verified rate for a randomized method with constraints, and a reusable model of block-structured spaces, block projections and expectations over random index sequences.

Difficulty

The unconstrained analysis of the paper (Theorem 1) bounds the distance to the optimum by a level-set radius and uses the decrease $f(x)-f(T_i(x))\ge(\|f'_i(x)\|^*_{(i)})^2/(2L_i)$ of a gradient step. Neither carries over: with constraints the gradient at the optimum need not vanish, so the decrease of a projected step is not controlled by the gradient norm, and the unconstrained recursion $\varphi_k-\varphi_{k+1}\ge(\varphi_k-f^*)^2/C$ is not available. A different potential is needed, and its one-step estimate (4.7) is the central milestone. For the linear rate, the contraction factor must be shown nonnegative without assuming $\sigma\le1$, which is where footnote 2 enters.

Formalization scope

$\mathbb R^N$ is the dependent product Blocks E $=\prod_{i:\mathrm{Fin}\,n}E_i$, each $E_i$ a finite-dimensional real inner product space whose inner product is the paper's $\langle B_i\cdot,\cdot\rangle$. Indices are 0-based. The dual norm is the operator norm of linear functionals, and $f'_i(x)$ is the Fréchet derivative of $f$ composed with the block inclusion. Random draws are explicit index sequences, so $\varphi_k$ is the finite average of $f(x_k)$ over all $n^k$ sequences of draws; no measure theory is involved.

Explicit choices where the paper is silent:

• $n\ge1$, every block nontrivial ($n_i\ge1$), and $L_i>0$ are hypotheses.
• Every $Q_i$ is nonempty, and $x_0\in Q$. The paper leaves both implicit; without $x_0\in Q$ the iterates are infeasible and $\varphi_k-f^*$ can be negative.
• $u^{(i)}(x)$ is a choice among the minimizers of the block subproblem. Under the hypotheses the minimizer exists and is unique, so the choice is the paper's update.
• $R_1(x_0)$ is never computed: the theorem takes any $R$ with $\|x-x_*\|_1\le R$ for every feasible $x$ with $f(x)\le f(x_0)$ and every optimal solution $x_*$. This is equivalent to the paper's bound when $R_1(x_0)$ is finite and avoids the default value of a supremum. The level set is taken inside $Q$, the reading of the p. 7 definition for problem (4.1).
• $f^*$ is the constrained optimum $f(x_*)$ for an optimal solution $x_*\in Q$, not an unconstrained minimum.
• Strong convexity is (3.1) on all of $\mathbb R^N$ in $\|\cdot\|_1$. The linear rate does not assume $\sigma\le1$; footnote 2 derives it.
• Printed typos are corrected in the Lean: $U_i^T$ in (4.2) is $U_i$; $u^i$ in (4.3) is $u^{(i)}$.

A formalization in which the update is an arbitrary point of $Q_i$ or an unprojected gradient step, the draws are not uniform, or $f^*$ is the unconstrained minimum, proves a different theorem and is ruled out by the definitions above.

Needed infrastructure: existence and the variational characterization of the minimizer of a strongly convex quadratic over a closed convex set (Mathlib has projections onto closed convex sets in Hilbert spaces), the block descent inequality (2.3) obtained from (2.2), and manipulation of the finite expectations over index sequences (conditioning on the last draw). The block model, the weighted norm and the expectation are shared with the other missions of this series. Proofs of the milestones, and of (2.3) as a supporting lemma, are welcome.

Selected references

• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, CORE Discussion Paper 2010/2, Université catholique de Louvain, 2010. https://core.ac.uk/download/6430808.pdf
• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2) (2012), 341–362. https://doi.org/10.1137/100802001
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (Section 2.1, cited in the proof). https://doi.org/10.1007/978-1-4419-8853-9
• P. Tseng and S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Mathematical Programming 117 (2009), 387–423. https://doi.org/10.1007/s10107-007-0170-0

Motivation

City logistics often moves goods in two stages: large trucks bring freight from a central depot to a few intermediate satellites, and small vehicles distribute it from the satellites to the customers. The two-echelon capacitated vehicle routing problem (2E-CVRP) is the basic optimization model of such systems; it contains the capacitated location-routing problem as a special case. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) gave an exact method that solved benchmark instances out of reach for earlier algorithms.

Their method does not attack the whole problem at once. It enumerates configurations, sets of first-level (depot–satellite) routes, discards most of them with cheap tests, and solves a second-level problem only for the survivors. The correctness of the method rests on two facts stated in §5 of the paper: the problem decomposes exactly over configurations (Eq. (26)), and the pruning tests of Propositions 1 and 2 never discard the configuration of a solution better than the incumbent. This mission formalizes those facts.

Setting

An instance has a depot $0$, satellites $N_S$ and customers $N_C$, a symmetric cost $d$ on the edges (with the fixed vehicle costs folded in), positive integer demands $q_i$ with total $q_{\mathrm{tot}}$, $m^1$ first-level vehicles of capacity $Q_1$, $m_k$ second-level vehicles of capacity $Q_2<Q_1$ at satellite $k$ with a global limit $m^2$, satellite capacities $B_k$ and handling costs $H_k$.

A first-level route $r\in\mathcal M$ leaves the depot, visits a set $R_r$ of satellites and returns; its cost $g_r$ is the length of the closed walk. A second-level route $l\in\mathcal R_k$ leaves satellite $k$, visits a set $R_{kl}$ of customers of total demand $w_{kl}\le Q_2$ and returns; its cost $c_{kl}$ is the walk length plus $H_k w_{kl}$. Formulation $F$ chooses binary $x_{kl}$, $y_r$ and integer deliveries $q_{kr}\ge0$ minimizing $\sum c_{kl}x_{kl}+\sum g_r y_r$ subject to: each customer on exactly one used second-level route; at most $m_k$ used routes at $k$ and $m^2$ in total; load at $k$ at most $B_k$; at most $m^1$ first-level routes; the deliveries to $k$ equal the load leaving $k$; each used first-level route carries at most $Q_1$. Its optimal value is $z(F)$, $+\infty$ when infeasible.

The set of configurations is

$$\mathcal P=\{M\subseteq\mathcal M:\ |M|Q_1\ge q_{\mathrm{tot}},\ |M|\le m^1\}.$$

For $M\subseteq\mathcal M$, $N_S(M)=\bigcup_{r\in M}R_r$, $M_k=\{r\in M:k\in R_r\}$ and $U(M)=\sum_{r\in M}g_r$. Problem $F(M)$ is $F$ with the first-level routes fixed to $M$: second-level routes only at satellites of $N_S(M)$, real deliveries $q_{kr}\ge0$ for $r\in M$, and $\sum_{k\in R_r}q_{kr}\le Q_1$. Its value $z(F(M))$ is $+\infty$ when infeasible.

The bounds of §5.1 use multipliers $\lambda_i$, $\mu_k\le0$, $\mu_0\le0$ and marginal costs $\beta_{ik}$ satisfying the penalty system (12), $\sum_i a_{ikl}\beta_{ik}\le c_{kl}-\sum_i a_{ikl}\lambda_i-\mu_k-\mu_0$ for every route $l$ of satellite $k$:

$$\mathrm{LB}_R=\sum_{i}\min_{k\in N_S}\beta_{ik}+\sum_i\lambda_i+\sum_{k\in N_S}m_k\mu_k+m^2\mu_0,$$ $$\mathrm{LBW}(M)=\sum_{i}\min_{k\in N_S(M)}\beta_{ik}+\sum_i\lambda_i+\sum_{k\in N_S(M)}m_k\mu_k+m^2\mu_0.$$

Formalization targets

Goal: Proposition 1, necessity of conditions (b)–(e)

Let $z(\mathrm{UB})$ be a real number and $(x,y,q)$ a feasible solution of $F$ of cost less than $z(\mathrm{UB})$, with configuration $M=\{r:y_r=1\}$. Then $M\in\mathcal P$ and

$$\sum_{r\in M}\min\Bigl\{Q_1,\sum_{k\in R_r}m_kQ_2\Bigr\}\ge q_{\mathrm{tot}},\qquad \sum_{r\in M}\sum_{k\in R_r}m_k\ge\Bigl\lceil\frac{q_{\mathrm{tot}}}{Q_2}\Bigr\rceil,$$ $$U(M)<z(\mathrm{UB})-\mathrm{LB}_R,\qquad U(M)<z(\mathrm{UB})-\mathrm{LBW}(M).$$

Milestones

1. Eq. (26): $z(F)=\min_{M\in\mathcal P}\{U(M)+z(F(M))\}$.
2. §5.1: $\mathrm{LB}_R$ is at most the second-level routing cost of every feasible solution of $F$.
3. §5.1: $\mathrm{LBW}(M)\le z(F(M))$.
4. Proposition 2: if $\theta(k)$ bounds from below the supply to satellite $k$ in every feasible solution of $F(M)$, and $\sum_{k\in N_S(M)}\lceil\theta(k)/Q_2\rceil>m^2$ or $\lceil\theta(k)/Q_2\rceil>m_k$ for some $k\in N_S(M)$, then $F(M)$ is infeasible.
5. §5.2.2, Eq. (33): the capacity constraints $\sum_{k\in N_S(M)}\sum_{l:R_{kl}\cap H\neq\emptyset}x_{kl}\ge\lceil\sum_{i\in H}q_i/Q_2\rceil$, $|H|\ge2$, hold for every feasible solution of $F(M)$.

Significance

Eq. (26) is what makes the method exact: once every configuration that can carry a solution better than the incumbent is examined, the best $U(M)+z(F(M))$ is the optimum. Propositions 1 and 2 are what make it fast: they remove configurations from $\mathcal P$ before any second-level problem is solved. If a pruning test discarded the configuration of a cheaper solution, the method would return a suboptimal value and still report it as optimal; the formal statements rule this out for every instance, not just the benchmark ones. The capacity constraints (33) play the same role inside $F(M)$: a cut that removed a feasible solution would make the bound $z(\bar F(M))$ invalid.

The paper's proofs are in an electronic companion; none of these statements has been machine-checked before, and none is on the platform. The formalization also records exactly what the tests need: positive demands, integral vehicle counts, and the sign conditions on the multipliers, and nothing about the optimality of the incumbent.

Difficulty

Most statements are elementary counting and Lagrangean weak-duality arguments over finite index sets. The work lies in the bookkeeping between two formulations with different index sets: $F$ sums over all satellites, $F(M)$ only over $N_S(M)$, and a solution of one must be turned into a solution of the other. One step is not elementary: $F$ has integer deliveries and $F(M)$ real ones, so the inequality $z(F)\le U(M)+z(F(M))$ in (26) needs an integral delivery plan from a fractional one. That is an integrality property of a bipartite transportation problem (routes to satellites, integral capacities and demands), which no counting argument gives.

Formalization scope

Satellites and customers are Fin ns and Fin nc, 0-based. The route families $\mathcal M$ and $\mathcal R$ are arbitrary finite families of elementary routes with costs computed along the closed walk; the paper uses all such routes, so every statement here is a generalization. Demands are positive integers; the triangle inequality is not assumed. Binary variables are Bool; optimal values are infima in EReal, with ⊤ for an infeasible problem. A configuration is a Finset of route indices. The penalties are any $\lambda$, $\mu\le0$, $\mu_0\le0$ and $\beta$ satisfying (12), not only those producing the paper's bound LD1. Ceilings of $q_{\mathrm{tot}}/Q_2$ and $\sum_{i\in H}q_i/Q_2$ are natural-number ceilings of rationals; those in Proposition 2 are integer ceilings of reals.

The goal departs from the printed proposition in three disclosed ways. Only necessity is stated: the "if" direction is false, because (b)–(e) ignore the satellite capacities $B_k$. Condition (a), $|R_r\cap R_{r'}|\le1$, is omitted: it holds for some optimal solution, not every one (its split-delivery analogue is posed, and open, on the platform as SplitDeliveryVRPTW.Known.exists_optimal_split_customers; it is not reused here). "An optimal solution" becomes "a feasible solution of cost below $z(\mathrm{UB})$", the property the paper's own justification uses. Proposition 2 is stated with $\theta$ as a hypothesis; the paper's computation of $\theta$ by problem (27)–(32) is not formalized, because (32) forces positive deliveries that $F(M)$ does not require. The goal is not trivialized by an infeasible hypothesis: feasible solutions of $F$ exist on small instances, and a toy instance was checked in Lean.

A complete development needs finite-sum manipulations, Lagrangean weak duality for (12), and, for (26), integrality of bipartite transportation polytopes, which is reusable well beyond this mission. Proofs of any milestone, and a general transportation-integrality lemma, are welcome.

Selected references

• R. Baldacci, A. Mingozzi, R. Roberti, R. Wolfler Calvo, An Exact Algorithm for the Two-Echelon Capacitated Vehicle Routing Problem, Operations Research 61(2), 298–314, 2013. https://doi.org/10.1287/opre.1120.1153
• R. Baldacci, A. Mingozzi, A unified exact method for solving different classes of vehicle routing problems, Mathematical Programming 120(2), 347–380, 2009. https://doi.org/10.1007/s10107-008-0218-9
• G. Perboli, R. Tadei, D. Vigo, The two-echelon capacitated vehicle routing problem: models and math-based heuristics, Transportation Science 45(3), 364–380, 2011. https://doi.org/10.1287/trsc.1110.0368

Motivation

In a time-inconsistent control problem, a control that is optimal when planned at time $t$ stops being optimal when the problem is re-solved at a later time. Two sources of time inconsistency are common in finance and economics. One is a variance term in the objective, as in continuous-time Markowitz mean–variance portfolio selection (Zhou–Li 2000; Basak–Chabakauri 2010). The other is a state-dependent target, as in Björk–Murgoci–Zhou 2014. Dynamic programming does not apply. A standard response is to look for an equilibrium: a control that no planner at any time $t$ can improve by an infinitesimal deviation on $[t,t+\varepsilon)$.

Hu, Jin and Zhou define open-loop equilibria for a general stochastic linear–quadratic (LQ) problem with both sources of time inconsistency. They give a sufficient condition through a flow of forward–backward SDEs, which is the subject of mission I of this series. This mission covers §4 of the paper: the scalar-state case with deterministic coefficients, where the equilibrium is computed explicitly from a system of coupled Riccati equations. Mission III covers §5, the mean–variance application with random coefficients.

Setting

On a probability space carrying a standard $d$-dimensional Brownian motion $W$ with its filtration $(\mathcal F_t)$, the state $X$ is scalar ($n=1$) and the control $u$ takes values in $\mathbb R^l$:

$$dX_s=[A_sX_s+B_s'u_s+b_s]\,ds+[C_sX_s+D_su_s+\sigma_s]'\,dW_s,\qquad X_0=x_0.$$

The coefficients are deterministic functions on $[0,T]$: $A_s,b_s,Q_s\in\mathbb R$, $B_s\in\mathbb R^l$, $C_s,\sigma_s\in\mathbb R^d$, $D_s\in\mathbb R^{d\times l}$ and $R_s\in\mathbb R^{l\times l}$ symmetric. $A,B,C,D,Q,R$ are bounded, $b,\sigma$ are square integrable, $Q\ge0$, $R\succeq0$, and $G\ge0$. At time $t$, in state $x_t$, the planner evaluates

$$J(t,x_t;u)=\tfrac12\mathbb E_t\!\int_t^T\!\big(Q_sX_s^2+\langle R_su_s,u_s\rangle\big)ds+\tfrac12\mathbb E_t[GX_T^2]-\tfrac h2\big(\mathbb E_t[X_T]\big)^2-(\mu_1x_t+\mu_2)\,\mathbb E_t[X_T],$$

where $\mathbb E_t=\mathbb E[\,\cdot\mid\mathcal F_t]$. The third term (the variance-like term) and the fourth term (which depends on $x_t$) make the problem time-inconsistent. A control $u^*$ with state $X^*$ is an equilibrium (Definition 2.1) if, for every $t\in[0,T)$ and every $\mathcal F_t$-measurable square-integrable $v$, the spike $u^{t,\varepsilon,v}=u^*+v\mathbf 1_{[t,t+\varepsilon)}$ satisfies

$$\liminf_{\varepsilon\downarrow0}\frac{J(t,X^*_t;u^{t,\varepsilon,v})-J(t,X^*_t;u^*)}{\varepsilon}\ge0.$$

With $\Gamma^{(1)}_s=\mu_1e^{\int_s^TA_r\,dr}$, $|C|^2=C'C$ and $K=(R+MD'D)^{-1}$, the coupled Riccati system (4.9) for deterministic $(M,N)$ is

$$\begin{aligned}\dot M&=-\big[2A+|C|^2+\Gamma^{(1)}B'K(B+D'C)\big]M-Q+(B+D'C)'K(B+D'C)M^2-B'K(B+D'C)MN,& M_T&=G,\\ \dot N&=-\big[2A+\Gamma^{(1)}B'KB\big]N+B'K(B+D'C)MN-B'KBN^2,& N_T&=h.\end{aligned}$$

Given $(M,N)$, a linear ODE (4.8) determines $\Phi$ with $\Phi_T=-\mu_2$. The candidate equilibrium is the linear feedback (4.4)

$$u^*_s=\alpha_sX^*_s+\beta_s,\quad\alpha_s=-K_s\big[(M_s-N_s-\Gamma^{(1)}_s)B_s+M_sD_s'C_s\big],\quad\beta_s=-K_s(\Phi_sB_s+M_sD_s'\sigma_s).$$

Formalization targets

Goal: Theorem 4.4

Suppose $G\ge h>0$ and one of three cases holds:

• (i) $R\succeq\delta I$, $\frac{QD'D+|C|^2R}{l}+\Gamma^{(1)}\mathcal S(D'CB')\succeq0$ and $B=\lambda D'C$ with $\lambda\ge0$;
• (ii) the first two conditions of (i) and $D'D\succeq\delta I$;
• (iii) $R\equiv0$, $D'D\succeq\delta I$, $Q+\Gamma^{(1)}B'(D'D)^{-1}(B+D'C)\ge0$ and $Q+\Gamma^{(1)}B'(D'D)^{-1}D'C\ge0$.

Then

$$\text{(4.9) has a unique positive solution pair }(M,N)\text{ on }[0,T],$$

and, for every solution $\Phi$ of (4.8), the closed-loop equation of (4.4) has a solution, and the feedback control along every closed-loop state is an equilibrium.

Milestones

• Proposition 4.1: a positive solution $(M,J)$ of the transformed system (4.10) gives the positive solution $(M,M/J)$ of (4.9).
• Theorem 4.2: existence and uniqueness of positive solutions of (4.10) and (4.9) in the standard case $R\succeq\delta I$.
• Theorem 4.3: existence for (4.13) and (4.9) in the singular case $R\equiv0$.
• Three steps from the proof of Theorem 4.4:
  • $\alpha$ is bounded, so $u^*$ is admissible and $X^*$ has continuous paths with $\mathbb E\sup_s|X^*_s|^2<\infty$;
  • the ansatz $p(s;t)=M_sX^*_s-N_s\mathbb E_t[X^*_s]-\Gamma^{(1)}_sX^*_t+\Phi_s$, $k(s;t)=M_s[C_sX^*_s+D_su^*_s+\sigma_s]$ solves the adjoint flow (3.10);
  • the identity $\Lambda(s;t)=N_s[X^*_s-\mathbb E_tX^*_s]B_s+\Gamma^{(1)}_s(X^*_s-X^*_t)B_s$ holds, and $\Lambda$ satisfies condition (3.4).

Significance

The theorem gives an equilibrium in closed form, as a linear feedback of the current state with deterministic gains. That makes the equilibrium computable and comparable with the classical, time-consistent LQ regulator. Setting $h=\mu_1=0$ recovers a standard LQ problem, but (4.9) differs from the classical Riccati equation even then: it is a nonsymmetric coupled system (footnote 2, p. 10), and the cases (i)–(iii) are the conditions under which it is solvable. The mean–variance results of §5 (mission III) follow the same pattern.

The result is proved in the paper; to our knowledge it has not been formalized. A formal proof needs global existence for a nonlinear, nonautonomous ODE system with Carathéodory coefficients, obtained by truncation and a priori bounds. It also needs linear SDEs with bounded feedback, Itô calculus for products of deterministic and Itô processes, and the sufficient condition of mission I. Uniqueness in case (iii) is claimed by Theorem 4.4 but not proved in Theorem 4.3; it is part of the goal.

Difficulty

The system (4.9) is quadratic in $(M,N)$. Its solutions can blow up in finite time, and $(R+MD'D)^{-1}$ can degenerate when $M$ changes sign. Picard–Lindelöf therefore gives only local solutions, and a global solution needs a priori bounds $0<\eta\le M\le L$ and $J\ge1$, with $\eta$ and $L$ independent of the truncation level. Those bounds are where the case hypotheses enter. In the stochastic half, the equilibrium property is not proved by computing $J$ directly. It requires checking that the explicit candidate meets the flow-of-FBSDE sufficient condition, and the flow carries a parameter $t$ and the conditional expectations $\mathbb E_t[X^*_s]$ for every $s\ge t$.

Formalization scope

The general model (data, standing assumptions, states, conditional cost, spike, equilibrium) is stated for arbitrary $n$ and instantiated at $n=1$ through toData. It is built on the published substrate Peng1990_SMP_Stochastic (Brownian motion, natural filtration, $L^2_{\mathcal F}$, Itô integrals, SDE solutions). The formalization commits to the following choices.

• Definition 2.1 uses $\liminf$ in $\overline{\mathbb R}$, along every sequence $\varepsilon_k\downarrow0$, almost surely for each sequence, and for every version of the state and of the perturbed states. The page writes $\lim$, which need not exist.
• The filtration is the natural, uncompleted filtration of $W$, not the augmented one.
• The state from time $t$ is encoded through the full horizon. The spike is additive on $[t,t+\varepsilon)$.
• "Essentially bounded" and "a.s., a.e." are read $d\mathbb P\otimes ds$-a.e.
• Every ODE ((4.8), (4.9), (4.10), (4.13)) is stated in integral form on $[0,T]$, because the coefficients are only bounded measurable. A solution includes invertibility of $R+MD'D$ (resp. $D'D$) on $[0,T]$. Uniqueness means agreement on $[0,T]$.
• The constants $\delta,\lambda$ are uniform in $s$, and the case conditions hold for every $s\in[0,T]$. In $\frac{QD'D+|C|^2R}{l}$, $l$ is the control dimension.
• "Let $\Phi$ be a solution of (4.8)" means every solution. "$u^*$ is an equilibrium" means that a closed-loop state exists and that the feedback is an equilibrium along every closed-loop state.
• Conditional-expectation families $\mathbb E_t[X^*_s]$ are handled through arbitrary progressive versions. Condition (3.4) is stated exactly: its first part as a localization on $\mathcal F_t$-sets, its second part with a jointly measurable version and "a.e. $s$".
• The paper's "$\beta$ uniformly bounded" is false when $\sigma$ is only square integrable. The milestone states the true claim: $\alpha$ is essentially bounded on $[0,T]$ (the coefficients are only essentially bounded) and $\beta$ is square integrable.

The goal's conclusion is Definition 2.1 itself; it does not mention $\Lambda$, $p$ or (3.4). Existence of the closed-loop state is asserted, not assumed. A formalization that assumes existence, or that replaces equilibrium by condition (3.4), is a different and weaker theorem.

Theorem 3.3 (the $n=1$ sufficient condition) is not posed here. Under the shared model it is mission I's goal at $n=1$. Contributions are welcome on the ODE layer (truncation, comparison and Gronwall bounds for Carathéodory systems), on linear SDEs with bounded feedback, and on the Itô product rule. These parts are reusable well beyond this paper.

Selected references

• Y. Hu, H. Jin, X. Y. Zhou, Time-Inconsistent Stochastic Linear–Quadratic Control, arXiv:1111.0818v1, 2011; SIAM J. Control Optim. 50(3), 2012. https://arxiv.org/abs/1111.0818
• T. Björk, A. Murgoci, X. Y. Zhou, Mean–variance portfolio optimization with state-dependent risk aversion, Mathematical Finance 24(1), 2014. https://doi.org/10.1111/j.1467-9965.2011.00515.x
• S. Basak, G. Chabakauri, Dynamic mean–variance asset allocation, Review of Financial Studies 23(8), 2010. https://doi.org/10.1093/rfs/hhq028
• X. Y. Zhou, D. Li, Continuous-time mean–variance portfolio selection: a stochastic LQ framework, Applied Mathematics and Optimization 42, 2000. https://doi.org/10.1007/s002450010003
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054
• J. Yong, X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3
• Missions I and III of this series: the sufficient condition (Theorem 3.2) and the mean–variance equilibrium (Theorem 5.4).

Motivation

A prophet inequality compares a gambler who sees independent random rewards one at a time, and must accept or reject each on arrival, with a prophet who sees all rewards in advance. The classical inequality of Krengel, Sucheston and Garling (1977–78, as cited in the paper) says that when only one reward may be kept, a single threshold rule earns at least half of $\mathbb E[\max_i X_i]$, and Samuel-Cahn (1984) showed that the threshold can be chosen as a median. Such statements are the analytical core of sequential posted-price mechanisms: Hajiaghayi, Kleinberg and Sandholm (2007) observed that threshold rules are truthful online auctions, and Chawla, Hartline, Malec and Sivan (2010) showed that sequential posted prices approximate the optimal Bayesian revenue in many settings, with prophet inequalities for the feasibility constraint as the key technique.

When several items may be accepted subject to a combinatorial constraint, the natural constraints in this application are matroids (for example, at most $k$ items, or at most one item per group) and intersections of matroids (for example, bipartite matchings, which are intersections of two partition matroids). Kleinberg and Weinberg (STOC 2012) proved that for every matroid there is an online algorithm with expected payoff at least half of the expected maximum-weight basis, and that for the intersection of $p$ matroids the summed version of the same algorithm earns at least $\frac{1}{4p-2}$ of the expected optimum. This mission formalizes the second result.

Timeline:

• 1977–78: Krengel–Sucheston and Garling, single-choice prophet inequality with factor 2.
• 1984: Samuel-Cahn, the median threshold rule attains factor 2.
• 2007: Hajiaghayi–Kleinberg–Sandholm, threshold rules from prophet inequalities read as truthful online auction mechanisms.
• 2010: Chawla–Hartline–Malec–Sivan, sequential posted pricing; factor 2 for matroids when the algorithm may choose the order in which elements are observed.
• 2012: Kleinberg–Weinberg, factor 2 for matroids and $4p-2$ for intersections of $p$ matroids, against online weight-adaptive adversaries.

Setting

A finite ground set $\mathcal U$ carries $p \ge 1$ matroids $\mathcal M_1,\dots,\mathcal M_p$ with independent sets $\mathcal I_1,\dots,\mathcal I_p$ and closure operators $\mathrm{cl}_1,\dots,\mathrm{cl}_p$. A set is feasible if it lies in $\mathcal I = \bigcap_j \mathcal I_j$. Each element $x$ has a random weight $w(x) \ge 0$; the weights are independent and $w(x)$ has law $F_x$. For a set $S$, $w(S) = \sum_{x \in S} w(x)$, $\mathrm{OPT}(w) = \max\{w(S) : S \in \mathcal I\}$, and $\mathrm{OPT} = \mathbb E[\mathrm{OPT}(w)]$.

An online weight-adaptive adversary reveals the elements one at a time; it chooses the $i$-th element $x_i$ after learning $w(x_1),\dots,w(x_{i-1})$, but without knowing $w(x_i)$ or any other unrevealed weight. A threshold algorithm offers $x_i$ a threshold $T_i$ computed from what has been revealed and from the set $A_{i-1}$ already selected, and selects $x_i$ exactly when $A_{i-1}\cup\{x_i\}\in\mathcal I$ and $w(x_i) \ge T_i$.

The algorithm of the paper uses a ghost sample $w'$, an independent copy of $w$. Let $B$ be a $w'$-maximum feasible set. For a set $A$ and each $j$, $R_j(A) \subseteq B \setminus A$ is a set of maximum $w'$-weight with $A \cup R_j(A) \in \mathcal I_j$ and $B \subseteq \mathrm{cl}_j(A \cup R_j(A))$, and $C_j(A) = B \setminus R_j(A)$. Put $R(A) = \bigcap_j R_j(A)$ and $C(A) = \bigcup_j C_j(A)$. For a parameter $\alpha$, the summed thresholds are

$$T(A,i) = \sum_{j=1}^p \frac1\alpha\, \mathbb E_{w'}\big[w'(R_j(A)) - w'(R_j(A \cup \{x_i\}))\big],$$

and the algorithm of §4.2 uses $T_i = T(A_{i-1}, i)$. An algorithm has $\alpha$-balanced thresholds (Definition 3) if, for every input sequence with selected set $A$ and every $V$ disjoint from $A$ with $A \cup V \in \mathcal I$,

$$\sum_{x_i\in A} T_i \ge \frac1\alpha \mathbb E\Big[\sum_j w'(C_j(A))\Big], \qquad \sum_{x_i\in V} T_i \le \frac1\alpha \mathbb E\Big[\sum_j w'(R_j(A))\Big].$$

Formalization targets

Goal: the prophet inequality for $p$ matroids

For every $p \ge 1$, all matroids $\mathcal M_1,\dots,\mathcal M_p$ on $\mathcal U$, all laws $F_x$ on $[0,\infty)$ with finite means, and every online weight-adaptive adversary, the algorithm of §4.2 with $\alpha = 2p$ selects a set $A$ with

$$\mathbb E[w(A)] \ge \frac{1}{4p-2}\, \mathbb E[\mathrm{OPT}(w)].$$

For $p = 1$ this is the factor-2 matroid prophet inequality.

Proposition 3

If a threshold algorithm has $\alpha$-balanced thresholds for some $\alpha \ge 2$, then against every online weight-adaptive adversary

$$\mathbb E[w(A)] \ge \frac{\alpha - p}{\alpha(\alpha-1)}\, \mathrm{OPT}.$$

Milestones

Proposition 2 for each matroid $\mathcal M_j$; the identity between the two forms of $T(A,i,j)$; properties (13) and (14) for the summed thresholds; the identities (20)–(21); and the inequalities (23)–(24) of Appendix A. Together with Proposition 3 these give the goal.

Significance

The bound gives a posted-price style selection rule for any feasibility constraint that is an intersection of $p$ matroids, with a guarantee depending only on $p$; the paper's §5 shows that a ratio of order $p$ is necessary. Section 6 of the paper turns the result into sequential posted-price mechanisms for multi-dimensional mechanism design, and that application needs the guarantee against the online weight-adaptive adversary, not only against a fixed order. The reduction "balanced thresholds imply an approximation" (Proposition 3) is reusable for other threshold constructions.

The result is proved in the paper; to our knowledge no machine-checked proof exists. The mission produces a formal proof of the $\frac{1}{4p-2}$ guarantee, with the probabilistic part (the ghost-sample argument against an adaptive adversary) and the combinatorial part (the per-matroid exchange inequality) as separate milestones. The paper justifies the per-matroid use of Proposition 2 in one paragraph; because $B$ maximizes $w'$ over the intersection rather than over $\mathcal I_j$, the description of $R_j(A)$ as a maximum-weight basis of a contraction (Lemma 2 in the single-matroid case) does not apply verbatim, and the formal proof of that milestone is not a copy of the paper's single-matroid argument.

Difficulty

Two steps do not follow from routine bookkeeping. First, the inequality (23) compares the gambler's surplus, collected along an order that the adversary adapts to the realized weights, with the ghost sample's surplus on the random set $R(A)$. The index $x_i$ revealed at step $i$ is itself random, so the step "the weight of the element offered next is distributed as its ghost weight" has to be justified for an adaptively chosen index under a product measure; it fails for an adversary that may look at unrevealed weights. Second, the paper obtains (14) by applying the single-matroid Proposition 2 to each $\mathcal M_j$, but its proof of Proposition 2 describes $R(A)$ as a maximum-weight basis of a contraction, which uses that $B$ is optimal for the matroid in question. Here $B$ is optimal only for the intersection $\mathcal I$, so the obvious transfer of the single-matroid argument does not go through as written and the per-matroid statement needs its own proof.

Formalization scope

The ground set is a Fintype; the matroids are Mathlib's Matroid α, indexed by Fin p, each with ground set Set.univ; sets are Finset α. Weights are functions α → ℝ, the weight law is Measure.pi F, and every theorem assumes each F x is a probability measure with F x (Iio 0) = 0 and a finite mean. Expectations are Bochner integrals; under these assumptions every integrand is integrable. Ties in the maximizers $B$ and $R_j(A)$ are broken by a fixed rule that does not depend on the weights. $R_j(A)$ is taken disjoint from $A$. The threshold $\infty$ on infeasible steps is a feasibility test in the selection rule. Adversaries and generic threshold rules are deterministic, see only revealed weights, and are measurable in them; randomized adversaries are mixtures of deterministic ones. Generic thresholds in Proposition 3, (23) and (24) are non-negative, as in the paper's $T_i \in \mathbb R_+ \cup \{\infty\}$.

The goal fixes the thresholds to the summed thresholds of §4.2 with $\alpha = 2p$, computed from the ghost-sample objects. A version in which the thresholds are free parameters assumed to satisfy (13)–(14) would be Proposition 3 itself and is ruled out; conversely, Proposition 3 does not mention the §4.2 thresholds.

A complete development needs: elementary facts about maximizers over finite families; matroid exchange properties (a bijective exchange between equal-size independent sets, available in Schrijver's book but not in Mathlib); submodularity of weighted-rank-type functions; and the independence argument for adaptively chosen indices under a product measure. The last two are reusable beyond this mission, as is Proposition 3. Proofs of individual milestones and of these auxiliary facts are welcome.

Selected references

• R. Kleinberg, S. M. Weinberg, Matroid Prophet Inequalities, STOC 2012; arXiv:1201.4764v1. https://arxiv.org/abs/1201.4764, https://doi.org/10.1145/2213977.2213991
• U. Krengel, L. Sucheston, Semiamarts and finite values, Bull. Amer. Math. Soc. 83 (1977), 745–747.
• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Ann. Probab. 12 (1984). https://doi.org/10.1214/aop/1176993150
• M. T. Hajiaghayi, R. Kleinberg, T. Sandholm, Automated online mechanism design and prophet inequalities, Proc. 22nd AAAI Conference on Artificial Intelligence, 2007, pp. 58–65.
• S. Chawla, J. Hartline, D. Malec, B. Sivan, Multi-parameter mechanism design and sequential posted pricing, STOC 2010, pp. 311–320; arXiv:0907.2435. https://arxiv.org/abs/0907.2435
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer 2003 (Corollary 39.12a).