{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T11:59:54Z","timestamp":1792756794949,"version":"4.5.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319635156","type":"print"},{"value":"9783319635163","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-63516-3_2","type":"book-chapter","created":{"date-parts":[[2018,4,5]],"date-time":"2018-04-05T03:43:39Z","timestamp":1522899819000},"page":"31-59","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Cube-and-Conquer for Satisfiability"],"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":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,4,6]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Tanbir Ahmed, Oliver Kullmann, and Hunter Snevily. On the van der Waerden numbers w(2;3; t). Discrete Applied Mathematics, 174:27\u201351, September 2014.","DOI":"10.1016\/j.dam.2014.05.007"},{"key":"2_CR2","unstructured":"Fahiem Bacchus. Enhancing Davis Putnam with extended binary clause reasoning. In AAAI 2002, pages 613\u2013619, 2002."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Armin Biere. PicoSAT essentials. JSAT, 4(2-4):75\u201397, 2008.","DOI":"10.3233\/SAT190039"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Armin Biere. Bounded model checking. In Biere et al. [6], chapter 14, pages 455\u2013481.","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"2_CR5","unstructured":"Armin Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT race 2010. 2010."},{"key":"2_CR6","unstructured":"Armin Biere, Marijn J.H. Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of FAIA. IOS Press, February 2009."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394\u2013397, 1962.","DOI":"10.1145\/368273.368557"},{"key":"2_CR8","unstructured":"Olivier Dubois and Gilles Dequen. A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In Bernhard Nebel, editor, IJCAI, pages 248\u2013253. Morgan Kaufmann, 2001."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Niklas E\u00e9n and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, volume 3569 of Lecture Notes in Computer Science, pages 61\u201375. Springer, 2005.","DOI":"10.1007\/11499107_5"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, SAT, volume 2919 of LNCS, pages 502\u2013518. Springer, 2003.","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson. Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci., 89(4):543\u2013560, 2003.","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Youssef Hamadi. Conclusion to the special issue on parallel SAT solving. JSAT, 6(4):263, 2009.","DOI":"10.3233\/SAT190071"},{"key":"2_CR13","unstructured":"Youssef Hamadi, Sa\u00efd Jabbour, and Lakhdar Sais. ManySAT: a parallel SAT solver. JSAT, 6(4):245\u2013262, 2009."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Robert M. Haralick and Gordon L. Elliott. Increasing tree search efficiency for constraint satisfaction problems. Artif. Intell., 14(3):263\u2013313, 1980.","DOI":"10.1016\/0004-3702(80)90051-X"},{"key":"2_CR15","unstructured":"Willim D. Harvey and Matthew L. Ginsberg. Limited discrepancy search. In IJCAI 1995, pages 607\u2013613, 1995."},{"key":"2_CR16","unstructured":"Marijn J.H. Heule. The DRAT format and DRAT-trim checker. CoRR, http:\/\/arXiv.org\/abs\/1610.06229, 2016. Source code available from: https:\/\/github.com\/marijnheule\/drat-trim ."},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Marijn J.H. Heule, Warren A. Hunt, Jr, and Nathan Wetzler. Verifying refutations with Extended Resolution. In CADE, volume 7898 of LNAI, pages 345\u2013359. Springer, 2013.","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"2_CR18","unstructured":"Marijn J.H. Heule and Hans van Maaren. Look-Ahead Based SAT Solvers, chapter 5, pages 155\u2013184. Volume 185 of Biere et al. [6], February 2009."},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Marijn J.H. Heule, Mark Dufour, Joris E. van Zwieten, and Hans van Maaren. March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver. In Holger H. Hoos and David G. Mitchell, editors, SAT (Selected Papers, volume 3542 of Lecture Notes in Computer Science, pages 345\u2013359. Springer, 2004.","DOI":"10.1007\/11527695_26"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Marijn J.H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016, volume 9710 of Lecture Notes in Computer Science, pages 228\u2013245. Springer, 2016.","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"2_CR21","unstructured":"Marijn J.H. Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In Kerstin Eder, Jo\u00e3o Louren\u00e7o, and Onn Shehory, editors, Hardware and Software: Verification and Testing (HVC 2011), volume 7261 of Lecture Notes in Computer Science (LNCS), pages 50\u201365. Springer, 2012."},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Antti E. J. Hyv\u00e4rinen, Tommi Junttila, and Ilkka Niemel\u00e4. Partitioning SAT instances for distributed solving. In LPAR-17, volume 6397 of LNCS, pages 372\u2013386, 2010.","DOI":"10.1007\/978-3-642-16242-8_27"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Antti E. J. Hyv\u00e4rinen, Tommi Junttila, and Ilkka Niemel\u00e4. Grid-based SAT solving with iterative partitioning and clause learning. In CP 2011, volume 6876 of LNCS, 2011.","DOI":"10.1007\/978-3-642-23786-7_30"},{"key":"2_CR24","unstructured":"Hans Kleine B\u00fcning and Oliver Kullmann. Minimal Unsatisfiability and Autarkies, chapter 11, pages 339\u2013401. Volume 185 of Biere et al. [6], February 2009."},{"key":"2_CR25","unstructured":"Oliver Kullmann. Investigating the behaviour of a SAT solver on random formulas. Technical Report CSR 23-2002, University of Wales Swansea, Computer Science Report Series, October 2002. 119 pages."},{"key":"2_CR26","unstructured":"Oliver Kullmann. Fundaments of Branching Heuristics, chapter 7, pages 205\u2013244. Volume 185 of Biere et al. [6], February 2009."},{"key":"2_CR27","unstructured":"Oliver Kullmann. The OKlibrary: Introducing a \u201cholistic\u201d research platform for (generalised) SAT solving. Studies in Logic, 2(1):20\u201353, 2009."},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Oliver Kullmann. Green-Tao numbers and SAT. In Ofer Strichman and Stefan Szeider, editors, SAT 2010, volume 6175 of LNCS, pages 352\u2013362. Springer, 2010.","DOI":"10.1007\/978-3-642-14186-7_32"},{"key":"2_CR29","unstructured":"Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In IJCAI (1), pages 366\u2013371, 1997."},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Norbert Manthey, Marijn J.H. Heule, and Armin Biere. Automated reencoding of Boolean formulas. In Proceedings of Haifa Verification Conference 2012, 2012.","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Joao P. Marques-Silva, Ines Lynce, and Sharad Malik. Conflict-Driven Clause Learning SAT Solvers, chapter 4, pages 131\u2013153. Volume 185 of Biere et al. [6], February 2009.","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"2_CR32","unstructured":"Sid Mijnders, Boris de Wilde, and Marijn J.H. Heule. Symbiosis of search and heuristics for random 3-SAT. In David Mitchell and Eugenia Ternovska, editors, LaSh 2010, 2010."},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Peter van Beek. Backtracking search algorithms. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors, Handbook of Constraint Programming, chapter 4, pages 85\u2013134. 2006.","DOI":"10.1016\/S1574-6526(06)80008-8"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In ISAIM, 2008.","DOI":"10.1007\/978-3-540-72788-0_31"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Nathan Wetzler, Marijn J.H. Heule, and Warren A. Hunt, Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, SAT 2014, volume 8561 of LNCS, pages 422\u2013429. Springer, 2014.","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Siert Wieringa, Matti Niemenmaa, and Keijo Heljanko. Tarmo: A framework for parallelized bounded model checking. In Lubos Brim and Jaco van de Pol, editors, PDMC, volume 14 of EPTCS, pages 62\u201376, 2009.","DOI":"10.4204\/EPTCS.14.5"},{"key":"2_CR37","unstructured":"Hantao Zhang. Combinatorial designs by SAT solvers. In Biere et al. [6], chapter 17, pages 533\u2013568."},{"key":"2_CR38","unstructured":"Lintao Zhang and Sharad Malik. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In DATE, pages 10880\u201310885, 2003."}],"container-title":["Handbook of Parallel Constraint Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63516-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T12:48:43Z","timestamp":1751546923000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63516-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319635156","9783319635163"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63516-3_2","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}