The OR Formalization Drive

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

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested parties. Each party reports its private data, the algorithm computes an outcome, and payments are arranged so that no party gains by misreporting. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001). Their running example is task scheduling on unrelated machines: $k$ tasks are distributed among $n$ machines owned by different agents, each agent knows only its own processing times, and the designer wants to minimize the make-span.

Without incentives the problem is classical: minimizing make-span on unrelated machines is NP-hard and admits a polynomial 2-approximation (Lenstra, Shmoys, Tardos, 1990). With selfish agents the question changes: which approximation ratios can a truthful mechanism guarantee? This mission formalizes the paper's upper bound, the MinWork mechanism, which is the benchmark every later lower bound for truthful scheduling is compared with.

Timeline.

• 1961: Vickrey introduces the second-price auction (J. Finance 16).
• 1971–1973: Clarke and Groves generalize it to the VCG family of truthful mechanisms for utilitarian objectives (Groves, Econometrica 41, 1973).
• 1999/2001: Nisan and Ronen show MinWork is a strongly truthful $n$-approximation, and that no truthful mechanism beats ratio 2.
• 2007: Christodoulou, Koutsoupias and Vidali raise the deterministic lower bound to $1+\sqrt2$ for $n \ge 3$; Koutsoupias and Vidali later raise it to $1+\varphi \approx 2.618$.
• 2023: Christodoulou, Koutsoupias and Kovács prove the Nisan–Ronen conjecture: no deterministic truthful mechanism achieves a ratio below $n$ (STOC 2023, arXiv:2301.11905), so MinWork is optimal among deterministic truthful mechanisms.

Setting

There are $n$ agents and $k$ tasks. Agent $i$'s type is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive times, $t^i_j > 0$ being the time agent $i$ needs to perform task $j$. A type vector is $t = (t^1,\dots,t^n)$. An allocation $x$ sends each task $j$ to one agent; $x^i$ is the set of tasks agent $i$ receives. The make-span of $x$ is

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

and agent $i$'s valuation is $v^i(x,t^i) = -\sum_{j \in x^i} t^i_j$.

A direct mechanism asks every agent to declare a type, computes an allocation $x(d)$ from the declared vector $d$, and hands agent $i$ a payment $p^i(d)$. Agent $i$'s utility is $p^i(d) + v^i(x(d), t^i)$, with $t^i$ its true type. The mechanism is truthful if declaring $t^i$ maximizes agent $i$'s utility for every declaration of the others, and strongly truthful if truth-telling is the only such dominant strategy. An allocation rule is a $c$-approximation if $g(x(t),t) \le c \cdot g(y,t)$ for every type vector $t$ and every allocation $y$.

The MinWork mechanism allocates each task to an agent with minimal declared time for it, breaking ties arbitrarily. For each task it wins, an agent receives the second-best declared time $\min_{i' \ne i} d^{i'}_j$:

$$p^i(d) = \sum_{j \in x^i(d)} \min_{i' \neq i} d^{i'}_j .$$

The Lean development uses the same names: load, makespan, IsTruthful, IsStronglyTruthful, IsApprox, IsMinWorkAlloc, secondBest, minTime, minWorkPay.

Formalization targets

Goal: Theorem 4.1

For $n \ge 2$ and every MinWork allocation rule $x$ with payments $p$ as above,

$$(x,p)\ \text{is strongly truthful} \quad\text{and}\quad g(x(t),t) \le n \cdot g(y,t)\ \ \text{for all positive } t \text{ and all allocations } y .$$

Milestones

