key: cord-0046593-l0x0dthn
authors: Brakensiek, Joshua; Heule, Marijn; Mackey, John; Narváez, David
title: The Resolution of Keller’s Conjecture
date: 2020-05-30
journal: Automated Reasoning
DOI: 10.1007/978-3-030-51074-9_4
sha: 80605483c0bc18a0864dc3a7490886b47cde50de
doc_id: 46593
cord_uid: l0x0dthn

We consider three graphs, [Formula: see text], [Formula: see text], and [Formula: see text], 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 [Formula: see text]. 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 [Formula: see text] contains a facesharing pair of cubes. Since a faceshare-free unit cube tiling of [Formula: see text] exists (which we also verify), this completely resolves Keller’s conjecture.

In 1930, Keller conjectured that any tiling of n-dimensional space by translates of the unit cube must contain a pair of cubes that share a complete (n − 1)dimensional face [13] . Figure 1 illustrates this for the plane and the 3-dimensional space. The conjecture generalized a 1907 conjecture of Minkowski [24] in which the centers of the cubes were assumed to form a lattice. Keller's conjecture was proven to be true for n ≤ 6 by Perron in 1940 [25, 26] , and in 1942 Hajós [6] showed Minkowski's conjecture to be true in all dimensions. In 1986 Szabó [28] reduced Keller's conjecture to the study of periodic tilings. Using this reduction Corrádi and Szabó [3] introduced the Keller graphs: the graph G n,s has vertices {0, 1, . . . , 2s − 1} n such that a pair are adjacent if and only if they differ by exactly s in at least one coordinate and they differ in at least two coordinates. The size of cliques in G n,s is at most 2 n [5] and the size of the largest clique in G n,s is at most the size of the largest clique in G n,s+1 .

A clique in G n,s of size 2 n demonstrates that Keller's conjecture is false for dimensions greater than or equal to n. Lagarias and Shor [19] showed that Keller's conjecture is false for n ≥ 10 in 1992 by exhibiting clique of size 2 10 in G 10, 2 . In 2002, Mackey [22] found a clique of size 2 8 in G 8, 2 to show that Keller's conjecture is false for n ≥ 8. In 2011, Debroni, Eblen, Langston, Myrvold, Shor, and Weerapurage [5] showed that the largest clique in G 7,2 has size 124.

In 2015, Kisielewicz and Lysakowska [14, 16] made substantial progress on reducing the conjecture in dimension 7. More recently, in 2017, Kisielewicz [15] reduced the conjecture in dimension 7 as follows: Keller's conjecture is true in dimension 7 if and only if there does not exist a clique in G 7,3 of size 2 7 [21] .

The main result of this paper is the following theorem.

Theorem 1. Neither G 7,3 nor G 7,4 nor G 7,6 contains a clique of size 2 7 = 128.

Although proving this property for G 7,3 suffices to prove Keller's conjecture true in dimension 7, we also show this for G 7,4 and G 7,6 to demonstrate that our methods need only depend on prior work of Kisielewicz and Lysakowska [14, 16] . In particular, the argument for G 7,6 [14] predates and is much simpler than the one for G 7,4 [16] (although the publication dates indicate otherwise). It is not explicitly stated in either that it suffices to prove that G 7,4 or G 7,6 lacks a clique of size 128 to prove Keller's conjecture. We show this in the Appendix of the extended version, available at https://arxiv.org/abs/1910.03740.

We present an approach based on satisfiability (SAT) solving to show the absence of a clique of size 128. SAT solving has become a powerful tool in computeraided mathematics in recent years. For example, it was used to prove the Erdős discrepancy conjecture with discrepancy 2 [17] , the Pythagorean triples problem [10] , and Schur number five [7] . Modern SAT solvers can also emit proofs of unsatisfiability. There exist formally verified checkers for such proofs as developed in the ACL2, Coq, and Isabelle theorem-proving systems [4, 20] .

