arXiv · 2609.10585
EFX Allocations for Three Agents and Seven or Eight Chores
Abstract
We prove that every nonnegative additive chore instance with three agents and either seven or eight indivisible chores admits a chores-EFX allocation, in the zero-tolerant sense that every owned chore, including one of zero cost, is quantified in the trim. Both proofs are computer-assisted, but their machine formulas differ. For seven chores, hand-checkable canonicalization reduces nonexistence to a quantifier-free linear real arithmetic (QF_LRA) formula over 21 variables with one failure clause per complete allocation. For eight chores, instances in which two agents share a weakly cheapest chore are lifted from the seven-chore theorem through the matching insertion lemma of Kobayashi, Mahara, and Sakamoto, and the remaining pairwise-disjoint-argmin class reduces to a residual QF_LRA formula over 24 variables. Z3 5.1.0 and cvc5 1.3.4 report both formulas unsatisfiable. With the known $m\leq 2n$ theorem, this settles every three-agent instance with at most eight chores; $m=9$ is the next open cardinality, and additive chores can fail to admit EFX for every $n\geq 4$.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Xinkai Zhang. 2026-09-06. EFX Allocations for Three Agents and Seven or Eight Chores. https://arxiv.org/abs/2609.10585
Cite the original work for its findings. Save a collection to share your selection of sources.