1. Theorem 3.1 (Groves): a VGC mechanism is truthful. This is an existing platform theorem, used as a reference.
2. MinWork belongs to the VGC family. Its allocation maximizes $\sum_i v^i(t^i,x)$, and its payment is $\sum_{i'\ne i} v^{i'}(t^{i'},x(t)) + h^{-i}$ with $h^{-i} = \sum_j \min_{i'\ne i} t^{i'}_j$.
3. Claim 4.2: MinWork is strongly truthful.
4. $g(x(t),t) \le \sum_{j} \min_i t^i_j$.
5. $g(y,t) \ge \frac1n \sum_j \min_i t^i_j$ for every allocation $y$.
6. Claim 4.3: MinWork is an $n$-approximation.

Significance

The theorem gives the first positive result for truthful scheduling: a mechanism that is truthful in the strongest sense and is within a factor $n$ of optimal, whatever the tie-breaking rule. Every lower bound in the paper (Theorems 4.6, 4.10 and 4.12) and in the later literature measures itself against this ratio. Since the 2023 resolution of the Nisan–Ronen conjecture, the ratio $n$ is known to be tight for deterministic truthful mechanisms.

The result is proved in the paper; it is not known to be formalized in any proof assistant. The platform already has Groves' theorem in an abstract form (AGT.vcg_incentive_compatible). This mission connects that abstract statement to a concrete combinatorial mechanism, and it adds the strict part of strong truthfulness for any number of tasks and agents, which the paper proves only for one task and two agents. The vocabulary (make-span over unrelated machines, direct scheduling mechanisms, strong truthfulness) is shared with the seven later missions of this series.

Difficulty

Truthfulness follows from Groves' theorem once MinWork is identified as a VGC mechanism. The identification requires the payment identity at every declared vector and under every tie-breaking rule, including ties at the winning time. The main difficulty is the strict part of strong truthfulness. A misreport that differs from the truth only on one task must still be shown to lose strictly for some declarations of the others. Those declarations must stay positive, and on every other task they must leave the outcome unchanged. The paper's proof covers only one task and two agents and leaves the general case as "similar". Its printed inequality also has the two utilities in the wrong order (see below), so it cannot be transcribed directly.

Formalization scope

• Agents are Fin n and tasks are Fin k. An allocation is a function Fin k → Fin n, and an agent may receive no task. Types are positive reals, and every truthfulness and approximation quantifier ranges over positive true types, positive misreports and positive declarations of the others.
• Payments are handed to the agent, so utility is the payment minus the true time spent. Payments are computed from the declared vector, never from true types.
• The allocation rule is a parameter satisfying the MinWork specification (IsMinWorkAlloc). Every result holds for every tie-breaking rule, including rules that depend on the whole declared vector. No particular argmin is fixed.
• $n \ge 2$ is a hypothesis of the goal and of the truthfulness items: with a single agent the paper's second-best minimum is undefined. The approximation items need only $n \ge 1$. There is no hypothesis on $k$.
• The make-span and both minima are Finset.sup' / Finset.inf' over nonempty finite sets, so they are true maxima and minima with no default values.
• Strong truthfulness is formalized as truthfulness plus: every misreport $d^i \ne t^i$ is strictly worse than the truth for some positive declarations of the others. Given truthfulness this is equivalent to Definition 5. A formalization that states only that truth-telling is dominant, or proves strictness only for single-task instances, does not meet the goal. Neither does an existential ratio in place of $n$.
• Printed slip: in the proof of Claim 4.2 (p. 177) the case $d^i > t^i$ reads "the utility for agent $i$ is $t^i - d^i < 0$, instead of 0 in the case of truth-telling". With the Definition 11 payments the misreporting agent loses the task (utility 0), and the truthful agent wins it with utility $d^{3-i} - t^i > 0$. The milestone text keeps the paper's words; the Lean statements assert what the argument establishes.
• Out of scope: running time ("polynomial time"), and the paper's general revelation-principle framework (Proposition 2.1).
• Welcome contributions: proofs of the milestones, and a reusable lemma connecting the local VGC milestone to AGT.vcg_incentive_compatible.

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
• T. Groves, Incentives in Teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085
• W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16 (1961) 8–37. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• 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
• G. Christodoulou, E. Koutsoupias, A. Kovács, A Proof of the Nisan-Ronen Conjecture, STOC 2023. https://arxiv.org/abs/2301.11905

Motivation

Algorithms deployed on the Internet often take their inputs from parties who own them and who may lie when lying pays. Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) proposed studying optimization problems in this setting: the algorithm designer may hand out payments, and must guarantee that the intended output is produced when every participant acts in its own interest. The paper's central test case is scheduling on unrelated machines, a standard problem of combinatorial optimization, in which the machines are the selfish participants and only they know how long each job takes them.

For this problem the paper shows that incentives cost a factor of two at least: with two or more machines, no mechanism can guarantee a make-span below twice the optimum. This was the first lower bound separating what incentive-compatible mechanisms can achieve from what ordinary approximation algorithms can achieve, and it started a line of work on the "Nisan–Ronen conjecture" (that the right factor for $n$ machines is $n$), with improved lower bounds by Christodoulou, Koutsoupias and Vidali (Algorithmica, 2009) and by Koutsoupias and Vidali (Algorithmica, 2013), and a resolution announced by Christodoulou, Koutsoupias and Kovács (STOC 2023).

Setting

There are $n$ agents (machines) $i = 1,\dots,n$ and $k$ tasks $j = 1,\dots,k$. Agent $i$'s private type is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive real numbers, $t^i_j$ being the time agent $i$ needs for task $j$; a type vector is $t = (t^1,\dots,t^n)$. An allocation $x$ assigns every task to one agent; $x^i$ is the set of tasks given to agent $i$. For a set $X$ of tasks write $t^i(X) = \sum_{j\in X} t^i_j$. The objective is the make-span

$$g(x,t) = \max_{i} t^i(x^i),$$

and an allocation rule is a $c$-approximation if its make-span is at most $c$ times that of every allocation, on every type vector.

A mechanism $m = (o,p)$ gives each agent $i$ a set $A^i$ of strategies. On a strategy profile $a = (a^1,\dots,a^n)$ it outputs an allocation $o(a)$ and hands agent $i$ a payment $p^i(a)$. An agent of type $t^i$ has utility $p^i(a) - t^i(o^i(a))$. A strategy is dominant if it maximizes the agent's utility whatever the others play. The mechanism implements a $c$-approximation if every agent of every type has a dominant strategy and every profile of dominant strategies yields a $c$-approximate allocation.

A direct mechanism $(x,p)$ has $A^i$ equal to the set of types, and is truthful if reporting the true type is dominant. For a truthful mechanism, the price $p^i(X,t^{-i})$ is the payment agent $i$ receives when, against the others' reports $t^{-i}$, some report of its own makes it receive exactly $X$ (and $0$ if none does); the price difference is $\Delta^i(A,B) = p^i(A\cup B,t^{-i}) - p^i(A,t^{-i})$.

Formalization targets

Goal: Theorem 4.6

For every $n\ge 2$, $k\ge3$ and $c<2$, no mechanism with any strategy sets implements a $c$-approximation:

$$\forall\, (A, o, p):\quad \neg\ \mathrm{Implements}(o,p,c).$$

Milestones

1. Proposition 2.1 (revelation principle): a mechanism implementing a $c$-approximation yields a truthful direct mechanism whose allocation rule is a $c$-approximation.
2. Theorem 4.6 for truthful mechanisms (§4.3): no truthful direct mechanism has a $c$-approximate allocation rule for $c<2$. With milestone 1 it gives the goal.
3. Proposition 4.4 (independence): for a truthful mechanism, $t_1^{-i}=t_2^{-i}$ and $x^i(t_1)=x^i(t_2)$ imply $p^i(t_1)=p^i(t_2)$.
4. Proposition 4.5 (maximization): $x^i(t)$ maximizes $p^i(X,t^{-i}) - t^i(X)$ over attainable $X$.
5. Lemma 4.7: the price-difference inequalities satisfied by $x^i(t)$, and the uniqueness statement for sets satisfying them strictly.
6. Claim 4.8: for two agents, all-ones types and $0<\varepsilon<1$, moving agent 1's times to $\varepsilon$ on its own bundle and $1+\varepsilon$ elsewhere leaves the allocation unchanged.
7. The even case of the ratio: at that perturbed instance the mechanism's make-span is $|x^2(t)|$ while some allocation achieves $\tfrac12|x^2(t)| + k\varepsilon$.

Significance

The result. Theorem 4.6 shows that the requirement of dominant-strategy incentive compatibility, by itself, rules out approximation ratios below $2$ for scheduling on unrelated machines, a problem for which polynomial-time $2$-approximation algorithms that ignore incentives exist (Lenstra, Shmoys, Tardos 1990) and for which the exact optimum is computable in exponential time. Combined with the MinWork mechanism of the same paper (an $n$-approximation), it determines the optimal ratio for two machines. It is the base case of the Nisan–Ronen conjecture and the prototype of the "characterize truthful mechanisms by prices" technique used throughout later work on the conjecture.

Formalizing it. The theorem has been proved since 1999, but no machine-checked version is known to exist. The mission produces a formal account of general mechanisms with arbitrary strategy sets, dominant-strategy implementation, the revelation principle in that generality, and the price characterization of truthful mechanisms (independence and maximization). These are reusable for every other lower bound in this paper and for the later literature on the conjecture.

Difficulty

The statement quantifies over all mechanisms, with arbitrary strategy sets and arbitrary payment functions, so no finite search settles it. The revelation principle reduces to truthful direct mechanisms, but even these are an infinite-dimensional family: the allocation rule may break ties in any way, and prices may be any functions of the other agents' reports.

The printed argument also has two places that need care. Proposition 4.5 and Lemma 4.7, as printed, range over all sets of tasks, while Definition 12 gives unattainable sets price $0$; the statements hold only over attainable sets, and are formalized that way. And the case where agent 2's bundle has odd size is dispatched in one sentence ("which still yields the same allocation"), which the preceding lemma does not justify when agent 2's best bundle at the perturbed prices is not unique. A complete formal proof of the goal must supply an argument for that case.

Formalization scope

• Agents are Fin n, tasks Fin k; an allocation is a function Fin k → Fin n; bundles may be empty. The make-span is a finite maximum and assumes $n\ge1$ (NeZero n).
• Types, declarations and misreports are strictly positive reals throughout (Definition 10). Utility is quasi-linear; payments are handed to the agent and may have either sign.
• A general mechanism has strategy sets A : Fin n → Type u (any universe), output $o$ and payments $p$ on dependent strategy profiles. Implements requires both that every agent of every positive type has a dominant strategy and that every profile of dominant strategies yields a $c$-approximate allocation. Dominance is against every profile of the others, not only dominant ones. Without the existence clause, a mechanism with no dominant strategies would implement vacuously; the definition excludes that.
• Thresholds made explicit: $n\ge2$ and $k\ge3$, both taken from the proof ("We prove the theorem for the case of two agents"; "Let $k\ge3$"). The goal holds for each fixed $n$ and $k$ and every $c<2$, for every mechanism, with no restriction on tie-breaking and no requirement of strong truthfulness. At $n=1$ the claim is false.
• Proposition 2.1 is stated for task scheduling with the $c$-approximation specification; "truthful implementation" is read as truth-telling dominant and the truthful output $c$-approximate.
• Printed slips: Proposition 4.5 and Lemma 4.7 are stated over attainable sets; the "Moreover" of Lemma 4.7 requires $Y$ attainable. The odd case of the ratio step is not a milestone.
• The reduction from $n>2$ to two agents ("having the other agents be much slower") is not a separate milestone; the goal covers every $n\ge2$.
• Running time ("polynomial-time computable") is out of scope and not modelled.

Contributions of any of the milestones are welcome, as are alternative proofs of the goal that avoid the terse odd case.

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
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995 (revelation principle, p. 871).
• 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
• G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, Algorithmica 55 (2009).
• E. Koutsoupias, A. Vidali, A lower bound of 1+φ for truthful scheduling mechanisms, Algorithmica 66 (2013).
• G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023.

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

Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) asks how well a computational task can be carried out when its inputs are held by self-interested agents who may lie about them. Their test case is scheduling on unrelated machines: tasks must be assigned to agents (machines), each agent privately knows how long it needs for each task, and the planner wants to minimize the time at which the last agent finishes. The paper shows that the mechanism MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is truthful and loses a factor of at most $n$ against the optimum, and that no truthful mechanism can do better than a factor $2$. It then conjectures (Conjecture 4.9) that the factor $n$ cannot be improved by any truthful mechanism.