The outline of this paper is as follows. After describing some background concepts in Sect. 2, we present a compact encoding whether G n,s contains a clique of size 2 n as a propositional formula in Sect. 3. Without symmetry breaking, these formulas with n > 5 are challenging for state-of-the-art tools. However, the Keller graphs contain many symmetries. We perform some initial symmetry breaking that is hard to express on the propositional level in Sect. 4. This allows us to partially fix three vertices. On top of that we add symmetry-breaking clauses in Sect. 5. The soundness of their addition has been mechanically verified. We prove in Sect. 6 the absence of a clique of size 128 in G 7,3 , G 7,4 and G 7,6 . We optimize the proofs of unsatisfiability obtained by the SAT solver and certify them using a formally verified checker. Finally we draw some conclusions in Sect. 7 and present directions for future research. 

We present the most important background concepts related to this paper and introduce some properties of G n,s . First, for positive integers k, we define two sets: [k] := {1, 2, . . . , k} and k := {0, 1, . . . , k − 1}.

Keller Graphs. The Keller graph G n,s consists of the vertices 2s n . Two vertices are adjacent if and only if they differ by exactly s in at least one coordinate and they differ in at least two coordinates. Figure 2 shows a visualization of G 2,2 . As noted in [5] , {sw + s n : w ∈ {0, 1} n } is a partition of the vertices of G n,s into 2 n independent sets. Consequently, any clique in G n,s has at most 2 n vertices. For example, V (G 2,2 ) is partitioned as follows:

We use the above observation for encoding whether G n,s has a clique of size 2 n . Instead of searching for such a clique on the graph representation of G n,s , which consists of (2s) n vertices, we search for 2 n vertices, one from each sw + s n , such that every pair is adjacent.

For every i ∈ 2 n , we let w(i) = (w 1 , w 2 , . . . , w n ) ∈ {0, 1} n be defined by i = n k=1 2 k−1 · w k . Given a clique of size 2 n , we let c i be its unique element in sw(i) + s n and we let c i,j be the jth coordinate of c i . Useful Automorphisms of Keller Graphs. Let S n be the set of permutations of [n] and let H s be the set of permutations of 2s generated by the swaps (i i + s) composed with any permutation of s which is identically applied to s + s . The maps

where σ ∈ S n and τ 1 , τ 2 , . . . , τ n ∈ H s are automorphisms of G n,s . Note that applying an automorphism to every vertex of a clique yields another clique of the same size.

Propositional Formulas. We consider formulas in conjunctive normal form (CNF), which are defined as follows. A literal is either a variable x (a positive literal ) or the negation x of a variable x (a negative literal ). The complement l of a literal l is defined as l = x if l = x and l = x if l = x. For a literal l, var (l) denotes the variable of l. A clause is a disjunction of literals and a formula is a conjunction of clauses.

An assignment is a function from a set of variables to the truth values 1 (true) and 0 (false). A literal l is satisfied by an assignment α if l is positive and α(var (l)) = 1 or if it is negative and α(var (l)) = 0. A literal is falsified by an assignment if its complement is satisfied by the assignment. A clause is satisfied by an assignment α if it contains a literal that is satisfied by α. A formula is satisfied by an assignment α if all its clauses are satisfied by α. A formula is satisfiable if there exists an assignment that satisfies it and unsatisfiable otherwise.

Clausal Proofs. Our proof that Keller's conjecture is true for dimension 7 is predominantly a clausal proof, including a large part of the symmetry breaking. Informally, a clausal proof system allows us to show the unsatisfiability of a CNF formula by continuously deriving more and more clauses until we obtain the empty clause. Thereby, the addition of a derived clause to the formula and all previously derived clauses must preserve satisfiability. As the empty clause is trivially unsatisfiable, a clausal proof shows the unsatisfiability of the original formula. Moreover, it must be checkable in polynomial time that each derivation step does preserve satisfiability. This requirement ensures that the correctness of proofs can be efficiently verified. In practice, this is achieved by allowing only the derivation of specific clauses that fulfill some efficiently checkable criterion.

