{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T07:10:13Z","timestamp":1758265813183,"version":"3.41.0"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,9,12]],"date-time":"2019-09-12T00:00:00Z","timestamp":1568246400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000925","name":"John Templeton Foundation","doi-asserted-by":"publisher","award":["60842"],"award-info":[{"award-number":["60842"]}],"id":[{"id":"10.13039\/100000925","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["Doctoral Prize Fellowship Leroy Chew"],"award-info":[{"award-number":["Doctoral Prize Fellowship Leroy Chew"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Theory"],"published-print":{"date-parts":[[2019,12,31]]},"abstract":"<jats:p>Modern QBF solvers typically use two different paradigms, conflict-driven clause learning (CDCL) solving or expansion solving. Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of these solvers, with Q-Resolution and its extensions relating to CDCL solving and \u2200Exp+Res relating to expansion solving. This article defines two novel calculi, which are resolution-based and enable unification of some of the principal existing resolution-based QBF calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based calculus \u2200Exp+Res.<\/jats:p>\n          <jats:p>However, the proof complexity of the QBF resolution proof systems is currently not well understood. In this article, we completely determine the relative power of the main QBF resolution systems, settling in particular the relationship between the two different types of resolution-based QBF calculi: proof systems for CDCL-based solvers (Q-resolution, universal, and long-distance Q-resolution) and proof systems for expansion-based solvers (\u2200Exp+Res and its generalizations IR-calc and IRM-calc defined here).<\/jats:p>\n          <jats:p>The most challenging part of this comparison is to exhibit hard formulas that underlie the exponential separations of the aforementioned proof systems. To this end, we exhibit a new and elegant proof technique for showing lower bounds in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to lengths-of-proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for Q-resolution and universal Q-resolution. Variants of the formulas are hard for even stronger systems such as long-distance Q-resolution and extensions.<\/jats:p>\n          <jats:p>With a completely different and novel counting argument, we show the hardness of the prominent formulas of Kleine B\u00fcning et al. [51] for the strong expansion-based calculus IR-calc.<\/jats:p>","DOI":"10.1145\/3352155","type":"journal-article","created":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T12:28:56Z","timestamp":1568377736000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["New Resolution-Based QBF Calculi and Their Proof Complexity"],"prefix":"10.1145","volume":"11","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[{"name":"Institute of Computer Science, Friedrich Schiller University Jena, Germany"}]},{"given":"Leroy","family":"Chew","sequence":"additional","affiliation":[{"name":"School of Computing, University of Leeds, West Yorkshire, UK"}]},{"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[{"name":"IST\/INESC-ID, Universidade de Lisboa, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2019,9,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Sanjeev Arora and Boaz Barak. 2009. Computational Complexity -- A Modern Approach. Cambridge University Press. I--XXIV 1--579 pages.   Sanjeev Arora and Boaz Barak. 2009. Computational Complexity -- A Modern Approach. Cambridge University Press. I--XXIV 1--579 pages.","DOI":"10.1017\/CBO9780511804090"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.04.014"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0152-6"},{"volume-title":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. 3694--3701","year":"2015","author":"Balabanov Valeriy","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Valeriy Balabanov Magdalena Widl and Jie-Hong R. Jiang. 2014. QBF Resolution systems and their proof complexities. In SAT. 154--169.  Valeriy Balabanov Magdalena Widl and Jie-Hong R. Jiang. 2014. QBF Resolution systems and their proof complexities. In SAT. 154--169.","DOI":"10.1007\/978-3-319-09284-3_12"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_7_1","volume-title":"Franz Baader and Andrei Voronkov (Eds.)","volume":"3452","author":"Benedetti Marco","year":"2004"},{"key":"e_1_2_1_8_1","first-page":"1","article-title":"QBF-based formal verification: Experience and perspectives","volume":"5","author":"Benedetti Marco","year":"2008","journal-title":"JSAT"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Olaf Beyersdorff and Joshua Blinkhorn. 2016. Dependency schemes in QBF calculi: Semantics and soundness. In Principles and Practice of Constraint Programming - CP. 96--112.  Olaf Beyersdorff and Joshua Blinkhorn. 2016. Dependency schemes in QBF calculi: Semantics and soundness. In Principles and Practice of Constraint Programming - CP. 96--112.","DOI":"10.1007\/978-3-319-44953-1_7"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2840728.2840740"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44465-8_8"},{"volume-title":"Proc. Symposium on Theoretical Aspects of Computer Science (STACS). LIPIcs series, 76--89","year":"2015","author":"Beyersdorff Olaf","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","unstructured":"Olaf Beyersdorff Leroy Chew and Mikol\u00e1\u0161 Janota. 2016. Extension variables in QBF resolution. In Beyond NP Papers from the 2016 AAAI Workshop.  Olaf Beyersdorff Leroy Chew and Mikol\u00e1\u0161 Janota. 2016. Extension variables in QBF resolution. In Beyond NP Papers from the 2016 AAAI Workshop."},{"key":"e_1_2_1_14_1","unstructured":"Olaf Beyersdorff Leroy Chew Meena Mahajan and Anil Shukla. 2017. Feasible interpolation for QBF resolution calculi. Logical Methods in Computer Science 13 (2017). Issue 2.  Olaf Beyersdorff Leroy Chew Meena Mahajan and Anil Shukla. 2017. Feasible interpolation for QBF resolution calculi. Logical Methods in Computer Science 13 (2017). Issue 2."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3157053"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Olaf Beyersdorff Leroy Chew Renate A. Schmidt and Martin Suda. 2016. Lifting QBF resolution calculi to DQBF. In SAT.  Olaf Beyersdorff Leroy Chew Renate A. Schmidt and Martin Suda. 2016. Lifting QBF resolution calculi to DQBF. In SAT.","DOI":"10.1007\/978-3-319-40970-2_30"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2016.11.011"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2010.09.007"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2013.06.002"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499937.2499941"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933597"},{"key":"e_1_2_1_22_1","unstructured":"Armin Biere. 2004. Resolve and expand. In SAT. 238--246.  Armin Biere. 2004. Resolve and expand. In SAT. 238--246."},{"key":"e_1_2_1_23_1","volume-title":"Frontiers in Artificial Intelligence and Applications","volume":"185","author":"Biere Armin","year":"2009"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032276"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Uwe Bubeck and Hans Kleine B\u00fcning. 2007. Bounded universal expansion for preprocessing QBF. In Theory and Applications of Satisfiability Testing - SAT. 244--257.   Uwe Bubeck and Hans Kleine B\u00fcning. 2007. Bounded universal expansion for preprocessing QBF. In Theory and Applications of Satisfiability Testing - SAT. 244--257.","DOI":"10.1007\/978-3-540-72788-0_24"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.009"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087534"},{"key":"e_1_2_1_29_1","unstructured":"Leroy Chew. 2017. QBF Proof Complexity. Ph.D. Dissertation. University of Leeds.  Leroy Chew. 2017. QBF Proof Complexity. Ph.D. Dissertation. University of Leeds."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2018.05.005"},{"key":"e_1_2_1_31_1","unstructured":"Stephen A. Cook and Phuong Nguyen. 2010. Logical Foundations of Proof Complexity. Cambridge University Press.   Stephen A. Cook and Phuong Nguyen. 2010. Logical Foundations of Proof Complexity. Cambridge University Press."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Uwe Egly. 2016. On stronger calculi for QBFs. In SAT.  Uwe Egly. 2016. On stronger calculi for QBFs. In SAT.","DOI":"10.1007\/978-3-319-40970-2_26"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-016-9501-2"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Uwe Egly Florian Lonsing and Magdalena Widl. 2013. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving See McMillan et al. {57} 291--308.  Uwe Egly Florian Lonsing and Magdalena Widl. 2013. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving See McMillan et al. {57} 291--308.","DOI":"10.1007\/978-3-642-45221-5_21"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01744431"},{"key":"e_1_2_1_37_1","unstructured":"Enrico Giunchiglia Paolo Marin and Massimo Narizzano. 2009. Reasoning with quantified Boolean formulas. See Biere et al. {23} 761--780.  Enrico Giunchiglia Paolo Marin and Massimo Narizzano. 2009. Reasoning with quantified Boolean formulas. See Biere et al. {23} 761--780."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_9"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622559.1622569"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_8"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Alexandra Goultiaeva Martina Seidl and Armin Biere. 2013. Bridging the gap between dual propagation and CNF-based QBF solving. In Design Automation and Test in Europe DATE. 811--814.   Alexandra Goultiaeva Martina Seidl and Armin Biere. 2013. Bridging the gap between dual propagation and CNF-based QBF solving. In Design Automation and Test in Europe DATE. 811--814.","DOI":"10.7873\/DATE.2013.172"},{"key":"e_1_2_1_42_1","unstructured":"Alexandra Goultiaeva Allen Van Gelder and Fahiem Bacchus. 2011. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In IJCAI. 546--553.   Alexandra Goultiaeva Allen Van Gelder and Fahiem Bacchus. 2011. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In IJCAI. 546--553."},{"key":"e_1_2_1_43_1","unstructured":"Johan H\u00e5stad. 1987. Computational Limitations of Small-depth Circuits. MIT Press Cambridge MA.   Johan H\u00e5stad. 1987. Computational Limitations of Small-depth Circuits. MIT Press Cambridge MA."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9390-4"},{"key":"e_1_2_1_45_1","unstructured":"Mikol\u00e1\u0161 Janota. 2017. An Achilles\u2019 heel of term-resolution. CoRR abs\/1704.01071 (2017). https:\/\/arxiv.org\/abs\/1704.01071.  Mikol\u00e1\u0161 Janota. 2017. An Achilles\u2019 heel of term-resolution. CoRR abs\/1704.01071 (2017). https:\/\/arxiv.org\/abs\/1704.01071."},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Mikol\u00e1\u0161 Janota Radu Grigore and Joao Marques-Silva. 2013. On QBF proofs and preprocessing See McMillan et al. {57} 473--489.  Mikol\u00e1\u0161 Janota Radu Grigore and Joao Marques-Silva. 2013. On QBF proofs and preprocessing See McMillan et al. {57} 473--489.","DOI":"10.1007\/978-3-642-45221-5_32"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.01.004"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.01.048"},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Toni Jussila Armin Biere Carsten Sinz Daniel Kr\u00f6ning and Christoph M. Wintersteiger. 2007. A first step towards a unified proof checker for QBF. In Theory and Applications of Satisfiability Testing - SAT. 201--214.   Toni Jussila Armin Biere Carsten Sinz Daniel Kr\u00f6ning and Christoph M. Wintersteiger. 2007. A first step towards a unified proof checker for QBF. In Theory and Applications of Satisfiability Testing - SAT. 201--214.","DOI":"10.1007\/978-3-540-72788-0_21"},{"key":"e_1_2_1_50_1","unstructured":"Hans Kleine B\u00fcning and Uwe Bubeck. 2009. Theory of quantified Boolean formulas. See Biere et al. {23} 735--760.  Hans Kleine B\u00fcning and Uwe Bubeck. 2009. Theory of quantified Boolean formulas. See Biere et al. {23} 735--760."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1025"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9067-0"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_12"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275541"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_14"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_9"},{"key":"e_1_2_1_57_1","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan Aart Middeldorp and Andrei Voronkov (Eds.). 2013. Logic for Programming Artificial Intelligence and Reasoning LPAR. Springer.  Kenneth L. McMillan Aart Middeldorp and Andrei Voronkov (Eds.). 2013. Logic for Programming Artificial Intelligence and Reasoning LPAR. Springer.","DOI":"10.1007\/978-3-642-45221-5"},{"key":"e_1_2_1_58_1","unstructured":"Christos H. Papadimitriou. 1994. Computational Complexity. Addison-Wesley.  Christos H. Papadimitriou. 1994. Computational Complexity. Addison-Wesley."},{"key":"e_1_2_1_59_1","doi-asserted-by":"crossref","unstructured":"Tom\u00e1s Peitl Friedrich Slivovsky and Stefan Szeider. 2016. Long distance Q-resolution with dependency schemes. In SAT. 500--518.  Tom\u00e1s Peitl Friedrich Slivovsky and Stefan Szeider. 2016. Long distance Q-resolution with dependency schemes. In SAT. 500--518.","DOI":"10.1007\/978-3-319-40970-2_31"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"volume-title":"Proc. 11th Symposium on Discrete Algorithms. 128--136","year":"2000","author":"Pudl\u00e1k Pavel","key":"e_1_2_1_61_1"},{"key":"e_1_2_1_62_1","unstructured":"Jussi Rintanen. 2007. Asymptotically optimal encodings of conformant planning in QBF. In AAAI. AAAI Press 1045--1050.   Jussi Rintanen. 2007. Asymptotically optimal encodings of conformant planning in QBF. In AAAI. AAAI Press 1045--1050."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022607331053"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_36"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9114-5"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_33"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.10.020"},{"key":"e_1_2_1_70_1","doi-asserted-by":"crossref","unstructured":"Allen Van Gelder. 2011. Variable independence and resolution paths for quantified Boolean formulas. In Principles and Practice of Constraint Programming - CP. 789--803.   Allen Van Gelder. 2011. Variable independence and resolution paths for quantified Boolean formulas. In Principles and Practice of Constraint Programming - CP. 789--803.","DOI":"10.1007\/978-3-642-23786-7_59"},{"key":"e_1_2_1_71_1","volume-title":"Michela Milano (Ed.)","volume":"7514","author":"Gelder Allen Van","year":"2012"},{"key":"e_1_2_1_72_1","doi-asserted-by":"crossref","unstructured":"Allen Van Gelder. 2013. Primal and dual encoding from applications into quantified Boolean formulas. In CP. 694--707.  Allen Van Gelder. 2013. Primal and dual encoding from applications into quantified Boolean formulas. In CP. 694--707.","DOI":"10.1007\/978-3-642-40627-0_51"},{"key":"e_1_2_1_73_1","doi-asserted-by":"crossref","unstructured":"H. Vollmer. 1999. Introduction to Circuit Complexity -- A Uniform Approach. Springer Verlag Berlin.   H. Vollmer. 1999. Introduction to Circuit Complexity -- A Uniform Approach. Springer Verlag Berlin.","DOI":"10.1007\/978-3-662-03927-4"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/774572.774637"},{"key":"e_1_2_1_75_1","doi-asserted-by":"crossref","unstructured":"Lintao Zhang and Sharad Malik. 2002. Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In Principles and Practice of Constraint Programming - CP. 200--215. http:\/\/link.springer.de\/link\/service\/series\/0558\/bibs\/2470\/24700200.htm.   Lintao Zhang and Sharad Malik. 2002. Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In Principles and Practice of Constraint Programming - CP. 200--215. http:\/\/link.springer.de\/link\/service\/series\/0558\/bibs\/2470\/24700200.htm.","DOI":"10.1007\/3-540-46135-3_14"}],"container-title":["ACM Transactions on Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3352155","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3352155","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:26:15Z","timestamp":1750206375000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3352155"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,12]]},"references-count":75,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12,31]]}},"alternative-id":["10.1145\/3352155"],"URL":"https:\/\/doi.org\/10.1145\/3352155","relation":{},"ISSN":["1942-3454","1942-3462"],"issn-type":[{"type":"print","value":"1942-3454"},{"type":"electronic","value":"1942-3462"}],"subject":[],"published":{"date-parts":[[2019,9,12]]},"assertion":[{"value":"2018-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-09-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}