{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:02:02Z","timestamp":1777125722113,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642027765","type":"print"},{"value":"9783642027772","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_29","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T02:58:18Z","timestamp":1245985098000},"page":"298-311","source":"Crossref","is-referenced-by-count":11,"title":["Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques"],"prefix":"10.1007","author":[{"given":"Jingchao","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"Pipatssrisawat, K., Darwiche, A.: Rsat 2.0: SAT solver description. In: SAT 2007 competition (2007)"},{"key":"29_CR2","unstructured":"March_ks SAT solver, the version of SAT 2007 competition, http:\/\/www.st.ewi.tudelft.nl\/sat\/download.php"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The Complexity of Theorem Proving Procedures. In: 3rd ACM Symp. on Theory of Computing, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"key":"29_CR4","unstructured":"Crawford, J.M., Kearns, M.J., Schapire, R.E.: The Minimal Disagreement Parity Problem as a Hard Satisfiability Problem. Draft version (1995)"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L.T., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Design Automation Conference, DAC (2001)","DOI":"10.1145\/378239.379017"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-79719-7_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"V. Ryvchin","year":"2008","unstructured":"Ryvchin, V., Strichman, O.: Local Restarts. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 271\u2013276. Springer, Heidelberg (2008)"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11527695_25","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Berre Le","year":"2005","unstructured":"Le Berre, D., Simon, L.: Fifty-five solvers in vancouver: The SAT 2004 competition. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 321\u2013344. Springer, Heidelberg (2005)"},{"key":"29_CR9","unstructured":"Li, C.M.: Integrating Equivalency Reasoning into Davis-Putnam Procedure. In: AAAI-2000, Austin, Texas (2000)"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-540-24605-3_34","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Berre Le","year":"2004","unstructured":"Le Berre, D., Simon, L.: The essentials of the SAT 2003 competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 452\u2013467. Springer, Heidelberg (2004)"},{"key":"29_CR11","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/s10472-005-0431-7","volume":"43","author":"L. Simon","year":"2005","unstructured":"Simon, L., Le Berre, D., Hirsch, E.: The SAT 2002 competition. Annals of Mathematics and Artificial Intelligence (AMAI)\u00a043, 343\u2013378 (2005)","journal-title":"Annals of Mathematics and Artificial Intelligence (AMAI)"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"Velev, M., Bryant, R.: Effective use of Boolean Satisfiability Procedures in the Formal Verification Superscalar and VLIW Microprocessors. In: Design Automation Conferece, DAC (2001)","DOI":"10.1109\/DAC.2001.935509"},{"key":"29_CR13","unstructured":"E\u00e9n, N., S\u00f6r\u00e9nsson, N.: Minisat v2.0 (beta) solvers description, SAT-race (2006), http:\/\/minisat.se"},{"key":"29_CR14","unstructured":"Rsat SAT solver homepage, http:\/\/reasoning.cs.ucla.edu\/rsat\/"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/11527695_12","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Heule","year":"2005","unstructured":"Heule, M., Van Maaren, H.: Aligning CNF- and Equivalence-Reasoning. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 145\u2013156. Springer, Heidelberg (2005)"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-72788-0_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"M. Heule","year":"2007","unstructured":"Heule, M., Van Maaren, H.: Effective Incorporation of double look-ahead procedures. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 258\u2013271. Springer, Heidelberg (2007)"},{"key":"29_CR17","unstructured":"SAT 2007 Competition Homepage, http:\/\/www.satcompetition.org\/2007\/"},{"key":"29_CR18","unstructured":"Heule, M.: March: towards a look-ahead SAT solver for general purposes, Master thesis (2004)"},{"key":"29_CR19","unstructured":"Chen, J.C.: The SAT solver, MoRsat. In: SAT 2009 Competition (2009) (submitted)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T22:57:55Z","timestamp":1558393075000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}