Abstract
We consider three graphs, 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. 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 contains a facesharing pair of cubes. Since a faceshare-free unit cube tiling of exists (which we also verify), this completely resolves Keller’s conjecture.
Cite
CITATION STYLE
Brakensiek, J., Heule, M., Mackey, J., & Narváez, D. (2020). The Resolution of Keller’s Conjecture. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12166 LNAI, pp. 48–65). Springer. https://doi.org/10.1007/978-3-030-51074-9_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
