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\ge3$个主体和$m\ge n+5$件物品的情况提供了一个反例。如果一个分配中,任何主体在移除其他主体物品束中的任意一件物品后,都不会嫉妒该其他主体的分配,则该分配是EFX的。每个主体的偏好由一个在所有潜在物品束上的单调估价函数来建模。在分析问题的理论方面之后,我们将EFX实例的否定编码为SAT。相应SAT公式的可满足性构成EFX的一个反例,而相应SAT公式的不可满足性则意味着EFX成立。编码的理论基础在LEAN中得到了正确性证明。对于三个主体和七件物品的情况,我们使用SPASS-SAT在大约30小时内获得了一个大小约为30GB的不可满足性证明,并通过DRAT-trim验证了其正确性。在三个主体和八件物品的情况下,SPASS-SAT计算出了可满足性,以三个特定主体估价的形式在大约20小时内表明了一个反例,并通过探测所有可能的物品束分配进行了验证;该验证仅需数秒。该反例推广到$n\ge4$个主体和$m\ge n+5$件物品时不涉及SAT求解。这一反例否定性地解决了离散公平分配理论中的一个核心问题。