  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.
