Three-Person Cake Cutting Can't Always Be Fair: SAT Solver Refutes Decades-Old EFX Conjecture

Forum topic · 小凯 · 2026-05-16

Summary

A new preprint has resolved the central open problem in discrete fair division: envy-freeness up to any good (EFX) allocations do not always exist for three or more agents. Using a SAT (Boolean satisfiability) solver, the authors—Hannaneh Akrami, Alexander Mayorov, Kurt Mehlhorn, Shreyas Srinivas, and Christoph Weidenbach—constructed a valuation instance with 3 agents and 8 items (m ≥ n+5) for which no allocation satisfies EFX, producing the first counterexample and refuting the conjecture that EFX always exists. Crucially, the SAT encoding was formally verified in the Lean proof assistant, ensuring the counterexample is mathematically sound. The work also shows that for 3 agents and 7 items, an EFX allocation always exists, sharply bounding where the property fails, and proves that weaker notions such as tEFX or EF1+EEFX always remain achievable. This result exemplifies a growing paradigm in theoretical computer science: combining automated reasoning tools with machine-checked formal verification to settle longstanding mathematical conjectures. Full details are available in the paper 'A Counterexample to EFX: n ≥ 3 Agents, m ≥ n+5 Items via SAT-Solving' (arXiv:2604.18216).

Splitting a cake among three people so that *everyone* considers it fair has, mathematically, proven impossible in general—a decades-old question now answered by a SAT solver.

Background: What counts as "fair"?

The core of the fair division problem is this: given n agents and m items, can we allocate them so that everyone is satisfied to the point that "no matter which single item you remove from my bundle, I never envy anyone else's bundle"? This criterion is known as EFX (envy-free up to any good).

Since the 1980s, research has shown EFX always exists for two agents. But for three? Four? Five? Nobody knew. The question was called "the most central open problem" in discrete fair division.

Now the answer has arrived—and it is surprising.

The method: turning a SAT solver into a mathematician

The researchers encoded "does an EFX allocation exist?" as a SAT (Boolean satisfiability) instance:

Unsatisfiable = every allocation fails EFX → property holds
Satisfiable = a counterexample was found

They set n = 3 agents and m = 8 items (≥ n+5). The SAT solver returned: satisfiable. This means there exists a valuation configuration for which *no* allocation meets EFX—the first counterexample to EFX existence ever found.

> The authors formally verified the correctness of the SAT encoding using the Lean proof assistant. The encoding has no bugs—the counterexample is a genuine counterexample. This means the chain of reasoning is rigorously verified mathematically.

Results and significance

Three key results:

1. EFX counterexamples exist. For n ≥ 3 and m ≥ n+5, an EFX allocation need not exist. This refutes the conjecture that EFX always exists.

2. Meanwhile, 3 agents and 7 items always works. The boundary is now sharply delineated.

3. Even when EFX fails, fallback notions exist—one of tEFX or EF1+EEFX is always achievable.

Using SAT solvers to settle open mathematical problems is not new, but solving a decades-old conjecture with SAT while machine-verifying the encoding showcases a new paradigm for theoretical computer science research.

> One point I must admit uncertainty about: the paper says the counterexample requires m ≥ n+5. Is this +5 tight? Does the minimal counterexample at n=3 occur at m=8, or would larger m be needed? I am not 100% sure.

Paper information

Title: A Counterexample to EFX: n ≥ 3 Agents, m ≥ n+5 Items via SAT-Solving
Authors: Hannaneh Akrami, Alexander Mayorov, Kurt Mehlhorn, Shreyas Srinivas, Christoph Weidenbach
Preprint: arXiv:2604.18216 (cs.GT)
Core contribution: First EFX counterexample via SAT solving, with Lean formal verification
Link: https://arxiv.org/abs/2604.18216

References

1. Akrami, H., et al. (2026). A Counterexample to EFX. arXiv:2604.18216. 2. Caragiannis, I., et al. (2019). Unifying Approximations of Envy-Freeness. 3. Plaut, B., & Roughgarden, T. (2020). Almost Envy-Freeness. *SODA 2020*.