arxiv: 2604.18216 · v3 · submitted 2026-04-20 · 💻 cs.GT · cs.DS

Recognition: unknown

A Counterexample to EFX n ge 3 Agents, m ge n + 5 Items, Submodular Valuations via SAT-Solving

Alexander Mayorov, Christoph Weidenbach, Hannaneh Akrami, Kurt Mehlhorn, Shreyas Srinivas

Authors on Pith no claims yet

Pith reviewed 2026-05-10 03:22 UTC · model grok-4.3

classification 💻 cs.GT cs.DS

keywords EFXfair divisionindivisible goodsmonotone valuationsSAT solvingcounterexampleenvy-freenessallocation

0 comments

The pith

EFX allocations do not always exist for three or more agents and at least eight indivisible goods under monotone valuations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper examines the existence of EFX allocations, where no agent envies another's bundle after any single item is removed, for agents with monotone valuations over indivisible goods. It proves that EFX allocations always exist for three agents and seven goods by showing that the negation leads to an unsatisfiable SAT formula, verified via a large proof. For three agents and eight goods, the SAT solver finds a satisfying assignment that supplies explicit monotone valuations with no EFX allocation, and this instance extends directly to any larger number of agents n at least three paired with at least n plus five goods. The result settles in the negative a central open question about whether EFX is guaranteed for all instances when the number of goods is sufficiently large.

Core claim

While EFX allocations exist for three agents and seven goods, there exist monotone valuation functions over three agents and eight goods for which no allocation satisfies the EFX condition, and this counterexample generalizes to n agents and m goods whenever n is at least three and m is at least n plus five.

What carries the argument

SAT encoding of the negation of EFX existence, whose satisfiability produces concrete counterexample valuations and whose unsatisfiability proves existence.

If this is right

For every n at least 3 and every m at least n+5, there exist monotone valuations with no EFX allocation.
The boundary for guaranteed EFX existence lies strictly between seven and eight goods when there are three agents.
SAT-based methods can decide EFX existence for small fixed numbers of agents and goods.
The negative result for large m holds without any further SAT computation once the three-agent eight-good instance is established.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The exact threshold separating guaranteed EFX existence from counterexamples may be m = n+4 for some n, which could be checked with the same encoding.
Practical fair-division procedures may need to fall back to weaker notions such as EF1 when the number of items exceeds the number of agents by five or more.
The Lean-verified encoding provides a reusable template for attacking other open existence questions in discrete fair division via SAT.

Load-bearing premise

The logical encoding of the negation of EFX existence into SAT is faithful to the original problem definition.

What would settle it

An explicit check showing that the three-agent eight-good valuation functions found by the solver do admit an EFX allocation would falsify the counterexample.

Figures

Figures reproduced from arXiv: 2604.18216 by Alexander Mayorov, Christoph Weidenbach, Hannaneh Akrami, Kurt Mehlhorn, Shreyas Srinivas.

**Figure 2.** Figure 2: The basic model of SAT 3. We also prove the invariance of valuation ordering and the EFX property under bijections of an allocInstance for the special case of Agents = Fin n and Goods = Fin m. Here n < m are both natural numbers and Fin n and Fin m respectively denote the type of natural numbers bounded strictly from above by n and m. This means by reordering the good sets in the specified item ordering of… view at source ↗

**Figure 3.** Figure 3: The basic literals of our SAT encoding and the allocation structure whose allocations will be [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗

**Figure 4.** Figure 4: Visualization of the counterexample to EFX existence for 3 agents and 8 goods. The colors [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗

**Figure 5.** Figure 5: Visualization of the marginal contributions in the counterexample to EFX existence for 3 agents [PITH_FULL_IMAGE:figures/full_fig_p014_5.png] view at source ↗

**Figure 6.** Figure 6: Some MMS-violations for the valuation v0, i.e., sets A, B, C, D such that A∪B = C∪D, A∩B = /0 = C ∩ D and min(v(A),v(B)) > max(v(C),v(D)). For v0 the values of the items are increasing, i.e., v(g0) < v(g1) < ... < v(g7). It appears that there is significant complementarity between elements g1 and g2, and between {g4,g7} and a further element in {g0,g3}. Note that {g4,g7} is a subset of D, and, by themselve… view at source ↗

**Figure 7.** Figure 7: Results of running the Z3 theorem prover on the LRA instances encoding existence of EFX for 3 [PITH_FULL_IMAGE:figures/full_fig_p016_7.png] view at source ↗

read the original abstract

The existence of EFX allocations is a central open problem in discrete fair division. An allocation is EFX (envy-free up to any good) if no agent envies another agent after the removal of any single good from the other agent's bundle. We resolve this longstanding question by providing the \textbf{first-ever counterexample} to the existence of EFX allocations for agents with monotone valuations, which in turn immediately implies a counterexample for submodular valuations. Specifically, we show that EFX allocations need not exist for instances with $n \ge 3$ agents and $m \ge n+5$ goods. In contrast, we prove that every instance with three agents and seven goods admits an EFX allocation. Both results are obtained via SAT solving. We encode the negation of EFX existence as a SAT instance: satisfiability yields a counterexample, while unsatisfiability establishes universal existence. The correctness of the encoding is formally verified in Lean. Finally, we establish positive guarantees for fair allocations with three agents and an arbitrary number of goods. Although EFX allocations may fail to exist, we prove that every instance with three agents and monotone valuations admits at least one of two natural relaxations of EFX: tEFX, or EF1 and EEFX.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 0 minor

Summary. The paper claims that EFX allocations exist for three agents and seven goods under monotone valuations, established via unsatisfiability of a SAT encoding whose correctness is proven in Lean and verified by a DRAT-trim proof. It provides an explicit counterexample for three agents and eight goods, obtained from a satisfiable SAT instance and confirmed by exhaustive enumeration of all 3^8 allocations. This counterexample is extended directly to all n ≥ 3 agents and m ≥ n + 5 goods. The work resolves negatively the existence question for EFX in these regimes.

Significance. The result settles a central open question in discrete fair division by exhibiting the first counterexample to EFX existence for monotone valuations when the number of goods is at least five more than the number of agents. Credit is due for the machine-checked Lean proof of the SAT encoding, the DRAT-verified unsatisfiability certificate for the 3+7 case, and the exhaustive enumeration verification for the 3+8 satisfiable instance; these elements provide unusually high assurance for a computational negative result.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript, accurate summary of the results, and recommendation to accept. We appreciate the recognition given to the machine-checked Lean proof, the DRAT-trim verification, and the exhaustive enumeration check.

Circularity Check

0 steps flagged

No significant circularity; direct computational counterexample with external verification

full rationale

The paper derives its central negative result (non-existence of EFX for n=3 m=8 and the extension to n>=4 m>=n+5) via SAT encoding of the negation of EFX, whose faithfulness is proven in Lean, followed by satisfiability yielding explicit valuations that are exhaustively verified by enumeration of all 3^8 allocations. The m=7 case uses a DRAT-verified unsatisfiability proof. The extension is a direct construction inheriting monotonicity non-existence without further solving. No step reduces by definition or self-citation to its own inputs; the encoding and verification are independent of the target counterexample values, and the result is self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the correctness of the SAT reduction from EFX non-existence; this is the only non-trivial assumption beyond standard monotone valuation definitions.

axioms (1)

domain assumption The reduction from the negation of EFX existence to SAT satisfiability is correct and complete.
Stated to be proven in Lean; no other axioms invoked.

pith-pipeline@v0.9.0 · 5678 in / 1090 out tokens · 43080 ms · 2026-05-10T03:22:23.900935+00:00 · methodology