{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T20:56:10Z","timestamp":1772830570172,"version":"3.50.1"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319092836","type":"print"},{"value":"9783319092843","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_12","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T09:43:21Z","timestamp":1404294201000},"page":"154-169","source":"Crossref","is-referenced-by-count":40,"title":["QBF Resolution Systems and Their Proof Complexities"],"prefix":"10.1007","author":[{"given":"Valeriy","family":"Balabanov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Magdalena","family":"Widl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie-Hong R.","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V. Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.-H.R.: Unified QBF Certification and Its Applications. Formal Methods in System Design\u00a041, 45\u201365 (2012)","journal-title":"Formal Methods in System Design"},{"key":"12_CR2","series-title":"Lecture Notes in Artificial Intelligence","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 (LNAI), vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"12_CR3","unstructured":"Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification, http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11499107_32","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Dershowitz","year":"2005","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded Model Checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 408\u2013414. Springer, Heidelberg (2005)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-Solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-45221-5_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"U. Egly","year":"2013","unstructured":"Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol.\u00a08312, pp. 291\u2013308. Springer, Heidelberg (2013)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-30494-4_15","volume-title":"Formal Methods in Computer-Aided Design","author":"E. Giunchiglia","year":"2004","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE++: An Efficient QBF Solver. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 201\u2013213. Springer, Heidelberg (2004)"},{"key":"12_CR8","unstructured":"Goultiaeva, A., Van Gelder, A., Bacchus, F.: A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 546\u2013553. AAAI Press (2011)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M. Janota","year":"2012","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with Counterexample Guided Refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 114\u2013128. Springer, Heidelberg (2012)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Jiang, J.-H.R., Lin, H.-P., Hung, W.-L.: Interpolating Functions from Large Boolean Relations. In: Proc. International Conference on Computer-Aided Design (ICCAD), pp. 779\u2013784. IEEE\/ACM (2009)","DOI":"10.1145\/1687399.1687544"},{"issue":"1","key":"12_CR11","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine B\u00fcning","year":"1995","unstructured":"Kleine B\u00fcning, H., Karpinski, M., Fl\u00f6gel, A.: Resolution for Quantified Boolean Formulas. Information and Computation\u00a0117(1), 12\u201318 (1995)","journal-title":"Information and Computation"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Lai, C.-F., Jiang, J.-H.R., Wang, K.-H.: BooM: A Decision Procedure for Boolean Matching with Abstraction and Dynamic Learning. In: Design Automation Conference (DAC), pp. 499\u2013504. ACM\/IEEE (2010)","DOI":"10.1145\/1837274.1837398"},{"key":"12_CR13","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3233\/SAT190077","volume":"7","author":"F. Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: A Dependency-Aware QBF Solver (System Description). Journal on Satisfiability, Boolean Modeling and Computation\u00a07, 71\u201376 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-Driven Clause Learning SAT Solvers. In: Handbook of Satisfiability, pp. 131\u2013153. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"12_CR15","unstructured":"Rintanen, J.: Asymptotically Optimal Encodings of Conformant Planning in QBF. In: National Conference on Artificial Intelligence (AAAI), pp. 1045\u20131050. AAAI Press (2007)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-72788-0_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"S. Staber","year":"2007","unstructured":"Staber, S., Bloem, R.: Fault localization and correction with QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 355\u2013368. Springer, Heidelberg (2007)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/11499107_21","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Gelder Van","year":"2005","unstructured":"Van Gelder, A.: Input Distance and Lower Bounds for Propositional Resolution Proof Length. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 282\u2013293. Springer, Heidelberg (2005)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/978-3-642-33558-7_47","volume-title":"Principles and Practice of Constraint Programming","author":"A. Gelder Van","year":"2012","unstructured":"Van Gelder, A.: Contributions to the Theory of Practical Quantified Boolean Formula Solving. In: Milano, M. (ed.) CP 2012. LNCS, vol.\u00a07514, pp. 647\u2013663. Springer, Heidelberg (2012)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict Driven Learning in a Quantified Boolean Satisfiability Solver. In: Proc. International Conference on Computer-Aided Design (ICCAD), pp. 442\u2013449. ACM (2002)","DOI":"10.1145\/774572.774637"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-45657-0_2","volume-title":"Computer Aided Verification","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The Quest for Efficient Boolean Satisfiability Solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 17\u201336. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:52:01Z","timestamp":1746291121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}