Skip to main content
Registrieren
Springer Professional
SUCHE
MENÜ 1 2 3 4
nach oben

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Erschienen in: Journal of Automated Reasoning 3/2022

06.05.2022

The Resolution of Keller’s Conjecture

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

Erschienen in: Journal of Automated Reasoning | Ausgabe 3/2022

Einloggen, um Zugang zu erhalten
share
TEILEN

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.
Vorheriger Artikel Special Issue of Selected Extended Papers of IJCAR 2020
Nächster Artikel Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 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 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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





Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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



 


Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
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.
 
Literatur
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.
Hajós, G.: Sur la factorisation des groupes abéliens. Casopis Pest Mat Fys 74, 157–162 (1950) MathSciNetMATH
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.
Mackey, J.: A cube tiling of dimension eight with no facesharing. Discrete Comput. Geom. 28(2), 275–279 (2002) MathSciNetCrossRef
24.
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.
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.
Metadaten
Titel
The Resolution of Keller’s Conjecture
verfasst von
Joshua Brakensiek
Marijn Heule
John Mackey
David Narváez
Publikationsdatum
06.05.2022
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 3/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09623-5

Weitere Artikel der Ausgabe 3/2022

Journal of Automated Reasoning 3/2022 Zur Ausgabe

OriginalPaper

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

OriginalPaper

Combination of Uniform Interpolants via Beth Definability

OriginalPaper

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

OriginalPaper

Polite Combination of Algebraic Datatypes

EditorialNotes

Special Issue of Selected Extended Papers of IJCAR 2020

Premium Partner