{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:50:45Z","timestamp":1725573045811},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540278290"},{"type":"electronic","value":"9783540315803"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11527695_12","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T17:06:47Z","timestamp":1292864807000},"page":"145-156","source":"Crossref","is-referenced-by-count":16,"title":["Aligning CNF- and Equivalence-Reasoning"],"prefix":"10.1007","author":[{"given":"Marijn","family":"Heule","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"van Maaren","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","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":"12_CR2","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":"12_CR3","unstructured":"Crawford, J.M., Kearns, M.J., Schapire, R.E.: The Minimal Disagreement parity problem as a hard satisfiability problem. Draft version (1995)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/11527695_26","volume-title":"Theory and Applications of Satisfiability Testing","author":"M.J.H. Heule","year":"2005","unstructured":"Heule, M.J.H., van Zwieten, J.E., Dufour, M., van Maaren, H.: March_eq, Implementing Efficiency and Additional Reasoning in a Look-ahead SAT Solver. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 345\u2013359. Springer, Heidelberg (2005)"},{"key":"12_CR5","unstructured":"Kullmann, O.: Investigating the behaviour of a SAT solver on random formulas. In: Submitted to Annals of Mathematics and Artificial Intelligence (2002)"},{"issue":"2","key":"12_CR6","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":"12_CR7","doi-asserted-by":"crossref","unstructured":"Simon, L., Le Berre, D., Hirsch, E.: The SAT 2002 competition. In: Accepted for publication in Annals of Mathematics and Artificial Intelligence (AMAI), vol.\u00a043, pp. 343\u2013378 (2005)","DOI":"10.1007\/s10472-004-9424-1"},{"key":"12_CR8","unstructured":"Simon, L.: Competition homepage. In: Sat 2003 (2003), http:\/\/www.lri.fr\/~simon\/contest03\/results\/"},{"key":"12_CR9","unstructured":"Simon, L.: Competition homepage. In: Sat 2004 (2004), http:\/\/www.lri.fr\/~simon\/contest\/results\/"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-46135-3_13","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"R. Ostrowski","year":"2002","unstructured":"Ostrowski, R., Gregoire, E., Mazure, B., Sais, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 185\u2013199. Springer, Heidelberg (2002)"},{"key":"12_CR11","unstructured":"Purdom, P., Sabry, A.: CNF Generator for Factoring Problems, http:\/\/www.cs.indiana.edu\/cgi-pub\/sabry\/cnf.htm"},{"issue":"3-5","key":"12_CR12","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."}],"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_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T06:11:57Z","timestamp":1559887917000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11527695_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278290","9783540315803"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/11527695_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}