# The Resolution of Keller’s Conjecture

- 189 Downloads

## Abstract

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.

## 1 Introduction

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 \le 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,\ldots , 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 \ge 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 \ge 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 Łysakowska [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 Łysakowska [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 computer-aided 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].

## 2 Preliminaries

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,\ldots ,k\}\) and \(\langle k\rangle := \{0,1,\ldots , k-1\}\).

*Keller Graphs.* The Keller graph \(G_{n,s}\) consists of the vertices \(\langle 2s\rangle ^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}\).

For every \(i \in \langle 2^n\rangle \), we let \(w(i) = (w_1, w_2,\dots , w_n) \in \{0,1\}^n\) be defined by \(i=\sum _{k=1}^n2^{k-1}\cdot w_k\). Given a clique of size \(2^n\), we let \(c_i\) be its unique element in \(s w(i) + \langle s\rangle ^n\) and we let \(c_{i,j}\) be the *j*th 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 \(\langle 2s\rangle \) generated by the swaps \((i\ i+s)\) composed with any permutation of \(\langle s\rangle \) which is identically applied to \(s + \langle s \rangle \). The maps

*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 \(\overline{x}\) of a variable *x* (a *negative literal*). The *complement* \(\overline{l}\) of a literal *l* is defined as \(\overline{l} = \overline{x}\) if \(l = x\) and \(\overline{l} = x\) if \(l = \overline{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 \(\alpha \) if *l* is positive and \(\alpha ( var (l)) = 1\) or if it is negative and \(\alpha ( 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 \(\alpha \) if it contains a literal that is satisfied by \(\alpha \). A formula is satisfied by an assignment \(\alpha \) if all its clauses are satisfied by \(\alpha \). 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 \wedge \dots \wedge C_m\), a *clausal proof* of *F* is a sequence \((C_{m+1},\omega _{m+1}), \dots , (C_n, \omega _n)\) of pairs where each \(C_i\) is a clause, each \(\omega _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}, \dots , F_n\), where \(F_i = C_1 \wedge \dots \wedge C_i\). A clausal proof is *correct* if every clause \(C_i\) (\(i > m\)) is redundant with respect to \(F_{i-1}\), and if this redundancy can be checked in polynomial time (with respect to the size of the proof) using the witness \(\omega _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.

## 3 Clique Existence Encoding

Recall that \(G_{n, s}\) has a clique of size \(2^n\) if and only if there exist vertices \(c_i \in sw(i) + \langle s \rangle ^n\) for all \(i \in \langle 2^n \rangle \) such that for all \(i \ne i'\) there exists at least two \(j \in [n]\) such that \(c_{i,j} \ne c_{i',j}\) and there exists at least one \(j \in [n]\) such that \(c_{i,j} = c_{i',j} \pm s\).

*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.

*j*th coordinate. If \(w(i) \oplus 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 \(j' \ne j\) for which \(c_{i,j'} \ne c_{i',j'}\)

*s*. Observe that \(c_{i,j} = c_{i',j} \pm s\) implies that \(c_{i,j} \ne c_{i',j}\) and \(x_{i,j,k} = x_{i',j,k}\) for all \(k \in \langle s \rangle \). We use auxiliary variables \(z_{i, i', j}\), whose truth implies \(c_{i,j} = c_{i',j} \pm s\), or written as an implication

*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.

Summary of variable and clause counts in the CNF encoding.

Clauses | New Variable Count | Clause Count |
---|---|---|

(1) | \(2^n \cdot n \cdot s\) | \(2^n \cdot n \cdot (1 + \left( {\begin{array}{c}s\\ 2\end{array}}\right) )\) |

(3) | \(2^{n-1}\cdot n\cdot s\cdot (n-1)\) | \(2^n\cdot n\cdot s\cdot (n-1)\) |

(4) | \(2^{n-1}\cdot n\) | |

(5) | \(2^{2n-2}\cdot n\) | \(2^{2n-1} \cdot n \cdot s\) |

(6) | \(\left( {\begin{array}{c}2^n\\ 2\end{array}}\right) \) | |

Total | \(2^{n-1}\cdot n\cdot (s(n+1) + 2^{n-1})\) | \(2^n\cdot n\cdot \left( \frac{3}{2} + \left( {\begin{array}{c}s\\ 2\end{array}}\right) + n\cdot s - s\right) + 2^{2n-1}n s + \left( {\begin{array}{c}2^n\\ 2\end{array}}\right) \) |

Summary of variable and clause counts of the CNF encoding for \(G_{7,3}\), \(G_{7,4}\), and \(G_{7, 6}\). These counts do not include the clauses introduced by the symmetry breaking.

Keller Graph | Variable Count | Clause Count |
---|---|---|

\(G_{7,3}\) | \(39\,424\) | \(200\,320\) |

\(G_{7,4}\) | \(43\,008\) | \(265\,728\) |

\(G_{7,6}\) | \(50\,176\) | \(399\,232\) |

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.

## 4 Initial Symmetry Breaking

Our goal is to prove that there exists no clique of size 128 in \(G_{7,s}\) for \(s \in \{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 \(\star _i\) to denote an element in \(\langle i \rangle \).

### Lemma 1

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) and (*s*, 1, 0, 0, 0, 0, 0).

### Proof

*K*be a clique of size 128 in \(G_{7,s}\). Consider the following sets of vertices in \(G_{6,s}\):

*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_{\ge s}\) differs by exactly

*s*in at least one coordinate. Although \(K_{<s}\) and \(K_{\ge 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}| \le 64\) and \(|K_{\ge s}| \le 64\). Since \(|K_{<s}| + |K_{\ge s}| = 128\), we conclude that \(|K_{<s}| = 64\) and \(|K_{\ge 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 \ne v'_1 \in \langle s\rangle \) 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)\). \(\square \)

### Theorem 2

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, \star _2, \star _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 \(\lambda \) be this least number.

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.

## 5 Clausal Symmetry Breaking

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,\star _s,\star _s,1,1,1)\) are in our clique *K*, which follows from Theorem 2. We will not use the observation that \(\star _s\) occurrences in \(c_3\) can be reduced to \(\star _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 \(\varPhi _{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 \(\varPhi _{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 \(\varPhi _{7,s}\). Symmetry breaking clauses are added in an incremental fashion. For each addition, a clausal proof of its validity with respect to \(\varPhi _{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].

### 5.1 The Last Three Coordinates of \(c_{19}\), \(c_{35}\) and \(c_{67}\)

\((c_{19,1},c_{19,2},c_{19,5})=(s,s+1,s+1)\),

\((c_{35,1},c_{35,2},c_{35,6})=(s,s+1,s+1)\),

\((c_{67,1},c_{67,2},c_{67,7})=(s,s+1,s+1)\).

*s*are positions 5 and 6, and since \(c_{19,5}\) and \(c_{35,6}\) are already set to \(s+1\), at least one of \(c_{19,6}\) and \(c_{35,5}\) has to be set to 1. Similarly, it is not possible for both \(c_{35,7}\) and \(c_{67,6}\) to not be 1 and for both \(c_{67,5}\) and \(c_{19,7}\) to not be 1. By the inclusion-exclusion principle, this reasoning alone discards \(3(s-1)^2s^4-3(s-1)^4s^2+(s-1)^6\) cases. All of these cases can be blocked by adding the binary clauses: \((x_{19,6,1}\vee x_{35,5,1}) \wedge (x_{35,7,1}\vee x_{67,6,1}) \wedge (x_{67,5,1}\vee x_{19,7,1})\). These three clauses are RAT clauses [12] with respect to the formula \(\varPhi _{7,s}\).

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\ge 4\). Figure 3 shows the 25 canonical cases for \(s=3\).

### 5.2 Coordinates Three and Four of Vertices \(c_3\), \(c_{19}\), \(c_{35}\) and \(c_{67}\)

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 \(\langle s-1 \rangle \) 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 \(\star _s\) cases for these four vertices. For \(s=4\) there are 1326 such equivalence classes, and for \(s=6\) there are \(1378 \) such equivalence classes. This gives a total of \(25 \times 861 = 21\,525\) cases to check for \(s = 3\), \(28 \times 1326 = 37\,128\) cases to check for \(s = 4\), and \(28 \times 1378 = 38\,584\) cases to check for \(s=6\).

### 5.3 Identifying Hardest Cases

*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 \ge 3\). We replace the hard case for each \(s\in \{3,4,6\}\) by the corresponding 33 cases, thereby increasing the total number of cases mentioned above by 32.

### 5.4 SAT Solving

## 6 Experiments

^{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.

^{3}

Summary of solve times for \(s = 3, 4, 6\). Times without a unit are in CPU hours. “No. Hard” is the number of subformulas which required more than 900 seconds to solve. “Hardest” is the solve time of the hardest subformula in CPU hours.

| Tot. Solve | Avg. Solve | Proof Opt. | Proof Cert. | No. Hard | Hardest |
---|---|---|---|---|---|---|

3 | 43.27 | 7.23 s | 22.46 | 4.98 | 28 form. | \({\approx }\,\,1.2\) |

4 | 77.00 | 7.46 s | 44.00 | 9.70 | 62 form. | \({\approx }\,\,2.7\) |

6 | 81.85 | 7.63 s | 34.84 | 14.53 | 63 form. | \({\approx }\,\,1.25\) |

### 6.1 Results for Dimension 7

Table 3 summarizes the running times are for experiment. The subformula-solving 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 \cdot 10^9\) proof steps (i.e., additions of redundant clauses). The DRAT-trim proof checker only used \(6.39 \cdot 10^8\) proof steps to validate the unsatisfiability of all subformulas. In other words, almost \(90\%\) of the clauses generated by CaDiCaL 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].

### 6.2 Refuting Keller’s Conjecture in Dimension 8

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.

## 7 Conclusions and Future Work

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.

## Footnotes

- 1.
Commit 92d72896c49b30ad2d50c8e1061ca0681cd23e60 of https://github.com/arminbiere/cadical.

- 2.
- 3.

## Notes

### 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.

## References

- 1.Aloul, F.A., Markov, I.L., Sakallah, K.A.: Shatter: efficient symmetry-breaking for Boolean satisfiability. In: Proceedings of the 40th Annual Design Automation Conference, DAC 2003, pp. 836–839. ACM, Anaheim (2003)Google Scholar
- 2.Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT competition 2018. In: Proceedings of SAT Competition 2018 – Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2018-1, pp. 13–14. University of Helsinki (2018)Google Scholar
- 3.Corrádi, K., Szabó, S.: A combinatorial approach for Keller’s conjecture. Period. Math. Hungar.
**21**, 91–100 (1990)MathSciNetCrossRefGoogle Scholar - 4.Cruz-Filipe, L., Heule, M.J.H., Hunt Jr., W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 26. LNCS (LNAI), vol. 10395, pp. 220–236. Springer, Cham (2017)CrossRefGoogle Scholar
- 5.Debroni, J., Eblen, J., Langston, M., Myrvold, W., Shor, P.W., Weerapurage, D.: A complete resolution of the Keller maximum clique problem. In: Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 129–135. SIAM, Society for Industrial and Applied Mathematics, Philadelphia (2011)Google Scholar
- 6.Hajós, G.: Uber einfache und mehrfache Bedeckung des n-dimensionalen Raumes mit einen Wurfelgitter. Math. Z.
**47**, 427–467 (1942)MathSciNetCrossRefGoogle Scholar - 7.Heule, M.J.H.: Schur number five. In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), pp. 6598–6606. AAAI Press (2018)Google Scholar
- 8.Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 591–606. Springer, Cham (2015)CrossRefGoogle Scholar
- 9.Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: de Moura, L. (ed.) CADE 26. LNCS (LNAI), vol. 10395, pp. 130–147. Springer, Cham (2017)CrossRefGoogle Scholar
- 10.Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228–245. Springer, Cham (2016)CrossRefGoogle Scholar
- 11.Heule, M.J.H., Schaub, T.: What’s hot in the SAT and ASP competition. In: Twenty-Ninth AAAI Conference on Artificial Intelligence 2015, pp. 4322–4323. AAAI Press (2015)Google Scholar
- 12.Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355–370. Springer, Heidelberg (2012)CrossRefGoogle Scholar
- 13.Keller, O.H.: Über die lückenlose Erfüllung des Raumes mit Würfeln. Journal für die reine und angewandte Mathematik
**163**, 231–248 (1930)MathSciNetzbMATHGoogle Scholar - 14.Kisielewicz, A.P.: Rigid polyboxes and Keller’s conjecture. Adv. Geom.
**17**(2), 203–230 (2017)MathSciNetCrossRefGoogle Scholar - 15.Kisielewicz, A.P.: Towards resolving Keller’s cube tiling conjecture in dimension seven. arXiv preprint arXiv:1701.07155 (2017)
- 16.Kisielewicz, A.P., Łysakowska, M.: On Keller’s conjecture in dimension seven. Electron. J. Comb.
**22**(1), P1–16 (2015)Google Scholar - 17.Konev, B., Lisitsa, A.: Computer-aided proof of Erdős discrepancy properties. Artif. Intell.
**224**(C), 103–118 (2015)CrossRefGoogle Scholar - 18.Kullmann, O.: On a generalization of extended resolution. Discret. Appl. Math.
**96–97**, 149–176 (1999)MathSciNetCrossRefGoogle Scholar - 19.Lagarias, J.C., Shor, P.W.: Keller’s cube-tiling conjecture is false in high dimensions. Bull. Am. Math. Soc.
**27**(2), 279–283 (1992)MathSciNetCrossRefGoogle Scholar - 20.Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura, L. (ed.) CADE 26. LNCS (LNAI), vol. 10395, pp. 237–254. Springer, Cham (2017)CrossRefGoogle Scholar
- 21.Łysakowska, M.: Extended Keller graph and its properties. Quaestiones Mathematicae
**42**(4), 551–560 (2019)MathSciNetCrossRefGoogle Scholar - 22.Mackey, J.: A cube tiling of dimension eight with no facesharing. Discret. Comput. Geom.
**28**(2), 275–279 (2002)MathSciNetCrossRefGoogle Scholar - 23.McKay, B.D., Piperno, A.: Nauty and Traces User’ Guide (version 2.6). http://users.cecs.anu.edu.au/~bdm/nauty/nug26.pdf
- 24.Minkowski, H.: Diophantische Approximationen. B.G. Teubner, Leipzig (1907)CrossRefGoogle Scholar
- 25.Perron, O.: Über lückenlose ausfüllung desn-dimensionalen raumes durch kongruente würfel. Math. Z.
**46**(1), 1–26 (1940)MathSciNetCrossRefGoogle Scholar - 26.Perron, O.: Über lückenlose ausfüllung desn-dimensionalen raumes durch kongruente würfel. ii. Math. Z.
**46**(1), 161–180 (1940)MathSciNetCrossRefGoogle Scholar - 27.Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput.
**2**(3), 293–304 (1986)MathSciNetCrossRefGoogle Scholar - 28.Szabó, S.: A reduction of Keller’s conjecture. Period. Math. Hung.
**17**(4), 265–277 (1986)MathSciNetCrossRefGoogle Scholar - 29.Wetzler, N.D., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014) CrossRefGoogle Scholar