{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T05:06:06Z","timestamp":1777957566637,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642452208","type":"print"},{"value":"9783642452215","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_21","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T09:28:23Z","timestamp":1386235703000},"page":"291-308","source":"Crossref","is-referenced-by-count":29,"title":["Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Magdalena","family":"Widl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_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":"21_CR2","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An Algorithm to Evaluate Quantified Boolean Formulae. In: AAAI\/IAAI (1998)"},{"issue":"7","key":"21_CR3","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.W.: A Machine Program for Theorem-Proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"21_CR4","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","volume":"26","author":"E. Giunchiglia","year":"2006","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause\/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas. Journal of Artificial Intelligence Research\u00a026, 371\u2013416 (2006)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-39071-5_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"A. Goultiaeva","year":"2013","unstructured":"Goultiaeva, A., Bacchus, F.: Recovering and Utilizing Partial Duality in QBF. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 83\u201399. Springer, Heidelberg (2013)"},{"key":"21_CR6","unstructured":"Goultiaeva, A., Van Gelder, A., Bacchus, F.: A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas. In: 22nd International Joint Conference on Artificial Intelligence (IJCAI), pp. 546\u2013553. AAAI Press (2011)"},{"issue":"1","key":"21_CR7","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":"21_CR8","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":"21_CR9","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":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39071-5_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"F. Lonsing","year":"2013","unstructured":"Lonsing, F., Egly, U., Van Gelder, A.: Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 100\u2013115. Springer, Heidelberg (2013)"},{"key":"21_CR11","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":"21_CR12","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":"21_CR13","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":"21_CR14","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":"21_CR15","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict Driven Learning in a Quantified Boolean Satisfiability Solver. In: 2002 IEEE\/ACM International Conference on Computer-Aided Design, pp. 442\u2013449 (2002)","DOI":"10.1145\/774572.774637"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","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. LNCS, vol.\u00a02470, pp. 200\u2013215. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-45221-5_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T02:08:15Z","timestamp":1746065295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}