← back to the atlas

d4-conf-sagt-2021-0027 (d4-conf-sagt-2021-0027)

Answer: Polynomial-time solvable in \(m,\tau,L\); a qualifying assignment always exists.

The anchor (named result in the paper)

Theorem 5.4 — class: algorithmic

The continuous mirror question, as graded

Given rational type masses \(\mu_t\), additive values \(v_t(g)\), per-capita supplies \(q_g\) for finitely many item categories \(g\), and a target \(\alpha\in(0,1]\), can one compute in time polynomial in the number of categories, support size \(\tau\), and input bit length a finite-support assignment of masses \(x_{t,b,p}\) to integral bundles \(b\in\mathbb{Z}_{\ge 0}^{G}\) and transfers \(p\)? Require each type’s assigned mass to equal \(\mu_t\), each category’s per-capita supply to equal \(q_g\), transfers to balance, and every positive-mass class to be envy-free toward every other positive-mass class. The assignment must have utilitarian welfare at least \(\alpha W^*\) and per-capita total transfer at most \(\alpha M^*+2\), where \(W^*\) is optimal per-capita welfare and \(M^*\) is the largest bundle value in a designated welfare-optimal assignment.

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

A society is given by its support: the list of \(\tau\) types with positive binary-rational masses \(\mu_t\), normalized by \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m\) item categories \(G\), with binary-rational per-capita supplies \(q_g\geq0\), additive values \(v_t(g)\in[0,1]\), and a binary-rational target \(\alpha\in(0,1]\). Bundles are \(b\in\mathbb Z_{\geq0}^{G}\), with \(v_t(b)=\sum_g v_t(g)b_g\); transfers \(p\in\mathbb Q\) give utility \(v_t(b)+p\).
An assignment is a finite list of classes \((t,b,p)\) with positive rational masses \(x_{t,b,p}\), satisfying \(\sum_{b,p}x_{t,b,p}=\mu_t\), \(\sum_{t,b,p}x_{t,b,p}b_g=q_g\), and \(\sum_{t,b,p}x_{t,b,p}p=0\).
Envy-freeness requires \(v_t(b)+p\geq v_t(c)+r\) for every pair of positive-mass classes \((t,b,p)\) and \((s,c,r)\), including classes of the same type.
Let \(W^*\) be maximum per-capita utilitarian welfare over assignments satisfying only the mass and supply constraints. The input includes a designated finite rational assignment \(y^*_{t,b}\), promised to attain \(W^*\); set \(M^*=\max\{v_t(b):y^*_{t,b}>0\}\).
A qualifying assignment is envy-free and satisfies \(\sum_{t,b,p}x_{t,b,p}(v_t(b)+p)\geq\alpha W^*\) and \(\sum_{t,b,p}x_{t,b,p}|p|\leq\alpha M^*+2\). All integers and rationals use binary encoding; \(L\) is the total input bit length, including the designated assignment and \(\alpha\).

Is finding a qualifying assignment, or deciding that none exists, solvable in time polynomial in \(m,\tau,L\), or is this problem NP-hard?

