Top

Journal of Automated Reasoning

Published in:

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

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article Special Issue of Selected Extended Papers of IJCAR 2020

next article Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

Commit 92d72896c49b30ad2d50c8e1061ca0681cd23e60 of

https://github.com/arminbiere/cadical.

https://github.com/marijnheule/Keller-encode.

https://doi.org/10.5281/zenodo.3755116.

This is a (ultimately equivalent) variant of a definition of Kisielewicz and Łysakowska [15‐17]. They defined for \(x \in \mathbb {R}^d\) and \(i \in [d]\), L(T, x, i) 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.

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)

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)

Corrádi, K., Szabó, S.: A combinatorial approach for Keller’s conjecture. Period Math. Hung. 21, 91–100 (1990)MathSciNetCrossRef

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)

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)

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.: Sur la factorisation des groupes abéliens. Casopis Pest Mat Fys 74, 157–162 (1950)MathSciNetMATH

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.: Schur number five. In: Proc. of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), AAAI Press, pp. 6598–6606 (2018)

10.

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.

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.

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.

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.

Keller, O.H.: Über die lückenlose Erfüllung des Raumes mit Würfeln. J. Reine Angew. Math. 163, 231–248 (1930)MathSciNetMATH

15.

Kisielewicz, A.P.: Rigid polyboxes and Keller’s conjecture. Adv. Geom. 17(2), 203–230 (2017)MathSciNetCrossRef

16.

Kisielewicz, A.P.: Towards resolving Keller’s cube tiling conjecture in dimension seven. arXiv preprint arXiv:1701.07155 (2017)

17.

Kisielewicz, A.P., Łysakowska, M.: On Keller’s conjecture in dimension seven. Electron. J. Comb. 22(1), P1-16 (2015)MathSciNetMATH

18.

Konev, B., Lisitsa, A.: Computer-aided proof of Erdős discrepancy properties. Artif. Intell. 224(C), 103–118 (2015)CrossRef

19.

Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96–97, 149–176 (1999)MathSciNetCrossRef

20.

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.

Lammich, P.: Efficient verified (UN)SAT certificate checking. In: Automated Deduction—CADE 26, Springer, pp. 237–254 (2017)

22.

Łysakowska, M.: Extended Keller graph and its properties. Quaest. Math. 42(4), 551–560 (2019)MathSciNetCrossRef

23.

Mackey, J.: A cube tiling of dimension eight with no facesharing. Discrete Comput. Geom. 28(2), 275–279 (2002)MathSciNetCrossRef

24.

McKay B.D., Piperno, A.: nauty and Traces user’s guide (version 2.6). http://users.cecs.anu.edu.au/~bdm/nauty/nug26.pdf (2017)

25.

Minkowski, H.: Diophantische Approximationen. Teubner, Leipzig (1907)CrossRef

26.

Perron, O.: Über lückenlose ausfüllung des \(n\)-dimensionalen Raumes durch kongruente würfel. Math. Z. 46(1), 1–26 (1940)MathSciNetCrossRef

27.

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.

Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symbol. Comput. 2(3), 293–304 (1986)MathSciNetCrossRef

29.

Shor, P.W.: Minkowski’s and Keller’s cube-tiling conjectures (2004)

30.

Szabó, S.: A reduction of Keller’s conjecture. Period. Math. Hung. 17(4), 265–277 (1986)MathSciNetCrossRef

31.

Szabó, S.: Cube tilings as contributions of algebra to geometry. Beiträge Algebra Geom. 34, 63–75 (1993)MathSciNetMATH

32.

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)

33.

Zong, C.: What is known about unit cubes. Bull. Am. Math. Soc. 42(2), 181–211 (2005)MathSciNetCrossRef

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

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 3/2022

Polite Combination of Algebraic Datatypes

Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains

Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols

Combination of Uniform Interpolants via Beth Definability

Special Issue of Selected Extended Papers of IJCAR 2020

Premium Partner