Non-Existence of EFX Chore Allocations for Monotone Cost Functions with Binary Marginals
Zehan Lin, Shengxin Liu, Biaoshuai Tao, Shengwei Zhou
cs.GT
Aug 11, 2026 · v1
TL;DR
Two impossibility counterexamples for EFX chore allocations under binary XOS and supermodular costs are formalized and verified in Lean 4.
Abstract
We study the existence of envy-free up to any item (EFX) allocations of indivisible chores when agents have monotone cost functions with binary marginals. For indivisible goods, the corresponding existence question is known to have an affirmative answer for general monotone functions with binary marginals. For chores, however, the existence of EFX allocation was previously known only for more restricted classes, while the general binary-marginal case remained unresolved. In this paper, we provide two counterexamples based on the same 18-agent, 53-chore word gadget, with one cost profile for binary XOS costs and another for binary supermodular costs. In both cases, a complete EFX allocation need not exist. Finally, we formalize and verify our main results in Lean 4.
Problem
For indivisible chores, whether EFX allocations exist under monotone cost functions with binary marginals was unresolved, while existence holds for goods and for restricted chore classes.
Approach
The authors construct a common 18-agent, 53-chore word gadget where each chore is an 18-bit string and agent costs depend only on the bits at their index. Two cost profiles are defined: one giving binary XOS costs (maximum of two binary additive functions) and another giving binary supermodular costs (nullity of a rank-two partition matroid). A key matching lemma about projection cliques underpins both non-existence proofs, which are then formalized and verified in Lean 4.
Results
There exist 18-agent, 53-chore instances with binary XOS costs and separately with binary supermodular costs for which no complete EFX allocation exists, resolving these cases negatively; existence for binary submodular costs remains open.
