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
1. Core Contribution
This paper resolves one of the most prominent open questions in discrete fair division: whether EFX allocations always exist for agents with monotone valuations. The answer is negative. Specifically, the authors demonstrate:
The EFX existence question has been called "one of the central questions in the theory of discrete fair division" (quoted from Ariel Procaccia's 2020 CACM editorial). Prior work had established existence only for special cases: identical valuations, two agents, three agents with restricted valuations, and n agents with at most n+3 goods. The gap between n+3 (known to exist) and n+5 (shown not to exist) leaves only the n+4 case open.
2. Methodological Rigor
The methodology is exceptionally rigorous, combining multiple layers of verification:
The multi-layered verification pipeline (SAT solver → independent SAT solver → DRAT-trim → Lean formalization → exhaustive counterexample checking) provides extremely high confidence. The only unverified component is the C++/Python encoding generator, but the Lean formalization of the abstract SAT model bridges this gap conceptually.
3. Potential Impact
Within fair division theory: This result fundamentally reshapes the landscape. It definitively shows that EFX is too strong a fairness notion for general monotone valuations, redirecting research toward:
Within computational methods for combinatorics: This adds to the growing body of work where SAT solvers resolve long-standing open problems (following results in Ramsey theory, combinatorics, etc.). The paper demonstrates a sophisticated pipeline: theoretical problem reduction → SAT encoding → solving → formal verification. The approach of extracting unit clauses from a solved instance to guide search on a harder instance is a practical methodological contribution.
Broader implications: Fair division has applications in resource allocation, spectrum allocation, inheritance disputes, and public housing. Understanding the theoretical limits of EFX informs which fairness guarantees can be promised in practice.
4. Timeliness & Relevance
The EFX existence question has been a focal point of the fair division community for several years, with incremental progress (3 agents proved in 2020, n+3 goods in 2023). The resolution of this question is timely and will likely catalyze significant follow-up work. The use of SAT solving for open mathematical/CS problems is itself a timely and growing methodology.
5. Strengths & Limitations
Key Strengths:
Notable Limitations:
Additional Observations:
The structural analysis of the counterexample (Figures 4-6) reveals significant complementarity between goods and violations of the MMS property—both expected given prior theoretical results. The observation that 272 out of 5,796 allocations violate only a single EFX condition suggests the counterexample is "barely" a counterexample, which could inform future simplification efforts.
The computational resources required (30 hours for 7 goods, 20 hours for 8 goods) are substantial but not extraordinary, and the result is fully reproducible.
Overall Assessment
This is a landmark result in fair division theory, settling a major open question with an innovative and rigorously verified computational approach. The combination of theoretical analysis, SAT-solving, and formal verification sets a high standard for computer-assisted proofs in combinatorics and economics.
Generated Apr 22, 2026
Comparison History (59)
Paper 1 resolves a central, long-standing open question in fair division (EFX existence) definitively in the negative, which is one of the most prominent problems in the field. Its methodological novelty—combining SAT-solving with formally verified LEAN proofs at massive scale—demonstrates a broadly applicable technique for combinatorial problems, enhancing cross-field impact. While Paper 2 also settles an important open question (EF1+PO for submodular valuations) with rigorous boundary mapping, EFX is a higher-profile problem and Paper 1's verified computational methodology offers greater breadth and timeliness.
While Paper 1 impressively resolves a major open problem in fair division, Paper 2 offers higher potential impact due to its extreme timeliness and broad real-world applicability. By unifying mechanism design with LLM alignment and autobidding, Paper 2 provides a foundational framework that formally explains phenomena like prompt engineering and jailbreaking. Its 'trilemma of aligned delegation' directly impacts the rapidly growing fields of AI safety, agentic AI, and digital economics, giving it significantly wider cross-disciplinary and industrial relevance.
Paper 2 resolves a central open question in the theory of discrete fair division by providing a counterexample to the existence of EFX allocations for monotone valuations. Solving a major, long-standing theoretical problem typically yields profound and lasting scientific impact, whereas Paper 1, while highly innovative and practical, presents a new mechanism rather than answering a foundational open mathematical question.
Paper 1 definitively resolves a major open question in the theory of discrete fair division, representing a significant mathematical and algorithmic breakthrough. Its innovative combination of SAT solving with formal verification (LEAN) ensures high methodological rigor. While Paper 2 addresses a timely and broadly relevant topic, Paper 1's concrete resolution of a central theoretical problem guarantees substantial and lasting scientific impact within its field.
Paper 2 likely has higher impact: it resolves a long-standing, foundational open question in mechanism design by pinning down a tight universal 1/2 efficiency guarantee for second-best bilateral trade, closing a major quantitative gap. The result is broadly relevant across economics, auction theory, market design, and theoretical CS, with clear implications for practical market mechanisms. Paper 1 is highly novel and rigorous (SAT+formal proof) and answers a central fair-division question, but its direct real-world applicability and cross-field reach are narrower than the bilateral trade efficiency bound.
Paper 2 resolves a central open question in discrete fair division theory — whether EFX allocations always exist — providing a verified counterexample for n≥3 agents and m≥n+5 items. This is a landmark result in computational social choice and combinatorics, settling a long-standing conjecture in the negative. While Paper 1 offers a thoughtful theoretical analysis of the representation-rationalizability tradeoff in RLHF with practical relevance, it provides incremental insight into a known tension rather than resolving a fundamental open problem. Paper 2's definitive resolution will reshape an entire research area and attract broad attention.
Paper 2 resolves a central open question in the theory of discrete fair division (the existence of EFX allocations for n >= 3) by providing a definitive counterexample. Solving a major open problem typically has a profound and immediate scientific impact within its field, establishing a new baseline for future research. While Paper 1 offers strong theoretical contributions to bandit settings and mechanism design, the definitive resolution of a prominent open question in Paper 2 grants it higher overall scientific impact.
Paper 2 likely has higher impact: it resolves multiple long-standing complexity questions around correlated equilibria beyond normal-form games, introduces strong evidence of intractability via Contr-hardness, proves unconditional information-theoretic lower bounds for swap regret, and provides algorithmic workarounds (FPTAS and specialized poly-time algorithms) with an additional fixed-point computation byproduct. Its results span game theory, learning/regret minimization, and computational complexity, with broad downstream relevance. Paper 1 is highly novel and rigorous (SAT+formal proof) and resolves a central fair-division question, but its impact is more concentrated within discrete fair division.
Paper 1 likely has higher scientific impact: it resolves a central open question in discrete fair division by providing a general counterexample to EFX existence (and a tight positive result for 3 agents/7 goods), changing the theoretical landscape and guiding future algorithmic/mechanism-design work. Its approach is methodologically rigorous (SAT encoding with certified proofs in LEAN and independently checked UNSAT/DRAT artifacts) and broadly relevant across theoretical CS, economics, and computational social choice. Paper 2 is timely and useful for LLM evaluation, but benchmarks often face rapid obsolescence and narrower long-term foundational impact.
Paper 1 likely has higher scientific impact because it resolves a central open problem in discrete fair division by giving a general counterexample to EFX existence (for n≥3, m≥n+5), which is a definitive theoretical result with broad downstream consequences. It is methodologically rigorous (formal encoding, SAT proofs, Lean-verified foundations, independently checkable certificates) and immediately reshapes a mature research area. Paper 2 is timely and potentially influential for AI multi-agent governance, but its impact depends more on how well the meta-game model matches real deployments and on subsequent empirical/behavioral validation.