{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:58:16Z","timestamp":1725533896082},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027765"},{"type":"electronic","value":"9783642027772"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_38","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T02:58:18Z","timestamp":1245985098000},"page":"412-426","source":"Crossref","is-referenced-by-count":11,"title":["Beyond CNF: A Circuit-Based QBF Solver"],"prefix":"10.1007","author":[{"given":"Alexandra","family":"Goultiaeva","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vicki","family":"Iverson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fahiem","family":"Bacchus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"38_CR1","unstructured":"Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: Proceedings of the AAAI National Conference (AAAI), pp. 1045\u20131050 (2007)"},{"key":"38_CR2","first-page":"417","volume-title":"Proceedings of the AAAI National Conference (AAAI)","author":"U. Egly","year":"2000","unstructured":"Egly, U., Eiter, T., Tompits, H., Woltran, S.: Solving advanced reasoning tasks using quantified boolean formulas. In: Proceedings of the AAAI National Conference (AAAI), pp. 417\u2013422. AAAI Press, Menlo Park (2000)"},{"key":"38_CR3","doi-asserted-by":"crossref","unstructured":"Mangassarian, H., Veneris, A.G., Safarpour, S., Benedetti, M., Smith, D.: A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test. In: International Conference on Computer-Aided Design (ICCAD), pp. 240\u2013245 (2007)","DOI":"10.1109\/ICCAD.2007.4397272"},{"key":"38_CR4","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"38_CR5","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"38_CR6","unstructured":"Benedetti, M.: sKizzo: a QBF decision procedure based on propositional skolemization and symbolic reasoning. Technical Report TR04-11-03 (2004)"},{"key":"38_CR7","doi-asserted-by":"crossref","unstructured":"Thiffault, C., Bacchus, F., Walsh, T.: Solving non-clausal formulas with DPLL search. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT) (2004)","DOI":"10.1007\/978-3-540-30201-8_48"},{"key":"38_CR8","doi-asserted-by":"crossref","unstructured":"Wu, C.A., Lin, T.H., Lee, C.C., Huang, C.Y.: QuteSAT: a robust circuit-based SAT solver for complex circuit structure. In: Design, Automation and Test in Europe Conference and Exposition (DATE), pp. 1313\u20131318 (2007)","DOI":"10.1109\/DATE.2007.364479"},{"key":"38_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/11814948_35","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"A. Sabharwal","year":"2006","unstructured":"Sabharwal, A., Ans\u00f3tegui, C., Gomes, C.P., Hart, J.W., Selman, B.: QBF modeling: Exploiting player symmetry for simplicity and efficiency. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 382\u2013395. Springer, Heidelberg (2006)"},{"key":"38_CR10","unstructured":"Zhang, L.: Solving QBF with combined conjunctive and disjunctive normal form. In: Proceedings of the AAAI National Conference (AAAI) (2006)"},{"key":"38_CR11","volume-title":"Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970","author":"G. Tseitin","year":"1983","unstructured":"Tseitin, G.: On the complexity of proofs in poropositional logics. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, vol.\u00a02. Springer, Heidelberg (1983); Originally published (1970)"},{"key":"38_CR12","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46135-3_14","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Van Hentenryck, P. (ed.) CP 2002, vol.\u00a02470, pp. 200\u2013215. Springer, Heidelberg (2002)"},{"key":"38_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/11814948_34","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"D. Tang","year":"2006","unstructured":"Tang, D., Malik, S.: Solving quantified boolean formulas with circuit observability don\u2019t cares. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 368\u2013381. Springer, Heidelberg (2006)"},{"key":"38_CR14","unstructured":"Benedetti, M., Lallouet, A., Vautard, J.: QCSP made practical by virtue of restricted quantification. In: Veloso, M.M. (ed.) Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), pp. 38\u201343 (2007)"},{"issue":"1","key":"38_CR15","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/s10601-008-9055-y","volume":"14","author":"U. Egly","year":"2009","unstructured":"Egly, U., Seidl, M., Woltran, S.: A solver for QBFs in negation normal form. Constraints\u00a014(1), 38\u201379 (2009)","journal-title":"Constraints"},{"key":"38_CR16","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas satisfiability library (QBFLIB) (2001), \n                    \n                      www.qbflib.org"},{"key":"38_CR17","unstructured":"St\u00e9phan, I.: Boolean propagation based on literals for quantified boolean formulae. In: 17th European Conference on Artificial Intelligence (2006)"},{"key":"38_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: skizzo: A suite to evaluate and certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"38_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-72788-0_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"H. Samulowitz","year":"2007","unstructured":"Samulowitz, H., Bacchus, F.: Dynamically partitioning for solving QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 215\u2013229. Springer, Heidelberg (2007)"},{"key":"38_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/3-540-45744-5_27","volume-title":"Automated Reasoning","author":"E. Giunchiglia","year":"2001","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QUBE: A system for deciding Quantified Boolean Formulas satisfiability. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol.\u00a02083, pp. 364\u2013369. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T19:19:58Z","timestamp":1552072798000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}