{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T17:50:23Z","timestamp":1791136223709,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642341878","type":"print"},{"value":"9783642341885","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34188-5_8","type":"book-chapter","created":{"date-parts":[[2012,10,11]],"date-time":"2012-10-11T10:04:33Z","timestamp":1349949873000},"page":"50-65","source":"Crossref","is-referenced-by-count":96,"title":["Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads"],"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":"Siert","family":"Wieringa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Ahmed, T., Kullmann, O., Snevily, H.: On the van der Waerden numbers w(2; 3, t). Tech. Rep. arXiv:1102.5433 [math.CO], arXiv (February 2011)"},{"key":"8_CR2","unstructured":"Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: AAAI 2002, pp. 613\u2013619 (2002)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"van Beek, P.: Backtracking search algorithms. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, ch.\u00a04, pp. 85\u2013134 (2006)","DOI":"10.1016\/S1574-6526(06)80008-8"},{"key":"8_CR4","unstructured":"Biere, A.: Bounded model checking. In: Biere, et al. (eds.) [6], ch.\u00a014, pp. 455\u2013481"},{"key":"8_CR5","unstructured":"Biere, A.: Lingeling, Plingeling, Picosat and Precosat at SAT race 2010 (2010)"},{"key":"8_CR6","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. FAIA, vol.\u00a0185. IOS Press (February 2009)"},{"issue":"7","key":"8_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"8_CR8","unstructured":"Dubois, O., Dequen, G.: A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In: Nebel, B. (ed.) IJCAI, pp. 248\u2013253. Morgan Kaufmann (2001)"},{"issue":"4","key":"8_CR9","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N. E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci.\u00a089(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"4","key":"8_CR10","first-page":"263","volume":"6","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y.: Conclusion to the special issue on parallel SAT solving. JSAT\u00a06(4), 263 (2009)","journal-title":"JSAT"},{"issue":"4","key":"8_CR11","first-page":"245","volume":"6","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. JSAT\u00a06(4), 245\u2013262 (2009)","journal-title":"JSAT"},{"issue":"3","key":"8_CR12","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0004-3702(80)90051-X","volume":"14","author":"R.M. Haralick","year":"1980","unstructured":"Haralick, R.M., Elliott, G.L.: Increasing tree search efficiency for constraint satisfaction problems. Artif. Intell.\u00a014(3), 263\u2013313 (1980)","journal-title":"Artif. Intell."},{"key":"8_CR13","unstructured":"Harvey, W.D., Ginsberg, M.L.: Limited discrepancy search. In: IJCAI 1995, pp. 607\u2013613 (1995)"},{"key":"8_CR14","unstructured":"Heule, M.J.H., van Maaren, H.: Look-Ahead Based SAT Solvers. In: Biere, et al. (eds.) [6], ch. 5, vol.\u00a0185, pp. 155\u2013184 (2009)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-16242-8_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A.E.J. Hyv\u00e4rinen","year":"2010","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Partitioning SAT Instances for Distributed Solving. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 372\u2013386. Springer, Heidelberg (2010)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-642-23786-7_30","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"A.E.J. Hyv\u00e4rinen","year":"2011","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Grid-Based SAT Solving with Iterative Partitioning and Clause Learning. In: Lee, J. (ed.) CP 2011. LNCS, vol.\u00a06876, pp. 385\u2013399. Springer, Heidelberg (2011)"},{"key":"8_CR17","unstructured":"Kleine B\u00fcning, H., Kullmann, O.: Minimal Unsatisfiability and Autarkies. In: Biere, et al. (eds.) [6], ch. 11, vol.\u00a0185, pp. 339\u2013401 (February 2009)"},{"key":"8_CR18","unstructured":"Kullmann, O.: Investigating the behaviour of a SAT solver on random formulas. Tech. Rep. CSR 23-2002, University of Wales Swansea, Computer Science Report Series, 119 pages (2002), http:\/\/www-compsci.swan.ac.uk\/reports\/2002.html"},{"key":"8_CR19","unstructured":"Kullmann, O.: Fundaments of Branching Heuristics. In: Biere, et al. (eds.) [6], ch. 7, vol.\u00a0185, pp. 205\u2013244 (February 2009)"},{"issue":"1","key":"8_CR20","first-page":"20","volume":"2","author":"O. Kullmann","year":"2009","unstructured":"Kullmann, O.: The OKlibrary: Introducing a \u201dholistic\u201d research platform for (generalised) SAT solving. Studies in Logic\u00a02(1), 20\u201353 (2009)","journal-title":"Studies in Logic"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-14186-7_32","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"O. Kullmann","year":"2010","unstructured":"Kullmann, O.: Green-Tao Numbers and SAT. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 352\u2013362. Springer, Heidelberg (2010)"},{"key":"8_CR22","unstructured":"Kullmann, O.: Computing ordinary and palindromic van der Waerden numbers via collaboration between look-ahead and conflict-driven SAT solvers (in preparation, February 2012)"},{"key":"8_CR23","unstructured":"Li, C.M.: Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: IJCAI, vol.\u00a0(1), pp. 366\u2013371 (1997)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-Driven Clause Learning SAT Solvers. In: Biere, et al. (eds.) [6], ch. 4, vol.\u00a0185, pp. 131\u2013153 (February 2009)","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"8_CR25","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.) LaSh 2010 (2010)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Wieringa, S., Niemenmaa, M., Heljanko, K.: Tarmo: A framework for parallelized bounded model checking. In: Brim, L., van de Pol, J. (eds.) PDMC. EPTCS, vol.\u00a014, pp. 62\u201376 (2009)","DOI":"10.4204\/EPTCS.14.5"},{"key":"8_CR27","unstructured":"Zhang, H.: Combinatorial designs by SAT solvers. In: Biere, et al. (eds.) [6], ch.\u00a017, pp. 533\u2013568"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34188-5_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T16:51:36Z","timestamp":1744303896000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34188-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642341878","9783642341885"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34188-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}