四个加法型主体与至多九种商品存在完整的EFX分配
Complete EFX Allocations Exist for Four Additive Agents and Up to Nine Goods
浏览论文内容
中文总结 AI 辅助
该研究证明四个加法型主体与至多九种商品存在完整的EFXo分配，突破了此前的边界，通过手工归约引理与机器验证证书库完成证明，并解释了问题的困难性来源。
中文摘要 AI 辅助
我们证明，每个包含四个主体、对非负实数具有加法估值且至多九种不可分商品的公平分配实例，都存在一种完整的分配，该分配在强零容忍意义下是无嫉妒（EFXo）的。m=9=n+5的情况超出了此前已知的四个主体完整EFX分配的边界（m≤n+3）。该证明结合了一组手工证明的归约定理与机器验证的证书库。估值多面体被一组更小的多面体覆盖；对于每个更小的多面体P，找到一个分配族F，其中包含P中每个估值对应的EFXo分配。验证F对P是否充分是无量词线性算术不可满足性判定，由独立验证者从头推导并求解，按条款佐证，且可由独立的小型第三方实现重新验证。m=8的情况通过两种方式确定：一是此前针对该规模的独立项目，二是作为m=9定理的一段式推论。我们还给出了该问题困难性的可能解释：困难性集中在近乎相同的估值上，此时所有4^9种分配中仅约0.14%为EFXo，且单个区域内的显式估值对会产生相反的强制分配结构，这一证据与任何求解器栈无关，对一般猜想具有相关性。
英文摘要
We prove that every fair-division instance with four agents, additive valuations over the non-negative reals, and at most nine indivisible goods admits a \emph{complete} allocation that is envy-free up to any good in the strong, zero-tolerant sense ($\EFXo$). The case $m=9=n+5$ lies beyond the previously known frontier for complete EFX with four agents ($m\le n+3$). The proof combines a small set of hand-proven reduction lemmas with a machine-verified certificate corpus. The valuation polytope is covered by a collection of smaller polytopes. For each smaller polytope $P$, a family $F$ of allocations is found that contains an $\EFXo$ allocation for every valuation in $P$. The check that $F$ suffices for $P$ is a quantifier-free linear-arithmetic unsatisfiability verdict, re-derived and solved from scratch by an independent certifier, corroborated per clause, and re-verifiable by a independent small third implementation. The $m=8$ case is established twice: by an earlier independent project at that size and as a one-paragraph padding corollary of the $m=9$ theorem. We additionally give a possible explanation why the problem is hard: difficulty concentrates on near-identical valuations, where only ${\approx}0.14\%$ of all $4^9$ allocations are $\EFXo$, and explicit valuation pairs inside a single region force opposite mandatory allocation structure, evidence relevant to the general conjecture independently of any solver stack.