Formally, clausal proof systems are based on the notion of clause redundancy. A clause C is redundant with respect to a formula F if adding C to F preserves satisfiability. Given a formula F = C 1 ∧ · · · ∧ C m , a clausal proof of F is a sequence (C m+1 , ω m+1 ), . . . , (C n , ω n ) of pairs where each C i is a clause, each ω i (called the witness) is a string, and C n is the empty clause [9] . Such a sequence gives rise to formulas F m , F m+1 , . . . , F n , where

and if this redundancy can be checked in polynomial time (with respect to the size of the proof) using the witness ω i .

An example for a clausal proof system is the resolution proof system, which only allows the derivation of resolvents (with no or empty witnesses). However, the resolution proof system does not allow to compactly express symmetry breaking. Instead we will construct a proof in the resolution asymmetric tautology (RAT) proof system. This proof system is also used to validate the results of the SAT competitions [11] . For the details of RAT, we refer to the original paper [9] . Here, we just note that (1) for RAT clauses, it can be checked efficiently that their addition preserves satisfiability, and (2) every resolvent is a RAT clause but not vice versa.

Recall that G n,s has a clique of size 2 n if and only if there exist vertices c i ∈ sw(i)+ s n for all i ∈ 2 n such that for all i = i there exists at least two j ∈ [n] such that c i,j = c i ,j and there exists at least one j ∈ [n] such that c i,j = c i ,j ± s.

Our CNF will encode the coordinates of the c i . For each i ∈ 2 n , j ∈ [n], k ∈ s , we define Boolean variables x i,j,k which are true if and only if c i,j = sw(i) j + k. We therefore need to encode that exactly one of

(1)

Next we enforce that every pair of vertices c i and c i in the clique differ in at least two coordinates. For most pairs of vertices, no clauses are required because w(i) and w(i ) differ in at least two positions. Hence, a constraint is only required for two vertices if w(i) and w(i ) differ in exactly one coordinate.

Let ⊕ be the binary XOR operator and e j be the indicator vector of the jth coordinate. If w(i) ⊕ w(i ) = e j , then in order to ensure that c i and c i differ in at least two coordinates we need to make sure that there is some coordinate

We use the Plaisted-Greenbaum [27] encoding to convert the above constraint into CNF. We refer to the auxiliary variables introduced by the encoding as y i,i ,j ,k , which if true imply x i,j ,k = x i ,j ,k , or written as an implication

The following two clauses express this implication

