The Resolution of Keller's Conjecture
This page provides access to results, proofs, and tools presented in the
IJCAR 2020 paper
The Resolution of Keller's Conjecture
by Joshua Brakensiek,
Marijn J.H. Heule,
John Mackey, and
David Narváez (best paper award).
A preprint is available on arXiv.
Introduction for the general public
Keller's conjecture,
a mathematical problem that has been open for almost a century,
was recently fully resolved by computer scientists and mathematicians at CMU, RIT, and
Stanford. To obtain this result, they combined decades of mathematical insights into
the conjecture with automated reasoning on a cluster of computers.
The conjecture involves a statement regarding tiling: Consider tiling a floor with square tiles, all of the same size. Is it the case that any gap-free tiling results in at least two fully connected tiles, i.e., tiles that have an entire edge in common? Some quick drawings show that this is indeed the case. The same is true if the statement is generalized from a two-dimensional floor to a three-dimensional space: when completely filling a space with equal-sized cubes, there must be two cubes that fully share a face. Going beyond three dimensions may seem difficult for non-mathematicians, but for experts it is not hard to show that the same pattern also holds when considering four or even five dimensions. In 1930, German mathematician Ott-Heinrich Keller therefore conjectured that it holds for any number of dimensions.
In the decades that followed, many advances were made regarding Keller's conjecture. Perron (1940) was the first to show that the conjecture holds in the six-dimensional case. However, Lagarias and Shor (1992) demonstrated that the conjecture is false for ten or more dimensions. This negative result was later improved by Mackey (2002) to eight or more dimensions. Until recently, the only remaining case---seven dimensions---was still open, despite various researchers producing new insights over the years. Now, recent work by Brakensiek, Heule, Mackey, and Narváez finally puts this last remaining issue to bed: the pattern holds in the seven-dimensional case. Their result was obtained with the aid of automated reasoning techniques that produced an enormous proof of roughly 200 gigabytes. The correctness of this proof has been verified with a so-called proof checker---a computer program that was itself proved to be correct.
The conjecture involves a statement regarding tiling: Consider tiling a floor with square tiles, all of the same size. Is it the case that any gap-free tiling results in at least two fully connected tiles, i.e., tiles that have an entire edge in common? Some quick drawings show that this is indeed the case. The same is true if the statement is generalized from a two-dimensional floor to a three-dimensional space: when completely filling a space with equal-sized cubes, there must be two cubes that fully share a face. Going beyond three dimensions may seem difficult for non-mathematicians, but for experts it is not hard to show that the same pattern also holds when considering four or even five dimensions. In 1930, German mathematician Ott-Heinrich Keller therefore conjectured that it holds for any number of dimensions.
In the decades that followed, many advances were made regarding Keller's conjecture. Perron (1940) was the first to show that the conjecture holds in the six-dimensional case. However, Lagarias and Shor (1992) demonstrated that the conjecture is false for ten or more dimensions. This negative result was later improved by Mackey (2002) to eight or more dimensions. Until recently, the only remaining case---seven dimensions---was still open, despite various researchers producing new insights over the years. Now, recent work by Brakensiek, Heule, Mackey, and Narváez finally puts this last remaining issue to bed: the pattern holds in the seven-dimensional case. Their result was obtained with the aid of automated reasoning techniques that produced an enormous proof of roughly 200 gigabytes. The correctness of this proof has been verified with a so-called proof checker---a computer program that was itself proved to be correct.
Figure 1: Two-dimensional tiling
Figure 2: Three-dimensional tiling
Figure 1: a gap-free tiling of the two-dimensional space with equal-sized square tiles. The bold blue edges denote that two tiles are fully connected.
Figure 2: a partial tiling of the three-dimensional space with equal-sized cubes. The only way to tile the entire space would result in a fully face-sharing square at the position of the blue squares.
Keller graphs
A crucial step in proving Keller's conjecture in the seventh dimension is a reformulation of the
problem as a property of Keller graphs, an invention by Corradi and Szabo in 1990. The Keller graphs are constructed using two parameters:
the dimension n and the shift s. Each vertex in a Keller graph can be considered a dice with
n dots such that each dot is colored using a palette of 2s colors. The colors come in s pairs of opposite colors. For
example, black and white are opposite colors. Red and green are opposite colors as well. Two vertices (dice)
are connected if 1) they have at least two dots that differ in color and 2) they have at least
one dot with opposite colors.
Let's consider the graph with n=2 an s=2. For the two pairs of opposite colors we will use black/white and red/green. Figure 3 shows this graph. All 16 different dice are shown. The top dice (black + white) is connected to the left-most dice (red + black) because both dots are different (requirement 1) and the color of their second dot is opposite (white versus black, thus requirement 2). The top dice is not connected to the dice with two red dots: The colors of both dots differ, but they don't have a dot with opposite colors.
Corradi and Szabo showed that Keller's conjecture is false for dimension n if there exists a Keller graph with dimension n and some shift s such that 2^n dice are fully connected. Keller's conjecture would have been false if there were 4 dice that were fully connected in the shown graph. However, observe that there are not even 3 dice that are fully connected.
Let's consider the graph with n=2 an s=2. For the two pairs of opposite colors we will use black/white and red/green. Figure 3 shows this graph. All 16 different dice are shown. The top dice (black + white) is connected to the left-most dice (red + black) because both dots are different (requirement 1) and the color of their second dot is opposite (white versus black, thus requirement 2). The top dice is not connected to the dice with two red dots: The colors of both dots differ, but they don't have a dot with opposite colors.
Corradi and Szabo showed that Keller's conjecture is false for dimension n if there exists a Keller graph with dimension n and some shift s such that 2^n dice are fully connected. Keller's conjecture would have been false if there were 4 dice that were fully connected in the shown graph. However, observe that there are not even 3 dice that are fully connected.
Figure 3: a Keller graph
Automated reasoning
Figure 4: a small Keller problem
In recent years Kisielewicz and Lysakowska made significant progress regarding Keller's conjecture.
In short, they showed that Keller's conjecture is false in the seventh dimension if and only if there exist 128 fully connected vertices in the Keller
graph with n=7 and s={3,4,6}.
We used automated reasoning to prove that they do not exist and thus Keller's conjecture holds in the seven-dimensional case.
Automated reasoning is also known as classical artificial intelligence and deals with mechanically answering logic questions. We exploit the fact that computers are typically much better in logic than humans. A powerful method to perform automated reasoning is encoding a given problem as a satisfiability problem. This approach was also used to solve other mathematical problems, such as the Pythagorean triples problem.
To illustrate the approach, consider the question whether there exist three dice with two dots that are completely connected based on the Keller graph connections, i.e., 1) they have at least two dots that differ in color and 2) they have at least one dot with opposite colors. Assume we use two pairs of opposite colors: black/white and red/green. Each of the in total six dots can have any of the four colors. So the search space is 4^6 = 4096 colorings. However, automated reasoning can determine that the colors and the two dots on a dice are interchangable. The symmetries due to the colors and the dots can be broken by enforcing that both dots of the top dice are colored black, thereby making the problem much easier. Additional automated reasoning techniques allow checking only a single coloring instead of all 4096 ones.
Automated reasoning is also known as classical artificial intelligence and deals with mechanically answering logic questions. We exploit the fact that computers are typically much better in logic than humans. A powerful method to perform automated reasoning is encoding a given problem as a satisfiability problem. This approach was also used to solve other mathematical problems, such as the Pythagorean triples problem.
To illustrate the approach, consider the question whether there exist three dice with two dots that are completely connected based on the Keller graph connections, i.e., 1) they have at least two dots that differ in color and 2) they have at least one dot with opposite colors. Assume we use two pairs of opposite colors: black/white and red/green. Each of the in total six dots can have any of the four colors. So the search space is 4^6 = 4096 colorings. However, automated reasoning can determine that the colors and the two dots on a dice are interchangable. The symmetries due to the colors and the dots can be broken by enforcing that both dots of the top dice are colored black, thereby making the problem much easier. Additional automated reasoning techniques allow checking only a single coloring instead of all 4096 ones.
Log files, sources, and proofs
The log files, instructions and the sources to reproduce our results, and the proofs are available on GitHub at
https://github.com/marijnheule/Keller-encode.
We wrote a tool that encodes as a satisfiability problem whether Keller graph with parameters n and s has a clique of size 2^n, or equivalently in the description above there are 2^n completely connected dice. The program is called Keller-encode. Automated reasoning showed that the encodings with n=7 and s={3,4,6} are unsatisfiable: i.e., no such clique exists. The satisfiability problems can be downloaded here:
We wrote a tool that encodes as a satisfiability problem whether Keller graph with parameters n and s has a clique of size 2^n, or equivalently in the description above there are 2^n completely connected dice. The program is called Keller-encode. Automated reasoning showed that the encodings with n=7 and s={3,4,6} are unsatisfiable: i.e., no such clique exists. The satisfiability problems can be downloaded here:
- Keller-7-3.cnf: n=7, s=3
- Keller-7-3-sbp.cnf: n=7, s=3, symmetries broken
- Keller-7-3.cnf: n=7, s=4
- Keller-7-3-sbp.cnf: n=7, s=4, symmetries broken
- Keller-7-3.cnf: n=7, s=6
- Keller-7-3-sbp.cnf: n=7, s=6, symmetries broken
Figure 5: the smallest counterexample of Keller's conjecture
Satisfiability problem and proof
The above Keller example can be encoded as a satisfiability problem using 24 boolean variables: variables that are either
true or false. For each dot on each dice there is one variable for each of the four colors.
Let variable x_{v,d,c} denote that dot d on dice v has color c. Encoding a problem as a satisfiability problem
can result in a large encodings with many variables. However, tools to solve satisfiability problems can deal
with many problems that have over a million variables.
Encoding the example problem requires three constraints. First, every dot on every dice must be colored. Second, each pair of dots on different dice should have a different color. Observe that if this is not the case, then requirement 1) is violated. Third, each pair of dice should have one dot such that the colors on this dot are opposite.
The building blocks of satisfiability problems are called clauses. The first constraint can be expressed using 6 clauses (one clause per dot). The second constraint can be expressed using 24 clauses, while the third constraint can be expressed using 48 clauses. Hence the total number of calsues is 78. These clauses are shown in the DIMACS format below. Each variable is represented by a number. The
The example formula is unsatisfiable. This means that there are no three dice with two dots that are completely connected based on the Keller graph connections. The above encoding is actually minimally unsatisfiable: removal of any clause makes the encoding satisfiable. Hence we need all clauses to prove unsatisfiablity. Below is a proof of unsatisfiability, which is a sequence of clauses. In this case the proof is similar is size compared to the encoding, but typically proofs are much larger than the encoding. Such proofs are hard to understand for humans, but they can be validated using highly trustworthy systems, so we can have confidence in their correctness.
Encoding the example problem requires three constraints. First, every dot on every dice must be colored. Second, each pair of dots on different dice should have a different color. Observe that if this is not the case, then requirement 1) is violated. Third, each pair of dice should have one dot such that the colors on this dot are opposite.
The building blocks of satisfiability problems are called clauses. The first constraint can be expressed using 6 clauses (one clause per dot). The second constraint can be expressed using 24 clauses, while the third constraint can be expressed using 48 clauses. Hence the total number of calsues is 78. These clauses are shown in the DIMACS format below. Each variable is represented by a number. The
0 symbol marks the end of a clause. The first
column shows the clauses of the first constraint, the second and thrid columns show the clauses
of the second constraint, and the last 4 columns show the clauses of the third constraint.
p cnf 24 78 1 2 3 4 0 -1 -9 0 -5 -13 0 -1 -5 11 15 0 -4 -5 10 15 0 -11 -13 17 23 0 -18 -21 4 7 0 5 6 7 8 0 -2 -10 0 -6 -14 0 -1 -6 11 16 0 -4 -6 10 16 0 -11 -14 17 24 0 -18 -22 4 8 0 9 10 11 12 0 -3 -11 0 -7 -15 0 -1 -7 11 13 0 -4 -7 10 13 0 -11 -15 17 21 0 -18 -23 4 5 013 14 15 16 0 -4 -12 0 -8 -16 0 -1 -8 11 14 0 -4 -8 10 14 0 -11 -16 17 22 0 -18 -24 4 6 017 18 19 20 0 -1 -17 0 -5 -21 0 -2 -5 12 15 0 -9 -13 19 23 0 -12 -13 18 23 0 -19 -21 1 7 021 22 23 24 0 -2 -18 0 -6 -22 0 -2 -6 12 16 0 -9 -14 19 24 0 -12 -14 18 24 0 -19 -22 1 8 0 -3 -19 0 -7 -23 0 -2 -7 12 13 0 -9 -15 19 21 0 -12 -15 18 21 0 -19 -23 1 5 0 -4 -20 0 -8 -24 0 -2 -8 12 14 0 -9 -16 19 22 0 -12 -16 18 22 0 -19 -24 1 6 0 -9 -17 0 -13 -21 0 -3 -5 9 15 0 -10 -13 20 23 0 -17 -21 3 7 0 -20 -21 2 7 0 -10 -18 0 -14 -22 0 -3 -6 9 16 0 -10 -14 20 24 0 -17 -22 3 8 0 -20 -22 2 8 0 -11 -19 0 -15 -23 0 -3 -7 9 13 0 -10 -15 20 21 0 -17 -23 3 5 0 -20 -23 2 5 0 -12 -20 0 -16 -24 0 -3 -8 9 14 0 -10 -16 20 22 0 -17 -24 3 6 0 -20 -24 2 6 0The example formula is unsatisfiable. This means that there are no three dice with two dots that are completely connected based on the Keller graph connections. The above encoding is actually minimally unsatisfiable: removal of any clause makes the encoding satisfiable. Hence we need all clauses to prove unsatisfiablity. Below is a proof of unsatisfiability, which is a sequence of clauses. In this case the proof is similar is size compared to the encoding, but typically proofs are much larger than the encoding. Such proofs are hard to understand for humans, but they can be validated using highly trustworthy systems, so we can have confidence in their correctness.
-4 -7 -14 24 13 017 -4 -6 19 0-4 3 -6 21 5 19 023 -2 21 -6 019 3 21 -6 1 5 05 7 3 21 1 8 0-19 1 21 13 23 8 0-6 13 16 21 -4 0-10 6 13 19 20 3 16 21 016 21 19 3 8 -4 -5 23 0-4 23 21 -5 19 8 3 017 -2 19 -5 21 023 8 3 1 -5 21 0-2 -5 24 15 22 024 22 3 1 -5 15 0-17 15 3 8 -5 0-24 17 1 21 15 -5 3 01 3 8 7 21 015 20 8 -5 -22 -1 0-22 2 21 8 -1 7 0-5 24 22 15 -1 018 10 22 -6 20 -1 010 20 -23 -1 -6 5 22 02 24 7 8 21 -1 0-6 -2 -1 0-2 7 8 21 -1 011 -5 21 -1 10 -24 6 010 -5 6 21 -24 -1 20 06 21 3 7 8 021 3 7 8 019 -6 -21 7 17 08 7 3 0-11 16 21 13 24 17 0-5 -1 -8 04 -18 7 3 0-23 24 5 -14 10 3 12 0-21 -14 3 10 7 12 0-18 7 3 022 1 21 -5 3 24 0-5 3 -8 18 0-4 -8 -15 21 0-15 21 18 -8 3 0-1 -8 5 -13 18 14 0-4 3 14 -8 18 -13 014 15 18 -8 3 021 18 -8 3 0-14 7 3 0-20 -21 14 -8 7 07 3 0-8 3 14 0-11 14 -18 17 8 -7 0-1 8 -18 -7 14 0-19 21 23 1 -4 10 8 0-18 14 3 0-4 8 18 3 10 1 017 19 18 -7 -2 10 0-17 3 -2 14 6 06 10 14 3 1 01 14 3 10 013 8 14 -1 18 -7 010 14 3 0-13 -10 3 17 8 0-11 -16 8 17 18 2 017 14 3 014 3 0-2 17 -14 13 -7 0-17 3 0-4 -13 23 11 10 0-11 -14 17 -7 13 013 17 3 08 3 03 0-6 9 -12 18 08 -10 6 7 9 24 0-12 24 7 18 9 0-14 -10 7 9 24 0-23 -18 9 024 7 18 9 018 9 7 07 -21 -9 6 06 7 9 09 13 0-6 13 0-18 13 -7 0-16 7 -9 6 -20 0-7 13 0-20 13 08 13 013 0-18 -23 -8 14 0-8 -9 0-9 018 8 08 00