← back to the atlas

d4-conf-sagt-2023-0003 (d4-conf-sagt-2023-0003)

Answer: Polynomial-time solvable; a direct mechanism satisfying every stated requirement exists for every input.

The anchor (named result in the paper)

Proposition 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor n agents with cost utilities, and n + 2 goods, there exists a picking sequence such that Sequential Allocation is strategyproof, and returns a Pareto efficient MMS allocation.

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

The continuous mirror question, as graded

Given a finite set \(J\) of voucher categories with rational costs \(c_j\), a rational per-capita supply vector \(b\) with \(\sum_{j\in J} b_j=1\), and a rational population distribution \(\mu\) over a finite support of approval types, define \(u_t(z)=\sum_{j\in t}c_jz_j\) for integral bundles \(z\in\mathbb Z_{\ge0}^{J}\). For each type \(t\), let \(M_t(b,c)\) be the supremum of \(v\) such that some distribution \(\pi\) over integral bundles has \(\mathbb E_\pi[z]=b\) and \(\pi(u_t(z)\ge v)=1\). Does there exist a direct mechanism, polynomial in the input bit length, that outputs polynomially represented bundle lotteries \((\pi_r^\mu)_{r\in\mathcal T}\) whose aggregate use is \(b\), gives every truthful type \(t\) its benchmark \(M_t(b,c)\) with probability one, is Pareto efficient among feasible measurable assignments, and satisfies \(\mathbb E_{\pi_t^\mu}[u_t(z)]\ge\mathbb E_{\pi_r^\mu}[u_t(z)]\) for every pair of types \(t,r\)?

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

