{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T22:52:59Z","timestamp":1648594379043},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2005,5]]},"DOI":"10.1007\/s10472-004-8427-2","type":"journal-article","created":{"date-parts":[[2005,4,15]],"date-time":"2005-04-15T10:22:01Z","timestamp":1113560521000},"page":"121-156","source":"Crossref","is-referenced-by-count":3,"title":["Resolution cannot polynomially simulate compressed-BFS"],"prefix":"10.1007","volume":"44","author":[{"given":"DoRon B.","family":"Motter","sequence":"first","affiliation":[]},{"given":"Jarrod A.","family":"Roy","sequence":"additional","affiliation":[]},{"given":"Igor L.","family":"Markov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"F. Aloul, I. Markov and K. Sakallah, Faster SAT and smaller BDDs via common function structure, in: Proc. Intl. Conf. Computer-Aided Design (2001).","DOI":"10.1109\/ICCAD.2001.968669"},{"key":"CR2","unstructured":"F. Aloul, M. Mneimneh and K. Sakallah, Backtrack search using ZBDDs, in: Intl. Workshop on Logic and Synthesis (IWLS) (2001)."},{"issue":"9","key":"CR3","doi-asserted-by":"crossref","first-page":"1117","DOI":"10.1109\/TCAD.2003.816218","volume":"22","author":"F. Aloul","year":"2003","unstructured":"F. Aloul, A. Ramani, I. Markov and K. Sakallah, Solving difficult instances of Boolean satisfiability in the presence of symmetry, IEEE Trans. on CAD 22(9) (2003) 1117?1137.","journal-title":"IEEE Trans. on CAD"},{"key":"CR4","unstructured":"P. Beame, H. Kautz and A. Sabharwal, Understanding the power of clause learning, in: Proc. of the 18th International Joint Conference on Artificial Intelligence (IJCAI-2003) (Morgan Kaufman, 2003)."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"P. Bjesse, G. Andersson, B. Cook and Z. Hanna, A proof engine approach to solving combinational design automation problems, in: Proc. IEEE\/ACM Design Automation Conference (2002).","DOI":"10.1145\/513918.514101"},{"key":"CR6","unstructured":"J. Bondy, Basic graph theory: paths and circuits, in: Handbook of Combinatorics, Vol. I (1995) p. 34."},{"key":"CR7","unstructured":"M. Cassatt, http:\/\/www.ibiblio.org\/wm\/paint\/auth\/cassatt\/."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"P. Chatalic and L. Simon, Multi-resolution on compressed sets of clauses, in: Proc. of 12th International Conference on Tools with Artificial Intelligence (ICTAI-2000) (November 2000).","DOI":"10.1109\/TAI.2000.889839"},{"key":"CR9","unstructured":"P. Chatalic and L. Simon, ZRes: the old DP meets ZBDDs, in: Proc. of the 17th Conf. of Autom. Deduction (CADE) (2000)."},{"key":"CR10","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0167-9260(94)00007-7","volume":"17","author":"O. Coudert","year":"1994","unstructured":"O. Coudert, Two-level logic minimization: an overview, Integration, the VLSI Journal 17 (1994) 97?140.","journal-title":"Integration, the VLSI Journal"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"O. Coudert, Solving graph optimization problems with ZBDDs, in: Proc. of the 1997 European Design and Test Conference (1997).","DOI":"10.1109\/EDTC.1997.582363"},{"key":"CR12","doi-asserted-by":"crossref","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. of the ACM 5 (1962) 394?397.","journal-title":"Comm. of the ACM"},{"key":"CR13","doi-asserted-by":"crossref","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, Journal of the ACM 7 (1960) 201?215.","journal-title":"Journal of the ACM"},{"key":"CR14","unstructured":"H. Dixon and M. Ginsberg, Inference methods for a pseudo-Boolean satifiability solver, in: Proc. of the 18th National Conference on Artificial Intelligence (AAAI-2002) (2002)."},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"P. Ferragina and G. Manzini, An experimental study of a compressed index, in: Proc. of 12th ACM?SIAM Symposium on Discrete Algorithms (SODA) (2001).","DOI":"10.1016\/S0020-0255(01)00098-6"},{"key":"CR16","volume-title":"Computers and Intractibility: A Guide to the Theory of NP-Completeness","author":"M. Garey","year":"2000","unstructured":"M. Garey and D. Johnson, Computers and Intractibility: A Guide to the Theory of NP-Completeness (Freeman, New York, 2000)."},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"J. 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":"CR18","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"A. Haken, The intractability of resolution, Theoretical Computer Science 39 (1985) 297?308.","journal-title":"Theoretical Computer Science"},{"key":"CR19","unstructured":"V. Kann, A compendium of NP optimization problems, http:\/\/www.nada.kth.se\/~viggo\/wwwcompendium\/node56.html."},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"O. Kullmann, Investigations on autark assignments, in: DAMATH: Discrete Applied Mathematics and Combinatorial Operations Research and Computer Science, Vol. 107 (2000).","DOI":"10.1016\/S0166-218X(00)00262-6"},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"J. Marques-Silva and K. Sakallah, GRASP: a new search algorithm for satisfiability, in: Proc. Intl. Conf. Computer-Aided Design (1996).","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"S. Minato, Zero-suppressed BDDs for set manipulation in combinatorial problems, in: Proc. of 30th ACM\/IEEE DAC (1993).","DOI":"10.1145\/157485.164890"},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"S. Minato, Representations of Discrete Functions (Kluwer Academic, 1996) pp. 1?26.","DOI":"10.1007\/978-1-4613-1385-4_1"},{"key":"CR24","unstructured":"A. Mishchenko, An introduction to zero-suppressed binary decision diagrams, http:\/\/www.ee.pdx.edu\/~alanmi\/research\/."},{"key":"CR25","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":"CR26","doi-asserted-by":"crossref","unstructured":"M. Moskewicz et al., Chaff: engineering an efficient SAT solver, in: Proc. of IEEE\/ACM Design Automation Conference (2001) pp. 530?535.","DOI":"10.1145\/378239.379017"},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"D. Motter and I. Markov, A compressed breadth-first search for satisfiability, in: Proc. 4th Workshop on Algorithm Engineering and Experiments (2002).","DOI":"10.1007\/3-540-45643-0_3"},{"key":"CR28","unstructured":"L. Simon, D. LeBerre and E. Hirsch, The SAT2002 competition, http:\/\/www.satlive.org\/SATCompetition\/2002\/onlinereport\/index.html."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-004-8427-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-004-8427-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-004-8427-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T22:12:16Z","timestamp":1586211136000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-004-8427-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5]]},"references-count":28,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2005,5]]}},"alternative-id":["5379427"],"URL":"https:\/\/doi.org\/10.1007\/s10472-004-8427-2","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,5]]}}}