Optimization

Motivation

Conjugate gradient methods minimize a smooth function $f:\mathbb R^n\to\mathbb R$ using only gradients and a handful of stored vectors. This makes them the standard choice when $n$ is too large for Newton or quasi-Newton methods, which store an $n\times n$ matrix. On a strictly convex quadratic with exact line searches the classical method of Hestenes and Stiefel terminates in at most $n$ steps. On general functions, and with the inexact line searches used in practice, its behaviour is much less clear.

D. F. Shanno's 1978 paper in Mathematics of Operations Research (doi:10.1287/moor.3.3.244) links conjugate gradient methods to quasi-Newton methods. It writes the search direction as $-\hat H g$, where $\hat H$ is a positive definite approximation of the inverse Hessian that is never stored. The resulting "memoryless" BFGS directions give descent without exact line searches. The paper's new algorithm uses two BFGS updates: one from the last restart and one from the current step. Its first update is scaled by the Oren–Spedicato factor $\gamma_t$. Shanno and Phua's CONMIN code implements the algorithm, and the memoryless BFGS direction is the one-pair case of the later limited-memory BFGS methods.

• 1952: Hestenes and Stiefel, linear conjugate gradients.
• 1964: Fletcher and Reeves, nonlinear conjugate gradients.
• 1969: Polak and Ribière, a second nonlinear variant.
• 1972: Beale, a restart procedure that keeps the computed direction $d_t$.
• 1977: Powell's restart criterion (Powell 1977).
• 1978: Shanno's reformulation as memoryless and two-update quasi-Newton methods (this paper).

Setting

Vectors are columns in $\mathbb R^n$. A prime denotes transpose: $u'v$ is the inner product and $uv'$ the outer product. An iterative method produces points $x_k$, steps $p_k = x_{k+1}-x_k = \alpha_k d_k$ along search directions $d_k$, gradients $g_k = \nabla f(x_k)$, and gradient changes $y_k = g_{k+1}-g_k$. A line search is exact when $p_k'g_{k+1} = 0$.

The BFGS update of a matrix $H$ with the pair $(p,y)$ is

