三个智能体与七个或八个杂务的EFX分配
EFX Allocations for Three Agents and Seven or Eight Chores
浏览论文内容
中文总结 AI 辅助
通过计算机辅助证明，我们证明了三个智能体在七个或八个不可分割杂务上总存在EFX分配，解决了该规模下的分配问题。
中文摘要 AI 辅助
我们证明了每个具有三个智能体和七个或八个不可分割杂务的非负可加杂务实例，在零容忍意义上（即每个拥有的杂务，包括零成本的杂务，都在修剪中被量化）都承认一个杂务-EFX分配。两个证明都是计算机辅助的，但它们的机器公式不同。对于七个杂务，可手工检查的规范化将不存在性归结为一个关于21个变量的无量词线性实数算术（QF_LRA）公式，每个完整分配有一个失败子句。对于八个杂务，两个智能体共享一个最便宜杂务的实例通过Kobayashi、Mahara和Sakamoto的匹配插入引理从七杂务定理提升，而剩余的成对不相交-argmin类归结为关于24个变量的残差QF_LRA公式。Z3 5.1.0和cvc5 1.3.4报告两个公式不可满足。结合已知的$m\leq 2n$定理，这解决了每个最多八个杂务的三智能体实例；$m=9$是下一个开放的基数，并且对于每个$n\geq 4$，可加杂务可能无法承认EFX。
英文摘要
We show that every additive chore instance with three agents and seven or eight indivisible chores has an EFX allocation. Costs may be arbitrary nonnegative reals. Together with the theorem of Kobayashi, Mahara, and Sakamoto for at most $2n$ chores, this settles the existence of EFX allocations for three agents and at most eight chores; for four or more agents, He and Tao have shown that EFX allocations of additive chores need not exist. Both proofs are computer-assisted. For seven chores, we normalize each agent's costs and sort the chores, and then express the nonexistence of an EFX allocation as a formula of quantifier-free linear real arithmetic with one clause per allocation; the SMT solvers Z3 and cvc5 show that this formula is unsatisfiable. For eight chores, if two agents share a cheapest chore, we remove that chore, apply the seven-chore result, and put the chore back using an insertion lemma of Kobayashi, Mahara, and Sakamoto. The remaining instances, in which the agents' sets of cheapest chores are pairwise disjoint, are handled by a second formula of the same kind.
发表机构
- Renmin University of China（中国人民大学）
机构由 AI 辅助整理，请以论文原文为准。
