Answer: —
Theorem 1 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateThe double round robin algorithm (Algorithm 1) returns an EF1 complete allocation in O(max{m2, mn}) time.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite type set \(T\), rational masses \(\mu_t\), rational per-capita supplies \(\rho_o\in[0,1]\) for item classes \(O\), and additive utilities \(u_t(o)\), find \(z_{t,B}\ge0\) over integral bundles \(B\subseteq O\) satisfying \(\sum_B z_{t,B}=\mu_t\) and \(\sum_{t,B\ni o}z_{t,B}=\rho_o\), such that for every ordered type pair \(t,s\) and every supported bundles \(B,D\), either \(u_t(B)\ge u_t(D)\) or some \(o\in B\cup D\) satisfies \(u_t(B\setminus\{o\})\ge u_t(D\setminus\{o\})\).
An instance has finite sets of types \(T\) and item classes \(O\), nonnegative rational masses \(\mu_t\), rational supplies \(\rho_o\in[0,1]\), and additive utilities \(u_t(B)=\sum_{o\in B}u_t(o)\).
A continuous allocation is numbers \(z_{t,B}\geq0\), for \(t\in T\) and \(B\subseteq O\), with \(\sum_B z_{t,B}=\mu_t\) and \(\sum_{t,B\ni o}z_{t,B}=\rho_o\) for every \(o\in O\). A bundle is supported for type \(t\) when \(z_{t,B}>0\).
It is EF1 if, for every ordered pair \(t,s\) and supported \(B,D\), either \(u_t(B)\geq u_t(D)\), or some \(o\in B\cup D\) satisfies \(u_t(B\setminus\{o\})\geq u_t(D\setminus\{o\})\).
Is feasibility of a continuous EF1 allocation in \(P\), or is it NP-hard?
For finite agents and indivisible items with additive utilities of either sign, a complete EF1 allocation can be computed in polynomial time by double round robin.
I do not settle the general complexity classification. I establish three partial results:
The complexity statements assume that the item utilities are rational and encoded in binary. The existence result in Section 4 also holds for real utilities.
For bundles \(B,D\subseteq O\), define
\(\Delta_t(B,D)=u_t(D)-u_t(B)\)
and
\(h_t(B,D)=\max\bigl(\{0\}\cup\{u_t(o):o\in D\setminus B\}\cup\{-u_t(o):o\in B\setminus D\}\bigr).\)
Lemma. The ordered comparison from type \(t\), holding \(B\), to bundle \(D\) satisfies EF1 exactly when
\(\Delta_t(B,D)\leq h_t(B,D).\)
Proof. If \(\Delta_t(B,D)\leq 0\), there is no envy. Otherwise, removing an item \(o\) from both bundles changes the envy gap to
\(\Delta_t(B,D)-u_t(o)\bigl(\mathbf{1}_{o\in D}-\mathbf{1}_{o\in B}\bigr).\)
Thus removing an item of \(D\setminus B\) reduces the gap by \(u_t(o)\), and removing an item of \(B\setminus D\) reduces it by \(-u_t(o)\). Removing a shared item leaves the gap unchanged. The claimed condition follows.
In particular, whether two labeled bundles are compatible can be checked in polynomial time.
Theorem. Every feasible instance has an EF1 allocation with at most \(|T|+|O|\) positive variables. These positive variables can be chosen rational with polynomial encoding length. Consequently, feasibility belongs to \(\mathrm{NP}\).
Proof. Let \(z\) be any feasible EF1 allocation, possibly with irrational entries, and let
\(S=\{(t,B):z_{t,B}>0\}.\)
Restrict the allocation variables to the labeled bundles in \(S\). The resulting allocation polytope is
\(P_S=\{x\in\mathbb{R}_{\geq 0}^{S}:Ax=b\},\)
where \(b\) consists of the masses and supplies. The column associated with \((t,B)\) has a \(1\) in type row \(t\), a \(1\) in each item row belonging to \(B\), and zeros elsewhere.
This polytope is nonempty because it contains \(z\). It is bounded because each variable associated with type \(t\) is at most \(\mu_t\). Hence it has an extreme point \(x\).
Every allocation in \(P_S\) is EF1: its support is a subset of \(S\), and deleting supported bundles cannot introduce a new pairwise violation.
Let \(J\) denote the positive coordinates of \(x\). The columns \(A_J\) are linearly independent. Otherwise, a nonzero vector \(d\) supported on \(J\) would satisfy \(Ad=0\). For sufficiently small positive \(\varepsilon\), both \(x+\varepsilon d\) and \(x-\varepsilon d\) would be nonnegative and belong to \(P_S\), contradicting extremality. Therefore
\(|J|\leq \operatorname{rank}(A)\leq |T|+|O|.\)
It remains to bound the encoding length. Put \(k=|J|\). Choose \(k\) rows on which the columns \(A_J\) form an invertible matrix \(C\). The positive coordinates solve
\(Cx_J=b',\)
where \(C\) is a square zero-one matrix and \(b'\) is a subvector of the rational input.
Let \(Q\) be the product of the denominators appearing in \(b\). Its binary length is at most the total encoding length of those denominators. Cramer's rule gives
\((x_J)_j=\dfrac{\det C_j(Qb')}{Q\det C},\)
where \(C_j(Qb')\) replaces column \(j\) of \(C\) by \(Qb'\). The determinant expansion yields
\(|\det C|\leq k!\)
and
\(|\det C_j(Qb')|\leq k!\max\{1,\|Qb'\|_\infty\}.\)
Thus each coordinate has polynomial encoding length.
A certificate lists these labeled bundles and their positive masses. A verifier checks the allocation equalities and all ordered comparisons between listed bundles using Section 1. There are polynomially many comparisons, and all arithmetic involves polynomial-length rational numbers. This proves membership in \(\mathrm{NP}\).
Theorem. Writing \(m=|O|\), feasibility can be decided in time \(f(m)\operatorname{poly}(L)\), where \(L\) is the input length.
Proof. Enumerate every family of bundles
\(\mathcal{F}\subseteq 2^O.\)
There are \(2^{2^m}\) such families. Interpret \(\mathcal{F}\) as a candidate family containing every bundle that will be supported by any type.
For each type \(t\), define its admissible bundles by
\(\mathcal{A}_t(\mathcal{F})=\{B\in\mathcal{F}:\Delta_t(B,D)\leq h_t(B,D)\text{ for every }D\in\mathcal{F}\}.\)
For this family, solve the rational linear feasibility problem with variables \(x_{t,B}\geq 0\), for \(B\in\mathcal{A}_t(\mathcal{F})\), subject to
\(\displaystyle\sum_{B\in\mathcal{A}_t(\mathcal{F})}x_{t,B}=\mu_t\quad\text{for every }t\in T,\)
and
\(\displaystyle\sum_{t\in T}\sum_{\substack{B\in\mathcal{A}_t(\mathcal{F})\\o\in B}}x_{t,B}=\rho_o\quad\text{for every }o\in O.\)
Accept if any of these linear programs is feasible.
For soundness, every supported bundle belongs to \(\mathcal{F}\). If \(B\) is supported for \(t\), its admissibility ensures the required comparison with every supported bundle \(D\).
For completeness, suppose an EF1 allocation exists. Choose \(\mathcal{F}\) to be exactly the union of its supported bundles over all types. Every bundle supported for \(t\) then belongs to \(\mathcal{A}_t(\mathcal{F})\), so that allocation satisfies the corresponding linear program.
Each program has at most \(|T|2^m\) variables and \(|T|+m\) equality constraints. Constructing it takes at most \(|T|4^m\) pairwise checks. Its rational encoding length is bounded by a function of \(m\) times a polynomial in \(L\). Polynomial-time rational linear programming therefore gives the asserted running time.
This proves polynomial-time solvability when the number of item classes is fixed, but not when it is unrestricted.
Put
\(M=\sum_{t\in T}\mu_t.\)
Theorem. Suppose there is an additive function \(v\) and scalars \(\alpha_t\in\mathbb{R}\) such that
\(u_t(o)=\alpha_t v(o)\quad\text{for every }t\in T,\ o\in O.\)
The scalars may be positive, negative, or zero. An EF1 allocation exists if and only if
\(\rho_o\leq M\quad\text{for every }o\in O.\)
For rational input, this gives a polynomial-time feasibility test.
Every allocation satisfies
\(\displaystyle\rho_o=\sum_{t,B\ni o}z_{t,B}\leq\sum_{t,B}z_{t,B}=M.\)
Conversely, suppose these inequalities hold. If \(M=0\), every supply is zero, and the zero allocation is EF1.
Assume \(M>0\), and put \(p_o=\rho_o/M\). Define a probability distribution on bundles by
\(\displaystyle q_B=\prod_{o\in B}p_o\prod_{o\notin B}(1-p_o).\)
The allocation \(z_{t,B}=\mu_tq_B\) has the prescribed type masses and supplies. Thus the polytope \(P\) of allocations satisfying the mass and supply constraints is nonempty. It is also compact, since it is closed and every coordinate lies between zero and its type mass.
Let \(c_t=\operatorname{sgn}(\alpha_t)\). First maximize
\(\displaystyle W(z)=\sum_{t,B}c_t v(B)z_{t,B}\)
over \(P\). Among its maximizers, minimize
\(\displaystyle Q(z)=\sum_{t,B}v(B)^2z_{t,B}.\)
Both objectives are continuous functions on finite-dimensional compact sets, so such an allocation \(z^*\) exists. These optimizations are used only for the existence proof.
We prove that \(z^*\) is EF1.
Let \(B\) be supported for \(t\), and \(D\) be supported for \(s\), with \(c_t\neq c_s\).
Exchange an equal positive amount \(\varepsilon\) of these two bundles between the types. Choosing \(\varepsilon\) no larger than either supporting mass makes this a feasible allocation: each type retains its mass, and aggregate item supplies remain unchanged.
The change in \(W\) is
\(\varepsilon(c_t-c_s)(v(D)-v(B)).\)
Optimality of \(W\) therefore implies
\((c_t-c_s)(v(B)-v(D))\geq 0.\)
If \(c_t=1\), then \(c_s<1\), so \(v(B)\geq v(D)\), and consequently \(u_t(B)\geq u_t(D)\).
If \(c_t=-1\), then \(c_s>-1\), so \(v(B)\leq v(D)\). Multiplication by the negative scalar \(\alpha_t\) again gives \(u_t(B)\geq u_t(D)\).
If \(c_t=0\), all utilities of type \(t\) are zero. Thus every ordered comparison between different sign groups is envy-free.
Suppose, toward a contradiction, that an ordered comparison from \((t,B)\) to \((s,D)\) violates EF1, with
\(c_t=c_s=c\in\{-1,1\}.\)
Define \(w=cv\). Then \(u_t=|\alpha_t|w\), so multiplying utilities by the positive constant \(|\alpha_t|\) does not change EF1. In particular,
\(\delta=w(D)-w(B)>0.\)
By Section 1, failure of EF1 implies that every positive quantity of either of the following forms is strictly less than \(\delta\):
At least one such positive quantity exists, because
\(\displaystyle\delta=\sum_{o\in D\setminus B}w(o)-\sum_{o\in B\setminus D}w(o)>0.\)
Choose one and call it \(r\). Thus \(0<r<\delta\).
If \(r=w(o)>0\) for \(o\in D\setminus B\), replace equal positive masses of \(B,D\) by
\(B'=B\cup\{o\},\qquad D'=D\setminus\{o\}.\)
If \(r=-w(o)>0\) for \(o\in B\setminus D\), instead use
\(B'=B\setminus\{o\},\qquad D'=D\cup\{o\}.\)
In either case, retain each modified bundle with its original type. This preserves all type masses and item supplies, and
\(w(B')=w(B)+r,\qquad w(D')=w(D)-r.\)
The value of \(W\) remains unchanged because both types have sign \(c\). Also, \(v(X)^2=w(X)^2\) for every bundle \(X\). Consequently, the change in \(Q\), for exchanged mass \(\varepsilon>0\), is
\(\varepsilon\bigl((w(B)+r)^2+(w(D)-r)^2-w(B)^2-w(D)^2\bigr)=2\varepsilon r(r-\delta)<0.\)
This contradicts the choice of \(z^*\).
Types with zero utility never envy. Together with Section 4.3, this proves that \(z^*\) is EF1 and completes the theorem.
For rational input, collinearity itself can be checked in polynomial time: choose any nonzero utility vector as \(v\), determine each candidate scalar from a nonzero coordinate of \(v\), and check all coordinates. If every utility vector is zero, the characterization applies directly.
The definition here disallows resolving envy by deleting only the other agent’s copy of a shared class. For nonnegative utilities, this is the distinction captured by fairness “without commons” in the literature on allocations with copies. See [Gafni, Huang, Lavi, and Talgam-Cohen](https://arxiv.org/abs/2109.08671).
A concrete example demonstrates the gap. Consider identical utilities with
\(u(c)=2,\qquad u(a)=u(b)=1,\)
and bundles
\(B=\{c\},\qquad D=\{c,a,b\}.\)
Under the ordinary interpretation with distinct physical copies, deleting the copy of \(c\) from the second bundle leaves value \(2\), equal to the first bundle’s value. The allocation therefore satisfies ordinary EF1.
Under the definition in the question, deleting \(c\) removes it from both bundles, leaving values \(0\) and \(2\). Deleting either \(a\) or \(b\) leaves values \(2\) and \(3\). Thus the ordered comparison from \(B\) to \(D\) violates the required EF1 condition.
This example only disproves a direct transfer of the finite-agent guarantee. It is not an infeasible continuous instance.
The arguments above establish membership in \(\mathrm{NP}\), an exact algorithm for a bounded number of classes, and a complete characterization for collinear utility vectors.
They provide neither a polynomial-time algorithm nor a hardness reduction for unrestricted utility vectors. That classification remains unresolved in this write-up.
⟨structured verdict parsed — rendered above⟩
Verdict: partial, with sound substantive results. The output establishes its three announced partial results under the stated binary rational input model. It does not resolve the unrestricted polynomial-time versus NP-hardness question, and explicitly acknowledges this. I found no false central step. The certificate proof has one minor omitted degenerate case.
1. Scope and input assumptions
The complexity claims explicitly assume binary-encoded rational utilities. This is a legitimate qualification: the task specifies rational masses and supplies but does not specify an encoding for utilities. The claims should retain this qualification.
Membership in \(\mathrm{NP}\), fixed-parameter tractability in the number of classes, and polynomial-time feasibility for collinear utilities do not classify the unrestricted problem. The final assessment must therefore be “partial,” regardless of the correctness of those results.
2. Exact pairwise EF1 condition
The calculation of the envy gap after deletion is correct:
\(\Delta_t(B,D)-u_t(o)(\mathbf{1}_{o\in D}-\mathbf{1}_{o\in B})\).
The three relevant possibilities are covered correctly:
Including zero in the maximum correctly incorporates the no-envy alternative. When the original gap is positive, a maximum large enough to eliminate it must come from an actual item, so the condition does not incorrectly permit a fictitious deletion.
Empty bundles, shared items, zero utilities, and negative utilities are all handled. For rational input, the comparison requires only polynomially many rational arithmetic operations of polynomial bit length.
Assessment: correct.
3. Polynomial-size certificates
The support restriction is valid. The original support is finite, and any allocation using a subset of it inherits every required EF1 comparison. No new labeled pair can appear.
The restricted feasible set is nonempty and bounded. The standard finite-dimensional polytope fact used here is that a nonempty bounded polyhedron has an extreme point; the stated hypotheses satisfy it.
The perturbation argument correctly proves that the columns corresponding to positive coordinates of an extreme point are independent. The perturbation is supported only on positive coordinates, so sufficiently small perturbations in either direction preserve nonnegativity. Thus the support bound \(|T|+|O|\) follows.
For positive support size \(k\), selecting an invertible \(k\)-row submatrix is justified by column independence. The Cramer’s rule expression is correct, including the denominator \(Q\det C\). The determinant bounds are also correct: each term in the replaced-column determinant contains exactly one entry from \(Qb'\), with all other factors zero or one.
The bit-length conclusion follows because:
The proposed certificate contains polynomially many bundle descriptions and rational masses. Checking its allocation equations and all ordered support comparisons suffices, including comparisons between bundles of the same type.
Minor issue: the determinant discussion does not separately handle \(k=0\). Feasible zero allocations can have empty support, and the displayed norm of an empty vector is not defined in the write-up.
Minimum clarification: explicitly dispose of the empty-support case before introducing Cramer’s rule. This is a routine edge-case clarification and does not affect the theorem.
Assessment: correct in substance, with this minor omission.
4. Algorithm parameterized by item classes
The enumeration contains exactly \(2^{2^m}\) candidate families.
Soundness is correct even if the chosen family contains bundles that ultimately receive zero mass: admissibility against the whole family implies admissibility against the actual support.
Completeness uses the correct quantifiers. If \(D\) belongs to the union of supported bundles, some type supports it. Hence the original EF1 condition supplies the comparison required for every bundle supported by type \(t\).
The bounds on variables, constraints, and pairwise checks are correct. The polynomial-time linear programming result needed is exact feasibility of explicitly represented rational linear systems in time polynomial in their binary encoding length. The displayed systems meet these hypotheses: their coefficient matrices contain only zeroes and ones, and their right-hand sides are rational input data.
Consequently, multiplying the enumeration count by the per-family construction and feasibility costs gives \(f(m)\operatorname{poly}(L)\), with a polynomial exponent independent of \(m\).
The empty family and types with zero mass cause no difficulty.
Assessment: correct. This establishes fixed-parameter tractability, not unrestricted polynomial time.
5. Collinear utility characterization
The necessity of \(\rho_o\leq M\) follows directly from nonnegativity and the mass equations.
The zero-total-mass case is handled explicitly. For positive total mass, the assumptions imply \(p_o\in[0,1]\), so the product distribution is valid and has the stated item marginals. Its use establishes ordinary feasibility without making an unsupported EF1 claim.
The feasible allocation set is finite-dimensional and compact. Both objectives are linear in the allocation variables, even though the coefficients of the second objective are squared bundle values. The first objective therefore attains its maximum, and its maximizer set is nonempty and compact; the second objective attains its minimum there. Real utility values do not invalidate this existence argument.
The whole-bundle exchange between different sign groups preserves all constraints. The displayed change in \(W\) has the correct sign. Its consequences for positive, negative, and zero utility types are all correct.
Within a nonzero sign group:
The argument also covers \(t=s\): a violation requires distinct original bundles, so a sufficiently small positive mass can be removed from both coordinates. Coincidences among modified and existing bundles do not invalidate the linear update.
The contradiction is therefore valid. Collinearity testing by exact rational coordinate ratios is polynomial time, with the all-zero case explicitly addressed.
Assessment: correct, including negative scalars and real utilities for the existence statement.
6. Finite-agent comparison
The example is numerically correct. The original values are \(2\) and \(4\). Deleting only the second agent’s physical copy of \(c\) produces equality at \(2\). Under the task’s deletion rule, deleting \(c\) gives values \(0\) and \(2\), while deleting either \(a\) or \(b\) gives \(2\) and \(3\). Thus the required comparison fails.
The cited paper does introduce fairness “without commons,” consistent with the contextual attribution. No theorem from that paper is needed for the example or earlier proofs. [Gafni, Huang, Lavi, and Talgam-Cohen](https://arxiv.org/abs/2109.08671)
The prover correctly limits the conclusion: this defeats a direct transfer of the finite-agent guarantee; it does not demonstrate an infeasible continuous instance.
Assessment: correct.
Actionable feedback
The existing partial results need only the empty-support clarification. Resolving the assigned target requires an additional unrestricted polynomial-time algorithm or a valid hardness reduction. That is substantive missing work, not an expositional repair. Nothing established here determines which alternative holds.
⟨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.