{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T07:50:10Z","timestamp":1758268210292,"version":"3.41.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2020,2,10]],"date-time":"2020-02-10T00:00:00Z","timestamp":1581292800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100007569","name":"Carl-Zeiss-Stiftung","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100007569","id-type":"DOI","asserted-by":"crossref"}]},{"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"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Theory"],"published-print":{"date-parts":[[2020,6,30]]},"abstract":"<jats:p>\n            We aim to understand inherent reasons for lower bounds for QBF proof systems and revisit and compare two previous approaches in this direction. The first of these relates size lower bounds for strong QBF Frege systems to circuit lower bounds via\n            <jats:italic>strategy extraction<\/jats:italic>\n            (Beyersdorff and Pich, LICS\u201916). Here, we show a refined version of strategy extraction and thereby for any QBF proof system obtain a trichotomy for hardness: (1) via circuit lower bounds, (2) via propositional Resolution lower bounds, or (3) \u201cgenuine\u201d QBF lower bounds. The second approach tries to explain QBF lower bounds through\n            <jats:italic>quantifier alternations<\/jats:italic>\n            in a system called relaxing QU-Res (Chen, ACM TOCT 2017). We prove a strong lower bound for relaxing QU-Res, which at the same time exhibits significant shortcomings of that model. Prompted by this, we introduce a hierarchy of new systems that improve Chen\u2019s model and prove a strict separation for the complexity of proofs in this hierarchy. We show that lower bounds in our new model correspond to the trichotomy obtained via strategy extraction.\n          <\/jats:p>","DOI":"10.1145\/3378665","type":"journal-article","created":{"date-parts":[[2020,3,4]],"date-time":"2020-03-04T11:08:20Z","timestamp":1583320100000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Reasons for Hardness in QBF Proof Systems"],"prefix":"10.1145","volume":"12","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[{"name":"Institute of Computer Science, Friedrich Schiller University Jena, Germany"}]},{"given":"Luke","family":"Hinde","sequence":"additional","affiliation":[{"name":"School of Computing, University of Leeds, UK"}]},{"given":"J\u00e1n","family":"Pich","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, UK"}]}],"member":"320","published-online":{"date-parts":[[2020,2,10]]},"reference":[{"volume-title":"Proceedings of the Conference on Theory and Applications of Satisfiability Testing (SAT\u201914)","author":"Balabanov Valeriy","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700369156"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1410"},{"key":"e_1_2_1_4_1","first-page":"1","article-title":"QBF-based formal verification: Experience and perspectives","volume":"5","author":"Benedetti Marco","year":"2008","journal-title":"J. Sat. Boolean Model. Comput."},{"volume-title":"Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science (STACS\u201918)","year":"2018","author":"Beyersdorff Olaf","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","unstructured":"Olaf Beyersdorff Joshua Blinkhorn and Luke Hinde. 2019a. Size cost and capacity: A semantic technique for hard random QBFs. Logic. Methods Comput. Sci. 15 1 (2019).  Olaf Beyersdorff Joshua Blinkhorn and Luke Hinde. 2019a. Size cost and capacity: A semantic technique for hard random QBFs. Logic. Methods Comput. Sci. 15 1 (2019)."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2840728.2840740"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_2"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44465-8_8"},{"volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS\u201915)","year":"2015","author":"Beyersdorff Olaf","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","unstructured":"Olaf Beyersdorff Leroy Chew Meena Mahajan and Anil Shukla. 2017a. Feasible interpolation for QBF resolution calculi. Logic. Methods Comput. Sci. 13 (2017). Issue 2.  Olaf Beyersdorff Leroy Chew Meena Mahajan and Anil Shukla. 2017a. Feasible interpolation for QBF resolution calculi. Logic. Methods Comput. Sci. 13 (2017). Issue 2."},{"key":"e_1_2_1_12_1","first-page":"141","article-title":"Understanding cutting planes for QBFs. Info","volume":"262","author":"Beyersdorff Olaf","year":"2018","journal-title":"Comput."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Olaf Beyersdorff and Luke Hinde. 2019. Characterising tree-like frege proofs for QBF. Info. Comput. 268 (2019).  Olaf Beyersdorff and Luke Hinde. 2019. Characterising tree-like frege proofs for QBF. Info. Comput. 268 (2019).","DOI":"10.1016\/j.ic.2019.05.002"},{"volume-title":"Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201917)","year":"2017","author":"Beyersdorff Olaf","key":"e_1_2_1_14_1"},{"key":"e_1_2_1_15_1","first-page":"320","article-title":"Proof systems that take advice. Info","volume":"209","author":"Beyersdorff Olaf","year":"2011","journal-title":"Comput."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933597"},{"key":"e_1_2_1_17_1","unstructured":"A. Blake. 1937. Canonical Expressions in Boolean Algebra. Ph.D. Dissertation. University of Chicago.  A. Blake. 1937. Canonical Expressions in Boolean Algebra. Ph.D. Dissertation. University of Chicago."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.009"},{"key":"e_1_2_1_20_1","article-title":"Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness","volume":"9","author":"Chen Hubie","year":"2017","journal-title":"Trans. Comput. Theory"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-005-0282-2"},{"key":"e_1_2_1_22_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_23_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_9"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_26"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-016-9501-2"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01744431"},{"volume-title":"Handbook of Satisfiability","author":"Giunchiglia Enrico","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"volume-title":"Randomness and Computation, Advances in Computing Reasearch, Vol 5","author":"H\u00e5stad Johan","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.01.004"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.01.048"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2003.12.003"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_18"},{"key":"e_1_2_1_36_1","first-page":"12","article-title":"Resolution for quantified Boolean formulas. Info","volume":"117","author":"B\u00fcning Hans Kleine","year":"1995","journal-title":"Comput."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/225488"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19900360106"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98334-9_19"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_12"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_27"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_31"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2010.10.002"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200117"},{"volume-title":"Proceedings of the 22nd AAAI Conference on Artificial Intelligence. 1045--1050","year":"2007","author":"Rintanen Jussi","key":"e_1_2_1_46_1"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/11564751_43"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.10.020"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_47"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/774572.774637"}],"container-title":["ACM Transactions on Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3378665","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3378665","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:19Z","timestamp":1750200079000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3378665"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,10]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,6,30]]}},"alternative-id":["10.1145\/3378665"],"URL":"https:\/\/doi.org\/10.1145\/3378665","relation":{},"ISSN":["1942-3454","1942-3462"],"issn-type":[{"type":"print","value":"1942-3454"},{"type":"electronic","value":"1942-3462"}],"subject":[],"published":{"date-parts":[[2020,2,10]]},"assertion":[{"value":"2017-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-02-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}