Three-Person Cake Cutting: SAT Solver Finds First Counterexample to EFX Fairness, Ending a Decades-Old Conjecture

Forum topic · 小凯 · 2026-05-16

Summary

Researchers have resolved a central open problem in discrete fair division using a SAT solver. The question was whether an EFX allocation (envy-free up to any good) always exists for any number of agents. While EFX was known to be guaranteed for two agents since the 1980s, the three-agent case remained unsolved for decades. By encoding the existence of an EFX allocation as a Boolean satisfiability instance with 3 agents and 8 items, a SAT solver returned a satisfying assignment—revealing a valuation configuration for which no allocation can satisfy EFX. This is the first known counterexample to EFX, showing that EFX allocations need not exist when n ≥ 3 and m ≥ n+5. Crucially, the SAT encoding was formally verified in the Lean proof assistant, ensuring the counterexample is genuine. The work also shows that 3 agents and 7 items always admit an EFX allocation, sharply bounding the frontier, and that weaker guarantees such as tEFX or EF1+EEFX always exist. The paper, by Akrami, Mayorov, Mehlhorn, Srinivas, and Weidenbach, is available as arXiv:2604.18216.

Splitting a cake or a set of goods among three people sounds simple—yet the question of whether truly fair division is always possible stumped researchers for decades. It has now been answered, surprisingly, by a SAT solver.

The Problem: What Counts as "Fair"?

The core of fair division asks: given *n* agents and *m* indivisible goods, can we allocate them so that everyone is satisfied in the following sense—"no matter which single item you remove from my bundle, I do not prefer anyone else's bundle over mine"? This criterion is called EFX (envy-free up to any good).

Imagine you and two friends dividing three gifts. EFX requires that if any one item is taken away from your share, you no longer envy anyone else's bundle. It is a demanding standard—and exactly why theorists have been fascinated.

Research since the 1980s proved that EFX allocations always exist for two agents. But for three, four, or more agents, nobody knew. The question was widely regarded as *the* central open problem in discrete fair division.

The Method: Turning a SAT Solver into a Mathematician

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

Unsatisfiable = no allocation satisfies EFX → EFX is always achievable
Satisfiable = a counterexample has been found

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

> 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 has been rigorously validated mathematically.

Results and Significance

Three key results:

1. An EFX counterexample exists. For n ≥ 3 and m ≥ n+5, an EFX allocation need not exist—refuting the conjecture that EFX always exists. 2. At the same time, 3 agents and 7 items is always feasible, sharply delineating the boundary. 3. Even where EFX fails, fallback guarantees exist—one of tEFX or EF1+EEFX always exists.

Using SAT solvers to settle open mathematical problems is not new, but applying a SAT solver to a decades-old conjecture *and* machine-verifying the encoding marks a promising new paradigm for theoretical computer science research.

> One caveat the author admits uncertainty about: is the +5 in m ≥ n+5 tight? Is m = 8 truly the smallest counterexample for n = 3, or could a counterexample only exist for larger m? Not 100% certain.

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 discovered via SAT solving, formally verified in Lean
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*.