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
Erschienen in:
Parameterized Compilation Lower Bounds for Restricted CNF-Formulas Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer

verfasst von : Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek

Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2016

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set \(\mathbb {N}= \{1,2,\dots \}\) of natural numbers be divided into two parts, such that no part contains a triple (a, b, c) with \(a^2 + b^2 = c^2\) ? A prize for the solution was offered by Ronald Graham over two decades ago. We solve this problem, proving in fact the impossibility, by using the Cube-and-Conquer paradigm, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed to solve the problem on a cluster with 800 cores in about 2 days. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking.

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 "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

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
Vorheriges Kapitel Heuristic NPN Classification for Large Functions Using AIGs and LEXSAT
Nächstes Kapitel Deciding Bit-Vector Formulas with mcSAT
Fußnoten
1
In practice this is done using a single incremental CNF file. For details about the format, see http://​www.​siert.​nl/​icnf/​.
 
2
 
Literatur
1.
Mizar proof checker. Accessed: November 2015
2.
Coq proof manager. Accessed: November 2015
3.
The site of \(flyspeck\) project, the formal verification of the proof of Kepler Conjecture. Accessed: November 2015
4.
5.
Biere, A.: Picosat essentials. JSAT 4(2–4), 75–97 (2008)MATH
6.
Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Proceedings of SAT Competition 2013, p. 51 (2013)
7.
Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)MATH
8.
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
9.
Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings 3rd Annual ACM Symposium on Theory of Computing (STOC 1971), pp. 151–158 (1971)
10.
11.
Cooper, J., Poirel, C.: Note on the Pythagorean triple system (2008)
12.
Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Proceedings of 5th International Conference on Knowledge Representation and Reasoning, KR 1996, pp. 148–159. Morgan Kaufmann (1996)
13.
Dequen, G., Dubois, O.: kcnfs: an efficient solver for random k-SAT formulae. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 486–501. Springer, Heidelberg (2004)CrossRef
14.
Dransfield, M.R., Marek, V.W., Truszczyński, M.: Satisfiability and computing van der Waerden numbers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 1–13. Springer, Heidelberg (2004)CrossRef
15.
Dubois, O., Dequen, G.: A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In: International Joint Conferences on Artificial Intelligence (IJCAI), pp. 248–253 (2001)
16.
Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)CrossRef
17.
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRef
18.
Franco, J., Martin, J.: A history of satisfiability. In: Biere et al. [7], Chap. 1, pp. 3–74
19.
Garey, M.R., Johnson, D.S.: Computers and Intractability/A Guide to the Theory of NP-Completeness. W.H. Freeman and Company, New York (1979)MATH
20.
21.
Heule, M.J.H., Biere, A.: Clausal proof compression. In: 11th International Workshop on the Implementation of Logics (2015)
22.
Heule, M.J.H., Biere, A.: Compositional propositional proofs. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 444–459. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-48899-7_​31 CrossRef
23.
Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 345–359. Springer, Heidelberg (2013)CrossRef
24.
Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 591–606. Springer, Heidelberg (2015)CrossRef
25.
Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50–65. Springer, Heidelberg (2012)CrossRef
26.
Heule, M.J.H., van Maaren, H.: Look-ahead based SAT solvers. In: Biere et al. [7], Chap. 5, pp. 155–184
27.
Järvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129–144. Springer, Heidelberg (2010)CrossRef
28.
Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355–370. Springer, Heidelberg (2012)CrossRef
29.
Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatche, J.W. (eds.) Complexity of Computer Computations, pp. 85–103. Plenum Press, New York (1972)CrossRef
30.
Kay, W.: An overview of the constructive local lemma. Master’s thesis, University of South Carolina (2009)
31.
Kouril, M.: Computing the van der Waerden number \({W}(3,4) = 293\). INTEGERS: Electron. J. Comb. Number Theory 12(A46), 1–13 (2012)
32.
33.
34.
Kullmann, O.: Fundaments of branching heuristics. In: Biere et al. [7], Chap. 7, pp. 205–244
35.
Levin, L.: Universal search problems. Problemy Peredachi Informatsii 9, 115–116 (1973)MATH
36.
37.
Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), pp. 366–371. Morgan Kaufmann Publishers (1997)
38.
Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Proceedings of Haifa Verification Conference 2012 (2012)
39.
Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere et al. [7], Chap. 4, pp. 131–153
40.
Mijnders, S., de Wilde, B., Heule, M.J.H.: Symbiosis of search and heuristics for random 3-SAT. In: Mitchell, D., Ternovska, E. (eds.) Third International Workshop on Logic and Search (LaSh 2010) (2010)
41.
Myers, K.J.: Computational advances in Rado numbers. Ph.D. thesis, Rutgers University (2015)
42.
Rado, R.: Some partition theorems. In: Colloquia Mathematica Societatis János Bolyai 4. Combinatorial Theory and Its Applications III, pp. 929–936. North-Holland, Amsterdam (1970)
43.
Schur, I.: Über die Kongruenz \(x^m + y^m = z^m\) (mod p). Jahresbericht der Deutschen Mathematikervereinigung 25, 114–117 (1917)
44.
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning 2, pp. 466–483. Springer, Heidelberg (1983)CrossRef
45.
van der Waerden, B.L.: Beweis einer Baudetschen Vermutung. Nieuw Archief voor Wiskunde 15, 212–216 (1927)MATH
46.
Van Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: ISAIM (2008)
47.
Voevodski, V.: Lecture at ASC 2008, How I became interested in foundations of mathematics. Accessed: November 2015
48.
Wetzler, N., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Heidelberg (2014)
49.
Zhang, H.: Combinatorial designs by SAT solvers. In: Biere et al. [7], Chap. 17, pp. 533–568
50.
Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: DATE, pp. 10880–10885 (2003)
Metadaten
Titel
Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
verfasst von
Marijn J. H. Heule
Oliver Kullmann
Victor W. Marek
Copyright-Jahr
2016
Buch
Theory and Applications of Satisfiability Testing – SAT 2016

Print ISBN: 978-3-319-40969-6

Electronic ISBN: 978-3-319-40970-2

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-40970-2_15