EFX 存在性反例：基于 SAT 求解的 n ≥ 3 代理、m ≥ n + 5 物品、次调和价值函数
计算机科学与博弈论
2026-05-15 v3 数据结构与算法
摘要
EFX 分配的存在性是离散公平分配领域的一个核心开放问题。如果在移除另一名代理单个物品后，不存在代理 envy 另一个代理的分配，则该分配称为 EFX（envy-free up to any good，即对任意良好物品均无嫉妒）。我们通过提供首个反例，解决了该长期未解的问题，即证明对于具有单调价值函数的代理，EFX 分配可能不存在，这进一步立即推出次调和价值函数的反例。具体而言，我们表明对于包含 个代理和 个物品的实例，EFX 分配可能不存在。相反，我们证明了包含三个代理和七个物品的每个实例都 admits EFX 分配。这两项结果均通过 SAT 求解获得。我们将 EFX 存在性的否定编码为 SAT 实例：满足可得反例，而不满足可证明普遍存在。最终，我们在 Lean 中正式验证了该编码的正确性。最后，我们为三个代理和任意数量物品的公平分配建立了正向保证。尽管 EFX 分配可能不存在，我们证明了包含三个代理和单调价值函数的每个实例至少 admits 一种两种自然 EFX 松弛形式之一：tEFX，或 EF1 和 EEFX。
引用
@article{arxiv.2604.18216,
title = {A Counterexample to EFX $n \ge 3$ Agents, $m \ge n + 5$ Items, Submodular Valuations via SAT-Solving},
author = {Hannaneh Akrami and Alexander Mayorov and Kurt Mehlhorn and Shreyas Srinivas and Christoph Weidenbach},
journal= {arXiv preprint arXiv:2604.18216},
year = {2026}
}