{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:50:03Z","timestamp":1725475803283},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_35","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"449-454","source":"Crossref","is-referenced-by-count":21,"title":["ZRes: The Old Davis\u2013Putnam Procedure Meets ZBDD"],"prefix":"10.1007","author":[{"given":"Philippe","family":"Chatalic","sequence":"first","affiliation":[]},{"given":"Laurent","family":"Simon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"8","key":"35_CR1","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph - based algorithms for boolean function manipulation. IEEE Trans. on Comp.\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. on Comp."},{"key":"35_CR2","unstructured":"Chatalic, P., Simon, L.: Davis and putnam 40 years later: a first experimentation. Technical Report 1237, LRI, Orsay, France (2000), submitted to the Journal of Automated Reasoning"},{"key":"35_CR3","doi-asserted-by":"crossref","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM, 201\u2013215 (1960)","DOI":"10.1145\/321033.321034"},{"key":"35_CR4","unstructured":"de Kleer, J.: An improved incremental algorithm for generating prime implicates. In: AAAI 1992, pp. 780\u2013785 (1992)"},{"key":"35_CR5","doi-asserted-by":"crossref","unstructured":"Dechter, R., Rish, I.: Directional resolution: The Davis\u2013Putnam procedure, revisited. In: Proceedings of KR 1994, pp. 134\u2013145 (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50109-3"},{"key":"35_CR6","unstructured":"The DIMACS challenge benchmarks, ftp:\/\/ftp.rutgers.dimacs.edu\/challenges\/sat"},{"key":"35_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2892-7","volume-title":"Binary Decision Diagram: Theory and Implementation","author":"R. Drechsler","year":"1998","unstructured":"Drechsler, R., Becker, B.: Binary Decision Diagram: Theory and Implementation. Kluwer Academic Publisher, Dordrecht (1998)"},{"key":"35_CR8","unstructured":"Dubois, O.: Can a very simple algorithm be efficient for SAT?, ftp:\/\/ftp.dimacs.rutgers.edu\/pub\/challenges\/sat\/contributed\/dubois"},{"key":"35_CR9","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/0304-3975(77)90054-8","volume":"4","author":"Z. Galil","year":"1977","unstructured":"Galil, Z.: On the complexity of regular resolution and the Davis\u2013Putnam procedure. Theorical Computer Science\u00a04, 23\u201346 (1977)","journal-title":"Theorical Computer Science"},{"key":"35_CR10","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theorical Computer Science\u00a039, 297\u2013308 (1985)","journal-title":"Theorical Computer Science"},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"Logeman, G., Davis, M., Loveland, D.: A machine program for theorem-proving. Communications of the ACM, 394\u2013397 (1962)","DOI":"10.1145\/368273.368557"},{"key":"35_CR12","doi-asserted-by":"crossref","unstructured":"Minato, S.: Zero-suppressed bdds for set manipulation in combinatorial problems. In: 30th ACM\/IEEE Design Automation Conference (1993)","DOI":"10.1145\/157485.164890"},{"key":"35_CR13","unstructured":"Somenzy, F.: Cudd release 2.3.0., http:\/\/bessie.colorado.edu\/~fabio"},{"key":"35_CR14","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. Journal of the ACM\u00a034, 209\u2013219 (1987)","journal-title":"Journal of the ACM"},{"key":"35_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:42:44Z","timestamp":1556019764000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/10721959_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}