The Keller’s conjecture is a 90 years old conjecture by Ott-Heinrich Keller that in any tiling of Euclidean space by identical hypercubes there are two cubes that meet face to face. The conjecture was know to be true up to dimension 6, and false in dimensions higher than 7. The conjecture was open for dimension 7.

Joshua Brakensiek, Marijn J.H. Heule, John Mackey, and David Narváez translated the equivalent problem of finding cliques in specific graphs into SAT. Proving that they do not exist (UNSAT answer) implies that Keller’s conjecture holds for dimension 7.

The encoding required extensive symmetry breaking strategies to be solved.

The UNSAT proofs produced by the SAT solver CaDiCal (about 200 GB) have been checked by an independent certified checker.

That work received a best paper award at IJCAR.

The video of the presentation is available online.