EF2X Exists for Four Agents (aaai25-33480)

Given four rational type masses \(\mu_r\), a finite set \(M\) of item kinds with rational per-capita supplies \(b_g\), and four rational cancelable valuations \(v_r\) specified by value tables on \(2^M\), decide whether there exists a rational allocation law \(x_{r,B} \ge 0\) satisfying \(\sum_B x_{r,B} = \mu_r\) and \(\sum_{r,B:g \in B} x_{r,B} = b_g\), such that whenever \(x_{r,B} > 0\) and \(x_{s,C} > 0\), \(v_r(B) \ge \max_{D \subseteq C, |D|=2} v_r(C \setminus D)\), with the maximum defined as \(0\) when \(|C| < 2\).

A society is given by its support: the list of the \(\tau=4\) types with positive masses \(\mu_r\in\mathbb{Q}_{>0}\), encoded in binary, with \(\sum_{r=1}^{4}\mu_r=1\). Here \(\tau\) is the support size, not the number of possible types.
Let \(M\) be a finite set of \(m\) item kinds, with per-capita supplies \(b_g\in\mathbb{Q}\cap[0,1]\). A bundle \(B\subseteq M\) contains at most one item of each kind; empty bundles are allowed.
Each type has a monotone valuation \(v_r:2^M\to\mathbb{Q}_{\geq0}\), supplied as a complete binary-rational value table. Ties are allowed, and no normalization of \(v_r(\varnothing)\) is imposed.
Each valuation is cancelable: for all \(S,T\subseteq M\) and \(g\in M\setminus(S\cup T)\), \(v_r(S\cup\{g\})>v_r(T\cup\{g\})\) implies \(v_r(S)>v_r(T)\).
An allocation law consists of rational masses \(x_{r,B}\geq0\) satisfying \(\sum_{B\subseteq M}x_{r,B}=\mu_r\) and \(\sum_{r=1}^{4}\sum_{B\subseteq M:g\in B}x_{r,B}=b_g\).
Define \(w_r(C)=\max_{D\subseteq C,\,|D|=2}v_r(C\setminus D)\) when \(|C|\geq2\), and \(w_r(C)=0\) otherwise. The law is EF2X if, for every \(r,s\) and \(B,C\subseteq M\), \(x_{r,B}>0\) and \(x_{s,C}>0\) imply \(v_r(B)\geq w_r(C)\), including when \(r=s\).
Let \(L\) be the total binary input length, including all value tables; state running times in \(m,\tau,L\).

Is deciding whether such a rational EF2X allocation law exists solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

