三个人分蛋糕，理论上真的做不到公平——SAT 求解器终结了几十年的猜想

三个人分蛋糕，无论怎么切，总有人觉得不公平——这个数学问题困扰了研究者几十年，最终被一个 SAT 求解器找到了答案。

公平分配问题的核心是：给 n 个人分 m 件物品，能不能做到让所有人都满意到"无论从别人那里拿走哪一件东西，我都不会觉得我比他好"？这个标准叫 EFX（envy-free up to any good）。

1980 年代以来的研究证明了 EFX 在两个人时总是可行的。但三个人呢？四五六个人呢？没有人知道答案。这个问题被称为离散公平分配领域"最核心的开放问题"。

现在答案来了——而且令人惊讶。

什么样的分配才算"公平"？

想象你、小明和小红分三件礼物。EFX 的定义是：如果拿走你得到的任何一件物品，你不会嫉妒别人获得的那一堆。这听起来很苛刻——但也正是这种公平标准让理论家着迷。

几十年里，大量研究者试图证明 EFX 在任意人数下总是可行的，或者找到反例，都没成功。

方法：让 SAT 求解器成为数学家

研究者把"是否存在一个 EFX 分配"编码成了 SAT（布尔可满足性问题）实例：

• 不可满足 = 所有分法都不满足 EFX → 不可行
• 可满足 = 找到了反例

他们设定了 3 个人、8 件物品（≥ n+5）。SAT 求解器跑了之后返回：可满足。这意味着存在一种估值配置使得任何分配方案都无法达到 EFX 标准——这是历史上第一个 EFX 不可行的反例。

作者用 Lean 证明辅助器对 SAT 编码的正确性做了形式化验证。编码没有 bug——反例是真的反例。我对 Lean 验证只有粗浅的了解，但这个做法意味着推理链条在数学上被严格验证了。

结果与意义

三个关键结果：

① EFX 反例存在。当 n ≥ 3 且 m ≥ n+5 时，EFX 分配不一定存在。推翻了"EFX 总是存在"的猜想。

② 同时，3 人 7 件物品总是可行。严格划出了边界。

③ 即使 EFX 不行，也有候补方案——tEFX 或 EF1+EEFX 之一总是存在。

用 SAT 求解器解决开放数学问题不是新鲜事，但用 SAT 解一个几十年的猜想并且对编码做机器验证，展示了理论计算机科学研究的新范式。

我必须承认我不确定的一点：论文说反例要求 m ≥ n+5。这个 +5 是紧的吗？n=3 时 m=8 是最小反例就成立，还是 m 更大才能找到？我不是 100% 确定。

论文信息

• 标题：A Counterexample to EFX n ≥ 3 Agents, m ≥ n+5 Items via SAT-Solving
• 作者：Hannaneh Akrami, Alexander Mayorov, Kurt Mehlhorn, Shreyas Srinivas, Christoph Weidenbach
• 预印本：arXiv:2604.18216 (cs.GT)
• 核心贡献：用 SAT 求解发现 EFX 首个反例，Lean 形式化验证
• 论文链接：https://arxiv.org/abs/2604.18216

参考文献

1. Akrami, H., et al. (2026). A Counterexample to EFX. arXiv:2604.18216.
2. Caragiannis, I., et al. (2019). Unifying Approximations of Envy-Freeness.
3. Plaut, B., & Roughgarden, T. (2020). Almost Envy-Freeness. SODA 2020.

#EFX #FairDivision #SAT #FormalVerification #ComputationalSocialChoice #FeynmanLearning #智柴