Hannaneh Akrami, Alexander Mayorov, Kurt Mehlhorn et al.
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.