For four discrete agents with monotone cancelable valuations, a complete EF2X allocation always exists and can be computed in pseudopolynomial time; for three agents, a polynomial-time algorithm is known. [Source](https://arxiv.org/html/2412.00254v2)
No result settling this exact distributional feasibility problem was located in the literature search.

Polynomial-time solvability

The stated problem is polynomial-time solvable. The decisive assumptions are that the support size is fixed at \(\tau=4\) and that the complete value tables are included in the input. The algorithm below actually works for arbitrary nonnegative valuation tables; monotonicity and cancelability are unnecessary.

1. Encoding EF2X by utility thresholds

Write \(N=2^m\), the number of bundles. For each type \(r\), define the finite set of candidate thresholds
\[ \]
\(\displaystyle V_r=\{v_r(B):B\subseteq M\}.\)

Thus \(|V_r|\leq N\).

For a tuple \(a=(a_1,\ldots,a_\tau)\in V_1\times\cdots\times V_\tau\), define the bundles permitted for type \(s\) by

\(\displaystyle \mathcal A_s(a)=\{B\subseteq M:v_s(B)\geq a_s\text{ and }w_r(B)\leq a_r\text{ for every }r\}.\)

Consider the following linear feasibility problem, denoted \(\mathrm{LP}(a)\). Its variables are \(x_{s,B}\) for \(B\in\mathcal A_s(a)\), and its constraints are

\(\displaystyle x_{s,B}\geq0,\)

\(\displaystyle \sum_{B\in\mathcal A_s(a)}x_{s,B}=\mu_s\qquad(s=1,\ldots,\tau),\)

\(\displaystyle \sum_{s=1}^{\tau}\sum_{\substack{B\in\mathcal A_s(a)\\g\in B}}x_{s,B}=b_g\qquad(g\in M).\)

Variables for other bundles are understood to be zero.

Lemma. A rational EF2X allocation law exists if and only if \(\mathrm{LP}(a)\) has a rational feasible solution for at least one candidate tuple \(a\).

Proof, forward direction. Suppose \(x\) is a rational EF2X allocation law. Since \(\mu_r>0\), every type has at least one positively supported bundle. Therefore the minimum

\(\displaystyle a_r=\min\{v_r(B):x_{r,B}>0\}\)

exists and belongs to \(V_r\). Choose a positively supported bundle \(B_r\) attaining this minimum.

Let \(C\) be any bundle with \(x_{s,C}>0\), for any type \(s\). Applying EF2X to \(B_r\) and \(C\) gives

\(\displaystyle w_r(C)\leq v_r(B_r)=a_r\)

for every \(r\). Also \(v_s(C)\geq a_s\) by the definition of \(a_s\). Hence \(C\in\mathcal A_s(a)\). The original allocation law consequently satisfies \(\mathrm{LP}(a)\).

This argument includes \(r=s\), so it explicitly incorporates same-type comparisons.

Proof, reverse direction. Suppose \(x\) is a rational feasible solution of \(\mathrm{LP}(a)\). Whenever \(x_{r,B}>0\) and \(x_{s,C}>0\), membership in the permitted bundle sets gives

\(\displaystyle v_r(B)\geq a_r\geq w_r(C).\)

Thus every required EF2X inequality holds, including those with \(r=s\). The remaining constraints are precisely the type-mass and supply equations. Therefore \(x\) is a rational EF2X allocation law. This proves the lemma.

2. Exact feasibility and rationality

Each \(\mathrm{LP}(a)\) has at most \(\tau N\) variables and \(m+\tau\) equality constraints. Its constraint matrix has only zero and one entries, and its right-hand side consists of the input rationals \(\mu_s\) and \(b_g\).

We use the standard theorem that feasibility of explicitly encoded rational linear inequalities is decidable in time polynomial in their total binary encoding length. Equalities are represented by two inequalities. Thus all hypotheses of the polynomial-time linear-programming theorem are satisfied. [Khachiyan, *A polynomial algorithm in linear programming*](https://www.mathnet.ru/eng/dan42319).

Real feasibility here also implies rational feasibility. To verify this directly, observe that each variable satisfies

\(\displaystyle 0\leq x_{s,B}\leq\mu_s.\)

Consequently, a nonempty feasible region is a compact polytope and has a vertex. At a vertex, the matrix columns corresponding to positive variables must be linearly independent: otherwise, a nonzero dependence would permit sufficiently small perturbations in both directions, preserving all equations and nonnegativity, contradicting extremality.

There are therefore at most \(k\leq m+\tau\) positive variables. Selecting \(k\) independent rows gives a nonsingular square system determining them. Its matrix has integer entries and its right-hand side is rational, so Cramer’s rule gives rational coordinates.

These coordinates have polynomial binary length. Indeed, let \(D\) be the product of the input right-hand-side denominators. Its binary length is \(O(L)\), and multiplication by \(D\) makes the right-hand side integral, with entries between zero and \(D\). The determinant expansion bounds the matrix determinant by \(k!\) in absolute value and each replaced-column determinant by \(k!D\). Hence each coordinate requires \(O(L+k\log(k+1))\) bits.

3. Algorithm and running time

The algorithm proceeds as follows:

• Compute \(w_r(C)\) for every type and bundle using the supplied definition, retaining \(w_r(C)=0\) when \(|C|<2\).
• Enumerate all tuples in \(V_1\times\cdots\times V_\tau\).
• For each tuple, construct the permitted bundle sets and test \(\mathrm{LP}(a)\).
• Accept exactly when at least one of these linear programs is feasible.

The lemma and rationality argument prove correctness.

Computing all \(w_r(C)\) requires at most

\(\displaystyle O\bigl(\tau(1+m^2)2^m\bigr)\)

rational comparisons. Every comparison is exact and takes time polynomial in \(L\): each computed maximum is either zero or an existing table value.

There are at most \(N^\tau=2^{m\tau}\) threshold tuples. For each tuple, constructing the permitted sets requires \(O(\tau^2N)\) comparisons. An explicitly written linear program has encoding length

\(\displaystyle O\bigl(\tau N(m+\tau)+L\bigr).\)

Because the complete tables explicitly contain \(\tau N\) rational entries, \(L\geq\tau N\). Thus each linear program, and its feasibility test, has size and running time polynomial in \(m,\tau,L\).

The total bit running time is therefore bounded by

\(\displaystyle 2^{m\tau}\operatorname{poly}(m,\tau,L).\)

For the stipulated support size \(\tau=4\),

\(\displaystyle 2^{m\tau}=2^{4m}=N^4\leq(L/4)^4.\)

Consequently, the total running time is polynomial in \(m,\tau,L\) on the stated input class. More generally, the same proof gives polynomial time for every fixed support size; it does not establish a uniform polynomial bound when \(\tau\) is unbounded.

4. Scope of the conclusion

No assumption about ties or normalization was used. The thresholds are actual table values, and the prescribed zero value of \(w_r(C)\) for small bundles is preserved exactly.

The cited discrete four-agent theorem concerns complete allocations among four individual agents. Its existence guarantee and pseudopolynomial algorithm do not directly decide this distributional feasibility problem. [Ashuri, Gkatzelis, and Sgouritsa, *EF2X Exists For Four Agents*](https://arxiv.org/html/2412.00254v2). Here polynomial-time solvability follows instead from the threshold characterization, fixed support size, and explicit-table encoding.

⟨structured verdict parsed — rendered above⟩

Verification report

Verdict: proved. The output establishes polynomial-time decidability for the specified support size \(\tau=4\) and complete-table encoding. I found no mathematical errors or gaps requiring repair.

1. Threshold characterization

The candidate sets \(V_r\) contain every possible minimum supported utility for type \(r\), since they contain all its table values.

In the forward direction:

• The equation \(\sum_B x_{r,B}=\mu_r>0\) ensures that every type has a positively supported bundle.
• There are finitely many bundles, so the minimum defining \(a_r\) exists, belongs to \(V_r\), and is attained by a supported bundle \(B_r\).
• For every supported bundle \(C\) of every type \(s\), the stipulated EF2X condition applies to \(B_r,C\). Thus \(w_r(C)\leq a_r\) for every \(r\).
• The definition of \(a_s\) also gives \(v_s(C)\geq a_s\). Consequently every supported variable is permitted in the corresponding linear program.
• Restricting to permitted variables preserves all mass and supply equations because every omitted variable was zero.

All quantifiers are correct. In particular, the use of the EF2X condition when \(r=s\) is explicitly justified by the task.

In the reverse direction, any positively supported \(B\) of type \(r\) satisfies \(v_r(B)\geq a_r\), while any positively supported \(C\) of type \(s\) satisfies \(w_r(C)\leq a_r\). These conditions give exactly the required inequality \(v_r(B)\geq w_r(C)\).

The reverse implication does not require that a threshold be attained by the resulting allocation. The inequalities alone suffice.

Assessment: The equivalence is fully established.

2. Linear-programming feasibility

Each candidate produces a finite, explicitly representable linear program with rational coefficients. Its variables have nonnegativity constraints, and its remaining constraints are precisely the required equalities.

The cited theorem is stated sufficiently precisely: feasibility of explicitly encoded rational linear inequalities is decidable in polynomial time in their binary encoding length. Its hypotheses hold here. Representing equalities by pairs of inequalities is valid, including for dependent equations and feasible regions of lower dimension. The cited [Khachiyan paper](https://www.mathnet.ru/eng/dan42319) establishes polynomial-time feasibility for binary-encoded integer systems; the rational formulation used by the prover is its standard equivalent formulation.

If a permitted bundle set is empty, its type-mass equation becomes \(0=\mu_s\), correctly making that candidate infeasible. No assumption of a nonempty permitted set is needed.

Assessment: The theorem application is valid.

3. Rationality and certificate size

The rationality argument is correct:

• Nonnegativity and the type-mass equations imply \(0\leq x_{s,B}\leq\mu_s\).
• Hence any nonempty feasible region is a bounded, closed polytope and has a vertex.
• At a vertex, a dependence among the columns indexed by positive variables would allow sufficiently small perturbations in both directions. The positive coordinates remain nonnegative, zero coordinates remain fixed, and all equations remain satisfied. This contradicts extremality.
• Therefore the number \(k\) of positive variables is at most \(m+\tau\).
• Column independence supplies \(k\) independent rows, yielding the nonsingular square system used in the write-up.
• Cramer’s rule gives rational coordinates.

The claimed bit bound also checks out. The product \(D\) of the right-hand-side denominators has binary length \(O(L)\). Every right-hand-side entry lies in \([0,1]\), so its scaled value is an integer in \([0,D]\).

For the selected matrix, determinant expansion gives absolute determinant at most \(k!\). A determinant with one column replaced by the scaled right-hand side has absolute value at most \(k!D\). Thus the coordinate numerators and denominators have the claimed \(O(L+k\log(k+1))\) bit bound.

Assessment: Real feasibility implies rational feasibility, with the stated polynomial certificate size.

4. Running time and encoding

The preprocessing and enumeration bounds are valid.

• For each bundle \(C\), computing \(w_r(C)\) examines at most \(\binom{|C|}{2}\) table entries. The bound \(O(\tau(1+m^2)2^m)\) therefore holds.
• Every resulting maximum is zero or an input table value, so preprocessing does not increase rational bit lengths.
• There are at most \(N^\tau\) threshold tuples.
• Checking a bundle’s eligibility requires its own utility comparison and the comparisons against all \(\tau\) envy thresholds. Across all types and bundles, \(O(\tau^2N)\) comparisons suffice.
• The equality matrix has at most \((m+\tau)\tau N\) entries. Nonnegativity can be encoded as variable bounds or sparse inequalities, consistent with the stated encoding bound.

Because the complete tables contain \(\tau N\) explicitly encoded rational entries, \(L\geq\tau N\). With \(\tau=4\), the enumeration factor satisfies \(N^4\leq(L/4)^4\). Combining this with polynomial-time preprocessing, construction, and linear-programming feasibility gives a polynomial total bit running time on the stated input class.

The qualification concerning unbounded \(\tau\) is accurate: this enumeration does not establish a uniform polynomial-time bound when support size is unrestricted.

Assessment: The polynomial-time conclusion follows from the actual input encoding.

5. Scope and edge cases

The argument respects the task’s conventions:

• Ties cause no difficulty because both directions use weak inequalities.
• No assumption that \(v_r(\varnothing)=0\) is introduced.
• Bundles of size below two retain the prescribed value \(w_r(C)=0\).
• Bundles of size exactly two use \(v_r(\varnothing)\), as required.
• Supplies equal to zero or one are handled by the exact supply equations.
• An empty item set causes no failure in the characterization or algorithm.
• Monotonicity and cancelability are unused, so the asserted extension to arbitrary nonnegative rational valuation tables is supported.

The discrete four-agent result is background, not a premise of the algorithm. Its description agrees with the cited [source](https://arxiv.org/html/2412.00254v2), and no unjustified inference from discrete existence to distributional feasibility occurs.

Required feedback

No mathematical clarification or repair is needed. The stray empty display before the definition of \(V_r\) is a harmless formatting artifact.

⟨structured verdict parsed — rendered above⟩