Answer: Polynomial-time solvable; every valid instance admits an EF allocation with bounded charity.
Theorem 2 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateGiven an instance I = ⟨D, N, f⟩with piece- wise constant functions f, the About-To-Envy-Satisfied Al- gorithm computes an EF-with-bounded-charity allocation X = (X1, . . . , Xn) in polynomial time.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite catalogue of valuation types with masses summing to one, piecewise-constant valuations over finitely many divisible items in k regions, and capacities normalized per unit population, construct a mass allocation assigning every mass element to exactly one region and satisfying EF with bounded charity, with envy checked supportwise against every occupied type-and-bundle configuration.
A society is given by its support: the list of \(\tau\) valuation types with positive binary-rational masses \(p_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m=k\geq1\) divisible cakes, one per region. Partition each cake into common constant-density cells; let \(B\) be the total number of cells and \(r(s)\) the region of cell \(s\). Cell capacities \(c_s>0\), measured per unit population, and densities \(a_{ts}\geq0\) are binary rationals, with \(\sum_s a_{ts}c_s=1\) for every type. Region totals need not be equal. Write \(v_t(x)=\sum_s a_{ts}x_s\).
A mass allocation is a finite list of configurations \((t_h,r_h,x^h,z_h)\), with rational masses \(z_h>0\) and rational bundles \(x^h\geq0\), where \(x_s^h=0\) unless \(r(s)=r_h\). Require \(\sum_{h:t_h=t}z_h=p_t\) and \(\sum_h z_hx_s^h\leq c_s\). Thus every mass element receives exactly one region assignment; a type may split across configurations. Bundles are consumption per mass element, and resource use is mass times bundle.
Let \(q_s=c_s-\sum_hz_hx_s^h\), and let \(q^{(r)}\) retain only the residual cells in region \(r\). EF with bounded charity means \(v_{t_h}(x^h)\geq v_{t_h}(x^\ell)\) for every occupied pair \(h,\ell\), and \(v_{t_h}(x^h)\geq v_{t_h}(q^{(r)})\) for every occupied configuration \(h\) and every region \(r\). Unallocated resources are permitted; ties satisfy these weak inequalities.
Is constructing such an allocation, or determining that none exists, solvable in polynomial time in \(m,\tau,B,L\), or is it NP-hard, where \(L\) is the total binary input length?
For finitely many agents with piecewise-constant valuations, EF with bounded charity can always be constructed in polynomial time; requiring complete allocation instead makes EF existence NP-complete. [Zhou et al. (2024)](https://ojs.aaai.org/index.php/AAAI/article/view/28861/29638)
No result settling this precise mass-allocation problem was located in the literature search.
The problem is solvable in polynomial time. Every valid instance admits an EF allocation with bounded charity. An allocation can be constructed with at most \(\tau m\) occupied configurations and polynomial binary encoding length.
The construction uses a linear Fisher market. The crucial step is to turn each type’s purchases into population groups receiving bundles from individual regions.
Let \(S_+=\{s:\text{there exists }t\text{ with }a_{ts}>0\}\). Cells outside \(S_+\) are worthless to every type and will remain unallocated.
For each \(s\in S_+\), create a divisible good of supply \(1\), representing the entire cell. Create one buyer for each type \(t\), with budget \(p_t\) and linear utility coefficients
\(\displaystyle d_{ts}=a_{ts}c_s.\)
Thus purchasing an amount \(w_{ts}\) of this normalized good corresponds to consuming \(c_sw_{ts}\) units of cell \(s\).
We use the following established algorithmic result: a linear Fisher market with positive rational budgets and nonnegative rational utility coefficients admits an equilibrium computable exactly in polynomial time, provided every buyer values some good and every good is valued by some buyer. Rational equilibrium prices and allocations of polynomial encoding length can be obtained. See Devanur, Papadimitriou, Saberi, and Vazirani, [*Market Equilibrium via a Primal–Dual Algorithm for a Convex Program*](https://www.nikhildevanur.com/pubs/DPSV-JACM.pdf), particularly Section 2, Lemma 7.1, and Theorem 8.12.
All hypotheses hold here:
Compute rational equilibrium prices \(P_s\) and allocations \(w_{ts}\).
Here \(P_s\) is the price of one unit of the normalized good, hence the price of the entire original cell.
Every \(P_s\) is positive. Indeed, if a retained good had price zero, a buyer valuing it could obtain arbitrarily large utility at no cost, contradicting the existence of a utility-maximizing bundle under that buyer’s budget.
Market clearing therefore gives
\(\displaystyle \sum_t w_{ts}=1\qquad(s\in S_+).\)
Define
\(\displaystyle \beta_t=\max_{s\in S_+}\frac{d_{ts}}{P_s}>0.\)
Each buyer spends its entire budget: otherwise it could purchase more of a positively valued good and increase its utility. Thus
\(\displaystyle \sum_{s\in S_+}P_sw_{ts}=p_t.\)
Furthermore,
\(\displaystyle w_{ts}>0\quad\Longrightarrow\quad \frac{d_{ts}}{P_s}=\beta_t.\)
To justify this implication, suppose a buyer purchased a positive amount of a good with a strictly smaller utility-to-price ratio. Moving a positive amount of expenditure from that good to a maximizing good would preserve expenditure and strictly increase utility, contradicting optimality.
Define the price per unit of original cell capacity by
\(\displaystyle \lambda_s=\frac{P_s}{c_s}\qquad(s\in S_+).\)
Consequently,
\(\displaystyle a_{ts}\leq\beta_t\lambda_s,\)
with equality whenever \(w_{ts}>0\).
For each type \(t\) and region \(r\), define
\(\displaystyle z_{tr}=\sum_{\substack{s\in S_+\\r(s)=r}}P_sw_{ts}.\)
Whenever \(z_{tr}>0\), create one configuration of type \(t\), assigned to region \(r\), with mass \(z_{tr}\) and bundle
\(\displaystyle x_s^{tr}= \begin{cases} c_sw_{ts}/z_{tr},&s\in S_+\text{ and }r(s)=r,\\ 0,&\text{otherwise}. \end{cases}\)
There are at most \(\tau m\) configurations. All masses and bundles are rational, and each bundle uses only its assigned region.
Every occupied bundle has price exactly \(1\):
\(\displaystyle \sum_{s\in S_+}\lambda_sx_s^{tr} =\frac{1}{z_{tr}}\sum_{\substack{s\in S_+\\r(s)=r}}P_sw_{ts} =1.\)
For every type \(t\),
\(\displaystyle \sum_{r:z_{tr}>0}z_{tr} =\sum_{s\in S_+}P_sw_{ts} =p_t.\)
Thus every type’s entire mass receives a region assignment.
If \(z_{tr}=0\), then \(w_{ts}=0\) for every retained cell \(s\) in region \(r\): the summands defining \(z_{tr}\) are nonnegative and every \(P_s\) is positive.
Hence, for each \(s\in S_+\),
\(\displaystyle \sum_{\substack{t,r\\z_{tr}>0}}z_{tr}x_s^{tr} =c_s\sum_t w_{ts} =c_s.\)
Every retained cell is fully allocated. Cells outside \(S_+\) receive no allocation, so all capacity constraints hold.
For an occupied configuration \((t,r)\), every cell with \(x_s^{tr}>0\) satisfies \(w_{ts}>0\), and therefore \(a_{ts}=\beta_t\lambda_s\). It follows that
\(\displaystyle v_t(x^{tr}) =\sum_s a_{ts}x_s^{tr} =\beta_t\sum_{s\in S_+}\lambda_sx_s^{tr} =\beta_t.\)
In particular, all occupied configurations of the same type give that type exactly the same utility.
Consider any occupied configuration \((u,r')\), evaluated by any type \(t\). The inequality \(a_{ts}\leq\beta_t\lambda_s\) gives
\(\displaystyle v_t(x^{ur'}) \leq\beta_t\sum_{s\in S_+}\lambda_sx_s^{ur'} =\beta_t.\)
Every occupied configuration \((t,r)\) has own utility \(\beta_t\). Therefore
\(\displaystyle v_t(x^{tr})\geq v_t(x^{ur'}).\)
This proves every required occupied-pair envy inequality.
The residual vector satisfies
\(\displaystyle q_s= \begin{cases} 0,&s\in S_+,\\ c_s,&s\notin S_+. \end{cases}\)
For \(s\notin S_+\), every \(a_{ts}=0\). Consequently, for every type \(t\) and region \(r'\),
\(\displaystyle v_t(q^{(r')})=0.\)
Since occupied configurations have utility \(\beta_t>0\), every bounded-charity inequality holds.
The auxiliary market has \(\tau\) buyers and at most \(B\) goods. Computing the products \(d_{ts}=a_{ts}c_s\) produces a market of encoding length polynomial in \(m,\tau,B,L\).
The exact Fisher-market algorithm returns rational \(P_s\) and \(w_{ts}\) of polynomial encoding length in polynomial time. Constructing \(z_{tr}\) and \(x_s^{tr}\) requires only polynomially many rational additions, multiplications, and divisions. Each division uses a strictly positive denominator. These operations preserve polynomial encoding length.
Thus the resulting list of at most \(\tau m\) configurations is an exact, polynomial-size output computable in polynomial time. No expansion of the rational population masses into individual agents is needed.
The construction uses precisely the stipulated interpretation: bundles are consumption per mass element, and resource use is mass times bundle. A coordinate \(x_s^{tr}\) may exceed \(c_s\); feasibility is ensured by the proved aggregate capacity equations.
Splitting a type’s population across regions permits every resulting group to receive a bundle of price \(1\) and the same utility. A finite indivisible agent cannot generally undergo this splitting, so the construction does not transfer to the finite-agent complete-allocation problem.
⟨structured verdict parsed — rendered above⟩
The prover’s claim is proved for the precise mass-allocation model in USER_TASK. The construction satisfies feasibility, envy-freeness, bounded charity, and the required exact polynomial-time output bound. I found no major or minor mathematical issues.
The conversion to unit-supply goods uses utility coefficients \(d_{ts}=a_{ts}c_s\), correctly accounting for the original capacities. Removing cells outside \(S_+\) removes only cells valued at zero by every type.
Every buyer has positive budget \(p_t\) and values at least one retained good, since \(\sum_s d_{ts}=1\). Every retained good has a buyer with positive valuation by definition. Thus the hypotheses of the stated Fisher-market result are satisfied.
The citation supports exact polynomial-time computation: Section 2 treats rational utility coefficients and budgets; the introduction explicitly confirms polynomial-bit rational prices and allocations; Lemma 7.1 and Theorem 8.12 supply the cited denominator and running-time results. The prover uses the corrected journal version. [Devanur et al., *Market Equilibrium via a Primal–Dual Algorithm for a Convex Program*](https://www.nikhildevanur.com/pubs/DPSV-JACM.pdf).
The proof that every retained good has positive price is valid under the standard Fisher demand model: buyers maximize utility over nonnegative bundles subject to their budget, without individual supply constraints. A positively valued zero-price good would prevent the existence of a maximizing bundle.
Positive prices justify the stated market-clearing equations. Positive budgets and at least one positively valued good justify full budget expenditure.
The expenditure-transfer argument correctly proves that a positively purchased good must attain the buyer’s maximum utility-to-price ratio. Consequently, \(\beta_t>0\), and the conversion \(\lambda_s=P_s/c_s\) yields
\[
a_{ts}\leq\beta_t\lambda_s
\]
on retained cells, with equality whenever \(w_{ts}>0\).
The regional expenditure \(z_{tr}\) is nonnegative. A configuration is created only when \(z_{tr}>0\), so its bundle formula never divides by zero.
Its mass and coordinates are rational and nonnegative, and its nonzero coordinates belong exclusively to region \(r\). There is at most one configuration for each type-region pair, giving the claimed bound of \(\tau m\).
The unit-price calculation is correct:
\[
\sum_{s\in S_+}\lambda_sx_s^{tr}=1.
\]
Summing \(z_{tr}\) over occupied regions counts precisely the buyer’s total expenditure, so the resulting masses sum to \(p_t\). In particular, every type has at least one occupied configuration.
The implication from \(z_{tr}=0\) to \(w_{ts}=0\) for all retained cells in that region follows from nonnegative summands and strictly positive prices. Thus discarding zero-mass pairs discards no purchases.
For each retained cell, multiplying each constructed bundle coordinate by its configuration mass cancels the defining denominator. The resulting aggregate consumption is exactly \(c_s\sum_t w_{ts}=c_s\). Removed cells receive no allocation.
These calculations establish precisely the resource constraints in the task. No upper bound on an individual bundle coordinate is required by that definition.
Each positive coordinate of a type’s own bundle comes from a positive market purchase, where the utility-price inequality is an equality. Combined with unit bundle price, this gives own utility exactly \(\beta_t\), independently of its assigned region.
For any occupied configuration of any other type, applying type \(t\)’s utility-price inequalities to its coordinates gives evaluated utility at most \(\beta_t\). All occupied bundles are supported on \(S_+\), so the absence of prices for removed cells causes no omission.
Hence the argument covers every ordered occupied pair, including pairs of configurations belonging to the same type. The weak inequalities required by the task hold.
The resource calculation leaves zero residual on every retained cell. Every other residual cell has zero density for every type. Therefore every regional residual has value zero to every type.
Each occupied configuration has utility \(\beta_t>0\), so all required charity inequalities hold. Unequal regional capacities and regions containing only worthless cells do not affect this conclusion.
The market has \(\tau\) buyers and at most \(B\) goods, with polynomial input encoding length. The cited exact algorithm provides polynomial-bit rational equilibrium data.
The subsequent formulas involve sums of at most \(B\) products and a bounded number of arithmetic operations per output coordinate. Their numerator and denominator lengths remain polynomial, including division by positive regional expenditure. Small positive masses therefore introduce no encoding obstruction.
There are at most \(\tau m\) configurations, each with at most \(B\) coordinates. Thus both construction time and total output length are polynomial in the requested parameters. Since every valid instance receives an allocation, the nonexistence branch is unnecessary.
Repair feedback: None is needed. The claim depends on the explicitly permitted population splitting and aggregate resource constraints, and the prover correctly identifies both.
⟨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.