A Counterexample to EFX $n \ge 3$ Agents, $m \ge n + 5$ Items, Submodular Valuations via SAT-Solving
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916011205197824 |
|---|---|
| author | Akrami, Hannaneh Mayorov, Alexander Mehlhorn, Kurt Srinivas, Shreyas Weidenbach, Christoph |
| author_facet | Akrami, Hannaneh Mayorov, Alexander Mehlhorn, Kurt Srinivas, Shreyas Weidenbach, Christoph |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_18216 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Counterexample to EFX $n \ge 3$ Agents, $m \ge n + 5$ Items, Submodular Valuations via SAT-Solving Akrami, Hannaneh Mayorov, Alexander Mehlhorn, Kurt Srinivas, Shreyas Weidenbach, Christoph Computer Science and Game Theory Data Structures and Algorithms F.2.2 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. |
| title | A Counterexample to EFX $n \ge 3$ Agents, $m \ge n + 5$ Items, Submodular Valuations via SAT-Solving |
| topic | Computer Science and Game Theory Data Structures and Algorithms F.2.2 |
| url | https://arxiv.org/abs/2604.18216 |