Operations Research

Motivation

Edmonds showed that the convex hull of the matchings of a graph is described by the degree constraints together with the blossom inequalities, one for every odd set of nodes (Edmonds 1965). There are exponentially many of them, so any cutting-plane method for matching and b-matching problems must answer a separation question: given a fractional point, find a violated blossom inequality or certify that none exists. Padberg and Rao (1982) reduced this question to a purely graph-theoretic one, the odd minimum cut-set problem, and solved that problem in polynomial time with a single Gomory–Hu computation. The same subroutine underlies separation for many other odd-set constraints (for example the 2-matching and comb-type constraints of the travelling salesman polytope), and later work refined its running time (Letchford, Reinelt and Theis 2008).

This mission covers Section 1 of the paper: the combinatorial theorem about odd cuts, independent of matchings. A companion mission covers the reduction from capacitated b-matching separation (Section 3).

Setting

Let $G = (V, E)$ be a finite undirected graph without loops and multiple edges, with edge weights $c_e \ge 0$. Write $c_{ij}$ for the weight of the edge $[i, j]$, with $c_{ij} = c_{ji}$, and $c_{ij} = 0$ if there is no such edge. For $W \subseteq V$ the cut-set $(W : V - W)$ is the set of edges with exactly one end in $W$, and its capacity is

$$c(W : V - W) = \sum_{i \in W} \sum_{j \in V - W} c_{ij}.$$

A nonempty set $V_1 \subseteq V$ of nodes is labelled odd, the rest even. For $U \subseteq V$ the label $\lambda(U)$ is odd if $|U \cap V_1|$ is odd, and even otherwise; $\lambda(\emptyset)$ is even. The paper assumes throughout that $\lambda(V)$ is even, i.e. $|V_1|$ is even. A cut-set $(U : V - U)$ is odd if $\lambda(U)$ is odd, and an odd minimum cut-set is a solution $X$ of

$$c(X : V - X) = \min\{ c(U : V - U) : U \subseteq V,\ \lambda(U) \text{ odd} \}. \qquad (1.1)$$

A cut-set $(M : V - M)$ is a minimum cut-set with respect to all pairs of odd nodes if it separates two odd nodes and no cut-set separating two odd nodes has smaller capacity.

A cut-tree $G_T = (N, F)$ for the odd nodes is the output of the Gomory–Hu algorithm applied to all pairs of odd nodes (Gomory and Hu 1961). Each tree node contains exactly one odd node and possibly some even ones, so $N$ is identified with $V_1$, and each node $v$ of $G$ belongs to one tree node $\pi(v)$. Removing a tree edge $f = [r, s]$ splits $G_T$ into two subtrees; the nodes of $G$ in the tree nodes of the $r$-side subtree form a set $M$, and the weight of $f$ is $d_f = c(M : V - M)$. The defining property (Hu, Theorem 9.2) is that for every tree edge $f = [r, s]$ the cut-set $(M : V - M)$ is a minimum cut-set of $G$ separating $r$ and $s$. The cardinality of a subtree is its number of tree nodes.

Formalization targets

Goal: Theorem 1.1 (p. 70)

For every cut-tree $G_T$ of $G$ for the odd nodes:

1. some edge of $G_T$ decomposes it into two subtrees of odd cardinality; and
2. if $f^* = [r, s]$ is such an edge of minimum weight among all such edges, and $M$ is the $r$-side shore of $f^*$, then

$$c(M : V - M) = \min\{ c(U : V - U) : U \subseteq V,\ \lambda(U) \text{ odd} \}.$$

Because $|N| = |V_1|$ is even, the two subtrees have the same parity, so the condition is checked on one side.

Milestones

• Lemma 1.1 (p. 68). If $(M : V - M)$ is a minimum cut-set with respect to all pairs of odd nodes, there is an odd minimum cut-set $(X : V - X)$ with $X \subseteq M$ or $X \subseteq V - M$.
• Section 1, p. 70. If $f^*$ has minimum weight among all edges of $G_T$, its shore $M$ gives a minimum cut-set with respect to all pairs of odd nodes.

Significance

Theorem 1.1 turns problem (1.1), a minimization over exponentially many odd sets, into $|V_1| - 1$ maximum-flow computations followed by a scan of the tree edges. Combined with Section 3 of the paper, this gives a polynomial separation algorithm for the blossom inequalities of b-matching polytopes, and hence, by the equivalence of separation and optimization, a polynomial-time route to weighted b-matching through linear programming. The odd-cut routine is also used for separating the odd-set constraints of other polytopes.

