{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:21:51Z","timestamp":1725492111160},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439776"},{"type":"electronic","value":"9783540456438"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45643-0_3","type":"book-chapter","created":{"date-parts":[[2007,9,24]],"date-time":"2007-09-24T20:58:33Z","timestamp":1190667513000},"page":"29-42","source":"Crossref","is-referenced-by-count":13,"title":["A Compressed Breadth-First Search for Satisfiability"],"prefix":"10.1007","author":[{"given":"DoRon B.","family":"Motter","sequence":"first","affiliation":[]},{"given":"Igor L.","family":"Markov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,12]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"F. A. Aloul, I. L. Markov, and K. A. Sakallah. Faster SAT and Smaller BDDs via Common Function Structure. Proc. Intl. Conf. Computer-Aided Design, 2001.","DOI":"10.1109\/ICCAD.2001.968669"},{"key":"3_CR2","unstructured":"F. A. Aloul, M. Mneimneh, and K. A. Sakallah. Backtrack Search Using ZBDDs. Intl. Workshop on Logic and Synthesis, (IWLS), 2001."},{"key":"3_CR3","unstructured":"P. Beame and R. Karp. The efficiency of resolution and Davis-Putnam procedures. submitted for publication."},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"P. Chatalic and L. Simon. Multi-Resolution on Compressed Sets of Clauses. Proc. of 12th International Conference on Tools with Artificial Intelligence (ICTAI-2000), November 2000.","DOI":"10.1109\/TAI.2000.889839"},{"key":"3_CR5","unstructured":"P. Chatalic and L. Simon. ZRes: the old DP meets ZBDDs. Proc. of the 17th Conf. of Autom. Deduction (CADE), 2000."},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A Machine Program for Theorem Proving. Comm. ACM, 5:394\u2013397, 1962.","journal-title":"Comm. ACM"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. Jounal of the ACM, 7:201\u2013215, 1960.","journal-title":"Jounal of the ACM"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"P. Ferragina and G. Manzini. An experimental study of a compressed index. Proc. 12th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2001.","DOI":"10.1016\/S0020-0255(01)00098-6"},{"key":"3_CR9","series-title":"PhD thesis","volume-title":"Harnessing Computational Resources for Efficient Exhaustive Search","author":"R. Gasser","year":"1994","unstructured":"R. Gasser. Harnessing Computational Resources for Efficient Exhaustive Search. PhD thesis, Swiss Fed Inst Tech, Zurich, 1994."},{"key":"3_CR10","unstructured":"R. L. Graham, M. Gr\u00f6tschel, and L. Lov\u00e1sz, editors. Handbook of Combinatorics. MIT Press, January 1996."},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"J. F. Groote and H. Zantema. Resolution and binary decision diagrams cannot simulate each other polynomially. Technical Report UU-CS-2000-14, Utrecht University, 2000.","DOI":"10.1007\/3-540-45575-2_5"},{"key":"3_CR12","unstructured":"A. San Miguel. Random 3-SAT and BDDs: The Plot Thickens Further. CP, 2001."},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"S. Minato. Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems. 30th ACM\/IEEE DAC, 1993.","DOI":"10.1145\/157485.164890"},{"key":"3_CR14","unstructured":"A. Mishchenko. An Introduction to Zero-Suppressed Binary Decision Diagrams. http:\/\/www.ee.pdx.edu\/~alanmi\/research\/ ."},{"key":"3_CR15","unstructured":"A. Mishchenko. EXTRA v. 1.3: Software Library Extending CUDD Package: Release 2.3.x. http:\/\/www.ee.pdx.edu\/~alanmi\/research\/extra.htm ."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"M. Moskewicz et al. Chaff: Engineering an Efficient SAT Solver. Proc. of IEEE\/ACM DAC, pages 530\u2013535, 2001.","DOI":"10.1145\/378239.379017"},{"key":"3_CR17","unstructured":"J. P. Marques Silva and K. A. Sakallah. GRASP: A new search algorithm for satisfiability. ICCAD, 1996."},{"key":"3_CR18","unstructured":"F Somenzi. CUDD: CU Decision Diagram Package Release 2.3.1. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/cuddIntro.html ."},{"key":"3_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/BFb0016843","volume-title":"1st Intl. Conf. on Constraints in Comp. Logics","author":"T. E. Uribe","year":"1994","unstructured":"T. E. Uribe and M. E. Stickel. Ordered binary decision diagrams and the Davis-Putnam procedure. In J. P. Jouannaud, editor, 1st Intl. Conf. on Constraints in Comp. Logics, volume 845 of LNCS, pages 34\u201349. Springer, September 1994."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Urquhart. Hard examples for resolution. Journal of the ACM, 34, 1987.","DOI":"10.1145\/7531.8928"}],"container-title":["Lecture Notes in Computer Science","Algorithm Engineering and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45643-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T03:53:52Z","timestamp":1556855632000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45643-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439776","9783540456438"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45643-0_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}