That conjecture became the Nisan–Ronen conjecture, one of the central questions of algorithmic mechanism design. A sequence of papers raised the general lower bound from $2$ to $1 + \sqrt 2$ (Christodoulou, Koutsoupias and Vidali), to $1 + \varphi \approx 2.618$ (Koutsoupias and Vidali) and to larger constants, and Christodoulou, Koutsoupias and Kovács (STOC 2023) finally proved the conjecture for all deterministic truthful mechanisms. In the original paper, Nisan and Ronen confirm the conjecture for two restricted classes of mechanisms, with short direct arguments. This mission concerns the second class, local mechanisms (Theorem 4.12).

Setting

There are $k$ tasks $j \in \{1, \dots, k\}$ and $n$ agents $i \in \{1, \dots, n\}$. A type vector $t$ records, for every agent $i$ and task $j$, the positive time $t^i_j$ agent $i$ needs for task $j$. An allocation $x$ assigns every task to one agent; $x^i$ is the set of tasks of agent $i$. For a set $X$ of tasks write $t^i(X) = \sum_{j \in X} t^i_j$. The make-span of $x$ is $g(x, t) = \max_i t^i(x^i)$.

A direct mechanism $(x, p)$ asks every agent for its type, computes an allocation $x(t)$ from the declarations, and hands agent $i$ the payment $p^i(t)$. Agent $i$'s utility is $p^i(t) - t^i(x^i(t))$ measured with its true times. The mechanism is truthful if declaring the true type maximizes each agent's utility whatever the other agents declare. The allocation rule is a $c$-approximation if $g(x(t), t) \le c \cdot g(y, t)$ for every type vector $t$ and every allocation $y$.