The theorem has been proved since 1982 and is textbook material. What this mission adds is a machine-checked proof on a precise encoding of cut-trees. As far as the platform's corpus shows, neither the Gomory–Hu cut-tree property nor any odd-cut theorem has been formalized in Lean; Mathlib has trees and reachability in simple graphs but no cut-tree theory.

Difficulty

The obvious argument fails at the minimum. Every tree-edge shore separates two odd nodes, so a minimum-weight odd-splitting edge certainly yields an odd cut, but showing that no odd set $U$, however it cuts across the tree nodes, has smaller capacity requires relating an arbitrary odd $U$ to a tree edge whose shore is also odd and whose endpoints $U$ separates. The cut-tree only certifies minimality for cuts separating the two ends of a tree edge; an odd set $U$ may split many tree nodes and cross many shores at once, and nothing in the cut-tree property speaks about parity. Parity bookkeeping between odd labels in $G$ and odd cardinality of subtrees is the other place where care is needed: the two notions agree only because each tree node holds exactly one odd node.

Formalization scope

The graph is a weight function c : V → V → ℝ on a Fintype V, with hypotheses that it is symmetric and nonnegative; a missing edge has weight 0 and the diagonal never enters a cut. Node sets are Finset V and $V - W$ is the complement Wᶜ. The odd nodes form a Finset odd with odd.Nonempty and Even odd.card on every statement. The cut-tree is a SimpleGraph on the subtype {v // v ∈ odd} together with a map π : V → {v // v ∈ odd}; IsOddCutTree requires that the graph is a tree, that π fixes every odd node, and the Gomory–Hu minimality for every tree edge. The tree-edge weight $d_f$ is computed from the shore, not supplied as data. Minimality is always stated as ≤ against every competitor; no real infimum is taken.

The existence of a cut-tree (the Gomory–Hu theorem) is a hypothesis-side object and is not part of this mission; the theorems hold for every tree satisfying the cut-tree property. A statement in which the cut-tree assumption already says that the chosen edge's shore is an odd minimum cut, or in which "odd minimum cut" is minimized only over tree-edge shores, would make Theorem 1.1 definitional; both are ruled out, since IsOddMinCut ranges over every node set with odd label.

A complete development needs: submodularity-type identities for cut capacities (reusable for any cut problem), the structure of fundamental cuts of a tree (the two sides of a removed edge are complementary and the parities of $U \cap V_1$ along tree edges combine), and Lemma 1.1. Proofs of the milestones, alternative arguments for the goal that avoid the recursion, and a formal Gomory–Hu existence theorem are all welcome contributions.

Selected references

• M. W. Padberg and M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7(1), 67–80, 1982. https://doi.org/10.1287/moor.7.1.67
• R. E. Gomory and T. C. Hu, Multi-Terminal Network Flows, Journal of the SIAM 9(4), 551–570, 1961. https://doi.org/10.1137/0109047
• T. C. Hu, Integer Programming and Network Flows, Addison-Wesley, 1969 (Chapter 9, Theorem 9.2).
• J. Edmonds, Maximum Matching and a Polyhedron with 0,1-Vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
• A. N. Letchford, G. Reinelt and D. O. Theis, Odd Minimum Cut Sets and b-Matchings Revisited, SIAM Journal on Discrete Mathematics 22(4), 1480–1487, 2008. https://doi.org/10.1137/060664793

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

Motivation

Many problems in optimization reduce to finding a zero of a maximally monotone operator: minimizing a closed proper convex function (its subdifferential is maximally monotone), finding a saddle point of a convex–concave function, and solving monotone variational inequalities. The basic algorithm for this problem is the proximal point method of Martinet (1970) and Rockafellar (1976), which repeatedly applies the resolvent of the operator. The augmented Lagrangian method, the proximal method of multipliers, the Douglas–Rachford splitting method, ADMM and the primal–dual hybrid gradient method are all instances of it, so any speed-up of the proximal point method transfers to these widely used algorithms.

For convex minimization, Güler (1992) accelerated the proximal point method in the style of Nesterov, improving the rate of the function value from $O(1/i)$ to $O(1/i^2)$. For general maximally monotone operators no function value exists, and the natural measure of progress is the fixed-point residual $\|x_{i}-y_{i-1}\|$, the distance moved by one resolvent step. Gu and Yang (2020) showed that the plain proximal point method has the exact worst-case rate $O(1/i)$ for the squared residual. Relaxed and inertial variants had been studied, but none guaranteed an accelerated rate for this measure. Kim (arXiv:1905.05149, Math. Program. 2021) found one using the performance estimation problem (PEP) of Drori and Teboulle (2014): a new accelerated proximal point method whose squared fixed-point residual is at most $R^2/i^2$.

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. A set-valued operator $M:\mathcal H\to2^{\mathcal H}$ assigns a subset $Mx\subseteq\mathcal H$ to every point $x$. It is monotone if $\langle x-y,u-v\rangle\ge0$ whenever $u\in Mx$ and $v\in My$, and maximally monotone if moreover no monotone operator has a graph that properly contains the graph of $M$. The class of maximally monotone operators is $\mathcal M(\mathcal H)$, and $X_*(M)=\{x:0\in Mx\}$ is the set of zeros.

For a step size $\lambda>0$, the resolvent $J_{\lambda M}=(I+\lambda M)^{-1}$ maps $y$ to the unique $x$ with $y\in x+\lambda Mx$. It is single-valued for monotone $M$ and defined on all of $\mathcal H$ for maximally monotone $M$.

The general proximal point method with step coefficients $h=\{h_{i,k}\}$ starts at $y_0$ and iterates

$$x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=y_i+\sum_{k=0}^{i}h_{i+1,k+1}(x_{k+1}-y_k).$$

Kim's proposed accelerated proximal point method starts at $x_0=y_0=y_{-1}$ and iterates

$$x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=x_{i+1}+\frac{i}{i+2}(x_{i+1}-x_i)-\frac{i}{i+2}(x_i-y_{i-1}).$$

The coefficients (25) are $h_{i,k}=-\frac{2k}{i(i+1)}$ for $k<i$ and $h_{i,i}=\frac{2i}{i+1}$.

The PEP of Section 3 bounds the worst case of $\|x_N-y_{N-1}\|^2/R^2$ over all $M\in\mathcal M(\mathcal H)$ and all starts with $\|y_0-x_*\|\le R$. A semidefinite relaxation leads to the dual problem (D): minimize $c$ over nonnegative $a_2,\dots,a_N,b_N,c$ such that $\sum_{i=2}^Na_iA_{i-1,i}(h)+b_NB_N(h)+cC-u_Nu_N^\top\succeq0$. The matrices are explicit symmetric $(N+1)\times(N+1)$ matrices built from $h$ and the canonical basis $u_1,\dots,u_{N+1}$. Its optimal value is $\mathcal B_D(h)$.

Formalization targets

Goal: Theorem 4.1

For every $M\in\mathcal M(\mathcal H)$, every $\lambda>0$, every run of the proposed method, and every $x_*\in X_*(M)$ with $\|x_0-x_*\|\le R$ for a constant $R>0$,

$$\|x_i-y_{i-1}\|^2\le\frac{R^2}{i^2}\qquad\text{for every }i\ge1.$$

The constant is the paper's, and nothing is left unfixed.

Milestones

1. Lemma 4.1. For every $N\ge1$, $h$ from (25) with $a_i=\frac{2(i-1)i}{N^2}$, $b_N=\frac2N$, $c=\frac1{N^2}$ is feasible for (D) and for (HD) $=\min_h\mathcal B_D(h)$.
2. Section 3, (D). For any $h$ and any feasible point of (D), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le c$ for every run of the general method with $\|y_0-x_*\|\le R$.
3. Eq. (28). With $h$ from (25), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le\mathcal B_D(h)\le\frac1{N^2}$ for every $N\ge1$.
4. Proposition 4.1. The general method with (25) and the proposed method generate identical sequences from the same initial point.

Significance

Theorem 4.1 gives the first $O(1/i^2)$ rate for the fixed-point residual of a proximal point method on general maximally monotone operators. The rate uses no strong monotonicity, no smoothness, and no finite dimension. Because the proximal point method underlies the proximal method of multipliers, PDHG, Douglas–Rachford splitting and ADMM, the paper derives accelerated versions of each (Section 6). The same analysis also accelerates the forward method for cocoercive operators (Section 7). Later work related the method to the Halpern iteration (Lieder 2021) and showed that its rate is optimal among a broad class of fixed-point methods up to a constant (Park and Ryu 2022).

The result is proved in the paper, and to our knowledge no machine-checked proof exists. Formalizing it produces a verified chain of four results: an explicit semidefinite certificate (Lemma 4.1), the weak-duality step from an SDP certificate to an algorithmic bound, the resulting rate for the general method, and the algebraic identity between two recursions (Proposition 4.1). It also produces reusable definitions of monotone and maximally monotone set-valued operators on a real Hilbert space, which Mathlib does not have.

Difficulty

The obvious approach would be a Lyapunov (potential) function argument, but the paper does not give one. The rate comes out of a semidefinite program. Lemma 4.1 asks for positive semidefiniteness of an $(N+1)\times(N+1)$ matrix whose entries are double sums over $h$, uniformly in $N$. The passage from the dual certificate back to the iterates happens in an arbitrary, possibly infinite-dimensional Hilbert space, where each constraint matrix corresponds to a monotonicity inequality between iterates, so matrix positivity has to be turned into an inequality between inner products in $\mathcal H$. The PEP is a relaxation that discards constraints, so only weak duality is available, and a rate that holds only for $\dim\mathcal H\ge N+1$ (Lemma 3.1) is not what is asked. Proposition 4.1 is a two-level induction with index bookkeeping at $i=0,1$.

Formalization scope

$\mathcal H$ is any real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with no finite-dimensional specialization. An operator is M : H → Set H. Maximal monotonicity says that every monotone A with M x ⊆ A x for all x equals M.

The resolvent step is relational: $x_{i+1}=J_{\lambda M}(y_i)$ is encoded as $\lambda^{-1}(y_i-x_{i+1})\in Mx_{i+1}$. For monotone $M$ and $\lambda>0$ this determines $x_{i+1}$ uniquely, and for maximally monotone $M$ such an $x_{i+1}$ exists for every $y_i$ (Minty's theorem). No function-valued resolvent with junk values off its domain is used. Sequences are indexed by ℕ. The paper's $y_{-1}=y_0$ is y (0 - 1) = y 0 under natural-number subtraction. The general method has no $x_0$, so its initial-distance condition is on $y_0$, as in (17). The step size $\lambda$ is written lam.

PEP matrices are Matrix (Fin (N+1)) (Fin (N+1)) ℝ, with a 1-based basis basisVec N i $=u_i$. $\mathcal B_D(h)$ is the infimum of the feasible values of $c$ computed in EReal, so an infeasible $h$ gets the value $+\infty$ as in the paper; Eq. (28) compares it with the real bounds cast to EReal.

A formalization in which the iterate predicate cannot be satisfied, the residual is $\|x_i-x_{i-1}\|$, the correction term is dropped or has the wrong sign, the initial point is decoupled ($x_0\ne y_0$), or $M$ is only monotone on finitely many points, would state a different theorem, and none is used here.

Useful infrastructure includes a Minty-type existence lemma, uniqueness of the resolvent, and a lemma turning a positive semidefinite certificate into an inequality between inner products in $\mathcal H$ (via Matrix.PosSemidef and Gram matrices). These are reusable for PEP-based rates of other first-order methods. Proofs of any milestone, and of the goal by other routes, are welcome.

Selected references

• D. Kim, Accelerated proximal point method for maximally monotone operators, Math. Program. 190 (2021) 57–87; arXiv:1905.05149v4. https://arxiv.org/abs/1905.05149
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM J. Control Optim. 14 (1976) 877–898. https://doi.org/10.1137/0314056
• O. Güler, New proximal point algorithms for convex minimization, SIAM J. Optim. 2 (1992) 649–664. https://doi.org/10.1137/0802032
• Y. Drori, M. Teboulle, Performance of first-order methods for smooth convex minimization: a novel approach, Math. Program. 145 (2014) 451–482. https://doi.org/10.1007/s10107-013-0653-0
• G. Gu, J. Yang, Tight sublinear convergence rate of the proximal point algorithm for maximal monotone inclusion problems, SIAM J. Optim. 30 (2020) 1905–1921. https://doi.org/10.1137/19M1299049
• F. Lieder, On the convergence rate of the Halpern-iteration, Optim. Lett. 15 (2021) 405–418. https://doi.org/10.1007/s11590-020-01617-9
• J. Park, E. K. Ryu, Exact optimal accelerated complexity for fixed-point iterations, ICML 2022; arXiv:2201.11413. https://arxiv.org/abs/2201.11413
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5