Answer: —
Theorem 10 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateLet an instance with n ≥2 agents and identi- cal binary utility functions be given. Then, the EF1 exchange graph is connected. Moreover, an EF1 exchange path be- tween any two allocations can be found in polynomial time.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given rational masses \(w_\theta\) of recipient types \(\theta=(b_\theta^0,b_\theta^1)\), a common binary utility on finitely many good types, rational masses of available goods, and fixed bundle size \(q\), does there exist a finite sequence of pairwise swaps of positive mass that moves every type's current bundle distribution from \(b_\theta^0\) to \(b_\theta^1\) while every occupied intermediate bundle pair satisfies EF1?
Definitions. Let \(T\) be a finite set of agent types, with rational masses \(\mu_t>0\) summing to \(1\), goods \(G\), per-capita supplies \(b_g\in\mathbb Q_{\ge0}\), integral bundle sizes \(s_t\), and additive utilities \(u_t\).
A state is \(x\in\mathbb Z_{\ge0}^{G}\) with \(\sum_g x_g=s_t\). A feasible distribution \(\rho=(\rho_t)_t\) has rational \(\rho_t(x)\ge0\), \(\sum_x\rho_t(x)=\mu_t\), and \(\sum_{t,x}\rho_t(x)x_g=b_g\).
It is EF1 if, for every \(t,t'\) and states \(x,y\) of positive respective mass, some \(g\) with \(y_g>0\) satisfies \(u_t(x)\ge u_t(y-e_g)\).
An exchange of rational mass \(\delta>0\) selects positive-mass states \(x,y\) of types \(t,t'\), goods \(g,h\) with \(x_g,y_h>0\), and moves mass \(\delta\) from \(x,y\) to \(x-e_g+e_h,y-e_h+e_g\), respectively.
Target. Is deciding whether rational EF1 distributions \(\rho^A\) and \(\rho^B\) are connected by a finite sequence of such exchanges whose intermediate distributions are EF1 in \(\mathrm P\), or is it NP-hard?
Nearest known results. For finitely many agents and individually distinct goods, deciding whether two EF1 allocations are connected by sequential exchanges through EF1 allocations is PSPACE-complete.
No exact complexity result for the type-mass formulation above was verified.
The general complexity classification is not resolved here. In particular, the arguments below establish neither a polynomial-time algorithm nor \( \mathrm{NP} \)-hardness for arbitrary bundle sizes.
They do establish four rigorous facts:
The known \( \mathrm{PSPACE} \)-completeness result concerns named agents and individually distinct goods. Its reduction does not immediately survive type aggregation because same-type mass can split and perform exchanges unavailable to a single named agent. See the [original AAAI paper](https://ojs.aaai.org/index.php/AAAI/article/download/28836/29592).
Throughout the positive exchange lemmas and examples below, utilities of goods are nonnegative, as is standard for goods. The threshold characterization itself does not require this assumption.
For an evaluator type \(t\) and a nonempty state \(y\), define its EF1 remainder value by
\(r_t(y)=u_t(y)-\max_{g:y_g>0}u_t(g)\).
Because utilities are additive, removing a unit of good \(g\) gives
\(u_t(y-e_g)=u_t(y)-u_t(g)\).
Consequently, there exists a good \(g\) with \(y_g>0\) satisfying
\(u_t(x)\ge u_t(y-e_g)\)
if and only if
\(u_t(x)\ge r_t(y)\).
Let \(S_i=\{x:\rho_i(x)>0\}\). Define
\(L_t(\rho)=\min_{x\in S_t}u_t(x)\)
and
\(R_t(\rho)=\max_{i\in T,\ y\in S_i}r_t(y)\).
A feasible distribution \( \rho \) is EF1 if and only if
\(L_t(\rho)\ge R_t(\rho)\)
for every evaluator type \(t\).
The EF1 definition requires \(u_t(x)\ge r_t(y)\) simultaneously for every \(x\in S_t\) and every globally supported \(y\). This family of inequalities is equivalent to the minimum of the left-hand sides being at least the maximum of the right-hand sides. ∎
This gives a useful union-of-polytopes description. For a threshold vector \(\alpha\in\mathbb R^T\), let
\(A_\alpha=\{(i,z):u_i(z)\ge\alpha_i\text{ and }r_t(z)\le\alpha_t\text{ for every }t\in T\}\).
Every feasible distribution supported on \(A_\alpha\) is EF1. Conversely, if \(\rho\) is EF1, choosing \(\alpha_t=R_t(\rho)\) shows that its support lies in \(A_\alpha\).
Thus the EF1 region is an exact union of transportation polytopes obtained by forbidding type-state pairs. It is not, in general, a single convex polytope.
Consider two types of mass \(1/2\), goods \(a,b,c\), bundle size \(2\), and supplies
\(b_a=3/4,\quad b_b=1/2,\quad b_c=3/4\).
Let the utilities be
\(u_1(a)=5,\quad u_1(b)=8,\quad u_1(c)=0\),
and
\(u_2(a)=7,\quad u_2(b)=2,\quad u_2(c)=0\).
Define \( \rho^P \) by
Define \( \rho^Q \) by
Both have aggregate supply \((3/4,1/2,3/4)\).
For \( \rho^P \), the type-\(1\) minimum own utility is \(8\), while its maximum remainder value is \(r_1(2a)=5\). The type-\(2\) minimum own utility and maximum remainder value are both \(7\). Hence \( \rho^P \) is EF1.
For \( \rho^Q \), the type-\(1\) minimum own utility and maximum remainder value are both \(5\). The corresponding values for type \(2\) are both \(2\). Hence \( \rho^Q \) is EF1.
For every \(0<\lambda<1\), however, the distribution
\(\lambda\rho^P+(1-\lambda)\rho^Q\)
supports both the type-\(2\) state \(b+c\), whose type-\(2\) utility is \(2\), and the state \(2a\), whose type-\(2\) remainder value is
\(r_2(2a)=14-7=7\).
Thus the mixture is not EF1. In particular, connectivity cannot be proved by linear interpolation.
Although arbitrary convex mixtures can fail EF1, the supports of two EF1 distributions differing by one exchange are compatible.
Assume all single-good utilities are nonnegative. Suppose \( \rho' \) is obtained from an EF1 distribution \( \rho \) by one exchange, and \( \rho' \) is also EF1. Then the union of their supports satisfies all EF1 inequalities. Consequently, every feasible distribution supported on a subset of that union is EF1.
Write the exchanged states as
\(x=X+e_g,\quad y=Y+e_h\),
and their destinations as
\(x'=X+e_h,\quad y'=Y+e_g\).
Fix any evaluator with additive utility \(v\), and write \(r_v\) for its remainder function.
For a fixed multiset \(Y\), the quantity
\(r_v(Y+e_a)=v(Y)+v(a)-\max\{\max_{k:Y_k>0}v(k),v(a)\}\)
is nondecreasing as \(v(a)\) increases.
The pre-exchange EF1 inequalities include
\(v(x)\ge r_v(y)\),
while the post-exchange inequalities include
\(v(x')\ge r_v(y')\).
If \(v(g)\le v(h)\), then \(v(x)\le v(x')\) and \(r_v(y')\le r_v(y)\). Therefore
\(v(x)\ge r_v(y')\)
and
\(v(x')\ge r_v(y)\).
If \(v(g)\ge v(h)\), the post-exchange inequality and the reversed monotonicities give the same two cross inequalities.
Interchanging the roles of \(x\) and \(y\) proves the corresponding inequalities involving \(y,y',x,x'\).
It remains to compare \(x\) directly with \(x'\). Removing the newly inserted unit \(h\) from \(x'\) leaves \(X\), so \(r_v(x')\le v(X)\). Nonnegativity gives \(v(x)=v(X)+v(g)\ge v(X)\), and hence \(v(x)\ge r_v(x')\). The reverse inequality \(v(x')\ge r_v(x)\) follows symmetrically. The same argument applies to \(y,y'\).
Every pair of states in the union is therefore either contained in one endpoint support or covered by one of the cross inequalities above. Hence the union satisfies EF1. Removing supported states cannot decrease a type’s minimum own utility or increase its maximum remainder value, proving the final assertion. ∎
This lemma shows that a full-mass exchange between EF1 endpoints can be refined into arbitrarily small exchanges without losing EF1. It does not imply global connectivity.
The following example proves that arbitrary rational splitting does not make every pair of EF1 distributions connected.
Let
\(T=\{1,2\},\quad \mu_1=\mu_2=1/2,\quad s_1=s_2=4\).
There are eight goods \(g_1,\ldots,g_8\), each with per-capita supply \(b_{g_i}=1/2\). Partition them into
\(H=\{g_1,g_2\},\quad M=\{g_3,g_4,g_5,g_6\},\quad Z=\{g_7,g_8\}\).
Utilities are constant on these groups:
Let
\(x=e_{g_1}+e_{g_2}+e_{g_7}+e_{g_8}\)
and
\(y=e_{g_3}+e_{g_4}+e_{g_5}+e_{g_6}\).
Define
\(\rho^A_1(x)=1/2,\quad \rho^A_2(y)=1/2\),
and
\(\rho^B_1(y)=1/2,\quad \rho^B_2(x)=1/2\).
Both distributions are feasible.
Both \( \rho^A \) and \( \rho^B \) are EF1, but no finite EF1 exchange sequence connects them.
For \( \rho^A \), type \(1\) has own utility \(u_1(x)=6\), while \(r_1(y)=8-2=6\). Type \(2\) has own utility \(u_2(y)=4\), while \(r_2(x)=6-3=3\). Thus \( \rho^A \) is EF1.
For \( \rho^B \), type \(1\) has own utility \(8\), at least both relevant remainder values \(6\) and \(3\). Type \(2\) has own utility \(6\), at least both relevant remainder values \(3\). Thus \( \rho^B \) is EF1.
For a distribution \( \rho \), define the type-specific aggregate amount of good \(g\) by
\(a_{t,g}(\rho)=\sum_z\rho_t(z)z_g\).
An exchange between two states of the same type preserves every \(a_{t,g}\). Since \( \rho^A \) and \( \rho^B \) have different type-specific aggregates, any connecting sequence would contain an exchange between distinct types that changes these aggregates. Consider the first such exchange.
Before that exchange, only same-type exchanges have occurred. Hence type \(1\) still has no \(M\)-goods, while type \(2\) has only \(M\)-goods.
Every supported type-\(2\) state therefore consists of four \(M\)-goods. From type \(1\)'s perspective, such a state has utility \(8\) and remainder value \(6\). EF1 consequently requires every supported type-\(1\) state to have utility at least \(6\).
A type-\(1\) state contains only \(H\)- and \(Z\)-goods. If it contains \(k\) units from \(H\), its type-\(1\) utility is \(3k\), so EF1 implies \(k\ge2\). The type-\(1\) aggregate contains an average of exactly two \(H\)-goods per type-\(1\) individual. Since every supported state has at least two, every supported type-\(1\) state has exactly two \(H\)-goods and two \(Z\)-goods.
Now consider the first cross-type exchange. Type \(2\) must give an \(M\)-good.
If type \(1\) gives an \(H\)-good, its destination state has one \(H\)-good, one \(M\)-good, and two \(Z\)-goods. Its type-\(1\) utility is \(3+2=5\). The type-\(2\) destination state contains one \(H\)-good and three \(M\)-goods, whose type-\(1\) remainder value is
\(3+3\cdot2-3=6\).
Both destination states receive positive mass, so EF1 would require \(5\ge6\), a contradiction.
If type \(1\) gives a \(Z\)-good, its destination contains two \(H\)-goods, one \(M\)-good, and one \(Z\)-good. Its type-\(2\) remainder value is
\(2\cdot3+1-3=4\).
The type-\(2\) destination contains three \(M\)-goods and one \(Z\)-good, so its own type-\(2\) utility is \(3\). EF1 would require \(3\ge4\), again a contradiction.
Thus no first cross-type exchange exists. Since the target has different type-specific aggregates, it is unreachable. ∎
The argument permits arbitrary rational exchange masses, arbitrary preliminary same-type splitting, and repeated copies of a good within intermediate states.
Assume \(s_t=1\) for every type. Every state is \(e_g\), and removing its sole good leaves the zero state. Hence a distribution is EF1 exactly when
\(\rho_t(e_g)>0\Longrightarrow u_t(g)\ge0\).
Let
\(E=\{(t,g):u_t(g)\ge0\}\).
A feasible EF1 distribution is therefore a nonnegative rational matrix \(p=(p_{tg})_{(t,g)\in E}\) with row sums \(\mu_t\) and column sums \(b_g\).
A nontrivial exchange is precisely a square move
\(m_{t,t';g,h}=-e_{tg}-e_{t'h}+e_{th}+e_{t'g}\),
where \(t\ne t'\), \(g\ne h\), and all four pairs belong to \(E\).
For \(S\subseteq E\), define its square closure \(\operatorname{cl}(S)\) as the least subset of \(E\) satisfying the following rule: if \((t,g),(t',h)\) are present and all four edges of the corresponding square belong to \(E\), then \((t,h),(t',g)\) are also present.
Let \(\mathcal M(C)\) denote the set of square-move vectors whose four edges lie in \(C\).
For unit bundles, two feasible EF1 distributions \(p\) and \(q\) are connected if and only if
\(\operatorname{cl}(\operatorname{supp}p)=\operatorname{cl}(\operatorname{supp}q)=C\)
and
\(q-p\in\operatorname{span}_{\mathbb Q}\mathcal M(C)\).
These conditions are decidable in polynomial time.
For necessity, consider one legal square move. Its two destination edges belong to the closure of the source support. Conversely, the two source edges belong to the closure of the new support because the same square move can be reversed. Thus square closure is invariant under every exchange. Every exchange difference is also a rational multiple of a vector in \(\mathcal M(C)\), proving the span condition.
For sufficiency, begin from \(p\). Follow the finite construction of its closure. Whenever the closure rule adds a new diagonal, fire a sufficiently small positive rational amount of the corresponding square move, smaller than both positive source entries. This adds the desired edges without removing existing support. After finitely many steps one reaches a distribution \(p^\circ\) positive on every edge of \(C\). Construct \(q^\circ\) analogously from \(q\).
All differences \(p^\circ-p\) and \(q^\circ-q\) lie in \(\operatorname{span}_{\mathbb Q}\mathcal M(C)\). Hence
\(q^\circ-p^\circ=\sum_{i=1}^k\lambda_i m_i\)
for rational coefficients \(\lambda_i\) and square vectors \(m_i\); signs can be absorbed by reversing moves.
Both \(p^\circ\) and \(q^\circ\) are strictly positive on \(C\). Let
\(\eta=\min_{e\in C}\min\{p^\circ_e,q^\circ_e\}>0\).
Choose an integer \(N\) with
\(N>\eta^{-1}\sum_i|\lambda_i|\).
In each of \(N\) rounds, execute the moves \(m_i\) with amounts \(|\lambda_i|/N\). At the beginning of round \(r\), the state is \(p^\circ+r(q^\circ-p^\circ)/N\). During the round, every coordinate deviates from this line segment by less than \(\eta\), so every source entry remains positive. After all rounds the distribution is \(q^\circ\). Reversing the closure-building path from \(q\) to \(q^\circ\) completes the path to \(q\).
Square closure can be computed by repeatedly scanning at most \(O(|T|^2|G|^2)\) squares. The rational span condition is tested by Gaussian elimination on the corresponding square vectors. Both computations have polynomial bit complexity. ∎
If \(s_t=1\) for every type and all utilities are nonnegative, every two feasible distributions are connected.
In this case \(E=T\times G\). Ignore goods with zero supply. If there is only one type or one positive-supply good, the feasible distribution is unique.
Otherwise, let \(S\) be the support of any feasible distribution. For a desired pair \((t,g)\), choose some supported \((t,h)\) in row \(t\) and some supported \((t',g)\) in column \(g\). If \((t,g)\) is not already supported, then \(t\ne t'\) and \(g\ne h\), so the corresponding square rule adds \((t,g)\). Hence every feasible support has closure equal to the complete active bipartite graph.
Finally, square vectors span the space of matrices with zero row and column sums. Indeed, after fixing a row \(t_0\) and column \(g_0\), the squares on \(\{t,t_0\}\times\{g,g_0\}\) determine every entry with \(t\ne t_0\) and \(g\ne g_0\); the zero-margin conditions determine the remaining row and column. Since \(q-p\) has zero margins, Theorem 6.1 applies. ∎
The disconnected example rules out the simplest possible polynomial answer, namely that every valid instance is automatically a yes-instance. The unit-bundle theorem shows that any hardness begins at bundle size at least \(2\).
The finite-agent \( \mathrm{PSPACE} \)-hardness reduction cannot simply be copied by assigning one type to each named agent. Fractional splitting and same-type exchanges introduce additional states and paths. A hardness proof therefore needs gadgets whose barriers survive all same-type redistributions, as Proposition 5.1 does locally.
Conversely, the threshold representation does not immediately yield a polynomial algorithm: it is a union of support-defined polytopes, and the number of integral states can be exponential when bundle sizes are binary encoded.
Thus the justified conclusion is that the general target remains open, with a complete polynomial classification only for unit bundles and a rigorous nonconnectivity obstruction for larger bundles.
⟨structured verdict parsed — rendered above⟩
The prover correctly states that it does not resolve the requested general complexity classification. It establishes substantial special-case and structural results, but neither a polynomial-time algorithm nor NP-hardness for arbitrary bundle sizes follows. The proper status is therefore partial.
The cited paper does verify PSPACE-completeness for the named-agent, individually distinct-goods model, not for the type-mass model considered here. Its formal exchanges involve distinct named agents and indivisible goods, so the prover accurately identifies a model mismatch. [AAAI paper](https://ojs.aaai.org/index.php/AAAI/article/download/28836/29592)
The statement that the general question remains unresolved by this output is accurate. None of Sections 2–6 supplies a reduction proving hardness or an algorithm for arbitrary \(s_t\).
Thus the output does not satisfy the target request to decide between polynomial-time solvability and NP-hardness, although it does not falsely claim otherwise.
For a nonempty state \(y\), the equivalence
\[ u_t(x)\ge u_t(y-e_g)\text{ for some }g \quad\Longleftrightarrow\quad u_t(x)\ge u_t(y)-\max_{g:y_g>0}u_t(g) \]
is correct, including when utilities may be negative.
Taking the minimum over supported states of evaluator type \(t\) and the maximum over all globally supported states then proves Proposition 2.1.
There is, however, an unhandled domain issue. The task only says that bundle sizes are integral; it does not explicitly require \(s_t\ge1\). If some positive-mass type has \(s_t=0\), its supported state is empty, the existential condition in the stated EF1 definition has no admissible \(g\), and \(r_t(y)\) is undefined. Consequently, the claimed “exact” characterization and the sets \(A_\alpha\) do not cover the literal task domain. The write-up must either assume all \(s_t\ge1\) or specify how EF1 and \(r_t(0)\) are defined for empty states.
Subject to nonempty states, the union-of-transportation-polytopes description is correct.
All feasibility and EF1 calculations check:
Hence every strict mixture violates EF1. This section is correct.
The monotonicity calculation for \(r_v(Y+e_a)\) is correct when \(Y\ne0\). If \(Y=0\), the displayed formula contains a maximum over an empty set. Since the lemma includes unit-size bundles, this case must be stated separately or an explicit convention supplied.
More importantly, the proof says:
“Fix any evaluator with additive utility \(v\)”
and then asserts that endpoint EF1 includes \(v(x)\ge r_v(y)\) and \(v(x')\ge r_v(y')\). This is false for an arbitrary evaluator. The left state in an EF1 comparison must belong to the evaluator’s own type. Those inequalities are available only when \(v\) is the utility of the type owning \(x,x'\).
The lemma appears sound in substance, but the proof must be reorganized by owner type:
The phrase “union of their supports” is also ambiguous because support was previously defined separately for each type. The asserted consequence is correct only for the componentwise union of type-state supports, not for an untyped union that permits a state to be reassigned to another type.
These are proof-presentation gaps rather than evidence that the lemma is false.
The endpoint calculations, aggregate invariance, and two obstruction cases are correct.
Before the first effective cross-type exchange:
Both possible categories of good surrendered by type \(1\) lead to the claimed violations \(5<6\) or \(3<4\).
There is a small logical omission in the sentence “Before that exchange, only same-type exchanges have occurred.” The exchange definition does not require \(g\ne h\), so an earlier cross-type exchange with \(g=h\) is possible. Such an exchange is an identity operation, but the proof must explicitly delete these null exchanges or choose the first cross-type exchange that changes the type-specific aggregates.
With that clarification, Proposition 5.1 is rigorous and constitutes genuine progress.
The structural characterization is mathematically sound.
For \(s_t=1\), EF1 indeed reduces to the support restriction \(u_t(g)\ge0\). Legal nontrivial exchanges are precisely rational multiples of allowed square vectors.
The necessity argument correctly establishes invariance of square closure, including when an exchange exhausts a source entry: the reverse square recovers the removed source edges in the new support’s closure.
For sufficiency:
The closure and rational-span tests have polynomial dimension in \(|T||G|\). The corollary for nonnegative utilities is also correct after deleting zero-supply columns.
However, the polynomial-time claim lacks a required input-model hypothesis. The task specifies rational masses and supplies but does not say how utilities are represented. Computing \(E=\{(t,g):u_t(g)\ge0\}\) is a polynomial-time operation only if utility values have an explicit finite representation, such as binary-encoded rationals, or if polynomial-time sign comparisons are available. The same issue affects the underlying complexity target itself. The prover must state the assumed utility encoding before Theorem 6.1 can be accepted as a formal complexity result.
The proof establishes polynomial-time decidability, not necessarily a polynomial-length exchange sequence; the potentially large \(N\) does not undermine the stated decision result.
The nonconvexity example, disconnected instance, and unit-bundle reachability characterization are genuine and largely correct contributions. The local exchange lemma needs type-indexing and empty-state clarifications, and the complexity theorem needs an explicit representation assumption. Most importantly, no result classifying the general continuous type-mass problem is proved.
⟨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.