For a truthful mechanism the payment to agent $i$ depends only on the set it receives and on the declarations $t^{-i}$ of the others (Proposition 4.4). This gives the price offered to agent $i$ for a set $X$ (Definition 12):

$$p^i(X, t^{-i}) = \begin{cases} p^i(t'^i, t^{-i}) & \text{if some } t'^i \text{ gives } x^i(t'^i, t^{-i}) = X, \\ 0 & \text{otherwise.} \end{cases}$$

A mechanism is local (Definition 14) if $p^i(X, t^{-i})$ depends only on the other agents' times $\{t^l_j : l \ne i, j \in X\}$ on the tasks of $X$. MinWork is local: its price for $X$ is $\sum_{j \in X} \min_{l \ne i} t^l_j$.

Formalization targets

Goal: Theorem 4.12

For every $n \ge 1$, every $k \ge n^2$ and every real $c < n$, no truthful local mechanism is a $c$-approximation:

$$\forall (x, p) \text{ truthful and local},\ \forall c < n:\quad \exists\, t,\ y \quad g(x(t), t) > c \cdot g(y, t).$$

The bound holds for every $c < n$, so together with MinWork it shows that $n$ is the exact best ratio for local truthful mechanisms.

Milestones

1. Proposition 4.4 (Independence). Payments depend only on the allocated set and on $t^{-i}$.
2. Proposition 4.5 (Maximization). $x^i(t)$ maximizes $p^i(X, t^{-i}) - t^i(X)$ over the sets $X$ that agent $i$ can obtain.
3. Lemma 4.13. Every type vector has type vectors arbitrarily close to it at which each agent's maximizing set is unique.
4. Claim 4.14, first step. If $x^i(t)$ is the unique maximizer, lowering agent $i$'s times on $x^i(t)$ keeps $x^i(t)$.
5. Ratio step. An allocation that gives one agent $n$ tasks of time about $1$, while every other agent's own tasks are nearly free, has make-span about $n$, while splitting those $n$ tasks gives make-span about $1$.

Significance

The result. Theorem 4.12 settles the Nisan–Ronen conjecture for a natural class of mechanisms. Locality captures the mechanisms in which the price for a bundle of tasks is set only by the competition for those tasks. It includes MinWork and, more generally, every mechanism that prices tasks separately using the other agents' bids on them. The theorem says that for this class the trivial per-task auction is already optimal, so any improvement over the ratio $n$ must use prices that depend on the other agents' times on tasks outside the bundle.

Formalizing it. The statement is not open: it follows from the 2023 proof of the Nisan–Ronen conjecture, and Nisan and Ronen's own argument is much shorter. That argument is a sketch, though. Lemma 4.13 rests on an informal measure-theoretic appeal, and the core claim relies on a maximization property stated over all sets of tasks. A machine-checked proof pins down exactly which properties of truthful mechanisms the short argument needs. None of these results is known to have been formalized. The definitions (type vectors, truthful mechanisms, prices, locality) are shared with the other missions of this series.

Difficulty

An argument that looks at one agent at a time does not go through. Changing one agent's declaration changes the prices offered to every other agent, so an allocation that is stable for one agent can shift for another. The argument needs a type vector at which every agent's choice is strict, and only then can it lower times agent by agent and follow the allocation. Producing such a type vector is Lemma 4.13. The printed argument for it applies a "for almost every type vector" statement to sets defined by the price functions of an arbitrary mechanism, which need not be measurable. A proof must therefore work without any regularity of the mechanism. A second difficulty is Definition 12's convention that a set the agent cannot obtain has price $0$. Locality constrains these zero prices too, and the argument has to account for sets that are obtainable at one type vector and not at a nearby one.

Formalization scope

Agents are Fin n, tasks Fin k. An allocation is a function Fin k → Fin n, a type vector is Fin n → Fin k → ℝ, and a mechanism is a pair of functions alloc (declarations to allocation) and pay (declarations to the payment handed to each agent). Utilities are quasi-linear. All types, declarations and misreports are positive, and every truthfulness, locality and approximation quantifier ranges over positive type vectors. The make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]).

