← back to the atlas

Finding Fair Allocations under Budget Constraints (aaai23-25681)

Answer: \(\mathrm P\): every valid instance admits a rational \(\mathrm{EF2}\) allocation.

The anchor (named result in the paper)

Theorem 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor any given fair divi- sion instance with budget constraints ⟨[m], [n], {v(g)}g∈[m], {s(g)}g∈[m], {Ba}a∈[n]⟩, Algo- rithm 1 (DensestGreedy) computes an EF2 allocation in polynomial time.

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

The continuous mirror question, as graded

Given rational masses \(\lambda_r\) of recipient types \(r\) with budgets \(B_r\), and rational supplies \(\eta_q\) of indivisible item types \(q\) with sizes \(s_q\) and values \(v_q\), find rational masses \(y_{r,b}\) over integral bundles \(b \in \mathbb{Z}_{\ge 0}^Q\) satisfying \(s \cdot b \le B_r\), \(\sum_b y_{r,b} = \lambda_r\), and \(\sum_{r,b} y_{r,b} b_q \le \eta_q\). Treat unused supply as charity and require that every occupied bundle \(b\) of every recipient type is EF2 against every occupied bundle and every fitting integral charity subbundle, using the paper's additive-value envy predicate; decide whether such an allocation exists or output one.

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

A society is given by its support: \(\tau\geq1\) recipient types, each with positive binary-rational mass \(\lambda_r\), with \(\sum_r\lambda_r=1\), and positive rational budget \(B_r\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m\geq1\) item types \(q\), with positive binary-rational supplies \(\eta_q\), sizes \(s_q\), and values \(v_q\). All recipients share the additive valuation \(V(b)=\sum_qv_qb_q\); write \(S(b)=\sum_qs_qb_q\). Supplies need not sum to one, and equal value-to-size ratios are allowed.
An allocation consists of nonnegative rational masses \(y_{r,b}\) over integral bundles \(b\in\mathbb Z_{\geq0}^{m}\) with \(S(b)\leq B_r\), satisfying \(\sum_b y_{r,b}=\lambda_r\) and \(\sum_{r,b}y_{r,b}b_q\leq\eta_q\). Its charity vector is \(c_q=\eta_q-\sum_{r,b}y_{r,b}b_q\); a bundle is occupied when \(y_{r,b}>0\).
EF2 means that for every occupied \((r,b)\) and every integral \(f\) with \(S(f)\leq B_r\) that satisfies either \(f\leq b'\) for some occupied bundle \(b'\), or \(f\leq c\), there exists integral \(d\) with \(0\leq d\leq f\), \(\sum_qd_q\leq2\), and \(V(b)\geq V(f-d)\). Vector inequalities are componentwise; removals count individual copies, including copies of the same type. Comparisons include occupied bundles of the same recipient type.

