← back to the atlas

Fair and Truthful Mechanism with Limited Subsidy (aamas22-00063)

Answer: Polynomial-time implementable in \(m,\tau,L,\log N\), with polynomially many valuation queries.

The anchor (named result in the paper)

Theorem 3.1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor matroidal valuations, there is a polynomial- time implementable mechanism that is truthful, utilitarian optimal, and envy-free with each agent receiving subsidy 0 or 1, and the total subsidy being at most 𝑛−1. Before presenting our mechanism, let us illustrate the difficulty that arises by subsidizing agents: The following simple example shows that we have to give some subsidy to agents who want nothing even when the agents have binary additive valuations. Example 3.2.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given \(m\) indivisible goods, \(N\), a finite type set \(T\) of matroid-rank valuation oracles, and \(\mu\in\Delta(T)\) with \(\lambda_t=N\mu_t\in\mathbb{Z}_{\ge0}\), compute a mechanism for the \(\lambda_t\) identical agents that outputs integer counts \(x_{t,S,b}\) of agents receiving whole bundle \(S\subseteq M\) and subsidy \(b\in\{0,1\}\), satisfying \(\sum_{S,b}x_{t,S,b}=\lambda_t\), \(\sum_{t,S,b:e\in S}x_{t,S,b}\le1\), utilitarian optimality, envy-freeness across occupied cells, total subsidy at most \(N-1\), and truthful response to every unilateral report change \(t\to r\); determine whether this can be implemented in time polynomial in \(m\), \(|T|\), encoding length, and \(\log N\).

Packaged proof task (what the prover saw — nothing else)

