{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,15]],"date-time":"2026-10-15T13:34:53Z","timestamp":1792071293663,"version":"4.4.0"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319409696","type":"print"},{"value":"9783319409702","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_15","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T07:14:55Z","timestamp":1465542895000},"page":"228-245","source":"Crossref","is-referenced-by-count":133,"title":["Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer"],"prefix":"10.1007","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Oliver","family":"Kullmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Victor W.","family":"Marek","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"key":"15_CR1","unstructured":"Mizar proof checker. Accessed: November 2015"},{"key":"15_CR2","unstructured":"Coq proof manager. Accessed: November 2015"},{"key":"15_CR3","unstructured":"The site of $$flyspeck$$ project, the formal verification of the proof of Kepler Conjecture. Accessed: November 2015"},{"key":"15_CR4","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/j.dam.2014.05.007","volume":"174","author":"T Ahmed","year":"2014","unstructured":"Ahmed, T., Kullmann, O., Snevily, H.: On the van der Waerden numbers w(2; 3, t). Discrete Appl. Math. 174, 27\u201351 (2014)","journal-title":"Discrete Appl. Math."},{"issue":"2\u20134","key":"15_CR5","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"15_CR6","unstructured":"Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Proceedings of SAT Competition 2013, p. 51 (2013)"},{"key":"15_CR7","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"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)"},{"key":"15_CR8","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings 3rd Annual ACM Symposium on Theory of Computing (STOC 1971), pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"key":"15_CR10","unstructured":"Cooper, J., Overstreet, R.: Coloring so that no Pythagorean triple is monochromatic (2015). arXiv:1505.02222"},{"key":"15_CR11","unstructured":"Cooper, J., Poirel, C.: Note on the Pythagorean triple system (2008)"},{"key":"15_CR12","unstructured":"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\u2013159. Morgan Kaufmann (1996)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1007\/978-3-540-24605-3_36","volume-title":"Theory and Applications of Satisfiability Testing","author":"G Dequen","year":"2004","unstructured":"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\u2013501. Springer, Heidelberg (2004)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-24605-3_1","volume-title":"Theory and Applications of Satisfiability Testing","author":"MR Dransfield","year":"2004","unstructured":"Dransfield, M.R., Marek, V.W., Truszczy\u0144ski, M.: Satisfiability and computing van der Waerden numbers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 1\u201313. Springer, Heidelberg (2004)"},{"key":"15_CR15","unstructured":"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\u2013253 (2001)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, 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\u201375. Springer, Heidelberg (2005)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"15_CR18","unstructured":"Franco, J., Martin, J.: A history of satisfiability. In: Biere et al. [7], Chap. 1, pp. 3\u201374"},{"key":"15_CR19","volume-title":"Computers and Intractability\/A Guide to the Theory of NP-Completeness","author":"MR Garey","year":"1979","unstructured":"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)"},{"issue":"4","key":"15_CR20","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1145\/321850.321857","volume":"21","author":"LJ Henschen","year":"1974","unstructured":"Henschen, L.J., Wos, L.: Unit refutations and Horn sets. J. Assoc. Comput. Mach. 21(4), 590\u2013605 (1974)","journal-title":"J. Assoc. Comput. Mach."},{"key":"15_CR21","unstructured":"Heule, M.J.H., Biere, A.: Clausal proof compression. In: 11th International Workshop on the Implementation of Logics (2015)"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/978-3-662-48899-7_31","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"MJH Heule","year":"2015","unstructured":"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\u2013459. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48899-7_31"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/978-3-642-38574-2_24","volume-title":"Automated Deduction \u2013 CADE-24","author":"MJH Heule","year":"2013","unstructured":"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\u2013359. Springer, Heidelberg (2013)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1007\/978-3-319-21401-6_40","volume-title":"Automated Deduction - CADE-25","author":"MJH Heule","year":"2015","unstructured":"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\u2013606. Springer, Heidelberg (2015)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012)"},{"key":"15_CR26","unstructured":"Heule, M.J.H., van Maaren, H.: Look-ahead based SAT solvers. In: Biere et al. [7], Chap. 5, pp. 155\u2013184"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"15_CR29","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-1-4684-2001-2_9","volume-title":"Complexity of Computer Computations","author":"RM Karp","year":"1972","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatche, J.W. (eds.) Complexity of Computer Computations, pp. 85\u2013103. Plenum Press, New York (1972)"},{"key":"15_CR30","unstructured":"Kay, W.: An overview of the constructive local lemma. Master\u2019s thesis, University of South Carolina (2009)"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Kouril, M.: Computing the van der Waerden number $${W}(3,4) = 293$$ . INTEGERS: Electron. J. Comb. Number Theory 12(A46), 1\u201313 (2012)","DOI":"10.1515\/integ.2011.112"},{"issue":"1","key":"15_CR32","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1080\/10586458.2008.10129025","volume":"17","author":"M Kouril","year":"2008","unstructured":"Kouril, M., Paul, J.L.: The van der Waerden number $${W}(2,6)$$ is $$1132$$ . Exp. Math. 17(1), 53\u201361 (2008)","journal-title":"Exp. Math."},{"key":"15_CR33","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Appl. Math."},{"key":"15_CR34","unstructured":"Kullmann, O.: Fundaments of branching heuristics. In: Biere et al. [7], Chap. 7, pp. 205\u2013244"},{"key":"15_CR35","first-page":"115","volume":"9","author":"L Levin","year":"1973","unstructured":"Levin, L.: Universal search problems. Problemy Peredachi Informatsii 9, 115\u2013116 (1973)","journal-title":"Problemy Peredachi Informatsii"},{"issue":"2","key":"15_CR36","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/S0020-0190(99)00088-5","volume":"71","author":"CM Li","year":"1999","unstructured":"Li, C.M.: A constraint-based approach to narrow search trees for satisfiability. Inf. Process. Lett. 71(2), 75\u201380 (1999)","journal-title":"Inf. Process. Lett."},{"key":"15_CR37","unstructured":"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\u2013371. Morgan Kaufmann Publishers (1997)"},{"key":"15_CR38","doi-asserted-by":"crossref","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Proceedings of Haifa Verification Conference 2012 (2012)","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"15_CR39","unstructured":"Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere et al. [7], Chap. 4, pp. 131\u2013153"},{"key":"15_CR40","unstructured":"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)"},{"key":"15_CR41","unstructured":"Myers, K.J.: Computational advances in Rado numbers. Ph.D. thesis, Rutgers University (2015)"},{"key":"15_CR42","unstructured":"Rado, R.: Some partition theorems. In: Colloquia Mathematica Societatis J\u00e1nos Bolyai 4. Combinatorial Theory and Its Applications III, pp. 929\u2013936. North-Holland, Amsterdam (1970)"},{"key":"15_CR43","unstructured":"Schur, I.: \u00dcber die Kongruenz $$x^m + y^m = z^m$$ (mod p). Jahresbericht der Deutschen Mathematikervereinigung 25, 114\u2013117 (1917)"},{"key":"15_CR44","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning 2","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning 2, pp. 466\u2013483. Springer, Heidelberg (1983)"},{"key":"15_CR45","first-page":"212","volume":"15","author":"BL Waerden van der","year":"1927","unstructured":"van der Waerden, B.L.: Beweis einer Baudetschen Vermutung. Nieuw Archief voor Wiskunde 15, 212\u2013216 (1927)","journal-title":"Nieuw Archief voor Wiskunde"},{"key":"15_CR46","doi-asserted-by":"crossref","unstructured":"Van Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: ISAIM (2008)","DOI":"10.1007\/978-3-540-72788-0_31"},{"key":"15_CR47","unstructured":"Voevodski, V.: Lecture at ASC 2008, How I became interested in foundations of mathematics. Accessed: November 2015"},{"key":"15_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"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\u2013429. Springer, Heidelberg (2014)"},{"key":"15_CR49","unstructured":"Zhang, H.: Combinatorial designs by SAT solvers. In: Biere et al. [7], Chap. 17, pp. 533\u2013568"},{"key":"15_CR50","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: DATE, pp. 10880\u201310885 (2003)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T10:09:40Z","timestamp":1568023780000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}