Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Start single access now
Request access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning

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

Log in

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
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 [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.
 
Literature
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, ACM, Anaheim, CA, USA, DAC ’03, pp 836–839 (2003)
2.
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.
Corrádi, K., Szabó, S.: A combinatorial approach for Keller’s conjecture. Period Math. Hung. 21, 91–100 (1990) MathSciNetCrossRef
4.
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.
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.
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.
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.
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.
16.
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.
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.
23.
24.
25.
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.
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.
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

OriginalPaper

Polite Combination of Algebraic Datatypes

OriginalPaper

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

OriginalPaper

Combination of Uniform Interpolants via Beth Definability

EditorialNotes

Special Issue of Selected Extended Papers of IJCAR 2020

OriginalPaper

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

Premium Partner

Neuer Inhalt
    Image Credits