Skip to main content
main-content
Top

Hint

Swipe to navigate through the articles of this issue

Published in: Journal of Automated Reasoning 3/2022

06-05-2022

The Resolution of Keller’s Conjecture

Authors: Joshua Brakensiek, Marijn Heule, John Mackey, David Narváez

Published in: Journal of Automated Reasoning | Issue 3/2022

Login to get access
share
SHARE

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.
Appendix
Available only for authorised users
Footnotes
1
Commit 92d72896c49b30ad2d50c8e1061ca0681cd23e60 of
 
4
This is a (ultimately equivalent) variant of a definition of Kisielewicz and Łysakowska [1517]. They defined for \(x \in \mathbb {R}^d\) and \(i \in [d]\), L(Txi) to be the set of all \(i^{\text {th}}\) coordinates \(t_i\) of vectors \(t \in T\) such that \(([0,1)^d + t) \cap ([0,1]^d + x) \ne \emptyset \) and \(t_i \le x_i\). A tiling is s-discrete if and only if \(L(T, x, i) \le s\) for all x and i.
 
Literature
1.
go back to reference 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, ACM, Anaheim, CA, USA, DAC ’03, pp 836–839 (2003) 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, ACM, Anaheim, CA, USA, DAC ’03, pp 836–839 (2003)
2.
go back to reference Biere, A.: CaDiCaL, L., Plingeling, T.: YalSAT Entering the SAT Competition 2018. In: Proc. of SAT Competition 2018—Solver and Benchmark Descriptions, University of Helsinki, Department of Computer Science Series of Publications B, vol B-2018-1, pp 13–14 (2018) Biere, A.: CaDiCaL, L., Plingeling, T.: YalSAT Entering the SAT Competition 2018. In: Proc. of SAT Competition 2018—Solver and Benchmark Descriptions, University of Helsinki, Department of Computer Science Series of Publications B, vol B-2018-1, pp 13–14 (2018)
3.
go back to reference Corrádi, K., Szabó, S.: A combinatorial approach for Keller’s conjecture. Period Math. Hung. 21, 91–100 (1990) MathSciNetCrossRef Corrádi, K., Szabó, S.: A combinatorial approach for Keller’s conjecture. Period Math. Hung. 21, 91–100 (1990) MathSciNetCrossRef
4.
go back to reference Cruz-Filipe L., Heule M.J.H., Jr Hunt W.A., Kaufmann M., Schneider-Kamp P.: Efficient certified RAT verification. In: Automated Deduction—CADE 26, Springer, pp 220–236 (2017) Cruz-Filipe L., Heule M.J.H., Jr Hunt W.A., Kaufmann M., Schneider-Kamp P.: Efficient certified RAT verification. In: Automated Deduction—CADE 26, Springer, pp 220–236 (2017)
5.
go back to reference Debroni, J., Eblen, J., Langston, M., Myrvold, W., Shor, P., Weerapurage, D.: A complete resolution of the Keller maximum clique problem. In: Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, Society for Industrial and Applied Mathematics, Philadelphia, PA, USA, pp 129–135 (2011) Debroni, J., Eblen, J., Langston, M., Myrvold, W., Shor, P., Weerapurage, D.: A complete resolution of the Keller maximum clique problem. In: Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, Society for Industrial and Applied Mathematics, Philadelphia, PA, USA, pp 129–135 (2011)
6.
go back to reference Hajós, G.: Über einfache und mehrfache Bedeckung des \(n\)-dimensionalen Raumes mit einen Würfelgitter. Math. Z. 47, 427–467 (1942) CrossRef Hajós, G.: Über einfache und mehrfache Bedeckung des \(n\)-dimensionalen Raumes mit einen Würfelgitter. Math. Z. 47, 427–467 (1942) CrossRef
7.
8.
go back to reference Heule, M.J.H., Schaub, T.: What’s hot in the SAT and ASP competition. In: Twenty-Ninth AAAI Conference on Artificial Intelligence 2015, AAAI Press, pp. 4322–4323 (2015) Heule, M.J.H., Schaub, T.: What’s hot in the SAT and ASP competition. In: Twenty-Ninth AAAI Conference on Artificial Intelligence 2015, AAAI Press, pp. 4322–4323 (2015)
9.
go back to reference Heule, M.J.H.: Schur number five. In: Proc. of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), AAAI Press, pp. 6598–6606 (2018) Heule, M.J.H.: Schur number five. In: Proc. of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), AAAI Press, pp. 6598–6606 (2018)
10.
go back to reference Heule, M.J.H., Jr Hunt, W.A., Wetzler, N.D.: Expressing symmetry breaking in DRAT proofs. In: Proceedings of the 25th Int. Conference on Automated Deduction (CADE 2015), Springer, Cham, LNCS, vol 9195, pp. 591–606 (2015) Heule, M.J.H., Jr Hunt, W.A., Wetzler, N.D.: Expressing symmetry breaking in DRAT proofs. In: Proceedings of the 25th Int. Conference on Automated Deduction (CADE 2015), Springer, Cham, LNCS, vol 9195, pp. 591–606 (2015)
11.
go back to reference Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer. In: Proc. of the 19th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2016), Springer, Cham, LNCS, vol 9710, pp. 228–245 (2016) Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer. In: Proc. of the 19th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2016), Springer, Cham, LNCS, vol 9710, pp. 228–245 (2016)
12.
go back to reference Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26), Springer, Cham, LNCS, Vol. 10395, pp. 130–147 (2017) Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26), Springer, Cham, LNCS, Vol. 10395, pp. 130–147 (2017)
13.
go back to reference Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Proc. of the 6th Int. Joint Conference on Automated Reasoning (IJCAR 2012), Springer, Heidelberg, LNCS, Vol. 7364, pp. 355–370 (2012) Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Proc. of the 6th Int. Joint Conference on Automated Reasoning (IJCAR 2012), Springer, Heidelberg, LNCS, Vol. 7364, pp. 355–370 (2012)
14.
go back to reference Keller, O.H.: Über die lückenlose Erfüllung des Raumes mit Würfeln. J. Reine Angew. Math. 163, 231–248 (1930) MathSciNetMATH Keller, O.H.: Über die lückenlose Erfüllung des Raumes mit Würfeln. J. Reine Angew. Math. 163, 231–248 (1930) MathSciNetMATH
17.
go back to reference Kisielewicz, A.P., Łysakowska, M.: On Keller’s conjecture in dimension seven. Electron. J. Comb. 22(1), P1-16 (2015) MathSciNetMATH Kisielewicz, A.P., Łysakowska, M.: On Keller’s conjecture in dimension seven. Electron. J. Comb. 22(1), P1-16 (2015) MathSciNetMATH
18.
go back to reference Konev, B., Lisitsa, A.: Computer-aided proof of Erdős discrepancy properties. Artif. Intell. 224(C), 103–118 (2015) CrossRef Konev, B., Lisitsa, A.: Computer-aided proof of Erdős discrepancy properties. Artif. Intell. 224(C), 103–118 (2015) CrossRef
19.
20.
go back to reference 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) MathSciNetCrossRef 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) MathSciNetCrossRef
21.
go back to reference Lammich, P.: Efficient verified (UN)SAT certificate checking. In: Automated Deduction—CADE 26, Springer, pp. 237–254 (2017) Lammich, P.: Efficient verified (UN)SAT certificate checking. In: Automated Deduction—CADE 26, Springer, pp. 237–254 (2017)
23.
25.
26.
go back to reference Perron, O.: Über lückenlose ausfüllung des \(n\)-dimensionalen Raumes durch kongruente würfel. Math. Z. 46(1), 1–26 (1940) MathSciNetCrossRef Perron, O.: Über lückenlose ausfüllung des \(n\)-dimensionalen Raumes durch kongruente würfel. Math. Z. 46(1), 1–26 (1940) MathSciNetCrossRef
27.
go back to reference Perron, O.: Über lückenlose ausfüllung des \(n\)-dimensionalen raumes durch kongruente würfel II. Math. Z. 46(1), 161–180 (1940) MathSciNetCrossRef Perron, O.: Über lückenlose ausfüllung des \(n\)-dimensionalen raumes durch kongruente würfel II. Math. Z. 46(1), 161–180 (1940) MathSciNetCrossRef
28.
go back to reference Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symbol. Comput. 2(3), 293–304 (1986) MathSciNetCrossRef Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symbol. Comput. 2(3), 293–304 (1986) MathSciNetCrossRef
29.
go back to reference Shor, P.W.: Minkowski’s and Keller’s cube-tiling conjectures (2004) Shor, P.W.: Minkowski’s and Keller’s cube-tiling conjectures (2004)
31.
go back to reference Szabó, S.: Cube tilings as contributions of algebra to geometry. Beiträge Algebra Geom. 34, 63–75 (1993) MathSciNetMATH Szabó, S.: Cube tilings as contributions of algebra to geometry. Beiträge Algebra Geom. 34, 63–75 (1993) MathSciNetMATH
32.
go back to reference Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: International Conference on Theory and Applications of Satisfiability Testing, Springer, pp. 422–429 (2014) Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: International Conference on Theory and Applications of Satisfiability Testing, Springer, pp. 422–429 (2014)
Metadata
Title
The Resolution of Keller’s Conjecture
Authors
Joshua Brakensiek
Marijn Heule
John Mackey
David Narváez
Publication date
06-05-2022
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 3/2022
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09623-5

Other articles of this Issue 3/2022

Journal of Automated Reasoning 3/2022 Go to the issue

Premium Partner