{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T05:58:30Z","timestamp":1763704710843},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642237850"},{"type":"electronic","value":"9783642237867"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-23786-7_51","type":"book-chapter","created":{"date-parts":[[2011,8,31]],"date-time":"2011-08-31T07:58:42Z","timestamp":1314777522000},"page":"675-690","source":"Crossref","is-referenced-by-count":9,"title":["A More Efficient BDD-Based QBF Solver"],"prefix":"10.1007","author":[{"given":"Oswaldo","family":"Olivo","sequence":"first","affiliation":[]},{"given":"E. Allen","family":"Emerson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"51_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: Faster SAT and Smaller BDDs via Common Function Structure. In: Technical Report #CSE-TR-445-01. University of Michigan (2001)","DOI":"10.1109\/ICCAD.2001.968669"},{"key":"51_CR2","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/ICTAI.2004.106","volume-title":"16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI)","author":"G. Audemard","year":"2004","unstructured":"Audemard, G., Sas, L.: SAT Based BDD Solver for Quantified Boolean Formulas. In: 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pp. 82\u201389. IEEE Computer Society, Los Alamitos (2004)"},{"key":"51_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/10722167_11","volume-title":"Computer Aided Verification","author":"A. Ayari","year":"2000","unstructured":"Ayari, A., Basin, D.: Bounded Model Construction for Monadic Second-Order Logics. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 99\u2013113. Springer, Heidelberg (2000)"},{"key":"51_CR4","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Evaluating QBFs via Symbolic Skolemization. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, Springer, Heidelberg (2005)"},{"key":"51_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. J. Adv. Comp. Sci.\u00a058 (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"51_CR6","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, 677\u2013691 (1986)","journal-title":"IEEE Trans. on Comp."},{"key":"51_CR7","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1109\/LICS.1990.113767","volume-title":"Fifth Annual IEEE Symposium on Logic in Computer Science","author":"J.R. Burch","year":"1990","unstructured":"Burch, J.R., Clarke, E.M., Mcmillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 10 20 States and Beyond. In: Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 428\u2013439. IEEE Comput. Soc. Press, Los Alamitos (1990)"},{"key":"51_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/10721959_35","volume-title":"Automated Deduction - CADE-17","author":"P. Chatalic","year":"2000","unstructured":"Chatalic, P., Simon, L.: Zres:The old Davis-Putnam procedure meets ZBDDs. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831, pp. 449\u2013454. Springer, Heidelberg (2000)"},{"key":"51_CR9","first-page":"126","volume-title":"IEEE International Conference on Computer-Aided Design (ICCAD)","author":"O. Coudert","year":"1990","unstructured":"Coudert, O., Madre, J.C.: A Unified Framework for the Formal Verification of Sequential Circuits. In: IEEE International Conference on Computer-Aided Design (ICCAD), pp. 126\u2013129. IEEE, Los Alamitos (1990)"},{"key":"51_CR10","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"99","volume-title":"Handbook of Satisfiability","author":"A. Darwiche","year":"2009","unstructured":"Darwiche, A., Pipatsrisawat, K.: Complete Algorithms. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, pp. 99\u2013130. IOS Press, Amsterdam (2009)"},{"key":"51_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, M.: A computing procedure for quantification theory. J. ACM\u00a07, 201\u2013215 (1960)","journal-title":"J. ACM"},{"issue":"7","key":"51_CR12","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. Commun. ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"51_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-24605-3_30","volume-title":"Theory and Applications of Satisfiability Testing","author":"J. Franco","year":"2004","unstructured":"Franco, J., Kouril, M., Schlipf, J.S., Ward, J., Weaver, S., Dransfield, M., Vanfleet, W.M.: SBSAT: A State-Based, BDD-Based Satisfiability Solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 398\u2013410. Springer, Heidelberg (2004)"},{"key":"51_CR14","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A., Tacchella, O.: QUBE: A system for deciding Quantified Boolean Formulas Satisfiability. In: IJCAR, pp. 364\u2013369 (2001)","DOI":"10.1007\/3-540-45744-5_27"},{"key":"51_CR15","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"99","volume-title":"Handbook of Satisfiability","author":"E. Giunchiglia","year":"2009","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: QBF Reasoning. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, pp. 99\u2013130. IOS Press, Amsterdam (2009)"},{"key":"51_CR16","doi-asserted-by":"crossref","unstructured":"Huang, J., Darwiche, A.: Toward good elimination orders for symbolic SAT solving. In: 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pp. 566\u2013573 (2004)","DOI":"10.1109\/ICTAI.2004.115"},{"key":"51_CR17","doi-asserted-by":"crossref","unstructured":"Jin, H., Somenzi, F.: CirCUs: A hybrid satisfiability solver. In: International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 211\u2013223 (2004)","DOI":"10.1007\/11527695_17"},{"key":"51_CR18","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"99","volume-title":"Handbook of Satisfiability","author":"H. Kleine","year":"2009","unstructured":"Kleine, H., Bubeck, U.: QBF Theory. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, pp. 99\u2013130. IOS Press, Amsterdam (2009)"},{"key":"51_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"51_CR20","first-page":"71","volume":"7","author":"F. Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: A Dependency-Aware QBF Solver. J. Sat, Bool. Mod. and Comp.\u00a07, 71\u201376 (2010)","journal-title":"J. Sat, Bool. Mod. and Comp."},{"key":"51_CR21","unstructured":"Narizzano, M.: QBFLIB, The Quantified Boolean Formulas Satisfiability Library, http:\/\/www.qbflib.org\/"},{"key":"51_CR22","unstructured":"Olivo, O., Emerson, E.A.: A More Efficient BDD-Based QBF Solver. In: Tech Report, http:\/\/www.cs.utexas.edu\/~olivo\/CP\/More_Efficient_BDD_QBF_Tech_Report.pdf"},{"key":"51_CR23","doi-asserted-by":"crossref","unstructured":"Pigorsch, F., Schol, C.: Exploiting structure in an AIG based QBF solver. In: Proc. of DATE 2009 (2009) (to appear)","DOI":"10.1109\/DATE.2009.5090919"},{"key":"51_CR24","doi-asserted-by":"crossref","unstructured":"Plaisted, D.A., Biere, A., Zhu, Y.: A satisfiability procedure for quantified boolean formulae. J. Disc. App. Math.\u00a0130(2) (2003)","DOI":"10.1016\/S0166-218X(02)00409-2"},{"key":"51_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-540-74970-7_41","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"L. Pulina","year":"2007","unstructured":"Pulina, L., Tacchella, A.: A multi-engine solver for quantified Boolean formulas. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 574\u2013589. Springer, Heidelberg (2007)"},{"key":"51_CR26","unstructured":"Ranjan, R.K., Aziz, A., Brayton, R.K., Plessier, B., Pixley, C.: Efficient BDD Algorithms for FSM Synthesis and Verification. In: IEEE\/ACM Proceedings International Workshop on Logic Synthesis. IEEE\/ACM (1995)"},{"key":"51_CR27","first-page":"323","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"Rintanen, J.: Constructing conditional plans by a theorem prover. J. A.I.\u00a010, 323\u2013352 (1999)","journal-title":"J. A.I."},{"key":"51_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/11753728_60","volume-title":"Computer Science \u2013 Theory and Applications","author":"C. Sinz","year":"2006","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol.\u00a03967, pp. 600\u2013611. Springer, Heidelberg (2006)"},{"key":"51_CR29","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package, http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2013 CP 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23786-7_51","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,14]],"date-time":"2019-06-14T16:36:51Z","timestamp":1560530211000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23786-7_51"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642237850","9783642237867"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23786-7_51","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}