{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,12]],"date-time":"2026-05-12T03:57:46Z","timestamp":1778558266439,"version":"3.51.4"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,9,18]],"date-time":"2017-09-18T00:00:00Z","timestamp":1505692800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Basque Government Project","award":["S-PE12UN050(SAI12\/219)"],"award-info":[{"award-number":["S-PE12UN050(SAI12\/219)"]}]},{"DOI":"10.13039\/501100003451","name":"University of the Basque Country","doi-asserted-by":"crossref","award":["UFI11\/45"],"award-info":[{"award-number":["UFI11\/45"]}],"id":[{"id":"10.13039\/501100003451","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Spanish Project FORMALISM","award":["TIN2007-66523"],"award-info":[{"award-number":["TIN2007-66523"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Theory"],"published-print":{"date-parts":[[2017,9,30]]},"abstract":"<jats:p>\n            We present and study a framework in which one can present alternation-based lower bounds on proof length in proof systems for quantified Boolean formulas. A key notion in this framework is that of\n            <jats:italic>proof system ensemble<\/jats:italic>\n            , which is (essentially) a sequence of proof systems where, for each, proof checking can be performed in the polynomial hierarchy. We introduce a proof system ensemble called\n            <jats:italic>relaxing QU-res<\/jats:italic>\n            that is based on the established proof system\n            <jats:italic>QU-resolution<\/jats:italic>\n            . Our main results include an exponential separation of the treelike and general versions of relaxing QU-res and an exponential lower bound for relaxing QU-res; these are analogs of classical results in propositional proof complexity.\n          <\/jats:p>","DOI":"10.1145\/3087534","type":"journal-article","created":{"date-parts":[[2017,9,18]],"date-time":"2017-09-18T12:20:54Z","timestamp":1505737254000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Proof Complexity Modulo the Polynomial Hierarchy"],"prefix":"10.1145","volume":"9","author":[{"given":"Hubie","family":"Chen","sequence":"first","affiliation":[{"name":"Universidad del Pa\u00ed Vasco and IKERBASQUE, Basque Foundation for Science, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,9,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2016945.2016955"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911)","author":"Balabanov Valeriy","unstructured":"Valeriy Balabanov and Jie-Hong R. Jiang . 2011. Resolution proofs and skolem functions in QBF evaluation and applications . In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911) . 149--164. Valeriy Balabanov and Jie-Hong R. Jiang. 2011. Resolution proofs and skolem functions in QBF evaluation and applications. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911). 149--164."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201914)","author":"Balabanov Valeriy","unstructured":"Valeriy Balabanov , Magdalena Widl , and Jie-Hong R. Jiang . 2014. QBF resolution systems and their proof complexities . In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201914) . 154--169. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. 2014. QBF resolution systems and their proof complexities. In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201914). 154--169."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1410"},{"key":"e_1_2_1_5_1","first-page":"66","article-title":"Propositional proof complexity: Past, present and future","volume":"65","author":"Beame Paul","year":"1998","unstructured":"Paul Beame and Toniann Pitassi . 1998 . Propositional proof complexity: Past, present and future . Bull. EATCS 65 (1998), 66 -- 89 . Paul Beame and Toniann Pitassi. 1998. Propositional proof complexity: Past, present and future. Bull. EATCS 65 (1998), 66--89.","journal-title":"Bull. EATCS"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00493-004-0036-5"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_27"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44465-8_8"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science (STACS\u201915)","author":"Beyersdorff Olaf","year":"2015","unstructured":"Olaf Beyersdorff , Leroy Chew , and Mikol\u00e1s Janota . 2015 . Proof complexity of resolution-based QBF calculi . In Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science (STACS\u201915) . 76--89. Olaf Beyersdorff, Leroy Chew, and Mikol\u00e1s Janota. 2015. Proof complexity of resolution-based QBF calculi. In Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science (STACS\u201915). 76--89."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201916)","author":"Beyersdorff Olaf","unstructured":"Olaf Beyersdorff , Leroy Chew , Meena Mahajan , and Anil Shukla . Understanding cutting planes for QBFs . In Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201916) . Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding cutting planes for QBFs. In Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201916)."},{"key":"e_1_2_1_12_1","volume-title":"A game characterisation of tree-like Q-resolution size. Electronic Colloquium on Computational Complexity (ECCC)","author":"Beyersdorff Olaf","year":"2014","unstructured":"Olaf Beyersdorff , Leroy Chew , and Karteek Sreenivasaiah . 2014. A game characterisation of tree-like Q-resolution size. Electronic Colloquium on Computational Complexity (ECCC) ( 2014 ). Olaf Beyersdorff, Leroy Chew, and Karteek Sreenivasaiah. 2014. A game characterisation of tree-like Q-resolution size. Electronic Colloquium on Computational Complexity (ECCC) (2014)."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933597"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1025"},{"key":"e_1_2_1_16_1","volume-title":"Beyond Q-resolution and prenex form: A proof system for quantified constraint satisfaction. Logical Methods Comput. Sci. 10, 4","author":"Chen Hubie","year":"2014","unstructured":"Hubie Chen . 2014. Beyond Q-resolution and prenex form: A proof system for quantified constraint satisfaction. Logical Methods Comput. Sci. 10, 4 ( 2014 ). Hubie Chen. 2014. Beyond Q-resolution and prenex form: A proof system for quantified constraint satisfaction. Logical Methods Comput. Sci. 10, 4 (2014)."},{"key":"e_1_2_1_17_1","volume-title":"Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. CoRR abs\/1410.5369","author":"Chen Hubie","year":"2014","unstructured":"Hubie Chen . 2014. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. CoRR abs\/1410.5369 ( 2014 ). Hubie Chen. 2014. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. CoRR abs\/1410.5369 (2014)."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP\u201916)","author":"Chen Hubie","year":"2016","unstructured":"Hubie Chen . 2016 . Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness . In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP\u201916) . 94:1--94:14. Hubie Chen. 2016. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP\u201916). 94:1--94:14."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/800119.803893"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_21"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_47"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI\u201911)","author":"Goultiaeva Alexandra","year":"2011","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 Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI\u201911) . 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 Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI\u201911). 546--553."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_7"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_32"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_7"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 11th Annual ACM-SIAM Symposium on Discrete Algorithms. 128--136","author":"Pudl\u00e1k Pavel","year":"2000","unstructured":"Pavel Pudl\u00e1k and Russell Impagliazzo . 2000 . A lower bound for DLL algorithms for k-SAT (preliminary version) . In Proceedings of the 11th Annual ACM-SIAM Symposium on Discrete Algorithms. 128--136 . Pavel Pudl\u00e1k and Russell Impagliazzo. 2000. A lower bound for DLL algorithms for k-SAT (preliminary version). In Proceedings of the 11th Annual ACM-SIAM Symposium on Discrete Algorithms. 128--136."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11564751_43"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1120725.1120821"}],"container-title":["ACM Transactions on Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3087534","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3087534","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:13Z","timestamp":1750217413000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3087534"}},"subtitle":["Understanding Alternation as a Source of Hardness"],"short-title":[],"issued":{"date-parts":[[2017,9,18]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,9,30]]}},"alternative-id":["10.1145\/3087534"],"URL":"https:\/\/doi.org\/10.1145\/3087534","relation":{},"ISSN":["1942-3454","1942-3462"],"issn-type":[{"value":"1942-3454","type":"print"},{"value":"1942-3462","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,18]]},"assertion":[{"value":"2016-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}