arxiv: 2604.18216 · v3 · submitted 2026-04-20 · 💻 cs.GT · cs.DS

Recognition: no theorem link

A Counterexample to EFX n ge 3 Agents, m ge n + 5 Items, Submodular Valuations via SAT-Solving

Hannaneh Akrami , Alexander Mayorov , Kurt Mehlhorn , Shreyas Srinivas , Christoph Weidenbach

Authors on Pith no claims yet

Pith reviewed 2026-05-15 06:21 UTC · model grok-4.3

classification 💻 cs.GT cs.DS

keywords EFX allocationsfair divisioncounterexampleSAT solvingmonotone valuationssubmodular valuationsenvy-free allocations

0 comments

The pith

EFX allocations need not exist for three or more agents and at least five extra goods under monotone valuations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper settles a central open question by exhibiting the first counterexample showing that EFX allocations are not guaranteed to exist. It constructs an explicit instance with three agents and eight goods whose monotone valuations admit no allocation where each agent values every other bundle at most as much as their own after removing any one good. The same instance serves as a counterexample for submodular valuations. For comparison, the authors prove that every instance with three agents and seven goods does admit an EFX allocation. They further show that any three-agent monotone instance always admits at least one of two natural EFX relaxations.

Core claim

There exist instances with n ≥ 3 agents and m ≥ n + 5 goods under monotone valuations that admit no EFX allocation; the smallest such case found is n = 3, m = 8, obtained by encoding the negation of EFX existence as a SAT formula whose satisfying assignment yields the concrete counterexample valuations.

What carries the argument

SAT encoding of the statement 'no EFX allocation exists for these valuations', whose satisfiability directly produces a counterexample instance, with the encoding formally verified in Lean.

If this is right

EFX allocations exist for every instance with three agents and exactly seven goods.
Any three-agent monotone instance admits either a tEFX allocation or both an EF1 allocation and an EEFX allocation.
The non-existence result immediately transfers to submodular valuations since they form a subclass of monotone valuations.
Algorithms for computing fair allocations with three or more agents must accommodate cases where no EFX solution exists.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The sharp threshold between seven and eight goods for three agents suggests that existence proofs may require case analysis on the exact difference m - n.
Similar SAT encodings could be used to search for the minimal number of goods that force non-existence for four or more agents.
The existence of the two relaxations for three agents indicates that practical fair-division mechanisms can fall back to EF1-plus-EEFX or tEFX without sacrificing too much fairness.

Load-bearing premise

The SAT encoding correctly captures the logical negation of the existence of an EFX allocation for monotone valuations.

What would settle it

A direct check that the concrete valuation functions produced by the solver satisfy monotonicity yet possess no EFX allocation, or an error discovered in the Lean verification of the encoding.

Figures

Figures reproduced from arXiv: 2604.18216 by Alexander Mayorov, Christoph Weidenbach, Hannaneh Akrami, Kurt Mehlhorn, Shreyas Srinivas.

**Figure 2.** Figure 2: The basic model of SAT 3. We also prove the invariance of valuation ordering and the EFX property under bijections of an allocInstance for the special case of Agents = Fin n and Goods = Fin m. Here n < m are both natural numbers and Fin n and Fin m respectively denote the type of natural numbers bounded strictly from above by n and m. This means by reordering the good sets in the specified item ordering of… view at source ↗

