A Counterexample to EFX; Agents, Items, Monotone Valuations; via SAT-Solving
Hannaneh Akrami, Alexander Mayorov, Kurt Mehlhorn, Shreyas Srinivas, Christoph Weidenbach
Abstract
SAT solving has recently been proven effective in tackling open combinatorial problems. We contribute two additional results in the context of fair distribution of indivisible goods. Specifically, we demonstrate that EFX (envy-freeness up to any good) allocations always exist for three agents and seven goods, while we provide a counterexample for the case of agents and goods. An allocation is EFX if no agent would envy the allocation of any other agent if any single item were to be removed from the other agent's bundle of goods. Each agent's preferences are modeled by a monotone valuation function on all potential bundles. After analyzing theoretical aspects of the problem, we encode the negation of the EFX instances into SAT. Satisfiability of the respective SAT formula constitute a counter-example to EFX, unsatisfiability of the respective SAT formula implies that EFX holds. The theoretical foundations of the encoding are proven correct in LEAN. For the three agents and seven goods case, we obtained a proof of unsatisfiability using SPASS-SAT of size about 30 GB in about 30 hours. It was shown to be correct by DRAT-trim. In the case of three agents and eight goods, SPASS-SAT computed satisfiability indicating a counterexample in the form of three specific agent valuations in about 20 hours. It was verified by probing all possible bundle assignments; the verification takes seconds. The extension of the counterexample to agents and goods does not involve SAT-solving. This counterexample resolves, in the negative, one of the central questions in the theory of discrete fair division.
AI Impact Assessments
(3 models)Scientific Impact Assessment
Core Contribution
This paper resolves one of the most prominent open questions in discrete fair division theory: does an EFX (envy-free up to any good) allocation always exist? The answer is no—for n ≥ 3 agents and m ≥ n+5 goods with monotone valuations. The paper delivers two results via computer-assisted SAT solving:
1. Positive result: EFX allocations always exist for 3 agents and 7 goods (proved via unsatisfiability of the encoded negation, ~30 hours, 30GB DRAT proof).
2. Negative result: A concrete counterexample for 3 agents and 8 goods (found via satisfiability, ~20 hours), which generalizes to all n ≥ 3 agents with m ≥ n+5 goods through a clean theoretical extension.
The counterexample consists of three explicit monotone valuation functions over 2^8 = 256 subsets of 8 goods, for which no partition of goods into three non-empty bundles satisfies EFX. This is a landmark result: EFX existence was called "fair division's most enigmatic question" by Procaccia (CACM 2020), and the prior state of the art only established existence for up to n+3 goods.
Methodological Rigor
The paper demonstrates exceptional methodological rigor across multiple dimensions:
The extension to n ≥ 4 agents and m ≥ n+5 goods is purely theoretical (no SAT needed) and is elegantly constructed: agents 2 through n-1 share identical valuations that force a pigeonhole argument, reducing back to the 3-agent case.
Potential Impact
Within fair division theory, this result is transformative. It definitively closes the question of universal EFX existence for general monotone valuations and redirects the field toward:
For computational methods in combinatorics, this adds to a growing body of work demonstrating that SAT solvers can resolve deep mathematical questions (alongside Pythagorean triples, Schur numbers, etc.). The combination of SAT solving with formal verification in Lean sets a high standard for computer-assisted proofs.
For algorithm design, understanding that EFX cannot always be achieved may shift attention toward approximate fairness notions or restricted domains in practical allocation systems.
Timeliness & Relevance
The timing is excellent. EFX has been the central open question in discrete fair division for several years, with incremental progress (2 agents, then 3 agents with special valuations, then n+3 goods). The gap between n+3 (known positive) and this paper's n+5 (now negative) is razor-thin. The use of SAT solving for open combinatorial problems is a methodological trend gaining momentum, and applying it with Lean verification represents the state of the art in trustworthy computation.
Strengths
1. Resolution of a major open problem: This is unambiguous in significance—it answers a question that the community has been working toward for years.
2. Extraordinary verification pipeline: Two SAT solvers, DRAT-trim proof checking, Lean formalization of the encoding theory, and exhaustive verification of the counterexample.
3. Complete artifact availability: All code, proofs, SAT instances, and the 18.5GB DRAT proof are publicly available.
4. Insightful analysis of the counterexample: The paper goes beyond merely presenting the counterexample, analyzing marginal values, MMS violations, distance to EFX-ness, and structural properties that may inform future work.
5. Clean generalization: The extension to arbitrary n is elegant and requires no additional computation.
Limitations
1. Gap at m = n+4: The paper leaves open whether EFX exists for m = n+4 goods—the single remaining case between known existence and non-existence.
2. Additive valuations untouched: The counterexample relies on non-additive (complementary) valuations. EFX for additive valuations—arguably the most practically relevant case—remains open.
3. Limited structural understanding: While the analysis in Section 6 is valuable, the counterexample was found computationally and its "why" remains somewhat opaque. The authors acknowledge this and suggest simplification as future work.
4. Scalability of the approach: The SMT encoding failed for m=7, and the SAT encoding required ~30 hours even with theoretical reductions. Extending this methodology to harder instances may be infeasible.
5. The counterexample valuations are artificial: Ranks of subsets in a linear order, with strong complementarities—these are far from natural economic preferences, somewhat limiting practical implications.
Overall Assessment
This is a first-rate result that resolves a central open question in a well-established research area. The methodology is sound, the verification is multi-layered and rigorous, and the implications for future research are clearly articulated. The combination of theoretical insight, computational power, and formal verification exemplifies best practices in computer-assisted mathematics.
Generated Apr 21, 2026
Comparison History (57)
While both papers resolve central open questions in fair division, Paper 1 exhibits higher potential scientific impact through its groundbreaking methodological innovation. By successfully applying SAT-solving and formal verification (LEAN) to disprove the existence of EFX allocations—the most prominent open problem in the field—it introduces a powerful cross-disciplinary paradigm. This computer-assisted approach not only settles a major theoretical conjecture but also provides a scalable, rigorously verified framework for future economics and game theory research. Paper 2 is highly significant, yet Paper 1's integration of automated reasoning offers broader transformative potential across fields.
Paper 1 offers a unifying, general theory (within-range regret) for truthful delegation that spans auctions/autobidding and LLM agents, plus a fundamental trilemma linking guardrails, truthfulness, and capability. It is timely and highly relevant given widespread deployment of agentic systems, with direct implications for safety, alignment, and mechanism design, and includes empirical evaluation on production models. Paper 2 is a major theoretical milestone (EFX counterexample) with strong rigor and importance within fair division, but its impact is more specialized and less directly tied to immediate real-world deployments.
Paper 1 likely has higher scientific impact because it resolves a central open question in discrete fair division by providing a general counterexample to EFX existence (for n≥3, m≥n+5) under monotone valuations—an unambiguous theoretical breakthrough with broad implications for algorithmic fairness and mechanism design. Its methodology is unusually rigorous (SAT encoding, certified proofs, Lean formalization, independent proof checking). Paper 2 is innovative and timely with plausible applications, but relies on more assumptions (endogenous resolution, LLM-judge verification) and its real-world impact is less certain than a definitive negative resolution of a foundational conjecture.
Paper 2 resolves a central open question in discrete fair division theory — whether EFX allocations always exist — providing a definitive counterexample. This is a landmark result in theoretical computer science and economics, settling a long-standing conjecture that has driven substantial research. The methodological contribution (SAT-solving for combinatorial open problems, with formal verification in LEAN) adds further impact. Paper 1 offers useful modeling insights on AI-productivity paradoxes, but its contributions are more incremental and exploratory, whereas Paper 2 provides a conclusive resolution to a fundamental problem.
Paper 1 resolves a central open question in discrete fair division by providing a counterexample to EFX existence for general monotone valuations. EFX has been one of the most prominent open problems in computational economics and fair division since its introduction, attracting enormous attention. The negative resolution fundamentally redirects the field. While Paper 2 also resolves an important open question about bilateral trade efficiency with a tight bound, the EFX problem has broader recognition and more active research community engagement. Both are significant, but the EFX counterexample will likely reshape more research agendas.
Paper 2 likely has higher impact: it addresses a timely, widely relevant problem in RLHF/DPO used across modern AI systems, and frames a general, theoretically grounded tradeoff (representation vs. rationalizability) with an exact loss decomposition plus empirical validation. Its insights can influence reward modeling practice, benchmark design, and aggregation theory across ML and social choice. Paper 1 is highly novel and rigorous (SAT/Lean-verified counterexample resolving a central fair-division question) but is narrower in immediate real-world applicability and cross-field reach than RLHF theory.
Paper 2 likely has higher impact because it settles a central, long-standing open question in fair division by providing an explicit counterexample to EFX existence for broad regimes (n≥3, m≥n+5) under monotone valuations—immediately reshaping the research direction. It combines computational discovery (SAT) with formally verified foundations (LEAN) and independently checkable evidence, increasing credibility and reuse. Applications span algorithmic fairness, mechanism design, and economics. Paper 1 is technically deep and broad in complexity/learning theory, but its main contributions are hardness and relaxations in specialized game classes, which may diffuse immediate downstream consequences compared to a definitive negative resolution.
Paper 1 resolves a central, long-standing open question in the theory of discrete fair division (the existence of EFX allocations). By definitively answering this question using a novel combination of SAT-solving and formal verification (LEAN), it provides a landmark theoretical breakthrough with absolute methodological rigor. While Paper 2 is highly timely regarding LLM agents, Paper 1 represents a permanent, foundational mathematical contribution to computational social choice, algorithmic game theory, and combinatorial optimization.
Paper 2 likely has higher scientific impact because it resolves a central open question in discrete fair division by providing a counterexample to EFX existence (for n≥3, m≥n+5) under monotone valuations—an enduring theoretical problem with broad implications in economics, algorithmic game theory, and mechanism design. It also demonstrates rigorous, reproducible methodology (SAT encoding, Lean-checked foundations, DRAT-trim verification). Paper 1 offers a valuable benchmark for LLM negotiation evaluation with clear practical relevance, but its impact is more incremental and may be superseded by rapidly evolving evaluation paradigms.
Paper 2 addresses a highly timely and critical issue in AI safety and alignment, bridging mechanism design and LLM agent behavior. Its findings on the necessity of intrinsic prosociality have broad implications for the rapidly growing field of cooperative AI. While Paper 1 resolves a significant theoretical open problem in fair division, Paper 2 offers wider interdisciplinary relevance and stronger potential for real-world application in developing safe and beneficial AI systems.