Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning

06.05.2022

The Resolution of Keller’s Conjecture

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

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

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.
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.
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
Publikationsdatum
06.05.2022
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