**Figure 3.** Figure 3: The basic literals of our SAT encoding and the allocation structure whose allocations will be [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗

**Figure 4.** Figure 4: Visualization of the counterexample to EFX existence for 3 agents and 8 goods. The colors [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗

**Figure 5.** Figure 5: Visualization of the marginal contributions in the counterexample to EFX existence for 3 agents [PITH_FULL_IMAGE:figures/full_fig_p014_5.png] view at source ↗

**Figure 6.** Figure 6: Some MMS-violations for the valuation v0, i.e., sets A, B, C, D such that A∪B = C∪D, A∩B = /0 = C ∩ D and min(v(A),v(B)) > max(v(C),v(D)). For v0 the values of the items are increasing, i.e., v(g0) < v(g1) < ... < v(g7). It appears that there is significant complementarity between elements g1 and g2, and between {g4,g7} and a further element in {g0,g3}. Note that {g4,g7} is a subset of D, and, by themselve… view at source ↗

**Figure 7.** Figure 7: Results of running the Z3 theorem prover on the LRA instances encoding existence of EFX for 3 [PITH_FULL_IMAGE:figures/full_fig_p016_7.png] view at source ↗

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

They deliver a SAT-found counterexample showing EFX can fail for monotone valuations with three agents and eight goods, plus a matching positive result for seven goods, but the submodular claim does not follow.

read the letter

The paper's core result is a concrete counterexample, found by encoding the negation of EFX existence as a SAT problem, for three agents and eight goods under monotone valuations. They also prove that every instance with three agents and seven goods does admit an EFX allocation, again via SAT. The encoding is formally verified in Lean, which gives the computational search real weight. They further show that for three agents and any number of goods, one of two relaxations (tEFX, or EF1 plus EEFX) always exists. That combination of negative and positive results for small n is the actual advance here. The approach is straightforward and the verification step is a clear plus for reproducibility. The soft spot is the submodular part. The title and abstract present the result as a counterexample for submodular valuations, yet the search only enforces monotonicity. A monotone instance that is not submodular disproves existence only for the larger class; it does not automatically give a submodular counterexample. The abstract's phrasing that the monotone result 'immediately implies' one for submodular is incorrect unless the specific valuations satisfy the submodularity inequalities, which is not confirmed in the provided text. If the found instance happens to be submodular, that needs explicit checking and stating. This is a fixable gap rather than a fatal one, but it affects how the result is framed. The work is aimed at people in discrete fair division and algorithmic game theory who care about existence questions for EFX and its relaxations. It is worth sending to peer review because the computational resolution of the open parameter range is substantive and the Lean verification provides a verifiable anchor, even if the submodular claim requires clarification.

Referee Report

1 major / 0 minor

Summary. The paper claims to resolve the open question of EFX existence by exhibiting the first counterexample for n≥3 agents and m≥n+5 goods under monotone valuations (via SAT search whose encoding is Lean-verified), asserts that this immediately yields a submodular counterexample, proves that every 3-agent 7-good instance admits an EFX allocation, and shows that every 3-agent monotone instance admits either tEFX or both EF1 and EEFX.

Significance. A verified computational counterexample to EFX existence under monotone (and, if confirmed, submodular) valuations would settle a central open problem in discrete fair division. The combination of SAT encoding with Lean verification of the encoding constitutes a methodological strength that enhances reproducibility and trustworthiness of the negative result.

major comments (1)

[Abstract] Abstract: The assertion that a counterexample for monotone valuations 'in turn immediately implies a counterexample for submodular valuations' is incorrect. Submodular valuations are a strict subclass of monotone valuations; an instance whose valuations violate submodularity (e.g., by failing v(A∪{g})−v(A) ≥ v(B∪{g})−v(B) for some A⊆B, g∉B) disproves existence only for the larger class. The title and main claim target submodular valuations, yet the described encoding enforces only monotonicity. The manuscript must either exhibit the concrete valuation tables from the SAT solution and verify submodularity, or restrict its claim to monotone valuations.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed and constructive report. The major comment correctly identifies an imprecise claim in the abstract regarding the relationship between monotone and submodular valuations. We address this point below and will make the necessary revisions.

read point-by-point responses

Referee: [Abstract] Abstract: The assertion that a counterexample for monotone valuations 'in turn immediately implies a counterexample for submodular valuations' is incorrect. Submodular valuations are a strict subclass of monotone valuations; an instance whose valuations violate submodularity (e.g., by failing v(A∪{g})−v(A) ≥ v(B∪{g})−v(B) for some A⊆B, g∉B) disproves existence only for the larger class. The title and main claim target submodular valuations, yet the described encoding enforces only monotonicity. The manuscript must either exhibit the concrete valuation tables from the SAT solution and verify submodularity, or restrict its claim to monotone valuations.

Authors: We agree that the phrasing in the abstract is imprecise and does not logically follow: a counterexample under monotone valuations does not automatically yield one under the stricter submodular class. The SAT encoding indeed enforces only monotonicity (plus the negation of EFX). To address this, we will revise the abstract to state that we exhibit a counterexample for monotone valuations and note that the title's reference to submodular valuations requires verification of the specific instance. In the revised manuscript we will include the explicit valuation tables produced by the SAT solver (in an appendix, as they are lengthy) and provide a direct check confirming that these valuations satisfy the submodular inequality for all relevant sets. If any table entry fails submodularity we will instead restrict all claims to monotone valuations and adjust the title accordingly. This revision will be accompanied by a brief explanation of the encoding's monotonicity constraints. revision: yes

Circularity Check

0 steps flagged

Direct SAT-based counterexample search is self-contained

full rationale

The paper's central claim rests on encoding the negation of EFX existence as a SAT formula whose satisfiability produces an explicit counterexample instance, with the encoding formally verified in Lean. This is a computational search procedure rather than a mathematical derivation that reduces any quantity to itself by definition, renames a fitted parameter as a prediction, or relies on a load-bearing self-citation chain. The monotone-to-submodular implication is a straightforward set inclusion once an instance is exhibited; no equation or step in the provided text equates the output to its own input by construction. The result is therefore independent of the paper's own fitted values or prior self-referential theorems.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the correctness of the SAT reduction from EFX non-existence; no free parameters or new entities are introduced.

axioms (1)

domain assumption The SAT encoding accurately represents the non-existence of an EFX allocation under monotone valuations
The paper relies on this encoding; correctness is asserted via Lean verification.

pith-pipeline@v0.9.0 · 5570 in / 1151 out tokens · 54639 ms · 2026-05-15T06:21:13.268463+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Reference graph

Works this paper leans on

18 extracted references · 18 canonical work pages · 1 internal anchor

[1]

In: AAMAS 2026 (2026)

Afshinmehr, M., Ashuri, A., Mahmoudkhan, P., Mehlhorn, K.: EFX Allocations Exist on Triangle- Free Multi-Graphs. In: AAMAS 2026 (2026)

work page 2026
[2]

Akrami, H., Alon, N., Chaudhury, B.R., Garg, J., Mehlhorn, K., Mehta, R.: EFX: A simpler approach and an (almost) optimal guarantee via rainbow cycle number. Oper. Res.73(2), 738–751 (2025). https://doi.org/10.48550/ARXIV .2205.07638

work page internal anchor Pith review doi:10.48550/arxiv 2025
[3]

arXiv (2026)

Akrami, H., Mahara, R., Mehlhorn, K., Rathi, N.: Achieving EF1 and Epistemic EFX Guarantees Simultaneously. arXiv (2026)

work page 2026
[4]

www.SMT-LIB.org(2016)

Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org(2016)

work page 2016
[5]

In: Gurfinkel, A., Ganesh, V

Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: Cadical 2.0. In: Gurfinkel, A., Ganesh, V . (eds.) Computer Aided Verification - 36th International Conference, CA V 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 133–152. Springer (2024)

work page 2024
[6]

Springer, Berlin, Heidelberg, 1 edn

Bradley, A.R., Manna, Z.: The Calculus of Computation. Springer, Berlin, Heidelberg, 1 edn. (2007). https://doi.org/10.1007/978-3-540-74113-8

work page doi:10.1007/978-3-540-74113-8 2007
[7]

In: CADE

Bromberger, M., Fleury, M., Schwarz, S., Weidenbach, C.: SPASS-SATT - A CDCL(LA) solver. In: CADE. vol. 11716, pp. 111–122. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6_7, https://doi.org/10.1007/978-3-030-29436-6_7

work page doi:10.1007/978-3-030-29436-6_7 2019
[8]

JACM71, 1–27 (2024), a preliminary version appeared in EC ’20

Chaudhury, B.R., Garg, J., Mehlhorn, K.: EFX Exists for Three Agents. JACM71, 1–27 (2024), a preliminary version appeared in EC ’20

work page 2024
[9]

In: Proceedings of the 24th ACM Conference on Economics and Computation, EC 2023, London, United Kingdom, July 9-12, 2023

Christodoulou, G., Fiat, A., Koutsoupias, E., Sgouritsa, A.: Fair allocation in graphs. In: Proceedings of the 24th ACM Conference on Economics and Computation, EC 2023, London, United Kingdom, July 9-12, 2023. pp. 473–488. ACM (2023)

work page 2023
[10]

In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

mathlib Community, T.: The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. p. 367–381. CPP 2020, Association for Computing Machinery, New York, NY , USA (2020). https://doi.org/10.1145/3372885.3373824, https://doi.org/10.1145/3372885.3373824 8An allocation(X 1, . . . ,Xn)is EEFX ...

work page doi:10.1145/3372885.3373824 2020
[11]

In: Ball, T., Jones, R.B

Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification. pp. 81–94. Springer, Berlin, Heidelberg (2006)

work page 2006
[12]

Texts in Theoretical Computer Science

Kroening, D., Strichman, O.: Decision Procedures. Texts in Theoretical Computer Science. An EATCS Series, Springer, Berlin, Heidelberg, 2 edn. (2016). https://doi.org/10.1007/978-3-662-50497- 0

work page doi:10.1007/978-3-662-50497- 2016
[13]

Mathe- matics of Operations Research49(2), 1263–1277 (2023)

Mahara, R.: Extension of additive valuations to general valuations on the existence of EFX. Mathe- matics of Operations Research49(2), 1263–1277 (2023)

work page 2023
[14]

MIT Press (2003)

Moulin, H.: Fair division and collective welfare. MIT Press (2003)

work page 2003
[15]

In: TACAS 2008

de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS 2008. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008)

work page 2008
[16]

In: Au- tomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings

Moura, L.d., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Au- tomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. p. 625–635. Springer-Verlag, Berlin, Hei- delberg (2021). https://doi.org/10.1007/978-3-030-79876-5_37,https://doi.org/10.1007/ 978-3-030-79876-5_37

work page doi:10.1007/978-3-030-79876-5_37 2021
[17]

Plaut, B., Roughgarden, T.: Almost envy-freeness with general valuations. SIAM J. Discret. Math. 34(2), 1039–1068 (2020)

work page 2020
[18]

ThreeVals.txt

Wetzler, N., Heule, M., Jr., W.A.H.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Com- puter Science, vol. 8561, pp. 422–429. Springer (2014) A The Valuations Tables 2, 3, and 4 show the three valuations. B Further Theoretical Aspects of EFX We bri...

work page 2014