Conventions and explicit thresholds:

• $k \ge n^2$. The theorem is printed without a bound on the number of tasks, and its proof begins "Let $k \ge n^2$". The goal carries $k \ge n^2$ as a hypothesis.
• Truthfulness is assumed. §4.3 assumes throughout that the mechanism is truthful (by the revelation principle this is no loss). The goal quantifies over all truthful local mechanisms.
• Prices use Definition 12 literally, including the value $0$ for sets the agent cannot obtain, and locality is Definition 14 applied to that price function over all sets $X$, not only single tasks. When several declarations give the same set, the price uses one chosen witness; by Proposition 4.4 the choice does not matter for truthful mechanisms.
• Proposition 4.5 is stated over the sets the agent can obtain. As printed, over all subsets, it is false for a truthful mechanism that never leaves an agent idle and pays it negative amounts. Uniqueness of maximizers (Lemma 4.13, Claim 4.14) refers to the same family.
• Lemma 4.13 uses Mathlib's norm on Fin n → Fin k → ℝ, the sup norm. No measurability of the mechanism is assumed.
• Claim 4.14 is printed at $t^i_j = 1$ with $0 < \varepsilon < 1$. The first step is stated at any type vector, with $0 < \varepsilon \le t^i_j$ on the lowered tasks.
• Running time and computability are out of scope.