Is deciding whether such a rational EF2 allocation exists in \(\mathrm P\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard, where \(L\) is the total binary input length?

For explicitly listed finite agents and indivisible goods, an EF2 allocation always exists and is computable in polynomial time ([Barman et al.](https://arxiv.org/pdf/2208.08168)).
For divisible goods and finitely many agents, feasible envy-freeness with charity can coexist with Pareto optimality ([Barman, Caragiannis, and Shyam](https://arxiv.org/abs/2603.00411)); this concerns divisible bundles, rather than distributions over integral bundles. No result settling the precise mass model above was located.

Modeling choices made when packaging the task

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

Result

The decision problem is in \(\mathrm P\): every valid input admits a rational EF2 allocation.

The finite-agent existence theorem transfers to this mass model by clearing denominators. The essential point is that normalization makes the charity vector componentwise smaller, so every required charity comparison remains covered.

Finite-agent theorem used

For finitely many agents and individual goods with positive rational sizes and values, identical additive valuations, and positive rational agent budgets, there exists a feasible allocation satisfying the following property: for every agent \(a\) and every budget-feasible subset \(F\) of another agent’s bundle or of the unallocated goods, removing at most two individual goods from \(F\) leaves value at most the value of \(a\)’s bundle.

This is Theorem 1 and Definition 1 of [Barman, Khan, Shyam, and Sreenivas](https://arxiv.org/pdf/2208.08168). Their Appendix A addresses equal densities. Subsets containing fewer than two goods satisfy the stated version simply by removing all their goods.

Clearing denominators and constructing the mass allocation

Choose a positive integer \(N\) such that all numbers

\(n_r:=N\lambda_r\quad\text{and}\quad K_q:=N\eta_q\)

are integers. Such an \(N\) exists because the masses and supplies are rational. Positivity implies that these integers are positive, and normalization gives

\(\sum_{r=1}^{\tau}n_r=N.\)

Construct a finite instance with \(n_r\) distinct agents of recipient type \(r\), each having budget \(B_r\), and \(K_q\) distinct individual goods of item type \(q\), each having size \(s_q\) and value \(v_q\). All agents have the given identical additive valuation. Thus every hypothesis of the finite-agent theorem holds.

Apply that theorem. For each finite agent \(a\), let \(A_a\) be its allocated set of goods, and let \(b(a)\) be its integral type-count vector. Define

\(k_{r,b}:=\bigl|\{a:\ a\text{ has type }r,\ b(a)=b\}\bigr|,\qquad y_{r,b}:=k_{r,b}/N.\)

These are nonnegative rational masses with finite support. Every occupied bundle satisfies its type’s budget because its corresponding finite agents do. Moreover,

\(\sum_b y_{r,b}=n_r/N=\lambda_r.\)

Let \(C_q\) denote the number of unallocated finite goods of item type \(q\). Counting allocated copies gives

\(\sum_{r,b}y_{r,b}b_q=(K_q-C_q)/N\leq\eta_q.\)

Consequently the mass allocation is feasible, and its charity vector satisfies

\(c_q=\eta_q-\sum_{r,b}y_{r,b}b_q=C_q/N.\)

Verification of every EF2 comparison

Fix any occupied pair \((r,b)\). Choose a finite agent \(a\) of type \(r\) whose allocated type-count vector is \(b\). Fix any integral \(f\) with \(S(f)\leq B_r\) that qualifies for a comparison in the question.

If \(\sum_q f_q\leq2\), take \(d=f\). Then \(V(f-d)=0\leq V(b)\). Hence assume \(\sum_q f_q>2\).

Comparison with an occupied bundle. Suppose \(f\leq b'\) for an occupied bundle \(b'\). Choose a finite agent \(a'\) receiving type-count vector \(b'\). There is a subset \(F\subseteq A_{a'}\) containing exactly \(f_q\) goods of each type \(q\). Its size is \(S(f)\leq B_r\).

If \(a'=a\), then \(f\leq b\), and positivity of values gives \(V(f)\leq V(b)\); take \(d=0\). Otherwise, the finite EF2 guarantee supplies a subset \(D\subseteq F\) of at most two individual goods such that the value of \(F\setminus D\) is at most \(V(b)\). Let \(d_q\) count the goods of type \(q\) in \(D\). Then

\(0\leq d\leq f,\qquad \sum_qd_q\leq2,\qquad V(f-d)\leq V(b).\)

This argument includes comparisons between occupied bundles of the same recipient type.

Comparison with charity. Suppose \(f\leq c\). Since \(N\geq1\) and \(C_q\geq0\),

\(f_q\leq c_q=C_q/N\leq C_q\)

for every item type \(q\). Therefore the finite charity contains a subset \(F\) with type-count vector exactly \(f\). It is budget-feasible for \(a\). Apply the finite EF2 guarantee against charity and count the removed goods by type to obtain the same three required inequalities for \(d\).

Individual copies remain distinct in the finite instance, so removing two copies of the same type is covered. These cases exhaust all comparisons in the definition. Thus the constructed rational allocation is EF2.

Decision complexity

On every input satisfying the stated hypotheses, the correct answer is YES. The decision algorithm therefore returns YES; if input validity must also be checked, those rational-arithmetic checks take polynomial time in the binary input length.

The expanded finite instance may be exponentially large. This limits the construction’s running time, but does not affect the polynomial-time decision result.

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is proved. Every valid input admits a rational EF2 allocation, so the stated existence decision problem is in \(\mathrm P\). I found no major or minor mathematical issues.

Step-by-step verification

Theorem 1 establishes feasible EF2 allocations for finite instances with positive rational sizes, values, and budgets and identical additive valuations. Definition 1 quantifies over every subset of another agent’s bundle or charity that fits the comparing agent’s budget. Appendix A, Proposition 3, explicitly handles equal densities while preserving EF2 for the original instance. Thus repeated copies and equal value-to-size ratios do not invalidate the application. [Barman et al., Theorem 1, Definition 1, and Appendix A](https://arxiv.org/pdf/2208.08168).

The paper’s definition addresses subsets containing at least two goods. The prover explicitly covers smaller subsets by removing all their goods, which is permitted by the task’s “at most two” definition. This reconciliation is correct.

There are finitely many rational masses and supplies, so a common positive integer denominator \(N\) exists. Consequently,
\[ n_r=N\lambda_r,\qquad K_q=N\eta_q \]
are positive integers. The normalization condition implies
\[ \sum_{r=1}^{\tau}n_r=N. \]

The resulting instance has finitely many agents and individual goods. Its budgets, sizes, values, and common valuation satisfy every hypothesis stated by the prover for the finite-agent theorem. No assumption that supplies sum to one is used.

Each \(k_{r,b}\) counts finitely many agents, so
\[ y_{r,b}=k_{r,b}/N \]
is a nonnegative rational number. Only bundles received by finite agents can have positive mass.

An occupied pair \((r,b)\) has a corresponding finite agent of type \(r\), so its bundle satisfies \(S(b)\leq B_r\). Counting all agents of type \(r\) gives exactly
\[ \sum_b y_{r,b}=\lambda_r. \]

Each allocated good contributes exactly once to its type’s allocated count. Therefore,
\[ \sum_{r,b}y_{r,b}b_q =\frac{K_q-C_q}{N} \leq\eta_q. \]
Substitution into the task’s charity definition yields
\[ c_q=\frac{C_q}{N}. \]
Both identities are exact; there is no rounding or integrality assumption on \(c_q\).

For an arbitrary occupied pair \((r,b)\), positive mass ensures the existence of a finite agent \(a\) receiving \(b\).

If \(f\leq b'\) for an occupied bundle \(b'\), a corresponding agent \(a'\) owns enough distinct copies to realize \(f\) as a subset \(F\). Its size is exactly \(S(f)\), hence it fits \(a\)’s budget.

When \(a'=a\), componentwise containment and positive values imply \(V(f)\leq V(b)\), so zero removals suffice. Otherwise, the finite EF2 guarantee applies. Counting the removed individual goods by type produces an integral vector \(d\) satisfying all three required conditions.

This also covers comparisons between different occupied bundles of the same recipient type. For comparisons involving at most two copies, the prover’s preliminary choice \(d=f\) is valid, including the empty bundle.

For an integral comparison vector \(f\leq c\), the prover correctly uses
\[ f_q\leq\frac{C_q}{N}\leq C_q, \]
since \(N\geq1\) and \(C_q\geq0\).

Thus the finite charity contains enough individual copies to realize \(f\). The subset remains budget-feasible because sizes and budgets were not rescaled. Applying finite EF2 and counting removed copies gives the required vector \(d\).

Crucially, the comparison uses a subset with count vector \(f\), rather than a scaled vector. The direction of the charity inequality is correct. Removing two distinct goods of the same type correctly counts as two removals.

The construction establishes existence for every valid input. Therefore, returning YES decides the problem on its stated domain. If malformed inputs must be rejected, checking positivity, rational encodings, and the mass normalization requires only polynomial-time exact rational arithmetic.

The potentially exponential finite expansion affects the running time of this construction, but the task asks for an existence decision algorithm. No polynomial bound on the construction or allocation output is needed for the asserted decision result.

Repair feedback

No additional clarification or mathematical repair is required. The proof establishes universal rational existence and polynomial-time decision complexity. It does not establish a polynomial-time algorithm for outputting an allocation in the compressed input model, and it correctly acknowledges that limitation.

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