$$H^+ = H - \frac{p\,y'H + H y\,p'}{p'y} + \left(1+\frac{y'Hy}{p'y}\right)\frac{pp'}{p'y}.$$

A restart cycle begins at iteration $t$. At a later iteration $k>t$, Shanno's self-scaled restart matrix is

$$\hat H_k = \gamma_t\left(I - \frac{p_ty_t'+y_tp_t'}{p_t'y_t} + \frac{y_t'y_t}{p_t'y_t}\frac{p_tp_t'}{p_t'y_t}\right) + \frac{p_tp_t'}{p_t'y_t}, \qquad \gamma_t = \frac{p_t'y_t}{y_t'y_t}.$$

The matrix $\hat H_{k+1}$ is its BFGS update with $(p_k,y_k)$, and the self-scaled two-update direction is $d_{k+1} = -\hat H_{k+1}g_{k+1}$. The unscaled variant uses the BFGS update of $I$ in place of the first matrix.

Beale's direction is

$$d_{k+1} = -g_{k+1} + \frac{y_k'g_{k+1}}{d_k'y_k}d_k + \frac{y_t'g_{k+1}}{d_t'y_t}d_t.$$

The quadratic case has gradient $g(x) = Ax + c$ with $A$ symmetric positive definite.

Formalization targets

Goal: reduction of the self-scaled method to Beale's method

Let $A$ be symmetric positive definite, $g_i = Ax_i + c$ and $t<k$. Assume that for $t\le i\le k$ we have $x_{i+1} = x_i + p_i$, $p_i = \alpha_i d_i$ and $p_i'g_{i+1}=0$, that $p_t'Ap_i = 0$ for $t<i\le k$, and that $p_t, p_k \ne 0$. Then

$$-\hat H_{k+1}g_{k+1} = \gamma_t\left(-g_{k+1} + \frac{y_k'g_{k+1}}{d_k'y_k}d_k + \frac{y_t'g_{k+1}}{d_t'y_t}d_t\right).$$

This is the paper's claim that "for $f(x)$ quadratic with exact searches each of the above methods reduces exactly to Beale's method defined by (28)", with the conclusion (44). The scale is exactly $\gamma_t$.

Companion statements

• The unscaled two-update direction equals Beale's direction exactly.
• Both two-update directions are descent directions, $g_{k+1}'d_{k+1} < 0$, whenever $p_t'y_t > 0$ and $p_k'y_k > 0$. No exact search is needed.

Milestones on the path

• (34): the expansion of $-\hat H_{k+1}g_{k+1}$.
• (40): its form under an exact search.
• (41): gradients along a run on a quadratic.
• $p_t'g_{k+1} = 0$.
• (38), corrected by a factor 2: the action of the self-scaled restart matrix.
• (42): its form when $p_t'g_{k+1} = 0$.
• (43): the direction after substitution.

Significance

The result. The reduction says that the new algorithm reproduces Beale's restarted conjugate gradient directions on a quadratic with exact line searches. So it keeps the finite-termination and rate-of-convergence properties behind Beale's restart. Away from that setting it behaves as a quasi-Newton method, whose directions are descent directions under any line search with $p'y>0$. The two regimes are what justify relaxing the line search, which the paper's computations exploit. The scale $\gamma_t$ changes only the length of the step, not its direction.

Formalizing it. The claim is proved in the paper by a short computation, and no machine-checked version is known. This mission produces:

• a checked statement of the claim with every hypothesis explicit, including the conjugacy the proof takes as known;
• a corrected version of display (38), which is misprinted;
• reusable definitions of the additive BFGS update and of Beale's direction.

Difficulty

The obvious attempt is to expand both BFGS updates symbolically and compare with Beale's formula. This fails without two facts that are not algebraic identities. The first is that the restart step stays orthogonal to every later gradient, $p_t'g_{k+1}=0$. It needs the affine gradient of a quadratic, the exact search at the restart step, and conjugacy of $p_t$ with all later steps. The second is $y_k'p_t = 0$, which again comes from conjugacy. Beale's formula also has to be matched in its $d$-form: the coefficient $\frac{y'g}{d'y}d$ equals $\frac{y'g}{p'y}p$ only when the step length is nonzero. The descent statements need a different argument: the BFGS update of a positive definite matrix with $p'y>0$ must be shown to remain positive definite, and this has to be done twice.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The inner product $u'v$ is u ⬝ᵥ v, the outer product $uv'$ is vecMulVec u v, and $Hv$ is H *ᵥ v. The quadratic enters only through its gradient A *ᵥ x + c with A.PosDef. The paper's (4) is the case $c = -A\hat x$. Iterates, steps, directions and gradients are sequences indexed by ℕ. Division is Lean's total division. Every statement that divides therefore carries hypotheses making its denominators nonzero: $p_t \ne 0$ and $p_k\ne0$ in the quadratic statements, and $p_t'y_t\ne 0$ or $p'y>0$ in the generic ones.

The conjugacy $p_t'Ap_i=0$ for $t<i\le k$ is a hypothesis, exactly as the paper's proof uses it. It is not derived from a full run of Beale's algorithm. The range $k\le t+n-1$ of Beale's formula is not assumed.

Several formalizations would make the claim easier than the paper's, and none of them is used:

• defining the direction by the expanded formula (34), or the restart matrix by (38);
• adding orthogonality or conjugacy hypotheses beyond those listed;
• concluding only that the two directions are parallel;
• dropping the restart term of Beale's direction;
• allowing a zero denominator.

The generic milestones — (34), (40), (38), (42), (43) and the descent statements — are statements about arbitrary vectors and matrices and are reusable for any BFGS-based method. Proofs of any milestone, and alternative derivations of the goal, are welcome.

Selected references

• D. F. Shanno, Conjugate Gradient Methods with Inexact Searches, Mathematics of Operations Research 3(3) (1978) 244–256. https://doi.org/10.1287/moor.3.3.244
• E. M. L. Beale, A derivation of conjugate gradients, in F. A. Lootsma (ed.), Numerical Methods for Nonlinear Optimization, Academic Press, 1972, 39–43.
• M. J. D. Powell, Restart procedures for the conjugate gradient method, Mathematical Programming 12 (1977) 241–254. https://doi.org/10.1007/BF01593790
• M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, J. Res. Nat. Bur. Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
• S. S. Oren and E. Spedicato, Optimal conditioning of self-scaling variable metric algorithms, Mathematical Programming 10 (1976) 70–90. https://doi.org/10.1007/BF01580654

Motivation

Retailers hold point-of-sale data that their suppliers cannot observe, and large retailers sell access to it through data-sharing programs (Costco's CRX, Walmart's Retail Link and similar programs). When one retailer carries the substitutable products of two competing manufacturers, sharing its demand information is a strategic decision: a manufacturer who knows the demand signal sets his wholesale price in response to it, which changes the retailer's margin and the rival manufacturer's order uncertainty. Whether the retailer should sell the information, to how many manufacturers, and by which protocol, is the question of Shang, Ha and Tong (Management Science 62(1):245–263, 2016).

The paper belongs to the information-sharing literature of Li (2002), Li and Zhang (2008) and Ha, Tong and Zhang (2011), which studies competing supply chains or a single chain. The common-retailer structure differs: the retailer can price-discriminate between the manufacturers through the order in which she offers the information.

Setting

Two manufacturers $i \in \{1, 2\}$ sell substitutable products through one retailer. The demand for product $i$ is

$$q_i = a + \theta - (1+\phi)p_i + \phi p_j,$$

where $p_i$ is the retail price, $\phi > 0$ measures competition, and $\theta$ is a random shock with mean $0$ and variance $\sigma^2 > 0$. The retailer observes a demand signal $Y$ that is unbiased, $E[Y \mid \theta] = \theta$, and has linear expectation: $E[\theta \mid Y] = \beta Y$ for a weight $\beta$ (in the paper $\beta = t\sigma^2/(1+t\sigma^2)$, with $t$ the signal accuracy). The retailing cost is zero, and manufacturer $i$ produces $q$ units at cost $bq + c_d q^2$ with $b, c_d > 0$: a production diseconomy.

The game has four stages.

1. The retailer and the manufacturers contract on information sharing, which fixes each manufacturer's status $X_i \in \{I, U\}$ (informed or uninformed).
2. The retailer observes $Y$ and discloses it truthfully to the informed manufacturers.
3. The manufacturers set wholesale prices $w_i$ simultaneously, an informed one as a function of $Y$. The retailer then sets retail prices.
4. Demand realizes and payoffs are received.

The pricing stage is a Bayesian game. Its equilibrium ex ante profits are $\pi_M(n)$, $\pi_M^I(1)$, $\pi_M^U(1)$ for the manufacturers and $\pi_R(n)$ for the retailer, where $n$ is the number of informed manufacturers. They define a payoff table for the contracting stage.

Two contracting protocols are compared.

• Concurrent contracting: the retailer offers both manufacturers the same payment $T$, and they accept or reject simultaneously; a Pareto-optimal pure equilibrium is the outcome, and the retailer chooses $T$.
• Sequential contracting: the retailer offers one manufacturer $T_f$, he accepts or rejects, then the retailer offers the other $T_s$, and he decides having observed the first decision. The retailer cannot commit to $T_s = T_f$, and the solution is subgame perfect equilibrium.

Formalization targets

Goal: Proposition 4(d)

For every $\phi > 0$, $c_d > 0$ and every signal model, the pricing stage has an equilibrium; for every pricing equilibrium, both contracting games have equilibria; and for every concurrent outcome and every sequential subgame-perfect equilibrium (either first mover),

$$\Pi_R^{C} \le \Pi_R^{S}, \qquad \Pi_M^{S} \le \Pi_M^{C},$$

with both inequalities strict when $c_d > (\sqrt2 - 1)/(1+\phi)$. Here $\Pi_R$ is the retailer's profit after side payments and $\Pi_M$ the manufacturers' total profit net of them. The paper's word "higher" is read as $\ge$ because for small $c_d$ neither protocol sells information and all profits coincide.

Milestones

1. §4.1, Eq. (1): the retailer's best response $\hat p_i = \frac12(a + \beta Y + w_i)$ and the resulting demand.
2. Lemma 1: the pricing equilibrium exists, is unique, and is linear in $Y$.
3. §4.2: the closed forms of the seven ex ante profits.
4. Lemma 3: $\pi_M(2) > \pi_M^I(1) > \pi_M(0) > \pi_M^U(1)$, $\pi_R(0) > \pi_R(1) > \pi_R(2)$, $\pi_R(1) - \pi_R(2) > \pi_R(0) - \pi_R(1)$.
5. Proposition 1(b): without contracting, no information is shared.
6. Propositions 2 and 3: thresholds $c_d^C$ and $c_d^{S1}, c_d^{S2}$, depending only on $\phi$, at which the number of informed manufacturers changes under each protocol.
7. Proposition 4(a): $c_d^{S1} < c_d^C < c_d^{S2}$.

Significance

The result. Proposition 4(d) says that the order of the offers transfers surplus: selling information one manufacturer at a time lets the retailer exploit the manufacturers' fear of being the only uninformed firm, which raises her profit and lowers theirs. Propositions 2 and 3 show that concurrent contracting shares with both manufacturers or with neither, while sequential contracting can end with only one informed manufacturer. Together they give a complete map of the equilibrium sharing decisions in $(c_d, \phi)$ (Figure 1 of the paper).

Formalizing it. The results are proved in the paper, partly by "it can be shown" and "straightforward" steps: Lemma 3's proof is omitted, and so is the convexity of the function whose root is $c_d^{S2}$. No part of the paper has a machine-checked proof. A complete formalization would check every such step and make the equilibrium notions precise, in particular the Pareto selection and the tie-breaking at the thresholds, where the retailer is exactly indifferent.

Difficulty

Most of the work is in the contracting stage, not the algebra. The pricing stage must be solved over all square-integrable strategies measurable in the signal. Uniqueness is then almost sure and rests on the linear-expectation identities $E[\theta Y] = \sigma^2$ and $E[Y^2] = \sigma^2/\beta$. The concurrent game has multiple equilibria for intermediate payments, and the retailer's optimum lies at a payment where two equilibria coexist. The sequential game is a three-stage game with a continuum of offers: at each threshold the retailer is indifferent, and an SPE exists only if acceptance at indifference is chosen correctly. The threshold $c_d^{S2}$ has no closed form; it is the root of a convex rational function of $c_d$.

Formalization scope

The Lean development lives in the namespace InfoSharing.Diseconomy. Conventions:

• The probability space carries $\theta$ and $Y$ in $L^2$, with the two conditional-expectation identities holding almost everywhere. $\beta$ is a parameter fixed by $E[\theta \mid Y] = \beta Y$; Ericson's formula for $\beta$ is not formalized.
• Wholesale strategies are measurable, square-integrable functions of the signal value, and constants for an uninformed manufacturer. A pricing equilibrium is ex ante optimality over such strategies, which is equivalent to the paper's conditional optimization. The retailer's rule must be a best response at every wholesale-price pair.
• The payoff table is produced by an arbitrary pricing-equilibrium family, not by the §4.2 closed forms. A formalization that takes the closed forms as the definition of the profits would reduce the goal to algebra and a $2 \times 2$ game, and is ruled out.
• Payments are nonnegative, only pure strategies are used in the contracting games, and the concurrent outcome selects, among Pareto-optimal equilibria, the one best for the retailer.
• Threshold statements use two clauses: the printed value is attained on the closed region, and it is the only value on the region's interior. The thresholds depend only on $\phi$.
• Demands may be negative (θ is unbounded), as in the paper's formulas.

A complete development needs:

• the conditional-expectation algebra behind Lemma 1 and §4.2;
• rational-function inequalities for Lemma 3;
• a case analysis of the two contracting games.

The model layer is shared with the companion mission on production economy.

Selected references

• G. Shang, A. Y. Ha, S. Tong, Information Sharing in a Supply Chain with a Common Retailer, Management Science 62(1):245–263, 2016. https://doi.org/10.1287/mnsc.2014.2127
• W. A. Ericson, A note on the posterior mean of a population mean, Journal of the Royal Statistical Society B 31(2):332–334, 1969.
• L. Li, Information sharing in a supply chain with horizontal competition, Management Science 48(9):1196–1212, 2002. https://doi.org/10.1287/mnsc.48.9.1196.177
• L. Li, H. Zhang, Confidentiality and information sharing in supply chain coordination, Management Science 54(8):1467–1481, 2008. https://doi.org/10.1287/mnsc.1070.0851
• A. Y. Ha, S. Tong, H. Zhang, Sharing imperfect demand information in competing supply chains with production diseconomies, Management Science 57(3):566–581, 2011. https://doi.org/10.1287/mnsc.1100.1295
• X. Vives, Oligopoly Pricing: Old Ideas and New Tools, MIT Press, 1999.

Motivation

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested agents: the designer can pay the agents, and must choose payments so that each agent's own interest leads it to reveal what the algorithm needs. Nisan and Ronen introduced the framework with task scheduling on unrelated machines as the running example (Nisan–Ronen 2001). In the basic model, where payments depend only on what the agents declare, they showed that no truthful mechanism approximates the optimal make-span within a factor below 2, and that the natural mechanism only reaches a factor $n$.

Their Section 5 changes the information available: in a mechanism with verification the payments may also depend on the times in which the tasks were actually performed. With this extra information, an exact optimizer becomes a strongly truthful mechanism (Theorem 5.1, the Compensation-and-Bonus mechanism). Exact scheduling on unrelated machines is NP-hard, so the question is whether an approximation algorithm can take the optimizer's place. Theorem 5.6 of the paper shows that plugging a non-optimal algorithm into Compensation-and-Bonus destroys truthfulness in general. Theorem 5.9, the subject of this mission, shows that for the bounded problem a specific approximation scheme, the rounding algorithm of Horowitz and Sahni (1976), can be combined with a modified payment rule to give a truthful mechanism whose outcome is within a factor $1+\varepsilon$ of optimal.

Setting

There are $n$ agents and $k$ tasks. Agent $i$ needs time $t^i_j$ for task $j$; the vector $t = (t^i_j)$ is the type vector, and agent $i$ alone knows its row $t^i$. In the bounded scheduling problem (Definition 33) there are fixed numbers $0 < a < b$ with $a \le t^i_j \le b$ for all $i, j$, and every declaration lies in the same range. An allocation $x$ assigns each task to one agent; $x^i$ is the set of tasks of agent $i$.

A strategy of agent $i$ has two parts: a declaration $d^i \in [a,b]^k$, and an execution, which for each decision $x$ of the mechanism specifies the actual time $\tilde t_j \ge t^i_j$ in which agent $i$ performs each task $j \in x^i$. The mechanism chooses $x = x(d)$ from the declarations alone and afterwards observes the actual times $\tilde t$. The objective is the make-span with actual times,

$$g(x,\tilde t) = \max_i \sum_{j \in x^i} \tilde t_j .$$

Agent $i$ receives a payment $p^i$ and has utility $p^i - \sum_{j \in x^i} \tilde t_j$.

The corrected time vector of agent $i$ keeps agent $i$'s actual times on its own tasks and the other agents' declarations elsewhere: $\mathrm{corr}^i(x,d,\tilde t)_j = \tilde t_j$ for $j \in x^i$ and $d^l_j$ for $j \in x^l$, $l \ne i$. For a step $\delta > 0$, $\hat r = \delta\lceil r/\delta\rceil$ rounds $r$ up to a multiple of $\delta$, and $\hat g(x,\tau) = g(x,\hat\tau)$.

The rounding mechanism (Definition 34) allocates with an algorithm that exactly solves the problem with rounded declarations $\hat d$, and pays

$$p^i = \sum_{j\in x^i}\tilde t_j \;-\; \hat g\big(x, \mathrm{corr}^i(x, d, \tilde t)\big).$$

The first term, the compensation, uses exact actual times; the second, the bonus, uses rounded quantities.

A strategy is dominant if it is a best response to every declarations and executions of the others. The mechanism is truthful if every agent has a dominant strategy that declares its true type.

Formalization targets

Goal: Theorem 5.9 without running time

For every $\varepsilon > 0$, every $0 < \delta \le \varepsilon a$ and every allocation algorithm solving the rounded problem exactly, the rounding mechanism is truthful, and at every profile of dominant strategies from the class named in the proof (declarations with the true rounded values, executions whose rounded times equal the rounded true times),

$$g\big(x(d),\tilde t\big) \le (1+\varepsilon)\, g(y,t) \quad \text{for every allocation } y .$$

Milestones

1. The solution of the rounded problem is a $(1+\varepsilon)$-approximation: $g(x,\hat t) \le g(y,\hat t)\ \forall y$ implies $g(x,t) \le (1+\varepsilon) g(y,t)\ \forall y$.
2. After rounding, $\hat g$ is the make-span, $\hat g(x,\mathrm{corr}^*(x,d)) = g(x,\hat d)$, and each agent's utility equals its rounded bonus.
3. Every strategy with the true rounded values is dominant.
4. When all agents follow such strategies, the outcome is a $(1+\varepsilon)$-approximation.
5. Truth-telling with minimal execution is dominant; hence the mechanism is truthful.

Significance

The result shows that verification does more than make exact optimization truthful: it lets a polynomial-time approximation scheme be implemented in dominant strategies, provided the bonus is computed on the same rounded instance the algorithm optimizes. This contrasts with Theorem 5.6, where an arbitrary approximation algorithm inside Compensation-and-Bonus is not truthful, and with the factor-2 lower bound of the basic model. The principle it illustrates is that the payments must reward exactly the objective the algorithm optimizes.

The paper gives only a proof sketch. Formalizing it makes the argument's hypotheses explicit: which rounding step suffices, what the allocation algorithm must satisfy, and over which strategy profiles the approximation guarantee holds. No machine-checked version of this theorem or of the Compensation-and-Bonus argument is known to exist.

Difficulty

The sketch reduces the theorem to "arguments similar to those in 5.1", but the rounded setting departs from Theorem 5.1 in two ways. Rounding is many-to-one, so an agent's declaration and execution are pinned down only up to their rounded values, and the algorithm's optimality holds only for the rounded instance. Consequently the claim that the strategies with the true rounded values are the only dominant ones does not survive arbitrary tie-breaking: an agent that is always favoured on ties can overstate its rounded time by one step without ever losing, and two such lies at one profile can push the make-span above the $(1+\varepsilon)$ bound. The approximation guarantee therefore has to be stated for the strategy class the proof identifies, not derived from dominance alone. The remaining steps require exact bookkeeping of rounding across sums and of the corrected time vectors, which a proof sketch leaves implicit.

Formalization scope

• Agents are Fin n with [NeZero n], tasks Fin k; allocations are functions Fin k → Fin n; the make-span is a Finset.sup' over agents. Types and declarations satisfy a ≤ t i j ≤ b with 0 < a < b; actual times are only bounded below by the true times.
• roundUp δ r = δ * ⌈r / δ⌉. The statement holds for every $\delta \in (0,\varepsilon a]$, which covers the intended choice $\delta = \varepsilon a$; the paper leaves $\delta$ as "a function of $a$ and $\varepsilon$".
• The Horowitz–Sahni dynamic program is not formalized. The allocation algorithm is a parameter with the hypothesis that it solves the rounded problem exactly; ties are arbitrary, and the goal holds for every such algorithm. Running time ("polynomial time") is out of scope, and with it the role of the upper bound $b$, which is kept as part of the problem.
• An execution is a function of the decision (Definition 18). Dominance quantifies over all declarations in $[a,b]$ and all executions of the others.
• The payment uses the allocation $x(d)$ in the bonus. Definition 34 prints $x(\hat t)$; since the rounding algorithm rounds the declarations itself, $x(d)$ is the allocation actually computed. The hat on $\mathrm{corr}$ is absorbed by $\hat g$.
• The goal's approximation part is restricted to dominant profiles of the class named in the proof, because the unrestricted form (Definition 3, every dominant profile) is false for some tie-breaking rules; an explicit two-agent, one-task instance is recorded in the goal's Formalization Note.
• A formalization that measures the approximation with declared rather than actual times, lets the allocation read the true types, or states the approximation only at the truthful profile while claiming the general form, does not formalize this theorem.

Useful infrastructure: lemmas on Int.ceil rounding of finite sums and on Finset.sup' monotonicity, and a reusable model of mechanisms with verification. Proofs of the milestones in any order are welcome.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• E. Horowitz, S. Sahni, Exact and Approximate Algorithms for Scheduling Nonidentical Processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951

Motivation

Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: the algorithm must compute a good solution and, through payments, make it in each agent's interest to report its input honestly. Nisan and Ronen introduced the field with the problem of scheduling tasks on unrelated machines, where each machine is an agent that privately knows how long it needs for every task (Nisan–Ronen 2001).

The classical tool for truthfulness, the Vickrey–Groves–Clarke (VGC) family of mechanisms, requires the allocation to be exactly optimal. Exact optimization is often computationally out of reach: minimizing the make-span on unrelated machines is NP-hard, and even approximating it within a factor below 3/2 is NP-hard (Lenstra–Shmoys–Tardos 1990). A mechanism designer would therefore like to plug an approximation algorithm into a truthful mechanism and keep truthfulness. This mission formalizes a result showing that the simplest way of doing so fails in the model with verification, where the mechanism may pay after the tasks are performed and observes the actual execution times.

Timeline.

• 1999/2001: Nisan and Ronen define mechanisms with verification and the Compensation-and-Bonus mechanism, prove it strongly truthful when its allocation algorithm is optimal (their Theorem 5.1), and prove that replacing the optimal algorithm by a non-optimal approximation algorithm destroys truthfulness (Theorem 5.6, the goal here). They remark that a similar argument applies to VGC mechanisms.
• 2002: Lehmann, O'Callaghan and Shoham show the analogous failure for VGC payments with approximate allocation in combinatorial auctions (JACM 2002).
• 2007: Nisan and Ronen study which approximation algorithms can be made truthful within the VGC framework (JAIR 2007).

Setting

There are $n \ge 1$ agents and $k$ tasks. The type of agent $i$ is a vector $t^i = (t^i_1,\dots,t^i_k)$ of positive reals, $t^i_j$ being the minimum time agent $i$ needs for task $j$; a type vector is $t = (t^1,\dots,t^n)$. An allocation $x = (x^1,\dots,x^n)$ gives each task to one agent. The make-span is

$$g(x,t) = \max_i \sum_{j\in x^i} t^i_j,$$

and $x$ is optimal for $t$ if $g(x,t)\le g(y,t)$ for every allocation $y$.

In the model with verification, an agent's strategy has two parts: a declaration $d^i$ (any positive vector) and an execution plan that, for every allocation the mechanism may choose, fixes the actual time $\tilde t_j \ge t^i_j$ in which the agent performs each task $j$ it receives. An allocation algorithm $x(\cdot)$ maps the declarations to an allocation $x(d)$; the tasks are then executed, producing actual times $\tilde t$.

The Compensation-and-Bonus mechanism based on $x(\cdot)$ pays agent $i$

$$p^i(d,\tilde t) = \sum_{j\in x^i(d)} \tilde t_j \;-\; g\bigl(x(d), \operatorname{corr}^i(x(d),d,\tilde t)\bigr),$$

a compensation for the time actually spent plus a bonus equal to minus the make-span computed from agent $i$'s actual times on its own tasks and the other agents' declared times on theirs (the corrected time vector $\operatorname{corr}^i$). The agent's utility is its payment minus the time it spends. A strategy is dominant if it is at least as good as every alternative whatever the other agents declare and execute; the mechanism is truthful if every agent of every type has a dominant strategy that declares its true type.

Formalization targets

Goal: Theorem 5.6

Let $x(\cdot)$ be an allocation algorithm such that, for some real $c$,

$$g\bigl(x(t),t\bigr) \le c\, g(y,t)\quad\text{for every positive } t \text{ and every allocation } y,$$

and such that $g(y,t) < g(x(t),t)$ for some positive $t$ and some allocation $y$. Then the Compensation-and-Bonus mechanism based on $x(\cdot)$ is not truthful.

The ratio $c$ is arbitrary and existentially quantified: the theorem holds for every finite approximation ratio, so it is stated without a constant.

Milestones

• Claim 5.7. If the mechanism based on $x(\cdot)$ is truthful, $o$ is optimal for $t$ and $M$ is at least every entry of $t$, then replacing one agent's type by $t^i_j$ on $o^i$ and $M$ elsewhere gives a type vector $t'$ with $g(x(t'),t') \ge g(x(t),t)$.
• Corollary 5.8. Under the same assumptions, the type vector $s$ that makes this replacement for every agent satisfies $g(x(s),s) \ge g(x(t),t)$.
• Final step. $g(o,s) = g(o,t)$, $o$ is optimal for $s$, and every allocation $y\ne o$ has $g(y,s)\ge M$.

Significance

The result. Theorem 5.1 of the same paper shows that with an optimal algorithm the Compensation-and-Bonus mechanism is a strongly truthful implementation of make-span minimization. Theorem 5.6 shows that this guarantee is tied to exact optimization: it does not survive replacing the optimizer by any non-optimal approximation algorithm, whatever its ratio. It explains why the paper then turns to a restricted problem (bounded scheduling) and a mechanism designed around a specific rounding algorithm, and it is an early instance of the general tension between approximation and incentive compatibility.

Formalizing it. The result is proved in the paper; to the best of the platform's catalog it has not been formalized. The mission produces a machine-checked model of mechanisms with verification (declarations together with execution plans that may depend on the decision), the Compensation-and-Bonus payment rule for an arbitrary allocation algorithm, and Definition 19 truthfulness, together with a checked proof of the impossibility.

Difficulty

The argument is short on paper; the difficulty lies in the model. The paper's "$\infty$" is not a number, and a faithful statement must replace it by a finite value that is large enough to conflict with the approximation ratio yet keeps every type positive and entrywise above the true types; both requirements refer to data fixed earlier in the argument. The incentive step compares utilities in a mechanism where an agent's strategy is a declaration and an execution plan that may depend on the decision, and where the bonus mixes the agent's actual times with the other agents' declarations, so a naive reading in which only declarations matter (the direct-revelation model of §2) does not capture the claim. Finally, Corollary 5.8 concerns a type vector modified at every agent, while Claim 5.7 modifies one agent at a time, so the claim must be applicable at type vectors that are no longer the original one.

Formalization scope

• Agents are Fin n with [NeZero n], tasks Fin k, allocations are functions Fin k → Fin n, types and declarations are positive real vectors. Make-spans are Finset.sup' over the nonempty set of agents. With no agents no allocation algorithm meets the hypotheses, so requiring $n\ge 1$ loses nothing.
• An execution plan is a function of the allocation; feasibility is $\tilde t_j \ge t^i_j$ on the agent's own tasks. In the dominance quantifier the other agents' declarations are positive and their execution plans arbitrary; the agent's alternative declarations are positive and its alternative plans feasible for its true type.
• The allocation algorithm is an arbitrary function of the declarations; "approximation algorithm" is the hypothesis $\exists c$ above, "non-optimal" the hypothesis of one positive witness. The optimal allocation $\mathrm{opt}(t)$ in the milestones is any optimal allocation $o$, supplied as a parameter.
• The paper's $\infty$ is a real parameter $M$ with $M \ge t^l_j$ for all $l,j$; extended reals are not used.
• Claim 5.7 is stated for an arbitrary agent $i$, not only for agent 1, so that Corollary 5.8 can iterate it.
• Running time is not modelled; "algorithm" means function.
• Dropping the approximation hypothesis makes the statement false: an allocation rule that ignores the declarations is non-optimal, yet its Compensation-and-Bonus mechanism is truthful. Stating only "not strongly truthful", or proving the theorem for a fixed instance, would be a weaker claim.

Welcome contributions: proofs of the milestones and the goal, and reusable lemmas about the corrected time vector and the monotonicity of the make-span in the time vector.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• D. Lehmann, L. I. O'Callaghan, Y. Shoham, Truth revelation in approximately efficient combinatorial auctions, Journal of the ACM 49 (2002) 577–602. https://doi.org/10.1145/585265.585266
• N. Nisan, A. Ronen, Computationally Feasible VCG Mechanisms, Journal of Artificial Intelligence Research 29 (2007) 19–47. https://doi.org/10.1613/jair.2046
• E. Horowitz, S. Sahni, Exact and approximate algorithms for scheduling nonidentical processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951

Motivation

Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: an algorithm must not only compute a good solution but also pay the agents so that reporting their data truthfully is in their own interest. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001) with task scheduling on unrelated machines as the model problem. Each machine is owned by an agent who alone knows how long it takes for each task; the designer wants a schedule of small make-span.

The paper gives a truthful mechanism, MinWork, whose make-span is within a factor $n$ of optimal, and a lower bound of $2$ for every truthful mechanism. It conjectures that no truthful mechanism beats $n$ (Conjecture 4.9) and proves the conjecture for two natural classes. This mission is about one of them, additive mechanisms (Theorem 4.10, p. 180).

Timeline of the gap between $2$ and $n$:

• 1999/2001: Nisan and Ronen prove the lower bound $2$ for all truthful mechanisms and $n$ for additive and for local mechanisms.
• 2007: Christodoulou, Koutsoupias and Vidali raise the general lower bound to $1+\sqrt 2$ for $n\ge 3$ (SODA 2007; Algorithmica 2009).
• 2008: Christodoulou, Koutsoupias and Vidali characterize the truthful mechanisms for two machines (ESA 2008; arXiv 0807.3427); in parallel, Dobzinski and Sundararajan (EC 2008) characterize them and show that for two machines no truthful mechanism beats $2$.
• 2023: Christodoulou, Koutsoupias and Kovács prove the Nisan–Ronen conjecture: no truthful mechanism beats $n$ (STOC 2023; arXiv 2301.11905).

Setting

There are $n$ agents $i=1,\dots,n$ and $k$ tasks $j=1,\dots,k$. The type of agent $i$ is a vector $t^i=(t^i_1,\dots,t^i_k)$ of positive reals, $t^i_j$ being the time agent $i$ needs for task $j$; a type vector $t=(t^1,\dots,t^n)$ collects all types, and $t^{-i}$ denotes the types of the agents other than $i$. An allocation $x=(x^1,\dots,x^n)$ is a partition of the tasks, $x^i$ being the set given to agent $i$. For a set $X$ of tasks write $t^i(X)=\sum_{j\in X}t^i_j$. The make-span is

$$g(x,t)=\max_i t^i(x^i).$$

A direct mechanism $m=(x,p)$ maps every declared type vector $t$ to an allocation $x(t)$ and to payments $p^i(t)$ handed to the agents. An agent with true type $t^i$ gets utility $p^i(t)-t^i(x^i(t))$. The mechanism is truthful if, whatever the others declare, no agent gains by declaring a type other than its true one. It is a $c$-approximation if $g(x(t),t)\le c\,g(y,t)$ for every positive type vector $t$ and every allocation $y$.

The price offered for a set $X$ to agent $i$ (Definition 12) is the payment $p^i(t'^i,t^{-i})$ at any declaration $t'^i$ for which the mechanism gives agent $i$ exactly $X$, and $0$ if there is no such declaration. For truthful mechanisms this is well defined (Proposition 4.4, Independence). The mechanism is additive (Definition 13) if

$$p^i(X,t^{-i})=\sum_{j\in X}p^i(\{j\},t^{-i})$$

for every agent $i$, type vector $t$ and set $X$ of tasks. MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is additive.

Formalization targets

Goal: Theorem 4.10

For $n\ge 1$ agents and $k\ge n^2$ tasks, for every truthful additive mechanism $(x,p)$ and every real $c<n$,

$$\exists\,t,\ \exists\,y:\qquad g\bigl(x(t),t\bigr)>c\cdot g(y,t).$$

The goal leaves the mechanism, its tie-breaking and $c$ completely general. It says that the ratio $n$ of MinWork is optimal among additive mechanisms.

Milestones

1. Proposition 4.4 (Independence): the payment depends on agent $i$'s declaration only through its allocation.
2. Proposition 4.5 (Maximization): $x^i(t)$ maximizes $p^i(X,t^{-i})-t^i(X)$ over the sets $X$ agent $i$ can obtain against $t^{-i}$.
3. Pigeonhole: with $k\ge n^2$ tasks some agent receives at least $n$ tasks.
4. Claim 4.11: at the all-ones type vector $t$, lowering agent $i$'s times to $1-\epsilon$ on $x^i(t)$ and $\epsilon$ elsewhere keeps all of $x^i(t)$ with agent $i$, provided the empty set is attainable for agent $i$.
5. The ratio step: at that perturbed type vector, an allocation giving agent $i$ a fixed set of $n$ tasks has make-span at least $(1-\epsilon)n$, while some allocation has make-span at most $1+k\epsilon$.

Significance

Theorem 4.10 shows that the gap between MinWork's ratio $n$ and the general lower bound $2$ cannot be closed by any mechanism that prices tasks separately, and so any better mechanism would have to couple the prices of different tasks. It was the first class-restricted confirmation of Conjecture 4.9, which was eventually proved for all truthful mechanisms (Christodoulou–Koutsoupias–Kovács 2023). The additive case is the cleanest entry point: its proof needs only the two basic properties of truthful mechanisms, Independence and Maximization, which every later lower bound also uses.

All results here are proved on paper, and none has a machine-checked proof on Prove2Me as of this mission's drafting. The mission produces a formal model of scheduling mechanisms and prices that other lower bounds can reuse, formal statements of Independence and Maximization, and a formal proof of Theorem 4.10. Along the way the formalization corrects two points of the printed argument (see Formalization scope).

Difficulty

The work is to extract prices from an arbitrary truthful mechanism. Prices are defined through the attainable sets of Definition 12. A natural first idea replaces the mechanism by per-task prices $q^i_j(t^{-i})$ that the agent maximizes against. That gives a different class, because Definition 13 constrains the price of every set of tasks, including sets the mechanism never allocates, whose price is $0$.

Claim 4.11 is the critical step, and its printed argument does not go through for an arbitrary truthful additive mechanism. It needs the empty set to be attainable with price $0$. For a mechanism with a bounded ratio this holds, because a very slow agent must receive nothing, but this has to be derived from the approximation hypothesis. From that, one has to show that every task of $x^i(t)$ carries a single-task price of at least $1$. The final step also needs care. The paper's "w.l.o.g. $|x^1|=n$" is a further reduction, and the paper's bound $g\ge|x^1|$ has to be replaced by $(1-\epsilon)|x^1|$.

Formalization scope

• Representation. Agents are Fin n, tasks Fin k, type vectors Fin n → Fin k → ℝ, and an allocation is a map Fin k → Fin n sending each task to its agent. taskSet x i is $x^i$, and the make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]). A mechanism is a pair alloc, pay of arbitrary functions; nothing about its tie-breaking is fixed.
• Standing assumptions. Types are positive. Truthfulness, additivity and approximation quantify over positive type vectors only. Utility is quasi-linear, with payments handed to the agent.
• Prices. price follows Definition 12 literally: the payment at a Classical.choose witness declaration when the set is attainable, and $0$ otherwise. Additivity (IsAdditive) is required for every set of tasks, attainable or not, as Definition 13 states. It is a condition on prices, not on the payment function.
• Explicit threshold. The goal assumes $k\ge n^2$, the value the paper's proof starts from; the printed theorem does not mention $k$. It is stated for every $n\ge1$; at $n=1$ it holds because all allocations coincide.
• Printed slips, corrected. (1) Proposition 4.5 is stated over attainable sets: over all sets, with the price $0$ of unattainable sets, it fails for truthful mechanisms that never give the agent nothing and charge it. (2) Claim 4.11 carries the added hypothesis that $\emptyset$ is attainable for agent $i$. Without it the claim is false: a mechanism that always gives agent $i$ its $|x|$ cheapest tasks and pays nothing is truthful and additive. The claim is stated for an arbitrary agent $i$ instead of "agent 1 after relabelling". (3) The ratio step states $g\ge(1-\epsilon)n$ where the paper prints $g\ge|x^1|\ge n$, and states the paper's w.l.o.g. $|x^1|=n$ as a hypothesis of the step, not of the goal.
• Out of scope. Running time and the revelation principle are not modelled; the goal is stated for truthful direct mechanisms, as §4.3 fixes.
• Ruled out. A trivializing encoding would define additivity through the payment function instead of the prices of Definition 12, fix $n$, prove the ratio for one $c<n$ only, or drop truthfulness. The last makes the claim false: an optimal allocation rule with zero payments is additive and a $1$-approximation. The goal here quantifies over every $n$, every $c<n$ and every truthful additive mechanism.
• Non-vacuity. Every hypothesis of the goal except the ratio is satisfiable (a constant allocation with zero payments is truthful and additive), and the bound is tight by MinWork.
• Contributions welcome. Proofs of the milestones, a proof that a bounded-ratio mechanism makes $\emptyset$ attainable for every agent, and reuse of the model for the local-mechanism bound (Theorem 4.12).

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, SODA 2007; Algorithmica 55, 2009. https://doi.org/10.1007/s00453-008-9165-3
• G. Christodoulou, E. Koutsoupias, A. Vidali, A characterization of 2-player mechanisms for scheduling, ESA 2008. https://arxiv.org/abs/0807.3427
• S. Dobzinski, M. Sundararajan, On characterizations of truthful mechanisms for combinatorial auctions and scheduling, EC 2008, pp. 38–47.
• G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023. https://doi.org/10.1145/3564246.3585176 (arXiv:2301.11905)

Motivation

The capacitated vehicle routing problem (CVRP) asks for minimum-cost routes, starting and ending at a depot, that serve every customer exactly once without any vehicle carrying more than its capacity. It is one of the central problems of operations research and logistics, and exact algorithms for it have been built on branch-and-cut for three decades: a linear programming relaxation is strengthened at every node of a search tree by adding valid inequalities that the current LP solution violates.

The most important of these inequalities are the capacity inequalities. Deciding whether an LP solution violates one of them is strongly NP-hard, so practical codes rely on heuristics, and most heuristics first shrink the support graph: groups of customers are contracted into single supervertices so that the search runs on a smaller graph. Shrinking is only useful if it is safe, meaning it cannot hide a violated inequality. Before the work of Lysgaard, Letchford and Eglese, the standard safe rule allowed shrinking a single edge whose LP value is at least one (Augerat et al. 1998; Ralphs et al. 2003). Lysgaard, Letchford & Eglese (2004), whose separation routines were released as the widely used CVRPSEP package, generalized the rule to customer sets of any size in their Proposition 1, the only numbered result of the paper.

Setting

Let $G = (V, E)$ be the complete undirected graph on $V = \{0, 1, \dots, n\}$. Vertex $0$ is the depot and $V_c = \{1, \dots, n\}$ are the customers. Vehicles have capacity $Q > 0$ and each customer $i$ has an integer demand $q_i$ with $0 < q_i \le Q$. An LP point is a vector $x = (x_e)_{e \in E}$; $x_{ij}$ and $x_{ji}$ are the same variable, and LP solutions satisfy $x \ge 0$.

For a vertex set $S$, $\delta(S)$ is the set of edges with exactly one end-vertex in $S$ (edges to the depot included), and $x(\delta(S)) = \sum_{e \in \delta(S)} x_e$ is its cut value. For a customer set $S \subseteq V_c$:

• $q(S) = \sum_{i \in S} q_i$ is its total demand;
• $r(S)$, the bin-packing number, is the minimum number of bins of capacity $Q$ into which the items of sizes $q_i$, $i \in S$, can be packed;
• $k(S) = \lceil q(S)/Q \rceil \le r(S)$ is the rounded capacity bound.

The capacity inequalities and the rounded capacity inequalities (RCIs) are

$$x(\delta(S)) \ge 2r(S) \quad\text{and}\quad x(\delta(S)) \ge 2k(S), \qquad S \subseteq V_c,\ |S| \ge 2 .$$

The violation of such an inequality at $x$ is $2r(S) - x(\delta(S))$ (resp. $2k(S) - x(\delta(S))$); it is violated when this is positive.

Shrinking a customer set $S$ contracts it to one supervertex. The supervertices of the shrunk graph are then $S$ and the single customers outside $S$, so a union of supervertices is a customer set $T'$ with $S \subseteq T'$ or $S \cap T' = \emptyset$. Shrinking $S$ is safe if for every customer set $T$ with $|T| \ge 2$ whose inequality is violated, there is such a union $T'$ with $|T'| \ge 2$ and at least the same violation.

Formalization targets

Goal: Proposition 1

For every $x \ge 0$ and every customer set $S$ with

$$x(\delta(S)) \le 2 \qquad\text{and}\qquad x(\delta(R)) \ge 2 \ \text{ for every nonempty proper subset } R \subsetneq S,$$

shrinking $S$ is safe for the capacity inequalities $x(\delta(T)) \ge 2r(T)$.

Milestones (proof of Proposition 1, p. 426)

1. Monotonicity of the bin-packing number: $2r(S \cup T) - 2r(T) \ge 0$.
2. Submodularity of the cut function, in the paper's arrangement: $x(\delta(T)) - x(\delta(S \cup T)) \ge x(\delta(S \cap T)) - x(\delta(S))$ for $x \ge 0$.
3. The crossing-set inequality: if $T$ crosses $S$ ($T \cap S$, $T \setminus S$, $S \setminus T$ all nonempty), then $2r(T) - x(\delta(T)) \le 2r(S \cup T) - x(\delta(S \cup T))$.

Further statements on the same page

4. The same shrinking condition is safe for the rounded capacity inequalities $x(\delta(T)) \ge 2k(T)$, which are the inequalities the algorithm separates.
5. The paper's first separation heuristic checks the RCI for each connected component $S_i$ of the support graph on the customers, for each complement $V_c \setminus S_i$, and for the union of the components with no support edge to the depot. At an integer point satisfying the degree equations $x(\delta(\{i\})) = 2$ and the bounds $x_{ij} \in \{0,1\}$, $x_{0j} \in \{0,1,2\}$, this heuristic finds a violated RCI whenever one exists. This claim is stated in the paper without proof and is not needed for the goal.

Significance

Proposition 1 justifies contracting whole groups of customers before running separation heuristics, which shrinks the graph those heuristics work on while preserving every violated capacity inequality up to its violation. The rule is part of the separation routines of CVRPSEP and of later branch-and-cut and branch-cut-and-price codes for vehicle routing that reuse them.

The result is proved in the paper; to the best of the platform's records, none of it is formalized. The mission produces a reusable formal layer for the two-index CVRP formulation: cut values on the complete graph with a depot, the bin-packing number, the rounded capacity bound, and the notion of safe shrinking. Submodularity of the cut function (target 2) is a classical fact that the paper cites rather than proves; the platform already has a related statement for symmetric weight matrices on Boolean regions (EmergentGeometry.cutWeight_submodular), in a different representation. Target 5 records a claim of the paper that it asserts without proof.

Difficulty

When the violated set $T$ contains $S$ or misses it, $T$ itself is a union of supervertices and there is nothing to show. The difficulty is a set $T$ that crosses $S$: no union of supervertices is obviously as violated as $T$, because enlarging $T$ can raise its cut value — $x(\delta(S \cup T))$ can be smaller or larger than $x(\delta(T))$ depending on the edges leaving $S \setminus T$ — and the hypotheses on $S$ say nothing about $T$ directly. Both hypotheses on $S$ and the sign condition $x \ge 0$ matter here; for signed $x$ the statement fails. A violated $T$ strictly inside $S$ is not a crossing set in the paper's sense and has to be handled as well.

On the formal side, the bin-packing number is an optimum of a combinatorial problem; its properties must be derived from a definition by assignments to bins, and it is well defined only because every demand fits in one vehicle. Target 5 needs a structural understanding of integer points satisfying the degree equations, which the paper does not supply.

Formalization scope

Vertices are Fin (n+1), the depot is 0, and a customer set is a Finset (Fin (n+1)) not containing 0. The edge vector is a function x : Sym2 (Fin (n+1)) → ℝ on unordered pairs, and the cut value is ∑ i ∈ S, ∑ j ∈ Sᶜ, x s(i, j), which includes the edges to the depot. The capacity $Q$ is real (the paper does not say it is an integer) and demands are natural numbers with $0 < q_i \le Q$ for customers. The bin-packing number is the least number of bins over assignments of the customers of $S$ to bins of total demand at most $Q$; under $q_i \le Q$ this minimum exists. Of the LP point only $x \ge 0$ is assumed in Proposition 1 and targets 1–4, which is at least as strong as the paper's setting. The hypothesis "$x(\delta(R)) \ge 2$ for all $R \subset S$" ranges over nonempty proper subsets.

A formalization that lets $R = \emptyset$ in that hypothesis is vacuous, because $x(\delta(\emptyset)) = 0$; one that drops the condition "$S \subseteq T'$ or $S \cap T' = \emptyset$" from safe shrinking is trivial (take $T' = T$); and one that defines $r$ as $k$, as an arbitrary monotone function, or with a junk value $0$, or that omits the depot edges from the cut, states a different result. None of these is the mission's statement.

Needed infrastructure: finite sums over cuts of Sym2-indexed vectors, a working API for the bin-packing number, and, for target 5, connected components of the support graph (SimpleGraph.Reachable). The cut-function lemmas and the bin-packing number are reusable for any later formalization of CVRP polyhedra (framed capacity, comb and multistar inequalities). Contributions of general lemmas about cut functions on complete graphs are welcome as separate theorems.

Selected references

• J. Lysgaard, A. N. Letchford, R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming Ser. A 100 (2004) 423–445. https://doi.org/10.1007/s10107-003-0481-8
• G. L. Nemhauser, L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
• P. Augerat, J. M. Belenguer, E. Benavent, A. Corberán, D. Naddef, Separating capacity constraints in the CVRP using tabu search, European Journal of Operational Research 106 (1998) 546–557. https://doi.org/10.1016/S0377-2217(97)00290-7
• T. K. Ralphs, L. Kopman, W. R. Pulleyblank, L. E. Trotter, On the capacitated vehicle routing problem, Mathematical Programming 94 (2003) 343–359. https://doi.org/10.1007/s10107-002-0323-0

Motivation

Column generation solves linear programs with far more columns than can be written down: a restricted master problem holds a few columns, its dual multipliers are passed to a pricing problem, and the pricing problem returns a column to add. It is the standard engine behind branch-and-price for vehicle routing, crew scheduling and cutting stock, where the master problem is very often a set-partitioning problem (Lübbecke and Desrosiers 2005; Desrosiers and Lübbecke 2005).

Which column the pricing problem returns matters. The classical Dantzig rule picks the column of most negative reduced cost, but in set-partitioning masters with identical subproblems this rule tends to produce columns that are "weak" in the dual: their dual constraint is implied by the constraints of smaller columns. Sol (1994, PhD thesis, Eindhoven) called such columns redundant and studied pricing rules that avoid them. In their survey, Lübbecke and Desrosiers state the key fact as Proposition 2 (Operations Research 53(6), p. 1016): under ratio pricing, a strictly redundant column is never the optimal choice.

Setting

Let the rows of a set-partitioning master problem be $\{1,\dots,m\}$. A column is a subset $s$ of the rows, with incidence vector $\mathbf a_s \in \{0,1\}^m$ ($(\mathbf a_s)_i = 1$ iff $i \in s$). Let $\mathcal A$ be a finite collection of nonempty columns with costs $c_s$. The master problem is

$$\min \sum_{s \in \mathcal A} c_s \lambda_s \quad\text{s.t.}\quad \sum_{s \in \mathcal A} \mathbf a_s \lambda_s = \mathbf 1,\ \lambda \ge 0,$$

with $\lambda$ integer in the integer program. Its dual has one free multiplier $u_i$ per row and one constraint $\mathbf u^{\mathsf T}\mathbf a_s \le c_s$ per column.

A column $s$ is redundant, eq. (30), p. 1015, if

$$\mathbf a_s = \sum_{r \subset s} \mathbf a_r \lambda_r \qquad\text{and}\qquad c_s \ge \sum_{r \subset s} c_r \lambda_r ,$$

with $\lambda_r \ge 0$ and $r$ ranging over the columns of $\mathcal A$ that are proper subsets of $s$; then its dual constraint is implied by those of its subcolumns. It is strictly redundant if the cost inequality is strict. The pair $(\mathcal A, \mathbf c)$ has the subcolumn property if $c_r < c_s$ for all $r, s \in \mathcal A$ with $r \subsetneq s$. Given dual multipliers $\bar{\mathbf u} \in \mathbb R^m$, the ratio pricing problem (31) is

$$\min\left\{ \frac{c(\mathbf a) - \bar{\mathbf u}^{\mathsf T}\mathbf a}{\mathbf 1^{\mathsf T}\mathbf a} \;\middle|\; \mathbf a \in \mathcal A \right\},$$

the reduced cost per covered row. In Lean these objects are incidence, IsRedundant, IsStrictlyRedundant, SubcolumnProperty and pricingRatio in the namespace Lubbecke2005.SubcolumnPricing.

Formalization targets

Goal: Proposition 2 (p. 1016)

Let $(\mathcal A, \mathbf c)$ satisfy the subcolumn property, $\emptyset \notin \mathcal A$, and let $\bar{\mathbf u} \in \mathbb R^m$ be arbitrary. If $s \in \mathcal A$ is strictly redundant, then

$$\neg\Bigl(\forall \mathbf a \in \mathcal A:\ \frac{c_s - \bar{\mathbf u}^{\mathsf T}\mathbf a_s}{\mathbf 1^{\mathsf T}\mathbf a_s} \le \frac{c(\mathbf a) - \bar{\mathbf u}^{\mathsf T}\mathbf a}{\mathbf 1^{\mathsf T}\mathbf a}\Bigr),$$

that is, $\mathbf a_s$ is not an optimal solution of (31). The paper states the proposition and refers to Sol (1994) for the concept; it gives no proof.

Milestone: the cost shift (§5.1, p. 1016)

If only $c_r \le c_s$ holds for $r \subsetneq s$ in $\mathcal A$, the shifted costs $c'_s = c_s + |s|$ satisfy the subcolumn property, and on every $\lambda$ with $\sum_s \mathbf a_s \lambda_s = \mathbf 1$,

$$\sum_{s} c'_s \lambda_s = \sum_s c_s \lambda_s + m .$$

This is the paper's remark that the shift "adds to $z^\star$ a constant term equal to the number of rows and does not change the problem".

Significance

Proposition 2 is the paper's argument for alternative pricing rules (§5.2): it shows that dividing the reduced cost by the number of covered rows filters out a whole class of columns that contribute nothing to the dual polyhedron, whatever the current dual multipliers are. Steepest-edge pricing, Devex and the lambda pricing rule are motivated along the same lines. The cost-shift remark extends the proposition to cost structures that are only weakly monotone under inclusion, which covers the frequent case of costs that do not decrease when rows are added to a column.

The result is published and elementary once stated precisely, but the paper leaves the definition of redundancy informal (no sign on $\lambda$, no index set of the sum), and those choices decide whether the proposition is true. A formal statement pins them down. To our knowledge neither the proposition nor the vocabulary of redundant columns and ratio pricing has a machine-checked formalization; the definitions here are reusable for other statements about pricing rules in set-partitioning column generation.

Difficulty

The mathematical difficulty is modest; the difficulty is in the reading. With multipliers $\lambda_r$ of arbitrary sign in (30), the proposition is false: on rows $\{1,2,3\}$ take $s = \{1,2,3\}$, $r_1 = \{1,2\}$, $r_2 = \{2,3\}$, $r_3 = \{2\}$ with costs $2.2$, $2$, $2$, $1.9$ and $\bar{\mathbf u} = 0$; then $\mathbf a_s = \mathbf a_{r_1} + \mathbf a_{r_2} - \mathbf a_{r_3}$, $2.2 > 2.1$, the subcolumn property holds, and $s$ has the unique smallest ratio. The empty column is a second trap: its denominator $\mathbf 1^{\mathsf T}\mathbf a$ is zero. The formal statement has to exclude both, and has to keep the minimum in (31) over $\mathcal A$ only.

Formalization scope

Conventions committed to in Lean:

• Rows are Fin m (indexed from $0$); a column is a Finset (Fin m), and its incidence vector is the real 0/1 vector incidence s : Fin m → ℝ. The collection $\mathcal A$ is a Finset (Finset (Fin m)); costs are a function Finset (Fin m) → ℝ, of which only the values on $\mathcal A$ matter.
• Reading of (30): the multipliers are nonnegative ($\lambda_r \ge 0$), the Farkas form of "the corresponding constraint is redundant for the dual problem". The paper leaves the sign implicit; with signed multipliers the proposition fails (example above).
• Reading of $r \subset s$: proper inclusion, over columns $r \in \mathcal A$ only. With $r \subseteq s$ every column would be redundant via $\lambda_s = 1$.
• Strictly redundant: (30) with strict cost inequality; the equality part is unchanged.
• Reading of (31)'s denominator: $\emptyset \notin \mathcal A$ is a hypothesis of the goal ("a set-partitioning column covers at least one row"); it is named here as an addition to the literal text. The denominator is 1 ⬝ᵥ incidence a, which equals $|a|$.
• Dual multipliers: $\bar{\mathbf u} \in \mathbb R^m$ is arbitrary; no sign, no optimality for the restricted master.
• "Cannot be an optimal solution" is stated literally as the negation of "the ratio of $\mathbf a_s$ is at most the ratio of every column of $\mathcal A$"; this is equivalent to the existence of a column with strictly smaller ratio. No infimum over real sets is used.
• The subcolumn property is kept as a hypothesis because the paper states it, although the conclusion may hold without it.
• Cost shift: stated for real multipliers; the optimal value $z^\star$ is not formalized, and "does not change the problem" is rendered as the pointwise identity on the feasible set.

A trivializing formalization — a redundancy witness not tied to the proper subcolumns of $s$ in $\mathcal A$, signed multipliers, or an empty column with ratio $0$ — is ruled out by the definitions above.

Needed infrastructure is only finite sums of vectors in $\mathbb R^m$ and the identity $\mathbf 1^{\mathsf T}\mathbf a_s = |s|$. Contributions welcome: proofs of the goal and the milestone, and further statements from §5 (for example the redundancy characterisation of Sol 1994) built on the same definitions.

Selected references

• M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
• M. Sol, Column Generation Techniques for Pickup and Delivery Problems, PhD thesis, Eindhoven University of Technology, 1994 (cited in the paper as Sol 1994).
• J. Desrosiers and M. E. Lübbecke, A Primer in Column Generation, in Column Generation, Springer, 2005. https://doi.org/10.1007/0-387-25486-2_1
• F. Vanderbeck, Decomposition and Column Generation for Integer Programs, PhD thesis, Université catholique de Louvain, 1994.

Motivation

Many problems in statistics, signal processing and machine learning have the form

$$\min_x\ h(x) + P(\mathcal M x),$$

where $h$ is smooth (a least-squares loss, for instance), $P$ is a nonsmooth regularizer or constraint, and $\mathcal M$ is a linear map such as a finite-difference operator. When $P$ is nonconvex — the cardinality function $\|\cdot\|_0$, the $\ell_{1/2}$ quasi-norm, the indicator of a nonconvex set — the problem is NP-hard in general, and the realistic goal is a stationary point. The alternating direction method of multipliers (ADMM) is widely used on such problems because each iteration splits into a proximal step on $P$ and a smooth step on $h$, but for nonconvex $P$ it was long used without a convergence theory.

Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave one of the first general analyses. Their Theorem 1 shows that, under explicit conditions on the penalty parameter and a proximal term, every cluster point of a proximal ADMM sequence is stationary, and that a suitable start is strictly improved on. Earlier, Ames and Hong (arXiv:1401.5492) proved convergence of the plain ADMM for one specific nonconvex quadratic problem with an $\ell_1$ and norm-ball term; Li–Pong's argument follows their idea of bounding the dual changes by the primal changes, together with a descent analysis of the augmented Lagrangian from Wen, Peng, Liu, Bai and Sun (Optimization Online 2013/01/3730).

Setting

Let $h : \mathbb{R}^n \to \mathbb{R}$ be twice continuously differentiable with bounded Hessian $\nabla^2 h$, let $P : \mathbb{R}^m \to (-\infty, +\infty]$ be proper (finite somewhere, never $-\infty$) and closed (lower semicontinuous), and let $\mathcal M : \mathbb{R}^n \to \mathbb{R}^m$ be linear with adjoint $\mathcal M^*$.

A vector $v$ is a regular subgradient of $f$ at $x$ (with $f(x)$ finite) if $\liminf_{z \to x} \frac{f(z) - f(x) - \langle v, z-x\rangle}{\|z - x\|} \ge 0$. The limiting subdifferential $\partial f(x)$ collects all limits $v = \lim v^t$ of regular subgradients $v^t$ at points $x^t \to x$ with $f(x^t) \to f(x)$. A point $x$ is stationary if

$$0 \in \nabla h(x) + \mathcal M^* \partial P(\mathcal M x).$$

For $\beta > 0$ the augmented Lagrangian is $L_\beta(x,y,z) = h(x) + P(y) - \langle z, \mathcal M x - y\rangle + \frac\beta2\|\mathcal M x - y\|^2$, and for a convex $C^2$ function $\phi$ the Bregman distance is $D_\phi(x_1,x_2) = \phi(x_1) - \phi(x_2) - \langle\nabla\phi(x_2), x_1 - x_2\rangle$. The proximal ADMM generates, from arbitrary $x^0, z^0$,

$$y^{t+1} \in \operatorname{Arg\,min}_y L_\beta(x^t, y, z^t),\quad x^{t+1} \in \operatorname{Arg\,min}_x \{L_\beta(x, y^{t+1}, z^t) + D_\phi(x, x^t)\},\quad z^{t+1} = z^t - \beta(\mathcal M x^{t+1} - y^{t+1}).$$

Assumption 1 requires $\mathcal M\mathcal M^* \succeq \sigma\mathcal I$ for some $\sigma > 0$ (so $\mathcal M$ is surjective), Loewner bounds $\mathcal Q_1 \succeq \nabla^2 h \succeq \mathcal Q_2$, $\mathcal T_1^2 \succeq [\nabla^2\phi]^2 \succeq \mathcal T_2^2$ with $\mathcal T_1 \succeq \mathcal T_2 \succeq 0$, $\mathcal Q_3 \succeq [\nabla^2 h + \nabla^2 \phi]^2$, a strong-convexity margin $\mathcal Q_2 + \beta\mathcal M^*\mathcal M + \mathcal T_2 \succeq \delta\mathcal I$, and some $\gamma \in (0,1)$ with $\delta\mathcal I + \mathcal T_2 \succ \frac{2}{\sigma\beta}\big(\frac1\gamma \mathcal Q_3 + \frac1{1-\gamma}\mathcal T_1^2\big)$. Here $\|x\|^2_{\mathcal T} := \langle x, \mathcal T x\rangle$.

Formalization targets

Goal: Theorem 1 (p. 7)

Under the standing assumptions and Assumption 1, for every proximal ADMM sequence:

1. (Global subsequential convergence) at every cluster point $(x^*, y^*, z^*)$,

$$\lim_{t\to\infty}\|y^{t+1}-y^t\|^2 + \|x^{t+1}-x^t\|^2 + \|z^{t+1}-z^t\|^2 = 0,\qquad \nabla h(x^*) = \mathcal M^* z^*,\ \ -z^* \in \partial P(y^*),\ \ y^* = \mathcal M x^*,$$

and $x^*$ is stationary; 2. (Strict improvement) if $x^0$ is not stationary, $h(x^0) + P(\mathcal M x^0) < \infty$ and $\mathcal M^* z^0 = \nabla h(x^0)$, then every cluster point satisfies

$$h(x^*) + P(\mathcal M x^*) < h(x^0) + P(\mathcal M x^0).$$

The theorem does not assert that a cluster point exists; that is the subject of Theorem 2 of the same paper.

Milestones

In attack order: the robustness (3) of $\partial$; the optimality relations (11) of each iterate; the passage from (9) and (10) to (12) and stationarity; the dual-step bound (14); the one-step estimate (20) and its summed form (21) for $L_\beta$; the vanishing of the primal steps (16); the convergence (10) of $P(y^{t_i+1})$; and, for part (ii), $x^1 \ne x^0$, the first-step estimate (27) and the strict decrease after (28).

Significance

Theorem 1 turns the proximal ADMM into a method with a guarantee for a nonconvex $P$: any limit it produces is a stationary point, and with the initialization of part (ii) — for example, a stationary point of a convex relaxation — it cannot return to a stationary point worse than its start. The conditions are checkable: Remark 1 of the paper shows that the choice $\phi(x) = \frac L2\|x\|^2 - h(x)$ turns the $x$-update into a convex quadratic program, and that the last condition of Assumption 1 can be enforced by taking $\beta$ large when $\phi$, $\mathcal T_1$, $\mathcal T_2$ do not depend on $\beta$. The estimate (20) is reused by the paper's boundedness result (Theorem 2), and its whole-sequence convergence result for semi-algebraic data (Theorem 3) starts from Theorem 1.

The result is proved in the paper; Mathlib contains neither the limiting subdifferential nor any convergence theorem for ADMM, so none of it is formalized yet. A formalization would give a verified library of the limiting subdifferential of extended-real-valued functions, its robustness and its Fermat rule with a smooth sum, and the first formally verified convergence theorem for ADMM with a nonconvex term.

Difficulty

The obvious argument — "the augmented Lagrangian decreases, so it converges" — fails: $L_\beta$ need not decrease, because the multiplier step increases it by $\frac1\beta\|z^{t+1}-z^t\|^2$. The proof has to bound this increase by primal steps, which uses surjectivity of $\mathcal M$ and the squared Hessian bounds, and it produces a two-step recursion (involving $x^{t-1}$) rather than a monotone sequence. Nor is $L_\beta$ known to be bounded below; the proof uses the cluster point and lower semicontinuity to get a lower bound along a subsequence. Passing to the limit in the inclusion for $\partial P$ requires $P(y^{t_i+1}) \to P(y^*)$, which lower semicontinuity alone does not give. For part (ii), the start $y^0$ is not an iterate at all, so the first step needs its own estimate.

Formalization scope

Spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $\mathcal M$ is a continuous linear map and $\mathcal M^*$ is ContinuousLinearMap.adjoint. $P$ and $L_\beta$ take values in EReal; inequalities involving $L_\beta$ are written additively ($a \le b + r$ with real $r$), never through EReal.toReal. The Hessian is the derivative of the gradient. $\succeq$ is Mathlib's Loewner order on self-maps, which includes symmetry of the difference; $\succ$ adds positive definiteness. $\|x\|^2_{\mathcal T} = \langle x, \mathcal T x\rangle$ for every $\mathcal T$, possibly indefinite. The witnesses of Assumption 1 are explicit parameters, universally quantified. A proximal ADMM sequence is any triple of sequences satisfying the three updates (global minimizers, not necessarily unique); $x^0, z^0$ are free and $y^0$ is unconstrained. A cluster point is the limit along a strictly increasing subsequence. Stationarity is the inclusion (4) itself.

The limiting subdifferential keeps all three requirements of its definition — $x^t \to x$, $f(x^t) \to f(x)$ and $v^t \to v$ — and the domain condition $f(x) < \infty$; dropping $f$-attentive convergence or replacing $\partial$ by the convex subdifferential would make stationarity a different, and for nonconvex $P$ wrong, notion. Part (ii) is a strict inequality for every cluster point, and its hypotheses are exactly non-stationarity of $x^0$, finiteness of the objective at $x^0$ and $\mathcal M^* z^0 = \nabla h(x^0)$. The paper's assumption that proximal maps of $P$ exist is not a hypothesis, since no statement asserts that the iteration can be run.

Needed infrastructure: Fermat's rule and the smooth sum rule for regular subgradients, a diagonal argument for (3), Taylor bounds for $C^2$ functions with Loewner-bounded Hessians (the paper's (5) and (6)), strong convexity from a Hessian lower bound, and the monotonicity of the positive square root in the Loewner order. These are reusable well beyond this mission; contributions of any of them as separate lemmas are welcome.

Selected references

• G. Li, T. K. Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, SIAM J. Optim. 25(4), 2015. arXiv:1407.0753v6, https://arxiv.org/abs/1407.0753 (cited version), DOI https://doi.org/10.1137/140998135
• B. P. W. Ames, M. Hong, Alternating direction method of multipliers for sparse zero-variance discriminant analysis and principal component analysis, preprint, 2014. https://arxiv.org/abs/1401.5492
• Z. Wen, X. Peng, X. Liu, X. Bai, X. Sun, Asset allocation under the Basel accord risk measures, preprint, 2013. http://www.optimization-online.org/DB_HTML/2013/01/3730.html
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3