Notice that the implication is only in one direction as Plaisted-Greenbaum takes the polarity of constraints into account. The clauses that represent the other direction, i.e., (

are redundant (and more specifically, they are blocked [18] ).

Using the auxiliary variables, we can express the constraint (2) using clauses of length s · (n − 1)

The last part of the encoding consists of clauses to ensure that each pair of vertices in the clique have at least one coordinate in which they differ by exactly

We use auxiliary variables z i,i ,j , whose truth implies c i,j = c i ,j ± s, or written as an implication

Notice that the implication is again in one direction only. Below we enforce that some z i,i ,j variables must be true, but there are no constraints that enforce z i,i ,j variables to be false.

This can be written as a CNF using the following clauses:

Finally, to make sure that c i,j = c i ,j ± s for some j ∈ [n], we specify

The variables and clauses, including precise formulas for their counts, are summarized in Table 1 . The sizes of the CNF encodings (before the addition of symmetry breaking clauses) of G 7,3 , G 7,4 , and G 7,6 are listed in Table 2 . Notice that for fixed n, the dependence on s is quadratic, which is better than the s 2n dependence one would get in the naive encoding of G n,s as a graph. This compact encoding, when combined with symmetry breaking, is a core reason that we were able to prove Theorem 1.

The instances with n = 7 are too hard for state-of-the-art SAT solvers if no symmetry breaking is applied. We experimented with general-purpose symmetry-breaking techniques, similar to the symmetry-breaking predicates produced by shatter [1] . This allows solving the formula for G 7,3 , but the computation takes a few CPU years. The formulas for G 7,4 and G 7,6 with these symmetry-breaking predicates are significantly harder.

Instead we employ problem-specific symmetry breaking by making use of the observations in Sects. 4 and 5. This allows solving the clique of size 2 n existence problem for all three graphs in reasonable time. 

Our goal is to prove that there exists no clique of size 128 in G 7,s for s ∈ {3, 4, 6}.

In this section, and the subsequent, we assume that such a clique exists and adapt some of the arguments of Perron [25, 26] to show that it may be assumed to have a canonical form. We will use i to denote an element in i . Every pair of vertices in K <s differs by exactly s in at least one coordinate, because the corresponding pair of vertices in K can't differ by exactly s in the first coordinate. Similarly, every pair of vertices in K ≥s differs by exactly s in at least one coordinate. Although K <s and K ≥s are not necessarily cliques in G 6,s , they satisfy the first condition of the adjacency requirement. The partition of Sect. 2 can thus be applied to deduce that |K <s | ≤ 64 and |K ≥s | ≤ 64. Since |K <s | + |K ≥s | = 128, we conclude that |K <s | = 64 and |K ≥s | = 64.

By the truth of Keller's conjecture in dimension 6, K <s is not a clique in G 6,s . Thus, some pair of vertices in K <s are identical in five of the six coordinates. After application of an automorphism, we may without loss of generality assume that this pair is (s, 0, 0, 0, 0, 0) and (0, 0, 0, 0, 0, 0). Since the pair comes from K <s , there exist v 1 = v 1 ∈ s such that (v 1 , s, 0, 0, 0, 0, 0) and (v 1 , 0, 0, 0, 0, 0, 0) are in the clique. After application of an automorphism that moves v 1 to 1 and v 1 to 0, we deduce that without loss of generality (1, s, 0, 0, 0, 0, 0) and (0, 0, 0, 0, 0, 0, 0) are in the clique. Application of the automorphism that interchanges the first two coordinates yields a clique of size 128 containing the vertices c 0 = (0, 0, 0, 0, 0, 0, 0) and c 1 = (s, 1, 0, 0, 0, 0, 0).

If there is a clique of size 128 in G 7,s , then there is a clique of size 128 in G 7,s containing the vertices (0, 0, 0, 0, 0, 0, 0), (s, 1, 0, 0, 0, 0, 0), and (s, s + 1, 2 , 2 , 1, 1, 1).

Proof. Using the preceding lemma, we can choose from among all cliques of size 128 that contain c 0 = (0, 0, 0, 0, 0, 0, 0) and c 1 = (s, 1, 0, 0, 0, 0, 0), one in which c 3 has the fewest number of coordinates equal to 0. Let λ be this least number.

Observe that the first two coordinates of c 3 must be (s, s + 1) in order for it to be adjacent with both c 0 and c 1 . Thus, we have

In the above, we can apply automorphisms that fix 0 in the last five coordinates to replace s by 2 . We can apply an automorphism that permutes the last five coordinates to assume that the 0's and 1's in c 3 are sorted in increasing order. Notice that not all of the 2 coordinates in c 3 can be 0, because c 1 and c 3 are adjacent and must therefore differ in at least two coordinates. Hence at least the last coordinate of c 3 is 1.

Case 1) λ = 4. In this case c 3 = (s, s + 1, 0, 0, 0, 0, 1). In order for c 67 to be adjacent with c 0 , c 1 , and c 3 , it must start with (s, s + 1) and end with s + 1:

Not all s elements in c 67 can be 0, because c 3 and c 67 differ in at least two coordinates. However, if one of the s elements in c 67 is nonzero, then we can swap 1 and s + 1 in the last coordinate to obtain a clique in which c 3 has three or fewer coordinates equal to 0, contradicting λ = 4. Thus, λ ≤ 3.