Let \(J\) be a nonempty set of \(m\) voucher categories, with public costs \(c_j\in\mathbb Q_{\ge0}\) and supply \(b\in\mathbb Q_{\ge0}^{J}\), where \(\sum_j b_j=1\). The approval and report domain is \(\mathcal T=2^{\{j:c_j>0\}}\), including the empty type; bundles are \(z\in\mathbb Z_{\ge0}^{J}\), with utility \(u_t(z)=\sum_{j\in t}c_jz_j\).
A society is given by its support \(S\subseteq\mathcal T\): the list of its \(\tau\) types with positive binary rational masses \(\mu_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types; \(L\) is the total input bit length.
Define \(M_t(b,c)=\sup\{v\in\mathbb R_{\ge0}:\exists\pi,\ \mathbb E_\pi[z]=b,\ \Pr_\pi[u_t(z)\ge v]=1\}\), allowing arbitrary probability distributions on integral bundles with finite first moments.
A direct mechanism provides a lottery \(\pi_r^\mu\) for every report \(r\in\mathcal T\). Its representation is a succinct menu evaluator that, given a report, returns a finite list of integral bundles and rational probabilities; description size, list size, and numerical bit lengths must be polynomial in \(m,\tau,L\).
Require \(\sum_{t\in S}\mu_t\mathbb E_{\pi_t^\mu}[z]=b\), \(\Pr_{\pi_t^\mu}[u_t(z)\ge M_t(b,c)]=1\) for every \(t\in\mathcal T\), and \(\mathbb E_{\pi_t^\mu}[u_t(z)]\ge\mathbb E_{\pi_r^\mu}[u_t(z)]\) for every \(t,r\in\mathcal T\). An individual deviation leaves \(\mu\) fixed.
Model the population as an atomless probability space with type masses \(\mu\). Require Pareto efficiency in expected utility against all measurable assignments of bundle lotteries with aggregate expected supply \(b\): no alternative weakly improves almost everyone's utility and strictly improves it on a set of positive population mass.

Is there a direct mechanism satisfying these requirements for every input, with construction and report evaluation polynomial in \(m,\tau,L\), or is the associated feasibility/construction problem NP-hard?

For finite societies with \(n\) agents and \(n+2\) goods, a polynomial-time deterministic strategyproof mechanism produces a Pareto-efficient MMS allocation; with two agents and five goods, such a deterministic mechanism need not exist. [Botan et al.](https://arxiv.org/html/2407.13171v1)
No result settling the precisely defined distributional lottery problem above was located.

Modeling choices made when packaging the task

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

A polynomial-time mechanism exists

The distributional problem as stated is polynomial-time solvable. The construction below satisfies aggregate feasibility, the almost-sure benchmark guarantee for every type, strategyproofness for every pair of reports, and Pareto efficiency against arbitrary measurable lottery assignments.

The construction uses two features of the stated model: total expected supply is normalized to \(1\), and an individual deviation leaves \(\mu\) fixed.

1. Exact characterization of the benchmark

Let
\[ B=\{j\in J:b_j>0\}. \]
Because \(\sum_j b_j=1\), the set \(B\) is nonempty.

Lemma 1. For every \(t\in\mathcal T\),
\[ M_t(b,c)= \begin{cases} \min_{j\in B}c_j,&B\subseteq t,\\ 0,&B\not\subseteq t. \end{cases} \]
Both values are attained.

Proof. Consider any integral-bundle lottery with mean \(b\), and write
\[ N_t(z)=\sum_{j\in t}z_j. \]
If it guarantees a strictly positive utility, then \(N_t(z)\ge 1\) almost surely. Consequently,
\[ 1\le \mathbb E[N_t(z)] =\sum_{j\in t}b_j \le 1. \]
Equality forces \(B\subseteq t\). Thus, when \(B\not\subseteq t\), no strictly positive guarantee is possible. The guarantee \(0\) is attained, for example, by giving the singleton bundle \(e_j\) with probability \(b_j\).

Suppose now that \(B\subseteq t\). Every category in \(B\) has positive cost, since reports contain only positive-cost categories. The singleton lottery just described guarantees
\[ a=\min_{j\in B}c_j>0. \]

Conversely, any lottery guaranteeing a positive utility satisfies
\[ \sum_j z_j\ge 1 \quad\text{almost surely}, \qquad \mathbb E\!\left[\sum_j z_j\right]=1. \]
Hence \(\sum_j z_j=1\) almost surely. Moreover, \(z_j=0\) almost surely whenever \(b_j=0\). The lottery must therefore consist of singleton bundles, with probability \(b_j\) on \(e_j\). Every supplied category occurs with positive probability, so its guaranteed utility cannot exceed \(a\). This proves the formula and attainment. \(\square\)

Thus the nonzero benchmark requires an almost-surely nonempty bundle, consisting of supplied categories.

2. Constructing a fixed depletion schedule

Define the categories that some positive-mass type values:
\[ G=\{j\in J:b_j>0,\ c_j>0,\ \text{and }j\in s \text{ for some }s\in S\}. \]
Let
\[ q=\sum_{j\in G}b_j, \qquad d_j= \begin{cases} 0,&j\in G,\\ b_j,&j\notin G. \end{cases} \]
The vector \(d\) will be included in the expected bundle of every report. No supported type derives utility from its positive coordinates.

Fix a public ordering of categories to break cost ties. For a report \(r\) and a set \(A\subseteq G\), let \(i_r(A)\) be a category of maximum cost in \(r\cap A\), using that ordering. If \(r\cap A=\varnothing\), set \(i_r(A)=\bot\), and define \(e_\bot=0\).

Construct a schedule using only the fixed society \(\mu\):

\[ \rho_j=\sum_{\substack{s\in S\\i_s(A)=j}}\mu_s. \]

\[ h=\min_{\substack{j\in A\\\rho_j>0}}\frac{R_j}{\rho_j}. \]
Subtract \(h\rho_j\) from each residual supply and repeat.

Whenever \(A\ne\varnothing\), some consumption rate is positive: every remaining category has a supported approver, and that type selects some remaining approved category. Each phase exhausts at least one category. Thus the schedule ends after \(K\le m\) phases.

Write its available sets and durations as
\[ (A_1,h_1),\ldots,(A_K,h_K), \qquad T=\sum_{k=1}^K h_k. \]
When \(G=\varnothing\), take \(K=0\) and \(T=0\).

In phase \(k\), the total consumption rate is
\[ \lambda_k =\sum_{\substack{s\in S\\s\cap A_k\ne\varnothing}}\mu_s \le 1. \]
Since the schedule consumes exactly the supply in \(G\),
\[ q=\sum_{k=1}^K h_k\lambda_k \le \sum_{k=1}^K h_k=T. \tag{1} \]

For every report \(r\in\mathcal T\), define its expected bundle by
\[ x_r=d+\sum_{k=1}^K h_k e_{i_r(A_k)}. \tag{2} \]
This evaluates the report against the already constructed schedule. The schedule is not recomputed after an individual deviation.

3. Aggregate feasibility and strategyproofness

Lemma 2. The expected bundles in (2) satisfy aggregate feasibility and all expected-utility incentive constraints.

Proof of feasibility. For \(j\in G\), the schedule exhausts exactly \(b_j\), so
\[ \sum_{s\in S}\mu_s x_{s,j} =\sum_{k=1}^K h_k \sum_{\substack{s\in S\\i_s(A_k)=j}}\mu_s =b_j. \]
For \(j\notin G\), every report receives expected quantity \(d_j=b_j\), and the masses sum to \(1\). Hence
\[ \sum_{s\in S}\mu_s x_s=b. \]

Proof of strategyproofness. Fix arbitrary \(t,r\in\mathcal T\). Extend the utility formula linearly to nonnegative real vectors.

In each phase \(k\), truthful selection achieves
\[ u_t(e_{i_t(A_k)}) =\max\bigl(\{c_j:j\in t\cap A_k\}\cup\{0\}\bigr). \]
Any category selected by report \(r\) either belongs to \(t\cap A_k\), or gives type \(t\) utility zero. Therefore
\[ u_t(e_{i_t(A_k)}) \ge u_t(e_{i_r(A_k)}). \]
The common vector \(d\) contributes the same utility under both reports. Multiplying the phase inequalities by \(h_k\) and summing gives
\[ u_t(x_t)\ge u_t(x_r). \tag{3} \]
This holds for every pair of types, including types outside \(S\). \(\square\)

4. Finite lotteries preserving nonemptiness

The following rounding construction implements every expected bundle while controlling the total number of vouchers.

Lemma 3. Every rational vector \(x\in\mathbb Q_{\ge0}^J\) has a rational lottery on at most \(m+1\) integral bundles with mean \(x\). Every bundle in its support has total size at least
\[ \left\lfloor\sum_j x_j\right\rfloor. \]

Proof. Enumerate \(J\) as \(1,\ldots,m\), and set
\[ s_0=0, \qquad s_j=\sum_{\ell=1}^j x_\ell. \]
For a uniform random variable \(\alpha\in[0,1)\), define
\[ z_j(\alpha) =\lfloor s_j+\alpha\rfloor -\lfloor s_{j-1}+\alpha\rfloor. \tag{4} \]
These differences are nonnegative integers because the cumulative sums are nondecreasing.

For every nonnegative real \(a\),
\[ \mathbb E[\lfloor a+\alpha\rfloor]=a: \]
writing \(a=n+f\), where \(n\) is integral and \(0\le f<1\), the floor equals \(n+1\) with probability \(f\) and \(n\) otherwise. Consequently,
\[ \mathbb E[z_j(\alpha)]=s_j-s_{j-1}=x_j. \]
Telescoping also gives
\[ \sum_j z_j(\alpha)=\lfloor s_m+\alpha\rfloor \ge \lfloor s_m\rfloor. \tag{5} \]

The bundle changes only at the points
\[ 1-\{s_j\} \quad\text{with}\quad \{s_j\}>0, \]
where \(\{s_j\}\) denotes the fractional part. There are at most \(m\) such points. Partitioning \([0,1)\) at them gives at most \(m+1\) half-open intervals. Output the constant bundle on each interval with probability equal to its length. All endpoints and probabilities are rational. \(\square\)

For report \(r\), let \(\pi_r^\mu\) be the finite lottery obtained by applying Lemma 3 to \(x_r\).

Its mean is exactly \(x_r\), so aggregate feasibility and (3) give the required feasibility and strategyproofness for these lotteries.

Lemma 4. Every report’s lottery satisfies its almost-sure benchmark guarantee.

Proof. When \(B\not\subseteq t\), Lemma 1 gives \(M_t(b,c)=0\), and the guarantee follows from nonnegative utility.

Suppose \(B\subseteq t\). Type \(t\) approves every category in every nonempty \(A_k\), so it consumes at unit speed throughout the schedule. Therefore
\[ \sum_j x_{t,j} =\sum_j d_j+T =1-q+T \ge 1, \]
by (1).

Furthermore, \(x_{t,j}=0\) outside \(B\). Formula (4) then gives \(z_j=0\) outside \(B\) in every output bundle. By (5), every output bundle is nonempty. Each contains at least one category in \(B\), and therefore
\[ u_t(z)\ge \min_{j\in B}c_j=M_t(b,c). \]
Thus the benchmark is satisfied in every outcome of positive probability. \(\square\)

5. Pareto efficiency on the atomless population

Let \((\Omega,\mathcal F,P)\) be the population probability space, and let \(t(\omega)\) denote an individual’s type. The set of individuals whose type lies outside \(S\) has measure zero.

Define
\[ W=\sum_{j\in G}c_jb_j. \]

Lemma 5. Every measurable alternative lottery assignment with aggregate expected supply \(b\) has total expected utility at most \(W\). The constructed assignment attains \(W\).

Proof. For an alternative assignment, let \(y_j(\omega)\) be individual \(\omega\)’s expected quantity of category \(j\). Aggregate feasibility says
\[ \int_\Omega y_j(\omega)\,dP(\omega)=b_j. \]
By nonnegativity and finite aggregate supply, these quantities and the corresponding utilities are integrable.

Total expected utility is
\[ \int_\Omega \sum_{j\in t(\omega)}c_jy_j(\omega)\,dP(\omega) = \sum_j c_j \int_{\{\omega:j\in t(\omega)\}} y_j(\omega)\,dP(\omega). \tag{6} \]
For \(j\in G\), its contribution is at most \(c_jb_j\). For \(j\notin G\), its contribution is zero: either its cost is zero, its supply is zero, or its set of approvers has population measure zero. Thus (6) is at most \(W\).

In the constructed assignment, every unit consumed from \(G\) is assigned to a supported type that approves it. The schedule consumes all of \(b_j\) for each \(j\in G\). Hence its total expected utility is exactly \(W\). \(\square\)

If an alternative weakly improved almost everyone and strictly improved a set of positive measure, the utility difference would be an integrable, nonnegative function positive on a positive-measure set. Its integral would be strictly positive. That would make the alternative’s total utility exceed \(W\), contradicting Lemma 5.

Therefore the constructed assignment is Pareto efficient against the full class of measurable alternatives required in the question.

6. Polynomial construction and report evaluation

Only the listed support types are used to construct the schedule. Each of at most \(m\) phases requires finding their preferred remaining categories, summing rates, and updating at most \(m\) residual supplies. The number of rational operations is polynomial in \(m\) and \(\tau\).

It remains to verify polynomial numerical bit lengths.

Let \(D\) be the product of the denominators of the input masses, and let \(E\) be the product of the denominators of the input supplies. Both have bit length bounded by \(O(L)\). Every phase rate has the form
\[ \rho_j=\frac{a_j}{D}, \qquad 0\le a_j\le D, \]
with integral \(a_j\).

Initially, all residual supplies have common denominator \(E\). Suppose a phase’s residual supplies have common denominator \(EP\), and category \(\ell\), with positive rate \(a_\ell/D\), determines the phase duration. Writing its residual numerator as \(N_\ell\), the duration is
\[ h=\frac{DN_\ell}{EPa_\ell}. \]
If category \(j\) has residual numerator \(N_j\), its updated residual is
\[ \frac{N_ja_\ell-a_jN_\ell}{EPa_\ell}. \]
Thus each phase adds at most one factor bounded by \(D\) to the common denominator. After at most \(m\) phases, all durations and expected bundles have a common denominator dividing
\[ Q=E\prod_{k=1}^K a_{\ell_k}, \]
whose bit length is \(O((m+1)L)\).

Numerators also have polynomial bit length. Let
\[ \mu_{\min}=\min_{s\in S}\mu_s. \]
Every nonempty phase has at least one active supported type, so \(\lambda_k\ge\mu_{\min}\). Consequently,
\[ q=\sum_k h_k\lambda_k \ge \mu_{\min}T, \qquad T\le \frac{1}{\mu_{\min}}. \]
The reciprocal of \(\mu_{\min}\) has polynomial bit length, and every report’s total expected quantity is at most \(T+1\).

The menu evaluator stores the costs, tie order, vector \(d\), and at most \(m\) pairs \((A_k,h_k)\). Given a report, it:

All these operations, the menu description, the output list, and all numerical representations have size polynomial in \(m,\tau,L\). No enumeration of the full report domain is needed.

7. Conclusion

The construction gives a qualifying direct mechanism for every input. The benchmark is attained almost surely for every possible type, all reports satisfy the incentive inequalities with \(\mu\) fixed, and the supported population receives a Pareto-efficient allocation. Construction and report evaluation are polynomial in \(m,\tau,L\).

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the stated problem. The construction satisfies all four requirements, including guarantees and incentive constraints for types outside the population support. Its construction, menu representation, and report evaluation have polynomial size and running time. I found no mathematical errors or gaps requiring repair.

If a lottery guarantees positive utility to type \(t\), every outcome must contain at least one approved voucher. Thus \(\mathbb E[N_t(z)]\ge 1\). Since \(\sum_j b_j=1\), the displayed inequalities force \(\sum_{j\in t}b_j=1\), equivalently \(B\subseteq t\).

When \(B\subseteq t\), all supplied categories have positive cost because the report domain excludes zero-cost categories. A positive guarantee also forces total bundle size to be at least one almost surely. Its expectation is exactly one, so total bundle size equals one almost surely. Zero-mean nonnegative coordinates vanish almost surely. Consequently, the singleton probabilities are necessarily \(b_j\), and the maximum guarantee is exactly \(\min_{j\in B}c_j\).

The singleton lottery establishes attainment in both cases. This argument covers the empty type and inputs with supplied zero-cost categories: in those cases, \(B\subseteq t\) cannot hold for the relevant types, and the benchmark is zero.

Every category in \(G\) has a positive-mass supported approver. Therefore, whenever the available set is nonempty, at least one supported type selects a category, and some rate is positive. Every duration is consequently finite and strictly positive.

Taking the minimum residual-supply-to-rate ratio prevents negative residual supplies and exhausts at least one category per phase. Hence there are at most \(m\) phases, and the schedule exhausts exactly the supply in \(G\).

The identity \(q=\sum_k h_k\lambda_k\) correctly counts total consumption. Since \(\lambda_k\le 1\), the inequality \(q\le T\) follows. The explicit convention for \(G=\varnothing\) handles the empty schedule.

For categories in \(G\), summing supported types’ expected allocations reproduces the schedule’s aggregate consumption, which is \(b_j\). For other categories, the common vector \(d\) supplies exactly \(b_j\) after averaging over masses summing to one.

The incentive argument applies to arbitrary \(t,r\in\mathcal T\). In each fixed phase, truthful reporting selects a category maximizing the true type’s utility among available categories. Another report either selects a truly approved category of no greater cost or selects a category giving zero true utility. The common vector \(d\) cancels in the comparison.

Crucially, the phase sets and durations remain fixed under a deviation, exactly as stipulated in the task. No assumption that the deviating type belongs to \(S\) is used. Implementing the means by lotteries preserves these inequalities because utility is linear and the lotteries have finite first moments.

The floor differences in formula (4) are nonnegative integers. The stated expectation identity gives the required coordinate means, and telescoping gives the claimed lower bound on total bundle size.

Each cumulative sum contributes at most one breakpoint in \([0,1)\). Thus there are at most \(m+1\) intervals, with rational lengths and constant integral bundles. The half-open interval convention handles the breakpoints consistently; repeated breakpoints do not increase the support bound.

If \(x_j=0\), the adjacent cumulative sums coincide, so the corresponding output coordinate is zero in every bundle. This property is correctly used in the benchmark argument.

Types with zero benchmark satisfy the guarantee by nonnegative utility.

If \(B\subseteq t\), then \(t\) approves every category in every phase set, so its expected schedule allocation has total size \(T\). Including \(d\), its total expected quantity is \(1-q+T\ge 1\). Its expected bundle has no coordinates outside \(B\), and the rounding preserves those zeros.

Every output bundle therefore contains at least one voucher from \(B\). Every such voucher is approved by \(t\) and has cost at least \(\min_{j\in B}c_j\), proving the required guarantee. This reasoning also covers \(G=\varnothing\): then \(d=b\) and the expected total size is exactly one.

Finite aggregate expected supply and nonnegative quantities imply integrability of expected quantities and utilities, up to irrelevant null sets. The finite sum in formula (6) is therefore legitimate.

Each category in \(G\) contributes at most \(c_jb_j\) to total expected utility. A category outside \(G\) contributes zero for one of the reasons explicitly listed: zero cost, zero supply, or an approver set of population measure zero.

The construction attains the resulting bound \(W\), since every consumed voucher in \(G\) goes to a supported approver, and \(d\) gives supported types no utility.

Finally, an integrable utility improvement that is nonnegative almost everywhere and positive on a positive-measure set has strictly positive integral. Thus the stipulated Pareto improvement would contradict the established upper bound. The argument covers heterogeneous measurable alternatives within each type class, rather than only alternatives assigning a common lottery to each type.

The schedule uses at most \(m\) phases and only the explicitly listed \(\tau\) supported types. Its number of rational operations is polynomial.

The denominator calculation is valid. With mass denominator \(D\), every rate is \(a_j/D\), where \(0\le a_j\le D\). A phase introduces at most the additional factor \(a_\ell\) into the common residual denominator. The duration’s displayed denominator is the same updated denominator, so all durations, residuals, and report means have denominators dividing the stated \(Q\). Its bit length is \(O((m+1)L)\).

The bound \(T\le 1/\mu_{\min}\) controls magnitudes even when durations are large. Positive binary rational masses make this reciprocal have polynomial bit length. Together with the denominator bound, this establishes polynomial numerator lengths.

The stored schedule, cumulative sums, interval endpoints, probabilities, and integral output bundles consequently have polynomial representations. Exact rational arithmetic and comparisons therefore take polynomial time. Report evaluation does not enumerate the exponentially large report domain.

No additional clarification is needed to make the argument verifiable.

⟨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.