Let \(M\) contain \(m\) indivisible goods and let \(N\ge1\) be binary encoded. A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass as a binary rational; \(\tau\) is the support size, not the number of possible types. Each type has a matroid-rank valuation oracle \(v_t\); require \(\mu_t>0\), \(\sum_t\mu_t=1\), and \(\lambda_t=N\mu_t\in\mathbb Z_{>0}\). Let \(L\) be the input bit length, excluding oracle truth tables, and charge one unit per valuation query.
A deterministic count mechanism maps every such society to a sparse list of binary integer counts \(x_{t,S,b}\ge0\), where \(S\subseteq M\) is a whole bundle and \(b\in\{0,1\}\) is a nonnegative subsidy. Unallocated goods are allowed.
Require \(\sum_{S,b}x_{t,S,b}=\lambda_t\), \(\sum_{t,S,b:e\in S}x_{t,S,b}\le1\) for every \(e\in M\), and \(\sum_{t,S,b}b x_{t,S,b}\le N-1\). The allocation must maximize \(\sum_{t,S,b}x_{t,S,b}v_t(S)\) over all feasible integer bundle allocations.
For every pair of occupied cells \((t,S,b)\) and \((r,R,c)\), require \(v_t(S)+b\ge v_t(R)+c\).
Truthfulness is independent of how identical agents are assigned to cells: if one agent changes report from \(t\) to any matroid-rank type \(r\), producing multiplicities \(\lambda'=\lambda-\mathbf e_t+\mathbf e_r\) and output \(x'\), require \(v_t(S)+b\ge v_t(R)+c\) whenever \(x_{t,S,b}>0\) and \(x'_{r,R,c}>0\). A new report supplies its oracle; zero-mass types are omitted from the resulting support.

Is implementing such a truthful count mechanism possible in time polynomial in \(m,\tau,L,\log N\), or is computing its required outcomes NP-hard?

For explicitly listed agents, a polynomial-time truthful mechanism achieves utilitarian optimality, envy-freeness, subsidies in \(\{0,1\}\), and total subsidy at most \(N-1\). [Verified full version](https://arxiv.org/html/2105.01801).
No result settling this binary-multiplicity implementation was located.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Result

Such a deterministic truthful count mechanism is implementable in time polynomial in \(m,\tau,L,\log N\), with polynomially many valuation queries.

The key is to cap each type’s multiplicity at \(m+1\), run the subsidized egalitarian mechanism on this smaller population, and restore the omitted copies through empty-bundle counts. The proof below verifies preservation of the subsidy rule and the question’s universal, cell-by-cell truthfulness requirement.

1. Definitions and the explicit-agent result

For a labelled population with valuation profile \(P=(v_i)_{i=1}^n\), an allocation \(A=(A_i)_{i=1}^n\) is clean if \(v_i(A_i)=|A_i|\) for every agent.

For a nonnegative vector \(a\) of length \(n\), let \(a^\uparrow\) denote its coordinates sorted increasingly, and define

\(F_k(a)=\sum_{j=1}^k a^\uparrow_j\), for \(1\leq k\leq n\).

An allocation is Lorenz dominating if its valuation vector has at least as large an \(F_k\) as every allocation, for every \(k\). Write \(\mathcal D(P)\) for the clean Lorenz-dominating allocations.

Restricting comparisons to clean allocations does not change this definition: every matroid-rank bundle contains a basis of the same value, so every allocation can be cleaned without changing its valuation vector.

We use the following explicit-agent result from the cited paper.

Subsidized egalitarian theorem. For matroid-rank valuations, \(\mathcal D(P)\) is nonempty. A member \(A\in\mathcal D(P)\) and the quantities

\(d_i(P)=\min_{B\in\mathcal D(P)}|B_i|\)

are polynomial-time computable. Put \(H(P)=\max_j|A_j|\) and assign

\(p_i(A)=\begin{cases}1,&|A_i|=d_i(P)\text{ and }|A_i|<H(P),\\0,&\text{otherwise}.\end{cases}\)

For every deterministic selection of \(A(P)\in\mathcal D(P)\), this rule is truthful and envy-free, with total subsidy at most \(n-1\). Each agent’s reported utility is independent of the selected allocation. These are Lemmas 3.5, 3.8, 3.12, 3.18 and Proposition 3.7 in [Goko et al., *Fair and Truthful Mechanism with Limited Subsidy*](https://arxiv.org/html/2105.01801).

The computational statement applies to our oracle model. Its allocation subroutines use matroid intersection on pairs \((i,e)\): a direct sum of agents’ matroids, possibly truncated, intersects a partition matroid forbidding repeated goods. Independence is tested using \(v_i(X)=|X|\). Thus valuation oracles suffice; truth tables are unnecessary.

The quantity \(H(P)\) is well-defined independently of \(A\): two Lorenz-dominating allocations dominate each other, so all their sorted prefix sums, and hence their sorted valuation vectors, coincide.

2. Compressing multiplicities preserves Lorenz dominance

For the given multiplicities, define

\(k_t=\min\{\lambda_t,m+1\},\qquad K=\sum_t k_t,\qquad D=N-K.\)

Let \(P_\lambda\) be a conceptual labelled population containing \(\lambda_t\) copies of each type, and \(P_k\) the reduced population containing \(k_t\) copies.

Lemma 1. Every clean allocation for \(P_\lambda\) can be compressed to a clean allocation for \(P_k\), preserving every nonempty bundle and its type. Its valuation vector is the reduced vector with \(D\) additional zero coordinates. Conversely, every reduced clean allocation extends to a full clean allocation by adding empty bundles.

Proof. Disjoint nonempty bundles use distinct goods, so any allocation has at most \(m\) nonempty bundles.

If a type is truncated, its retained multiplicity is \(m+1\). Consequently, all its nonempty bundles fit among retained copies. Permute bundles within each type so that every omitted copy has an empty bundle, and delete these copies. Equal-type permutations preserve cleanliness.

Conversely, adding empty bundles preserves feasibility and cleanliness. Each deleted or added coordinate has value zero. \(\square\)

For a nonnegative vector \(a\) of length \(K\), write \(a\oplus0^D\) for its extension by \(D\) zero coordinates. Directly from sorting,

\(F_\ell(a\oplus0^D)=\begin{cases}0,&1\leq\ell\leq D,\\F_{\ell-D}(a),&D<\ell\leq N.\end{cases}\)

Therefore, for two reduced vectors \(a,b\),

\(a\text{ Lorenz dominates }b\quad\Longleftrightarrow\quad a\oplus0^D\text{ Lorenz dominates }b\oplus0^D.\)

Lemma 2. Compression carries every member of \(\mathcal D(P_\lambda)\) into \(\mathcal D(P_k)\), and extension carries every member of \(\mathcal D(P_k)\) into \(\mathcal D(P_\lambda)\). Moreover, \(H(P_\lambda)=H(P_k)\).

Proof. If a full allocation is Lorenz dominating, compare it with the extension of any reduced clean allocation. The displayed prefix identity proves that its compression dominates that reduced allocation.

Conversely, suppose a reduced allocation is Lorenz dominating. Compress any full clean competitor using Lemma 1. Reduced dominance and the prefix identity show that the extended allocation dominates the full competitor.

Cleaning preserves every competitor’s valuation vector, so these comparisons also establish dominance over allocations that are not clean. Finally, adding zeros preserves the largest coordinate. \(\square\)

3. Compression preserves the subsidy calculation

We must preserve the individual minima \(d_i\), rather than merely welfare or the sorted size vector.

Choose \(k_t\) retained labelled copies of each type.

Lemma 3. For every retained agent \(i\),

\(d_i(P_\lambda)=d_i(P_k).\)

For every omitted agent \(i\), \(d_i(P_\lambda)=0\).

Proof. Any reduced Lorenz-dominating allocation extends while preserving agent \(i\)’s bundle. Thus

\(d_i(P_\lambda)\leq d_i(P_k).\)

For the reverse inequality, take any full Lorenz-dominating allocation and compress it while keeping \(i\)’s bundle fixed.

If \(i\)’s type is untruncated, all its copies are retained. Otherwise, \(k_t=m+1\). If \(i\) has an empty bundle, the other \(m\) retained copies can accommodate all nonempty bundles of that type. If \(i\) has a nonempty bundle, at most \(m-1\) other copies of its type have nonempty bundles. Compression preserving \(i\) is therefore possible in either case.

By Lemma 2, the compressed allocation is Lorenz dominating. Hence

\(d_i(P_k)\leq d_i(P_\lambda).\)

Now consider an omitted agent of type \(t\). Necessarily \(\lambda_t>m+1\). Every allocation has an empty-bundle copy of that type, since at most \(m\) agents have nonempty bundles. Starting with a full clean Lorenz-dominating allocation, permute equal-type copies so that this empty bundle belongs to the designated omitted agent. The allocation remains clean and Lorenz dominating, proving that its minimum is zero. \(\square\)

Let \(A\in\mathcal D(P_k)\), and extend it by empty bundles. Lemmas 2 and 3 show that each retained agent receives exactly the same SE subsidy in the full and reduced populations.

Every omitted agent has bundle size zero and minimum zero. Its full-population SE subsidy is consequently

\(\beta=\begin{cases}1,&H(P_k)>0,\\0,&H(P_k)=0.\end{cases}\)

Thus the full SE outcome is recovered from the reduced outcome by adding empty-bundle copies with subsidy \(\beta\).

4. The count mechanism

The mechanism performs the following steps.

Fixing traversal orders and tie-breaking in the explicit algorithm makes this count mechanism deterministic.

By the preceding lemmas, its output is the aggregation of a valid SE outcome for the original \(N\)-agent population.

The required properties follow as follows.

The construction also covers \(m=0\): all bundles and subsidies are empty and zero, respectively.

5. Truthfulness for every pair of occupied cells

This step verifies the requirement that no assignment of identical agents to cells be fixed in advance.

First, \(\mathcal D(P)\) is invariant under permutations of equal-type agents. Such permutations preserve feasibility, cleanliness and the sorted valuation vector. Consequently, \(d_i(P)\) is equal for all agents of a given type.

It follows that every assignment of a constructed count outcome to labelled agents of matching types is a valid SE outcome: it is a within-type permutation of the full outcome established above, and the subsidy formula is preserved.

Now fix a true type \(t\), a report \(r\), and arbitrary occupied cells

\(x_{t,S,b}>0,\qquad x'_{r,R,c}>0,\)

where the second output corresponds to \(\lambda'=\lambda-\mathbf e_t+\mathbf e_r\).

Choose a conceptual labelled population and a designated agent \(i\) of true type \(t\). Assign the first count outcome so that \(i\) receives \((S,b)\). This is a valid SE outcome at the labelled profile \(P\).

Change only agent \(i\)’s report to \(r\). The resulting labelled profile \(P'\) has exactly the prescribed multiplicities \(\lambda'\). Assign the second count outcome so that \(i\) receives \((R,c)\). This is a valid SE outcome at \(P'\).

If \(v_r\ne v_t\), then \(P\ne P'\). Select these two allocations at these two profiles, and select any clean Lorenz-dominating allocation elsewhere. The SE theorem applies to every such deterministic selector. Its truthfulness gives

\(v_t(S)+b\geq v_t(R)+c.\)

If \(v_r=v_t\), the labelled valuation profile is unchanged. Allocation independence of each agent’s SE utility gives equality between the two displayed utilities.

Because both occupied cells were arbitrary, this proves the question’s full universal truthfulness condition. The argument also covers a newly introduced report and the disappearance of a zero-multiplicity type.

6. Running time and output size

The explicit reduced population satisfies

\(K=\sum_t\min\{\lambda_t,m+1\}\leq\tau(m+1).\)

Therefore, the explicit SE computation takes polynomial time and polynomially many valuation queries in \(m,\tau\). Each copied agent’s query is forwarded to its type’s given valuation oracle.

Computing multiplicities, comparing them with \(m+1\), and restoring counts use binary arithmetic polynomial in \(L,\log N\). No omitted agent is instantiated.

There are at most \(m\) occupied nonempty-bundle cells, since every such cell consumes at least one distinct good. There are at most \(2\tau\) empty-bundle cells. Counts use at most \(O(\log(N+1))\) bits each, so the sparse output also has polynomial size.

This proves polynomial-time implementability in the specified input and oracle model.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

The output resolves the task. The compression preserves the full SE outcome, including the individual subsidy calculations, and the truthfulness argument establishes the required inequality for every pair of occupied cells. I found no major or minor mathematical issues.

The prover states the necessary theorem precisely: existence and polynomial-time computation of clean Lorenz-dominating allocations and individual minima, the specified subsidy formula, envy-freeness, truthfulness for arbitrary deterministic allocation selection, and allocation-independent reported utility.

These claims agree with the SE rule and the cited results. In particular, arbitrary selection is permitted; no fixed priority ordering is required. The paper’s computational discussion uses matroid intersection and optimization over allocation size vectors, consistent with the prover’s valuation-oracle implementation. The hypotheses hold here: valuations are matroid ranks, agents have quasilinear utility, and unallocated goods are permitted. [Goko et al., Sections 3.1–3.3](https://arxiv.org/html/2105.01801#S3).

The independence test \(v_i(X)=|X|\) is valid for matroid-rank valuations. Direct sums, truncations, and the partition constraint on goods therefore admit the required oracle access.

Every nonempty bundle consumes at least one distinct good, so at most \(m\) agents receive nonempty bundles.

A truncated type retains \(m+1\) copies, enough to accommodate all nonempty bundles of that type. Permuting bundles among equal-type agents preserves both feasibility and cleanliness. Every deleted bundle is empty and has value zero.

Conversely, adding empty bundles is feasible and clean. Thus the full feasible clean valuation vectors correspond, up to coordinate permutation, to reduced vectors with exactly \(D\) additional zeros. The lemma does not assert preservation of arbitrary labelled coordinates; that stronger requirement is addressed separately in Lemma 3.

All coordinates are nonnegative, so the displayed prefix-sum identity for adding zeros is correct. It also covers \(D=0\), when its first branch has no applicable index.

The forward implication compares a compressed full Lorenz-dominating allocation with every reduced competitor through extension. The reverse implication compares an extended reduced allocation with every full competitor through compression. Both comparisons use exactly the established prefix identity.

Cleaning arbitrary allocations preserves their valuation vectors, so restricting these arguments to clean competitors loses nothing. Adding zero coordinates preserves the maximum coordinate, establishing equality of \(H\).

Extension preserves a retained agent’s bundle, giving
\(d_i(P_\lambda)\leq d_i(P_k)\).

The reverse inequality requires compression while fixing that agent’s bundle. The prover checks both necessary cases:

For an untruncated type, all copies remain available. Consequently, the compression preserves the designated bundle and remains Lorenz dominating by Lemma 2, establishing the reverse inequality.

An omitted agent belongs to a type with more than \(m+1\) copies. Since at most \(m\) agents receive nonempty bundles, an empty bundle exists within that type. Equal-type permutation assigns it to the designated omitted agent while preserving Lorenz dominance. Hence its minimum is zero.

These facts justify the restoration subsidy \(\beta\) exactly, including the case \(H(P_k)=0\).

Aggregation and restoration give exactly \(\lambda_t\) copies of each type. Restored bundles are empty, so goods constraints remain satisfied.

Since \(N\geq1\), the reduced population has \(K\geq1\). The subsidy calculation is valid:
\[ \sum_{t,S,b}b x_{t,S,b}\leq K-1+D\beta\leq K-1+D=N-1. \]
Every subsidy remains in \(\{0,1\}\).

Lorenz dominance at the final prefix proves welfare optimality over all bundle allocations. Every such allocation is compatible with zero subsidies, so the subsidy budget does not exclude a welfare competitor.

Labelled envy-freeness gives the required inequality between any two occupied cells. For \(m=0\), all valuations and bundle sizes are zero, so the subsidy formula gives zero throughout.

Equal-type permutations preserve the set of clean Lorenz-dominating allocations and make the individual minima equal within each type. They consequently preserve the subsidy rule. Thus every assignment of the constructed counts to matching labelled agents is a valid SE outcome.

For any chosen truthful cell and any chosen deviating cell, the designated agent can receive those cells at the two respective labelled profiles.

When \(v_r\neq v_t\), the profiles differ. A single deterministic selector can therefore select both specified allocations. The theorem’s quantification over arbitrary selectors yields
\(v_t(S)+b\geq v_t(R)+c\).
This selector is only a device for invoking the theorem; it need not be the compressed algorithm’s selector.

When \(v_r=v_t\), the valuation profile is unchanged, and allocation-independent utility gives equality. This avoids assigning two different outputs to one profile within a deterministic selector.

The reasoning accommodates newly introduced reports and disappearing types. It does not assume consistency between the retained labels before and after a deviation, which is essential for the requested cell-by-cell condition.

The bound \(K\leq\tau(m+1)\) limits the explicitly instantiated population polynomially. Forwarding copied agents’ queries to their type oracles preserves the valuation-query model.

Exact rational arithmetic, multiplicity comparisons, and restored binary counts require polynomial bit complexity in \(L\) and \(\log N\). No operation enumerates the omitted agents.

At most \(m\) occupied cells have nonempty bundles, and at most \(2\tau\) have empty bundles. Bundle encodings and binary counts therefore give polynomial output size.

No additional clarification or repair is needed.

⟨structured verdict parsed — rendered above⟩

Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.