Case 2) λ = 3, in which case c 3 = (s, s + 1, 0, 0, 0, 1, 1): s + 1 , 0 , 0 , 0 , 1 , 1 Since c 67 is adjacent with c 0 , c 1 , and c 3 , it must start with (s, s + 1) and end with s + 1. Similarly, since c 35 is adjacent with c 0 , c 1 , and c 3 , it must start with (s, s + 1) and have s + 1 as its penultimate coordinate. Since c 35 and c 67 are adjacent, either the last coordinate of c 35 must be 1, or the penultimate coordinate of c 67 must be 1. Without loss of generality we can assume that the penultimate coordinate of c 67 is 1 as we can permute the last two coordinates which would swap c 35 and c 67 without involving the other cubes. The remaining three s elements in c 67 cannot all be 0, since c 3 and c 67 differ in at least two coordinates. However, if one of the s elements is non-zero, then we can swap 1 and s + 1 in the last coordinate to obtain a clique in which c 3 has two or fewer coordinates equal to 0, contradicting λ = 3. Thus, we have λ ≤ 2 and c 3 = (s, s + 1, 2 , 2 , 1, 1, 1), as desired.

Notice that most of the symmetry breaking discussed in this section is challenging, if not impossible, to break on the propositional level: The proof of Lemma 1 uses the argument that Keller's conjecture holds for dimension 6, while the proof of Theorem 2 uses the interchangeability of 1 and s + 1, which is not a symmetry on the propositional level. We will break these symmetries by adding some unit clauses to the encoding. All additional symmetry breaking will be presented in the next section and will be checked mechanically.

Our symmetry-breaking approach starts with enforcing the initial symmetry breaking: We assume that vertices c 0 = (0, 0, 0, 0, 0, 0, 0), c 1 = (s, 1, 0, 0, 0, 0, 0) and c 3 = (s, s + 1, s , s , 1, 1, 1) are in our clique K, which follows from Theorem 2. We will not use the observation that s occurrences in c 3 can be reduced to 2 and instead add and validate clauses that realize this reduction.

We fix the above initial vertices by adding unit clauses to the CNF encoding. This is the only part of the symmetry breaking that is not checked mechanically. Let Φ 7,s be the formula obtained from our encoding in Sect. 3 together with the unit clauses corresponding to the 19 coordinates fixed among c 0 , c 1 and c 3 . In this section we will identify several symmetries in Φ 7,s that can be further broken at the CNF level by adding symmetry breaking clauses. The formula ultimately used in Sect. 6 for the experiments is the result of adding these symmetry breaking clauses to Φ 7,s . Symmetry breaking clauses are added in an incremental fashion. For each addition, a clausal proof of its validity with respect to Φ 7,s and the clauses added so far is generated, as well. Each of these clausal proofs has been validated using the drat-trim proof checker.

Our approach can be described in general terms as identifying groups of coordinates whose assignments exhibit interesting symmetries and calculating the equivalence classes of these assignments. Given a class of symmetric assignments, it holds that one of these assignments can be extended to a clique of size 128 if and only if every assignment in that class can be extended as well. It is then enough to pick a canonical representative for each class, add clauses forbidding every assignment that is not canonical, and finally determine the satisfiability of the formula under the canonical representative of every class of assignments: if no canonical assignment can be extended to a satisfying assignment for the formula, then the formula is unsatisfiable. In order to forbid assignments that are not canonical, we use an approach similar to the one described in [8] . Coordinates of c 19 , c 35 and c 67 The reasoning in the proof of Theorem 2 leads to the following forced settings, once we assign c 3 = (s, s + 1, s , s , 1, 1, 1) and apply unit propagation: 19, 7 to not be 1. By the inclusion-exclusion principle, this reasoning alone discards 3(s − 1) 2 s 4 − 3(s − 1) 4 s 2 + (s − 1) 6 cases. All of these cases can be blocked by adding the binary clauses: (x 19,6,1 ∨ x 35,5,1 ) ∧ (x 35,7,1 ∨ x 67,6,1 ) ∧ (x 67,5,1 ∨ x 19,7,1 ). These three clauses are RAT clauses [12] with respect to the formula Φ 7,s . Furthermore, among the remaining (2s − 1) 3 cases, several assignment pairs are symmetric. For example, the following two assignments are symmetric because one can be obtained from the other by swapping columns and rows: As with many problems related to symmetries, we can encode each assignment as a vertex-colored graph and use canonical labeling algorithms to determine a canonical assignment representing all the symmetric assignments of each equivalence class, and which assignments are symmetric to each canonical form. Our approach is similar to the one by McKay and Piperno for isotopy of matrices [23] .