For finite agents with normalized additive values, a polynomial-time algorithm achieves welfare at least \(\alpha\) times optimal and total absolute transfers at most \(n(\alpha\max_i v_i(A_i^*)+2)\). [Source](https://arxiv.org/pdf/2106.00841)
No result settling this exact mass-assignment problem with these welfare and transfer constraints was located in the literature search.

Modeling choices made when packaging the task

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

Result

The problem is polynomial-time solvable in \(m,\tau,L\). In fact, every input satisfying the promises admits a qualifying assignment.

The key is to simulate iterated maximum-weight matching without expanding rational masses into individual agents. Consecutive identical matching rounds can be batched, and only \(O(m)\) batches are needed.

1. Optimal welfare and a partial allocation

Define \(w_g=\max_t v_t(g)\), and extend this additively by \(w(b)=\sum_g w_gb_g\).

For every assignment satisfying the mass and supply constraints,

\[ \sum_{t,b}y_{t,b}v_t(b)\leq\sum_g q_gw_g. \]

Here and below, displayed formulas use the same mathematical notation as inline formulas.

The upper bound is attainable. Choose a positive integer \(N\) clearing the denominators of the masses and supplies. Form \(N\mu_t\) agents of each type and \(Nq_g\) copies of each category. Assign every item to an agent of a type maximizing its value. Dividing agent counts by \(N\) gives an admissible finite rational assignment. Consequently,

\(W^*=\sum_g q_gw_g.\)

Since the designated assignment attains this bound,

\(\sum_{t,b}y^*_{t,b}\sum_g b_g\bigl(w_g-v_t(g)\bigr)=0.\)

Every summand is nonnegative. Thus, whenever \(y^*_{t,b}>0\) and \(b_g>0\), we have \(v_t(g)=w_g\). In particular, every subbundle of such a bundle is valued by its designated type at its value under \(w\).

For each positive entry \(y^*_{t,b}\), select an integer subbundle \(X_{t,b}\leq b\) satisfying

\(\alpha v_t(b)\leq v_t(X_{t,b})\leq\alpha v_t(b)+1.\)

This can be done in polynomial time even when multiplicities are large: process the categories in order, taking whole multiplicities until the next category would reach the target, then take the required ceiling number of copies of that category. Categories of value zero can be skipped. If the target is zero, take the empty bundle. The overshoot is at most the value of one item, hence at most one.

Retain the original masses for these partial bundles. Their welfare is at least \(\alpha W^*\), and their supplies do not exceed the input supplies.

Put \(C=\alpha M^*+1\). For a partial class \(i\), with type \(t_i\), bundle \(X_i\), and mass \(a_i\), define its auxiliary subsidy by

\(A_i=C-w(X_i).\)

Because \(w(X_i)=v_{t_i}(X_i)\leq C\), we have \(0\leq A_i\leq C\). Moreover,

\(v_{t_i}(X_i)+A_i=C,\)

whereas, for every type \(t\) and every partial class \(i\),

\(v_t(X_i)+A_i\leq w(X_i)+A_i=C.\)

Thus the partial allocation is envy-free with these subsidies. Every type receives utility exactly \(C\).

It remains to allocate the residual supplies with subsidies between zero and one.

2. The finite matching theorem used

We use the following precise property of iterated maximum-weight matching.

Finite matching theorem. Consider finitely many agents with nonnegative additive valuations, with each item worth at most one to every agent. Repeatedly allocate one item to every agent using a maximum-weight matching between agents and remaining items; pad with zero-valued dummy items when necessary. The resulting allocation admits envy-eliminating subsidies between zero and one for every agent. This is proved for that matching procedure in Sections 3–4 of [Brustle et al., *One Dollar Each Eliminates Envy*](https://arxiv.org/pdf/1912.02797).

The theorem permits repeated valuations and arbitrary choices among maximum-weight matchings.

We will apply it to a finite expansion only to prove existence of bounded subsidies. Neither that expansion nor its individual matching rounds will be constructed.

3. A compact residual-allocation algorithm

We prove the following lemma.

Lemma. For positive rational type masses summing to one and nonnegative rational supplies \(r_g\), one can construct, in polynomial time, a finite rational assignment of those supplies admitting envy-eliminating subsidies in \([0,1]\).

3.1 Padding and a single round

If all supplies are zero, give everyone the empty bundle and subsidy zero.

Otherwise, put \(K=\lceil\sum_g r_g\rceil\), and introduce one dummy category with supply \(K-\sum_g r_g\) and value zero for every type. There are at most \(H=m+1\) categories, and total supply is the integer \(K\).

At any stage, let \(R_g\) denote the remaining supply. Its total is a nonnegative integer. Whenever this total is positive, it is at least one.

A fractional matching round is a solution of the transportation linear program

\(\max \sum_{t,g}v_t(g)z_{t,g},\)

subject to

\(\sum_g z_{t,g}=\mu_t\quad\text{for every }t,\)

\(\sum_t z_{t,g}\leq R_g\quad\text{for every }g,\)

and \(z_{t,g}\geq0\).

This program is feasible: if \(S=\sum_gR_g\geq1\), take \(z_{t,g}=\mu_tR_g/S\).

Fix an ordering of its coordinates. Among welfare-maximizing solutions, select the lexicographically largest coordinate vector. This is a unique vertex and can be obtained by polynomially many linear-programming calls: optimize welfare, fix its optimum, and then optimize and fix the coordinates successively.

Let

\(h_g=\sum_tz_{t,g}.\)

Thus \(\sum_gh_g=1\).

3.2 Batching repeated rounds

For the selected round, compute

\(k=\min_{g:h_g>0}\left\lfloor R_g/h_g\right\rfloor.\)

Because \(h_g\leq R_g\), we have \(k\geq1\).

Repeat this same round \(k\) times, then replace \(R_g\) by \(R_g-kh_g\). Store the pair consisting of the round profile \(z\) and its integer multiplicity \(k\).

Every repetition is a maximum-weight round. Indeed, the chosen profile remains feasible throughout the batch, while the feasible region only shrinks from that of the first round. A feasible maximizer of the larger region remains optimal in each smaller region.

3.3 Only linearly many batches occur

Call a category exhausted when its remaining supply becomes zero.

Suppose a selected round saturates a positive-supply category: \(h_g=R_g>0\). Then \(k=1\), so that batch exhausts the category.

Now suppose no positive-supply category is saturated. Consider the transportation program with the same available categories but without their supply upper bounds. Let \(z^0\) be its lexicographically selected welfare optimum.

We claim that the selected constrained optimum is \(z^0\). Otherwise, because every supply upper bound is slack, a sufficiently small positive movement from the constrained optimum toward \(z^0\) remains feasible. That movement improves the first differing objective in the ordered list consisting of welfare followed by the coordinates. This contradicts the constrained solution’s lexicographic optimality.

Therefore any round without a saturated category uses \(z^0\).

If its batch exhausts no category, the available-category set remains unchanged. Maximality of \(k\) ensures that, for some used category \(g\),

\(R_g-kh_g<h_g.\)

Hence \(z^0\) is infeasible at the next stage. The next selected round must therefore saturate a positive-supply category; otherwise the preceding claim would make it equal to \(z^0\). That next batch exhausts a category.

Thus every batch either exhausts a category itself or is immediately followed by a batch that does. Since at most \(H\) categories can be exhausted, there are at most \(2H\) batches.

4. Compact integer bundles and bounded subsidies

4.1 Polynomial encoding lengths

Choose a positive integer \(D\) clearing the denominators of all type masses and padded initial residual supplies. Its binary length is polynomial in the input length.

The transportation constraints are network-flow constraints. With integer masses \(D\mu_t\) and capacities \(DR_g\), their vertices are integral. Consequently, every selected vertex satisfies

\(Dz_{t,g}\in\mathbb Z_{\geq0}.\)

After a batch, \(D(R_g-kh_g)\) is again an integer. Thus this same denominator \(D\) works throughout the algorithm.

All remaining supplies are bounded by the initial supplies, and every batch multiplicity is at most \(K\). Their binary lengths remain polynomial. The linear programs have polynomial dimension and polynomial coefficient lengths.

4.2 Constructing a short list of integer bundles

Represent the agents of type \(t\) by an interval of length \(\mu_t\).

For each batch, partition this interval into consecutive pieces of lengths \(z_{t,g}\). A point in the piece for category \(g\) receives \(k\) copies of that category in the batch.

Refine the type interval at all boundaries from all batches. On each resulting cell, the complete integer bundle is constant. Because there are at most \(2H\) batches and at most \(H\) pieces per type per batch, there are \(O(\tau H^2)\) cells.

A cell’s rational length is its mass. The resulting finite assignment satisfies all type masses and padded supply equalities. Each bundle has exactly \(K\) items counting dummy items, so each coordinate has binary length at most \(O(\log(K+1))\).

Discard the dummy items.

4.3 Why subsidies in \([0,1]\) exist

For this proof only, expand the construction into \(D\) agents, with \(D\mu_t\) agents of type \(t\), and \(Dr_g\) item copies.

Every cell boundary is a multiple of \(1/D\), so the interval construction specifies an actual allocation to these agents.

Each fractional round realizes a matching: it assigns \(Dz_{t,g}\) type-\(t\) agents an item of category \(g\). This matching has maximum weight. Any matching of the expanded instance induces a feasible transportation profile, and its total weight is \(D\) times that profile’s objective value.

The entire batched construction is therefore a valid sequence of maximum-weight matching rounds in the expanded finite instance. All item values lie in \([0,1]\), including the dummy values. The finite matching theorem applies and gives subsidies in \([0,1]\).

To compute subsidies on the compact assignment, let residual cell \(j\) have type \(t_j\), bundle \(Y_j\), and mass \(b_j\). Solve the polynomial-size feasibility linear program

\(0\leq d_j\leq1,\)

\(v_{t_j}(Y_j)+d_j\geq v_{t_j}(Y_\ell)+d_\ell\quad\text{for all }j,\ell.\)

It is feasible. In the finite expansion, all agents corresponding to one cell have the same type and bundle; their mutual envy inequalities force their subsidies to be equal. Hence the finite theorem’s subsidies descend to a feasible vector for this compact program.

Its rational coefficients have polynomial encoding lengths, so a rational feasible vector of polynomial encoding length can be computed in polynomial time. This proves the lemma.

5. Combining the allocations

Apply the lemma to the residual supplies from Section 1.

For every partial class \(i\) and residual class \(j\) of the same type \(t\), create a combined class with

All these masses are positive rational numbers.

Because both component assignments have type mass \(\mu_t\), summing over \(j\) recovers \(a_i\), and summing over \(i\) recovers \(b_j\). Hence the combined assignment has the required type masses and full supplies.

To verify envy-freeness, compare an own combined class \((i,j)\) of type \(t\) with any combined class \((i',j')\). The partial-allocation inequalities give

\(v_t(X_i)+A_i=C\geq v_t(X_{i'})+A_{i'}.\)

The residual-allocation inequalities give

\(v_t(Y_j)+d_j\geq v_t(Y_{j'})+d_{j'}.\)

Adding them proves envy-freeness of the combined assignment, including comparisons between classes of the same type.

Nonnegative values imply that adding the residual bundles cannot reduce welfare. Therefore the combined allocation’s value welfare is at least \(\alpha W^*\).

6. Balanced transfers and the required bounds

Every combined subsidy satisfies

\(0\leq s_{i,j}\leq C+1=\alpha M^*+2.\)

Let its population-weighted mean be

\(\overline s=\sum_{i,j}x_{i,j}s_{i,j},\)

and define transfers by \(p_{i,j}=s_{i,j}-\overline s\).

Since the population mass is one,

\(\sum_{i,j}x_{i,j}p_{i,j}=0.\)

Subtracting the same constant from every subsidy preserves every envy inequality. Moreover, both \(s_{i,j}\) and \(\overline s\) belong to \([0,\alpha M^*+2]\), so

\(\sum_{i,j}x_{i,j}|p_{i,j}|\leq\alpha M^*+2.\)

Balanced transfers leave utilitarian welfare unchanged:

\(\sum_{i,j}x_{i,j}\bigl(v_{t_i}(B_{i,j})+p_{i,j}\bigr)=\sum_{i,j}x_{i,j}v_{t_i}(B_{i,j})\geq\alpha W^*.\)

Thus the assignment qualifies.

7. Running time and output size

Let \(J\) be the number of positive classes in the designated assignment. Its encoded list is part of the input, so \(J\) is polynomially bounded by \(L\).

Partial-bundle selection uses polynomially many rational arithmetic operations. The residual algorithm uses at most \(2(m+1)\) batches, polynomially many polynomial-size linear programs, and \(O(\tau(m+1)^2)\) residual classes. Combining the assignments creates at most the product of their class counts.

All bundle coordinates, masses, subsidies, and transfers have polynomial binary encoding lengths. Consequently, the complete construction, including its explicit output list, takes time polynomial in \(m,\tau,L\).

In particular, no promised input requires the algorithm to report nonexistence.

⟨structured verdict parsed — rendered above⟩

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

The argument establishes polynomial-time solvability under the intended binary-rational encoding of the valuations. I found no major error or missing mathematical lemma. There is one minor encoding assumption to state explicitly.

The task explicitly calls the masses, supplies, and target binary-rational, but describes the values only as \(v_t(g)\in[0,1]\). The prover’s exact arithmetic and rational linear programs assume that these values are also binary-rational numbers included in \(L\).

This is the natural intended interpretation of the computational problem, so it is a minor clarification rather than a substantive restriction.

Minimum clarification: Explicitly state that every \(v_t(g)\) is a binary-encoded rational and that its encoding contributes to \(L\).

The upper bound \(W^*\leq\sum_gq_gw_g\) follows directly from \(v_t(g)\leq w_g\), nonnegative bundle coordinates, and the supply equalities.

The finite expansion establishes attainability: clearing the mass and supply denominators gives integer agent and item counts, and every maximizing type has at least one representative because its mass is positive. Unrestricted bundle sizes allow every item to be allocated to a maximizing type. This expansion is used for existence, so its potentially exponential size does not invalidate the subsequent running-time claim.

The designated optimum therefore satisfies the displayed zero-sum identity. Its summands are nonnegative, so every category appearing in a positive-mass designated bundle has \(v_t(g)=w_g\). The conclusion about all subbundles follows.

The proposed category-by-category procedure reaches the target because \(\alpha\leq1\). At the category where it stops, the ceiling operation needs no more than the available multiplicity. Its overshoot is bounded by the value of one item, hence by one. Zero-value categories and a zero target are explicitly handled.

Thus each selected bundle satisfies
\(\alpha v_t(b)\leq v_t(X_{t,b})\leq\alpha v_t(b)+1\), and retaining the designated masses gives welfare at least \(\alpha W^*\).

Since \(w(X_i)=v_{t_i}(X_i)\leq\alpha M^*+1=C\), the auxiliary subsidies lie in \([0,C]\). The own-class utility equality and every cross-class utility inequality are valid. These inequalities include comparisons between classes of the same type.

The cited paper analyzes the stated procedure: repeatedly choose a maximum-weight matching on the remaining items and allocate one item per agent, with zero-valued dummy items where needed. Its analysis establishes subsidies of at most one per agent for the resulting allocation. It imposes no distinctness assumption on valuations or special tie-breaking requirement. See Algorithm 1 and Sections 3–4 of [Brustle et al., *One Dollar Each Eliminates Envy*](https://arxiv.org/pdf/1912.02797).

The prover states the relevant hypotheses precisely. The expanded residual instance has finitely many agents and items, nonnegative additive valuations, and individual item values in \([0,1]\). The theorem is applicable.

Padding makes the initial total supply an integer. Every round removes total mass one, so subsequent totals remain integers. Whenever the remaining total is positive, the displayed feasible profile is valid.

The transportation feasible region is bounded. Successively optimizing welfare and then every coordinate selects a unique point, which is a vertex of the original feasible polytope.

The batch multiplicity satisfies \(k\geq1\). Before each repetition, the selected profile remains feasible by the definition of \(k\). The new feasible region is contained in the first round’s feasible region, so retaining a feasible welfare maximizer preserves welfare optimality. This argument requires only maximum weight, which is exactly what the finite theorem needs.

If a positive-supply category is saturated, its ratio \(R_g/h_g\) is one, forcing \(k=1\), and that category is exhausted.

In the absence of saturation, every upper bound on an available category has positive slack. The stated small movement toward the unconstrained lexicographic optimum preserves feasibility. If the two solutions differ, that movement improves the first differing objective while preserving all preceding objectives. This contradicts lexicographic optimality.

Consequently, every round without saturation uses the same unconstrained profile for its current available-category set. If its maximal batch exhausts nothing, the available set remains unchanged, but at least one used category has remaining supply below the profile’s requirement. That profile is therefore infeasible next, forcing the next round to saturate a category.

The charging argument gives at most \(2H\) batches. It also covers termination: if the remaining total becomes zero, all remaining categories are exhausted. There is no dependence on the numerical magnitude of \(K\) in the batch count.

A common denominator for the masses and padded residual supplies has polynomial binary length. Scaling the transportation constraints by this denominator produces a network-flow polytope with integer data; its vertices are integral. The selected point is a vertex of that original polytope, so \(Dz_{t,g}\) is integral.

The batch updates preserve this denominator. Capacities never increase, and batch multiplicities are bounded by \(K\), so their encoding lengths remain polynomial.

The interval refinement correctly preserves correlations across batches without listing individual agents. With at most \(2H\) batches and at most \(H\) pieces per type per batch, the claimed \(O(\tau H^2)\) cell bound is valid. Nonempty cells have positive rational masses.

Each point receives one item in each conceptual round, hence exactly \(K\) padded items. Removing dummy items preserves all real-category supply equalities and all valuations.

Because every boundary is a multiple of \(1/D\), the interval construction can be interpreted consistently as an allocation to \(D\) agents. Each round assigns integer numbers \(Dz_{t,g}\) of agents to categories, within the remaining integer capacities.

Any matching of this expanded instance induces a feasible transportation profile. Its weight is \(D\) times the profile objective, so optimality of the selected profile establishes maximum weight of its matching realization. Repeated rounds within a batch remain valid by the feasibility argument already checked.

The finite theorem consequently supplies subsidies in \([0,1]\). Agents in the same cell have identical types and bundles; applying their mutual envy inequalities in both directions forces equal subsidies. Therefore those subsidies descend to the compact feasibility program.

Under the rational-value interpretation identified in item 1, this program has polynomially many variables and inequalities with polynomial coefficient lengths. Computing a rational feasible solution of polynomial encoding length is justified.

The product masses \(a_i b_j/\mu_t\) are positive because the component masses and \(\mu_t\) are positive. Their two marginal identities establish the required type masses and full supplies.

For an own combined class of type \(t\), both component envy inequalities compare against every possible opposing component class. Adding them proves the required combined envy inequality. No independence assumption about preferences is used beyond additivity.

Nonnegative residual values preserve the partial allocation’s welfare lower bound.

The combined subsidies and their population mean lie in \([0,\alpha M^*+2]\). Thus each centered transfer has absolute value at most \(\alpha M^*+2\); averaging over total population mass one gives exactly the required absolute-transfer bound.

Centering balances transfers and preserves all envy inequalities. Balanced transfers leave utilitarian welfare unchanged, so the welfare guarantee concerns the utility expression required by the task.

The designated class count is bounded by its explicit input length. The partial selection, bounded number of transportation programs, compact subsidy program, and product construction all have polynomial size. Products, divisions by positive rational masses, bundle evaluations, and transfer centering preserve polynomial encoding lengths.

The zero-residual case is explicitly handled. Zero supplies, zero valuations, \(M^*=0\), and \(\alpha=1\) do not break any step.

The prover has resolved the intended target, subject only to making the valuation encoding explicit. No further mathematical argument is needed to make the write-up 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.