We consider three graphs, $G_{7,3}$, $G_{7,4}$, and $G_{7,6}$, related to Keller's conjecture in dimension 7. The conjecture is false for this dimension if and only if at least one of the graphs contains a clique of size $2^7 = 128$. We present an automated method to solve this conjecture by encoding the existence of such a clique as a propositional formula. We apply satisfiability solving combined with symmetry-breaking techniques to determine that no such clique exists. This result implies that every unit cube tiling of $\mathbb{R}^7$ contains a facesharing pair of cubes. Since a faceshare-free unit cube tiling of $\mathbb{R}^8$ exists (which we also verify), this completely resolves Keller's conjecture.

翻译：我们考虑与7维凯勒猜想相关的三个图：$G_{7,3}$、$G_{7,4}$ 和 $G_{7,6}$。该猜想在此维度为假当且仅当至少其中一个图包含大小为 $2^7 = 128$ 的团。我们提出一种自动化方法，通过将此类团的存在性编码为命题公式来证明该猜想。结合可满足性求解与对称破缺技术，我们确定不存在这样的团。该结果表明 $\mathbb{R}^7$ 的每个单位立方体铺砌均包含一对共面立方体。由于 $\mathbb{R}^8$ 存在无共面单位立方体铺砌（我们亦验证了这一点），这完全解决了凯勒猜想。