This additional symmetry breaking reduces the number of cases for the last three coordinates of the vertices c 19 , c 37 , and c 67 from the trivial s 6 to 25 cases for s = 3 and 28 cases for s ≥ 4. Figure 3 shows the 25 canonical cases for s = 3. (0, 0, 1, 0, 1, 1) (0, 0, 1, 1, 1, 1) (0, 0, 1, 1, 1, 2) (0, 1, 1, 0, 0, 1) (0, 1, 1, 0, 1, 1)  (0, 1, 1, 0, 2, 1) (0, 1, 1, 1, 0, 2) (0, 1, 1, 1, 1, 0) (0, 1, 1, 1, 1, 1) (0, 1, 1, 1, 1, 2)  (0, 1, 1, 1, 2, 0) (0, 1, 1, 1, 2, 1) (0, 1, 1, 1, 2, 2) (0, 1, 1, 2, 1, 1) (0, 1, 1, 2, 2, 1)  (0, 2, 1, 1, 1, 1) (0, 2, 1, 1, 1, 2) (0, 2, 1, 2, 1, 1) (1, 1, 1, 1, 1, 1) (1, 1, 1, 1, 1, 2)  (1, 1, 1, 1, 2, 2) (1, 1, 1, 2, 2, 1) (1, 1, 2, 1, 2, 1) (1, 1, 2, 1, 2, 2) (1, 2, 2, 1, 1, 2)   Fig. 3 . The 25 canonical cases for s = 3. Each vector corresponds to the values of the coordinates (c19,6, c19,7, c35,5, c35,7, c67,5, c67,6 ). c 3 , c 19 , c 35 and c 67 The symmetry breaking in the previous subsection allows us to fix, without loss of generality, the last coordinate of c 19 to 1. It also constrains the third and fourth coordinates of c 3 to take values in 2 instead of s .

We break the computation into further cases by enumerating over choices for the third and fourth coordinates of vertices c 3 , c 19 , c 37 , and c 67 (Fig. 4) . Up to this point, our description of the partial clique is invariant under the permutations of s − 1 in the third and fourth coordinates as well as swapping the third and fourth coordinates. With respect to these automorphisms, for s = 3 there are only 861 equivalence classes for how to fill in the s cases for these four vertices. 

