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.
翻译：我们考虑与Keller猜想在7维度上相关的三个图，$G_{7,3}$，$G_{7,4}$ 和 $G_{7,6}$。如果至少其中一个图包含一个大小为 $2^7 = 128$ 的团，那么此猜想在此维度上是错误的。我们提出了一种自动化方法来解决此猜想，通过将这样的团的存在编码为命题公式。我们应用满足性求解和对称性破坏技术来确定不存在这样的团。该结果意味着$\mathbb{R}^7$的每个单位立方体铺砖都包含两个共享面的立方体对。由于存在一个不共享面的$\mathbb{R}^8$单位立方体铺砖（我们也验证了这一点），因此这完全解决了Keller猜想。
相关内容
微信扫码咨询专知VIP会员