{"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":1777125722685,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540278290","type":"print"},{"value":"9783540315803","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11527695_26","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T17:06:47Z","timestamp":1292864807000},"page":"345-359","source":"Crossref","is-referenced-by-count":23,"title":["March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver"],"prefix":"10.1007","author":[{"given":"Marijn","family":"Heule","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Dufour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joris","family":"van Zwieten","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"van Maaren","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Mitchel, D., Selmon, B., Levesque, H.: Hard and easy distributions of SAT problems. In: Proceedings of AIII 1992, pp. 459\u2013465 (1992)"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Le Berre, D.: Exploiting the Real Power of Unit Propagation Lookahead. In: LICS Workshop on Theory and Applications of Satisfiability Testing (2001)","DOI":"10.1016\/S1571-0653(04)00314-2"},{"key":"26_CR3","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":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"26_CR5","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. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"26_CR6","unstructured":"Dubois, O., Dequen, G.: A backbone-search heuristic for efficient solving of hard3-sat formulae. In: International Joint Conference on Artificial Intelligence 2001, vol.\u00a01, pp. 248\u2013253 (2001)"},{"key":"26_CR7","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.J.H. Heule","year":"2005","unstructured":"Heule, M.J.H., 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":"26_CR8","unstructured":"Kullmann, O.: Investigating the behaviour of a SAT solver on random formulas. In: Submitted to Annals of Mathematics and Artificial Intelligence (2002)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/BFb0017450","volume-title":"Principles and Practice of Constraint Programming - CP97","author":"C.M. Li","year":"1997","unstructured":"Li, C.M., Anbulagan: Look-Ahead versus Look-Back for Satisfiability Problems. In: Smolka, G. (ed.) CP 1997. LNCS, vol.\u00a01330, pp. 342\u2013356. Springer, Heidelberg (1997)"},{"issue":"2","key":"26_CR10","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/S0166-218X(02)00407-9","volume":"130","author":"C.M. Li","year":"2003","unstructured":"Li, C.M.: Equivalent literal propagation in the DLL procedure. The Renesse issue on satisfiability (2000). Discrete Appl. Math.\u00a0130(2), 251\u2013276 (2003)","journal-title":"The Renesse issue on satisfiability (2000). Discrete Appl. Math."},{"key":"26_CR11","unstructured":"Simon, L.: Competition homepage. In: Sat (2004), \n                    \n                      http:\/\/www.lri.fr\/~simon\/contest\/results\/"},{"key":"26_CR12","doi-asserted-by":"crossref","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. Accepted for publication in Annals of Mathematics and Artificial Intelligence (AMAI)\u00a043, 343\u2013378 (2005)","journal-title":"Accepted for publication in Annals of Mathematics and Artificial Intelligence (AMAI)"},{"issue":"3-5","key":"26_CR13","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/S0167-6377(98)00052-2","volume":"23","author":"J.P. Warners","year":"1998","unstructured":"Warners, J.P., van Maaren, H.: A two phase algorithm for solving a class of hard satisfiability problems. Oper. Res. Lett.\u00a023(3-5), 81\u201388 (1998)","journal-title":"Oper. Res. Lett."},{"key":"26_CR14","unstructured":"Zhang, H., Stickel, M.E.: Implementing the Davis-Putnam Method. In: SAT 2000, pp. 309\u2013326 (2000)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11527695_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T20:50:21Z","timestamp":1553287821000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11527695_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278290","9783540315803"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/11527695_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}