In initial experiments we observed for each s ∈ {3, 4, 6} that out of the many thousands of subformulas (cases), one subformula was significantly harder to solve compared to the other subformulas. Figure 5 shows the coordinates of the key vertices of this subformula for s ∈ {3, 4, 6}. Notice that the third and fourth coordinates are all 0 for all the key vertices. We therefore applied additional symmetry breaking in case all of these coordinates are 0. Under this case, the third and the fourth coordinates of vertex c 2 can be restricted to (0, 0), (0, 1), 1 , 0 , 0 , 0 , 0 , 0 (0, 0, 0, 0, 0, 0, 0) (3, 1, 0, 0, 0, 0, 0) (3, 4, 0, 0, 1, 1, 1) (3, 4, 0, 0, 4, 0, 1) (3, 4, 0, 0, 1, 4, 0) (3, 4, 0, 0, 0, 1, 4) (0, 0, 0, 0, 0, 0, 0) (4, 1, 0, 0, 0, 0, 0) (4, 5, 0, 0, 1, 1, 1) (4, 5, 0, 0, 5, 0, 1) (4, 5, 0, 0, 1, 5, 0) (4, 5, 0, 0, 0, 1, 5) (0, 0, 0, 0, 0, 0, 0) (6, 1, 0, 0, 0, 0, 0) (6, 7, 0, 0, 1, 1, 1) (6, 7, 0, 0, 7, 0, 1) (6, 7, 0, 0, 1, 7, 0) (6, 7, 0, 0, 0, 1, 7) and (1, 1), and the last three coordinates of c 2 can only take values in 3 . Furthermore, any assignment (a, b, c) to the last three coordinates of c 2 is symmetric to the same assignment "shifted right", i.e. (c, a, b) , by swapping columns and rows appropriately. These symmetries define equivalence classes of assignments that can also be broken at the CNF level. Under the case shown in Fig. 5 , there are only 33 non-isomorphic assignments remaining for vertex c 2 for s ≥ 3. We replace the hard case for each s ∈ {3, 4, 6} by the corresponding 33 cases, thereby increasing the total number of cases mentioned above by 32.

Each of the cases was solved using a SAT solver, which produced a proof of unsatisfiability that was validated using a formally verified checker (details are described in the following section). To ensure that the combined cases cover the entire search space, we constructed for each s ∈ {3, 4, 6} a tautological formula in disjunctive normal form (DNF). The building blocks of a DNF are conjuctions of literals known as cube. We will use α as a symbol for cubes as they can also be considered variable assignments. For each cube α in the DNF, we prove that the formula after symmetry breaking under α is unsatisfiable. Additionally, we mechanically check that the three DNFs are indeed tautologies.

We used the CaDiCaL 1 SAT solver developed by Biere [2] and ran the simulations on a cluster of Xeon E5-2690 processors with 24 cores per node. CaDiCaL supports proof logging in the DRAT format. We used DRAT-trim [29] to optimize the emitted proof of unsatisfiability. Afterwards we certified the optimized proofs with ACL2check, a formally verified checker [4] . All of the code that we used is publicly available on GitHub. 2 We have also made the logs of the computation publicly available on Zenodo. Table 3 summarizes the running times are for experiment. The subformulasolving runtimes for s = 3, 4 and 6 are summarized in cactus plots in Figs. 6, 7 and 8. The combined size of all unsatisfiability proofs of the subformulas of s = 6 is 224 gigabyte in the binary DRAT proof format. These proofs contained together 6.18 · 10 9 proof steps (i.e., additions of redundant clauses). The DRATtrim proof checker only used 6.39 · 10 8 proof steps to validate the unsatisfiability of all subformulas. In other words, almost 90% of the clauses generated by CaD-iCaL are not required to show unsatisfiability. It is therefore likely that a single DRAT proof for the formula after symmetry breaking can be constructed that is about 20 gigabytes in size. That is significantly smaller compared to other recently solved problems in mathematics that used SAT solvers [7, 10] . We ran all three experiments simultaneously on 20 nodes on the Lonestar 5 cluster and computing on 24 CPUs per node in parallel. All instances were reported unsatisfiable and all proofs of unsatisfiability were certified by the formally verified checker. This proves Theorem 1.

To check the accuracy of the CNF encoding, we verified that the generated formulas for G 8,2 , G 8,3 , G 8,4 and G 8,6 are satisfiable -thereby confirming that Keller's conjecture is false for dimension 8. These instances, by themselves, have too many degrees of freedom for the solver to finish. Instead, we added to the CNF the unit clauses consistent with the original clique found in the paper of Mackey [22] (as suitably embedded for the larger graphs). Specification of the vertices was per the method in Sect. 3 and 4. These experiments were run on Stanford's Sherlock cluster and took less than a second to confirm satisfiability. Figure 9 shows an illustration of a clique of size 256 in G 8,2 . This is the smallest counterexample for Keller's conjecture, both in the dimension (n = 8) as in the number of coordinates (s = 2). The illustration uses a black circle, black square, white circle, or white square to represent a coordinate set to 0, 1, 2, or 3, respectively. Notice that for each pair of vertices it holds that they have a complementary (black vs white) circle or square and at least one other different coordinate (black/white or circle/square or both). 

