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.
翻译:我们考虑三个图表,即$G$7,3美元、$G$7,4美元和$G$7,6美元,与Keller在维度上的推测有关。7. 如果而且只有当至少有一个图表包含一个大小为2,7美元=128美元的方块时,这一假设对于这个维度是虚假的。我们提出一种自动化方法来解决这一推测,将存在这种分类作为一种建议公式。我们运用了与对称破碎技术相结合的可视性解决方案来确定不存在这种分类。这个结果意味着每个单位的立方体在$mathbb{R$7$中都含有一对立方块。由于一个无面单位立方块的立方块是$mathb{R$8美元(我们也核查了这一点),这就完全解决了Keller的猜想。