Ruled-out trivializations: locality is not restricted to single tasks; the goal does not assume that maximizers are unique at every type vector (that is Lemma 4.13's conclusion at one point, not a hypothesis); and the bound holds for every $c < n$, not for some.

Needed infrastructure: finite sums over allocation fibres, sup norms on function spaces, and a genericity argument for finitely many affine functions (Lemma 4.13). The model file and the price and locality definitions are reusable in the other missions of the series. Proofs of individual milestones are welcome independently.

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
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995 (pp. 876–880, basic properties of truthful mechanisms).
• G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, Algorithmica 55 (2009).
• E. Koutsoupias, A. Vidali, A lower bound of 1+φ for truthful scheduling mechanisms, Algorithmica 66 (2013).
• G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023.

Motivation

Algorithmic mechanism design, introduced by Nisan and Ronen (Games Econ. Behav. 35, 2001), studies optimization problems whose input is held by self-interested agents. Each agent reports its private data to a protocol, and the protocol must choose an output and payments so that reporting the truth is in every agent's interest while the chosen output is close to optimal.

The paper's test case is task scheduling on unrelated machines: $k$ tasks must be assigned to $n$ agents, agent $i$ needs time $t^i_j$ for task $j$, and the goal is to minimize the make-span. For deterministic mechanisms the paper shows that truthfulness is costly: the MinWork mechanism achieves ratio $n$, and no mechanism achieves a ratio below $2$ (Theorem 4.6). Section 4.4 asks whether randomization helps and answers yes for two agents: a randomized mechanism, truthful for every outcome of its coins, achieves expected ratio $7/4 < 2$.

Timeline.

• 1979: Roberts characterizes weighted (affine) maximizers; the weighted Vickrey–Groves–Clarke (VGC) mechanisms are truthful.
• 1999: Lehmann supplies the case analysis that improves the authors' original bound of $1.823$ to $7/4$ (acknowledged on p. 182).
• 2001: Nisan and Ronen publish the randomly biased min work mechanism and Theorem 4.16.

Setting

There are two agents, $1$ and $2$, and $k$ tasks. A type vector $t = (t^1, t^2)$ gives, for each agent $i$ and task $j$, the positive time $t^i_j$ agent $i$ needs for task $j$. An allocation $x$ assigns each task to one agent; $x^i$ is the set of tasks of agent $i$. The make-span of $x$ is

$$g(x, t) = \max_{i \in \{1,2\}} \sum_{j \in x^i} t^i_j .$$

A direct mechanism receives declared types $d$ and returns an allocation $x(d)$ and payments $p^i(d)$ handed to the agents. Agent $i$ with true type $t^i$ gets utility $p^i(d) - \sum_{j \in x^i(d)} t^i_j$. The mechanism is truthful if declaring the true type maximizes an agent's utility whatever the other agent declares, and strongly truthful if in addition every false declaration is strictly worse for some declaration of the other agent.

A randomized mechanism is a probability distribution over deterministic mechanisms; its objective is the expected make-span. It is universally truthful if every mechanism in its support is truthful, and universally strongly truthful if moreover truth-telling is the only strategy dominant in every mechanism of the support.

The biased min work mechanism with parameters $\beta \ge 1$ and $s \in \{1,2\}^k$ treats each task $j$ separately. With $i = s_j$ the favoured agent and $i' = 3 - i$ the other: if $t^i_j \le \beta \cdot t^{i'}_j$, task $j$ goes to $i$, who is paid $\beta \cdot t^{i'}_j$; otherwise it goes to $i'$, who is paid $\beta^{-1} \cdot t^i_j$. The randomly biased min work mechanism draws $s$ uniformly from $\{1,2\}^k$ and uses $\beta = 4/3$. Its expected make-span is

$$\mathbb{E}_s\, g(x_s(t), t) = \frac{1}{2^k} \sum_{s \in \{1,2\}^k} g(x_s(t), t).$$

Formalization targets

Goal: Theorem 4.16

For every $k$: the randomly biased min work mechanism is universally strongly truthful, and for every positive type vector $t$ and every allocation $y$,

$$\frac{1}{2^k} \sum_{s \in \{1,2\}^k} g(x_s(t), t) \le \frac74\, g(y, t).$$

Milestones

• Theorem 3.2 (Roberts): for positive weights $\beta^i$, a mechanism whose output maximizes $\sum_i \beta^i v^i(t^i, o)$ and whose payments are $p^i = \frac{1}{\beta^i}\sum_{j \ne i}\beta^j v^j(t^j, o) + h^i(t^{-i})$ is truthful.
• Lemma 4.15: for every $\beta \ge 1$ and every $s$, the biased min work mechanism is strongly truthful.
• Lemma 4.17: the randomly biased min work mechanism is universally strongly truthful.
• Claim 4.19, part 5: allocating two tasks independently at random gives an expected make-span no larger than allocating their merge at random.
• Reduced case (Fig. 2, Cases 1–3): for $a, b, c, d \ge 0$ with $a + c = \frac43 b + d$,

$$\tfrac14\Big(\max(a+b+c+\tfrac43 d, 0) + \max(a+b+c, d) + \max(a+b+\tfrac43 d, \tfrac43 c) + \max(a+b, \tfrac43 c + d)\Big) \le \tfrac74 (a+c).$$

• Lemma 4.18: the $7/4$ bound on the expected make-span.

Significance

The result. Theorem 4.16 separates randomized from deterministic truthful mechanisms for scheduling two unrelated machines: $7/4$ against the deterministic lower bound of $2$. The notion of truthfulness it uses is the strong one, dominance for every coin outcome, so the separation does not rest on agents being risk-neutral or knowing the distribution. Later work on truthful randomized scheduling, and on the gap between deterministic and randomized truthful mechanisms, starts from this construction.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it is known. A formalization produces a checked definition of universal truthfulness for randomized mechanisms, a checked weighted VGC theorem usable for any affine-maximizer mechanism, and a checked version of the reduction argument (Claim 4.19), which the paper states in five informal instance transformations, one of them a limiting argument.

Difficulty

Truthfulness reduces to one task at a time, where the mechanism is a weighted VGC mechanism; the difficulty lies in the approximation bound. A naive task-by-task comparison with the optimum fails: the bound is on a maximum of two loads averaged over $2^k$ coin vectors, and the maximum does not decompose over tasks. The paper reduces an arbitrary instance to four tasks through transformations that each move the ratio in one direction, and the reduced instance still needs a three-way case analysis. Making the reduction rigorous is the main work: part 1 of Claim 4.19 replaces a ratio "arbitrarily close to $\beta$" by $\beta$, and under the mechanism's tie rule a task with ratio exactly $\beta$ is allocated by the coin rather than to the efficient agent.

Formalization scope

• Agents are Fin 2 (agent $1$ is 0, agent $2$ is 1); the other agent is other i = 1 - i. Tasks are Fin k; allocations are functions Fin k → Fin 2. The statements hold for every $k$, including $k = 0$.
• Types are positive: every truthfulness quantifier ranges over positive declarations, true types and misreports, and the approximation bound is stated on positive type vectors. The reduced-case and merging milestones are pure real inequalities with nonnegative times, since the paper represents missing tasks by zero times.
• Payments are handed to the agent; utility is quasi-linear.
• The make-span is a finite maximum (Finset.sup') over the two agents. The expected make-span is the average over all $2^k$ vectors $s$, which is exactly the expectation of Definition 15 for the uniform distribution; no measure theory is used.
• Universal (strong) truthfulness quantifies over all $s \in \{1,2\}^k$, the support of the uniform distribution. Truthfulness in expectation over $s$ is weaker and is not the notion stated.
• The tie rule of Fig. 1 ($\le$: ties go to the favoured agent) is kept.
• The goal fixes $\beta = 4/3$; only Lemma 4.15 is stated for every $\beta \ge 1$. The ratio is compared with every allocation $y$, not with one fixed allocation, and the average is over all $s$, not the best $s$.
• Roberts' theorem is stated for arbitrary output sets, type sets and valuations, with positive weights.
• "Polynomial time computable" in Theorem 4.16 is not formalized; running time is out of scope.
• Claim 4.19 (the reduction to the four-task case) is not a separate item beyond its part 5, because its parts are instance transformations with a limiting step, not a single statement; a solver may formalize the reduction in any form that proves Lemma 4.18.

Contributions welcome: proofs of the milestones, and reusable lemmas on averages of maxima over product coin spaces.

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
• K. Roberts, The characterization of implementable choice rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979, pp. 321–349.
• T. Groves, Incentives in teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085

Motivation

Scheduling tasks on machines owned by self-interested parties is the running example of Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001), the paper that introduced the study of mechanisms whose allocation rule is an algorithm with a computational objective. Each machine (agent) privately knows how long it needs for each task; the designer wants to minimize the make-span, the completion time of the last machine, and can only influence the agents through payments.

Without further information the designer is in a weak position: the paper shows that no mechanism approximates the optimal make-span within a factor below 2 (Theorem 4.6), and that the natural truthful mechanism, MinWork, only achieves a factor $n$. Section 5 of the paper observes that in many applications the designer learns more than the agents' reports: it can pay after the work is done and observe how long each task actually took. It introduces mechanisms with verification and shows that, with this extra information, the make-span can be minimized exactly by a strongly truthful mechanism. This mission formalizes that result, Theorem 5.1, together with the steps of its proof and the participation variant, Theorem 5.4.

Setting

There are $k$ tasks and $n$ agents. The type of agent $i$ is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive numbers, $t^i_j$ being the least time in which agent $i$ can perform task $j$. An allocation $x$ gives each task to one agent; $x^i$ is the set of tasks of agent $i$. For a type vector $t$ and for a vector $\tilde t$ of actual execution times the make-spans are

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

A mechanism with verification is a pair $(x, p)$. The allocation $x(d)$ is computed from the agents' declarations $d = (d^1,\dots,d^n)$ only. Each agent then performs its tasks, in any times $\tilde t_j \ge t^i_j$ it chooses, and the mechanism pays agent $i$ the amount $p^i(d, \tilde t)$, which may depend on the declarations and on the observed actual times. Agent $i$'s utility is $p^i(d,\tilde t) - \sum_{j \in x^i} \tilde t_j$. A strategy of agent $i$ therefore has two parts: a declaration $d^i$ and an execution plan $e^i$ that says, for every allocation, how long the agent takes on each of its tasks.

A strategy is dominant if it maximizes the agent's utility against all declarations and all execution plans of the other agents. The mechanism is truthful if, for every agent and type, declaring the true type (with a suitable execution plan) is dominant, and strongly truthful if the only dominant strategy is to declare the true type and to execute every task in minimal time.

The Compensation-and-Bonus mechanism uses an optimal allocation algorithm $x(\cdot)$ and pays

$$p^i(d,\tilde t) = \underbrace{\sum_{j \in x^i(d)} \tilde t_j}_{\text{compensation } c^i} \;\underbrace{-\, g\big(x(d), \mathrm{corr}^i(x(d), d, \tilde t)\big)}_{\text{bonus } b^i},$$

where the corrected time vector $\mathrm{corr}^i$ lists agent $i$'s own tasks at their actual times and every other task at the time declared by the agent it was given to.

Formalization targets

Goal: Theorem 5.1

For $n \ge 2$ agents and every optimal allocation algorithm (ties broken arbitrarily), the Compensation-and-Bonus mechanism is a strongly truthful implementation of task scheduling:

$$\text{strongly truthful} \quad\text{and}\quad g\big(x(D), \tilde t\big) \le \min_y g(y, t) \text{ whenever every agent plays a dominant strategy for its true type.}$$

Milestones (proof of Claim 5.2)

1. The utility of every agent equals its bonus.
2. For every allocation, the bonus of agent $i$ is maximized by executing its tasks in minimal time.
3. With $t = (d^{-i}, t^i)$, for every declaration $t'^i$,

$$-g\big(x(t), \mathrm{corr}^*(x(t), t)\big) \ge -g\big(x(t'^i, d^{-i}), \mathrm{corr}^*(x(t'^i, d^{-i}), t)\big).$$

