SAT solving has recently been proven effective in tackling open combinatorial problems. We contribute two additional results in the context of fair distribution of indivisible goods. Specifically, we demonstrate that EFX (envy-freeness up to any good) allocations always exist for three agents and seven goods, while we provide a counterexample for the case of $n \ge 3$ agents and $m \ge n + 5$ goods. An allocation is EFX if no agent would envy the allocation of any other agent if any single item were to be removed from the other agent's bundle of goods. Each agent's preferences are modeled by a monotone valuation function on all potential bundles. After analyzing theoretical aspects of the problem, we encode the negation of the EFX instances into SAT. Satisfiability of the respective SAT formula constitute a counter-example to EFX, unsatisfiability of the respective SAT formula implies that EFX holds. The theoretical foundations of the encoding are proven correct in LEAN. For the three agents and seven goods case, we obtained a proof of unsatisfiability using SPASS-SAT of size about 30 GB in about 30 hours. It was shown to be correct by DRAT-trim. In the case of three agents and eight goods, SPASS-SAT computed satisfiability indicating a counterexample in the form of three specific agent valuations in about 20 hours. It was verified by probing all possible bundle assignments; the verification takes seconds. The extension of the counterexample to $n \ge 4$ agents and $m \ge n + 5$ goods does not involve SAT-solving. This counterexample resolves, in the negative, one of the central questions in the theory of discrete fair division.

翻译：SAT求解近期被证明能有效处理开放性组合问题。我们为不可分割物品公平分配领域贡献了两项附加结果。具体而言，我们证明对于三个智能体和七个物品，EFX（至多任意单个物品无嫉妒性）分配总是存在；同时，我们为$n \ge 3$个智能体与$m \ge n + 5$个物品的情形提供了一个反例。若从任意其他智能体的物品组合中移除任意单个物品后，没有智能体会嫉妒该其他智能体的分配，则该分配满足EFX。每个智能体的偏好由其对所有可能物品组合的单调估值函数建模。在分析该问题的理论方面后，我们将EFX实例的否定形式编码为SAT。相应SAT公式的可满足性构成EFX的反例，而不可满足性则意味着EFX成立。该编码的理论基础在LEAN中得以证明。对于三个智能体与七个物品的情形，我们使用SPASS-SAT在大约30小时内获得了约30 GB大小的不可满足性证明，并通过DRAT-trim验证其正确性。对于三个智能体与八个物品的情形，SPASS-SAT在大约20小时内计算了可满足性，并以三个特定智能体估值函数的形式给出了反例。该反例通过探测所有可能的物品组合分配得以验证，验证过程耗时数秒。将反例推广至$n \ge 4$个智能体与$m \ge n + 5$个物品的情形无需依赖SAT求解。该反例否定了离散公平分配理论中的一个核心问题。