The Resolution of Keller's Conjecture

Understand

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.