4. Declaring the true type and executing in minimal time is dominant.
5. Claim 5.2: the mechanism is strongly truthful.

Further target: Theorem 5.4

For $n \ge 2$ there is a strongly truthful mechanism with an optimal allocation algorithm that satisfies participation constraints: an agent that performs its tasks in its declared times never ends with negative utility.

Significance

The result. Theorem 5.1 shows that the lower bound of 2 for task scheduling (Theorem 4.6) is an artefact of the information structure, not of incentives as such: once execution times are observable, the exact optimum is achievable in dominant strategies, and the agents have a unique rational behaviour. The construction also isolates a general principle, used again in §5.6 of the paper: an agent paid by the global objective value, computed with the others' declarations, has the designer's incentives. Theorem 5.4 shows that the bonus can be shifted to make participation individually rational, which the plain mechanism violates (its bonus is negative).

Formalizing it. The theorem is proved in the paper, in a few lines, and has no machine-checked version. A formalization has to settle what the paper leaves informal: what a strategy with an execution part is, over which strategies of the others dominance is quantified, what "the only dominant strategy" demands of the execution plan on allocations that seem never to arise, and which hypotheses on the number of agents the uniqueness needs. The model built here is also the base of two companion missions of the same series (Compensation-and-Bonus with a non-optimal allocation algorithm, and the rounding mechanism with verification).