In this paper, we analyzed maximal cliques in the graphs G 7,3 , G 7,4 , and G 7,6 by combining symmetry-breaking and SAT-solving techniques. For the initial symmetry breaking we adapt some of the arguments of Perron. Additional symmetry breaking is performed on the propositional level and this part is mechanically verified. We partitioned the resulting formulas into thousands of subformulas and used a SAT solver to check that each subformula cannot be extended to a clique of size 128. Additionally, we optimized and certified the resulting proofs of unsatisfiability. As a result, we proved Theorem 1, which resolves Keller's conjecture in dimension 7.

In the future, we hope to construct a formally verified argument for Keller's conjecture, starting with a formalization of Keller's conjecture down to the relation of the existence of cliques of size 2 n in Keller graphs and finally the correctness of the presented encoding. This effort would likely involve formally verifying most of the theory discussed in the Appendix of the extended version of the paper. On top of that, we would like to construct a single proof of unsatisfiability that incorporates all the clausal symmetry breaking and the proof of unsatisfiability of all the subformulas and validate this proof using a formally verified checker.

Furthermore, we would like to extend the analysis to G 7,s , including computing the size of the largest cliques for various values of s. Another direction to consider is to study the maximal cliques in G 8,s in order to have some sort of classification of all maximal cliques. Fig. 9 . Illustration of a clique of 256 vertices in G8,2. Each "dice" with eight dots represents a vertex, and each dot represents a coordinate. A black circle, black square, white circle, and white square represent a coordinate set to 0, 1, 2, and 3, respectively.

Shatter: efficient symmetry-breaking for Boolean satisfiability

CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT

A combinatorial approach for Keller's conjecture

Efficient certified RAT verification

A complete resolution of the Keller maximum clique problem

Uber einfache und mehrfache Bedeckung des n-dimensionalen Raumes mit einen Wurfelgitter

Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018)

Expressing symmetry breaking in DRAT proofs

Short proofs without new variables

Solving and verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer

What's hot in the SAT and ASP competition

Inprocessing rules

Über die lückenlose Erfüllung des Raumes mit Würfeln

Rigid polyboxes and Keller's conjecture

Towards resolving Keller's cube tiling conjecture in dimension seven

On Keller's conjecture in dimension seven. Electron

Computer-aided proof of Erdős discrepancy properties

On a generalization of extended resolution

Keller's cube-tiling conjecture is false in high dimensions

Efficient verified (UN)SAT certificate checking

Extended Keller graph and its properties

A cube tiling of dimension eight with no facesharing

Nauty and Traces User' Guide (version 2.6)

Über lückenlose ausfüllung desn-dimensionalen raumes durch kongruente würfel

Über lückenlose ausfüllung desn-dimensionalen raumes durch kongruente würfel. ii

A structure-preserving clause form translation

A reduction of Keller's conjecture

DRAT-trim: efficient checking and trimming using expressive clausal proofs

Acknowledgments. The authors acknowledge the Texas Advanced Computing Center (TACC) at The University of Texas at Austin, RIT Research Computing, and the Stanford Research Computing Center for providing HPC resources that have contributed to the research results reported within this paper. Joshua is supported by an NSF graduate research fellowship. Marijn and David are supported by NSF grant CCF-1813993. We thank Andrzej Kisielewicz and Jasmin Blanchette for valuable comments on an earlier version of the manuscript. We thank William Cooperman for helpful discussions on a previous attempt at programming simulations to study the half-integral case. We thank Alex Ozdemir for helpful feedback on both the paper and the codebase. We thank Xinyu Wu for making this collaboration possible.