Difficulty

Truthfulness (milestones 1–4) is short once the model is right. The difficulty is uniqueness. For a misreport or a slow execution to be excluded, one must exhibit, for every alternative strategy, declarations of the other agents under which that strategy is strictly worse. The declarations must be positive, the optimal allocation algorithm breaks ties arbitrarily, and agent $i$'s slower execution only hurts it when agent $i$ is the bottleneck. The paper's proof dismisses this step with "clearly, … there are circumstances"; the naive reading ("the others declare $+\infty$ elsewhere") is not available in a model with finite positive times, and the uniqueness clause must also cover the execution plan on every allocation, not only on the allocation produced by truthful play.

Formalization scope

• Agents are Fin n, tasks Fin k, allocations functions Fin k → Fin n; both make-spans are Finset.sup' over the nonempty set of agents ([NeZero n]).
• Types and declarations are positive real vectors; declarations range over this type space (Definition 18's "unrestricted" declaration is any element of it).
• An execution plan is a function from allocations to actual times; feasibility for type $t^i$ requires $\tilde t_j \ge t^i_j$ on the agent's own tasks only. In the dominance quantifier the other agents' plans are arbitrary.
• Payments are amounts handed to the agent; utility is quasi-linear.
• The optimal allocation algorithm is a parameter with the hypothesis that it minimizes $g(\cdot, d)$ on every positive $d$; every theorem holds for every such algorithm.
• Strong truthfulness constrains both parts of the strategy: the declaration equals the type, and the plan executes every task in minimal time under every allocation.
• Thresholds made explicit: $n \ge 2$ in Claim 5.2, Theorem 5.1 and Theorem 5.4 (not printed; with one agent every declaration is dominant, and the construction of Theorem 5.4 needs a second agent).
• Printed slips: the displayed inequality prints >=; Theorem 5.4 prints "strongly truthfulmechanism"; Definition 28 writes $\tilde t_j = t_j$ for $\tilde t_j = t^i_j$.
• Running time is out of scope.
• A formalization in which dominance is checked only against truthful other agents, in which the mechanism ignores executions, in which strong truthfulness constrains only the declaration, or in which the implementation clause is stated only at the truthful profile, is not the theorem and is ruled out by the statements.

Welcome contributions: proofs of the milestones, the uniqueness witnesses as reusable lemmas, and the contribution-based mechanism behind Theorem 5.4. Theorem 5.3 (generalized Compensation-and-Bonus) is not stated in this mission.

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
• T. Groves, Incentives in Teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995.

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