{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T07:14:22Z","timestamp":1761549262400,"version":"build-2065373602"},"reference-count":24,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T00:00:00Z","timestamp":1730160000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SAT"],"abstract":"<jats:p>We give an analogue of the Riis Complexity Gap Theorem in Resolution for Quantified Boolean Formulas (QBFs). Every first-order sentence \u03d5 without finite models gives rise to a sequence of QBFs whose minimal refutations in tree-like QBF Resolution systems are either of polynomial size (if \u03d5 has no models) or at least exponential in size (if \u03d5 has some infinite model). However, we show that this gap theorem is sensitive to the translation and different translations are needed for different QBF resolution systems. For tree-like Q-Resolution, the translation to QBF must be given additional structure in order for the polynomial upper bound to hold. This extra structure is not needed in the system tree-like \u2200Exp+Res, where we see the complexity gap on a natural translation to QBF.<\/jats:p>","DOI":"10.3233\/sat-231505","type":"journal-article","created":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T11:24:31Z","timestamp":1730201071000},"page":"9-25","source":"Crossref","is-referenced-by-count":0,"title":["The Riis Complexity Gap for QBF Resolution"],"prefix":"10.1177","volume":"15","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[{"name":"Institute of Computer Science, Friedrich Schiller University Jena, 07743 Jena, Germany"}]},{"given":"Judith","family":"Clymo","sequence":"additional","affiliation":[{"name":"School of Computing, University of Leeds, Leeds LS2 9JT, U.K."}]},{"given":"Stefan","family":"Dantchev","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Durham, Durham DH1 3LE, U.K."}]},{"given":"Barnaby","family":"Martin","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Durham, Durham DH1 3LE, U.K."}]}],"member":"179","published-online":{"date-parts":[[2024,10,29]]},"reference":[{"key":"10.3233\/SAT-231505_ref1","doi-asserted-by":"crossref","unstructured":"O.\u00a0Beyersdorff, Proof complexity of quantified Boolean logic\u00a0\u2013 a survey, in: Mathematics for Computation (M4C), M.\u00a0Benini, O.\u00a0Beyersdorff, M.\u00a0Rathjen and P.\u00a0Schuster, eds, World Scientific, Singapore, 2022, pp.\u00a0353\u2013391.","DOI":"10.1142\/9789811245220_0015"},{"key":"10.3233\/SAT-231505_ref2","unstructured":"O.\u00a0Beyersdorff, J.\u00a0Blinkhorn and L.\u00a0Hinde, Size, cost, and capacity: A semantic technique for hard random QBFs, Logical Methods in Computer Science 15(1) (2019)."},{"key":"10.3233\/SAT-231505_ref3","doi-asserted-by":"crossref","unstructured":"O.\u00a0Beyersdorff and B.\u00a0B\u00f6hm, Understanding the relative strength of QBF CDCL solvers and QBF resolution, Log. Methods Comput. Sci. 19(2) (2023).","DOI":"10.46298\/lmcs-19(2:2)2023"},{"issue":"2","key":"10.3233\/SAT-231505_ref4","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/3381881","article-title":"Frege systems for quantified Boolean logic","volume":"67","author":"Beyersdorff","year":"2020","journal-title":"J. ACM"},{"key":"10.3233\/SAT-231505_ref5","doi-asserted-by":"crossref","unstructured":"O.\u00a0Beyersdorff, L.\u00a0Chew and M.\u00a0Janota, On unification of QBF resolution-based calculi, in: Proc. Symposium on Mathematical Foundations of Computer Science (MFCS), 2014, pp.\u00a081\u201393.","DOI":"10.1007\/978-3-662-44465-8_8"},{"issue":"4","key":"10.3233\/SAT-231505_ref6","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/3352155","article-title":"New resolution-based QBF calculi and their proof complexity","volume":"11","author":"Beyersdorff","year":"2019","journal-title":"ACM Transactions on Computation Theory"},{"key":"10.3233\/SAT-231505_ref7","unstructured":"O.\u00a0Beyersdorff, L.\u00a0Chew, M.\u00a0Mahajan and A.\u00a0Shukla, Feasible interpolation for QBF resolution calculi, Logical Methods in Computer Science 13 (2017)."},{"key":"10.3233\/SAT-231505_ref8","doi-asserted-by":"crossref","unstructured":"O.\u00a0Beyersdorff, L.\u00a0Chew, M.\u00a0Mahajan and A.\u00a0Shukla, Are short proofs narrow? QBF resolution is not so simple, ACM Transactions on Computational Logic 19 (2018).","DOI":"10.1145\/3157053"},{"key":"10.3233\/SAT-231505_ref9","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.jcss.2016.11.011","article-title":"A game characterisation of tree-like Q-resolution size","volume":"104","author":"Beyersdorff","year":"2019","journal-title":"J. Comput. Syst. Sci."},{"issue":"23","key":"10.3233\/SAT-231505_ref10","doi-asserted-by":"publisher","first-page":"1074","DOI":"10.1016\/j.ipl.2010.09.007","article-title":"A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover\u2013delayer games","volume":"110","author":"Beyersdorff","year":"2010","journal-title":"Information Processing Letters"},{"issue":"18","key":"10.3233\/SAT-231505_ref11","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1016\/j.ipl.2013.06.002","article-title":"A characterization of tree-like resolution size","volume":"113","author":"Beyersdorff","year":"2013","journal-title":"Information Processing Letters"},{"key":"10.3233\/SAT-231505_ref12","doi-asserted-by":"crossref","unstructured":"O.\u00a0Beyersdorff, M.\u00a0Janota, F.\u00a0Lonsing and M.\u00a0Seidl, Quantified Boolean formulas, in: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, A.\u00a0Biere, M.\u00a0Heule, H.\u00a0van Maaren and T.\u00a0Walsh, eds, IOS Press, 2021, pp.\u00a01177\u20131221.","DOI":"10.3233\/FAIA201015"},{"key":"10.3233\/SAT-231505_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-023-09683-1"},{"key":"10.3233\/SAT-231505_ref14","doi-asserted-by":"crossref","unstructured":"S.\u00a0Dantchev, B.\u00a0Martin and S.\u00a0Szeider, Parameterized proof complexity, Computational Complexity 20 (2011). An extended abstract appeared at FOCS 2007.","DOI":"10.1007\/s00037-010-0001-1"},{"key":"10.3233\/SAT-231505_ref15","doi-asserted-by":"crossref","unstructured":"S.S.\u00a0Dantchev and S.\u00a0Riis, On relativisation and complexity gap, in: Computer Science Logic (CSL), 12th Annual Conference of the EACSL, M.\u00a0Baaz and J.A.\u00a0Makowsky, eds, Lecture Notes in Computer Science, Vol.\u00a02803, Springer, 2003, pp.\u00a0142\u2013154.","DOI":"10.1007\/978-3-540-45220-1_14"},{"key":"10.3233\/SAT-231505_ref16","unstructured":"I.P.\u00a0Gent, P.\u00a0Nightingale and A.G.D.\u00a0Rowley, Encoding quantified CSPs as quantified Boolean formulae, in: Proc. 16th European Conference on Artificial Intelligence (ECAI), 2004, pp.\u00a0176\u2013180."},{"issue":"6\u20137","key":"10.3233\/SAT-231505_ref17","doi-asserted-by":"publisher","first-page":"738","DOI":"10.1016\/j.artint.2007.11.003","article-title":"Solving quantified constraint satisfaction problems","volume":"172","author":"Gent","year":"2008","journal-title":"Artif. Intell."},{"key":"10.3233\/SAT-231505_ref18","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.tcs.2015.01.048","article-title":"Expansion-based QBF solving versus Q-resolution","volume":"577","author":"Janota","year":"2015","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.3233\/SAT-231505_ref19","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","article-title":"Resolution for quantified Boolean formulas","volume":"117","author":"Kleine B\u00fcning","year":"1995","journal-title":"Inf. Comput."},{"key":"10.3233\/SAT-231505_ref20","first-page":"125","volume-title":"First-Order Tableau Methods","author":"Letz","year":"1999"},{"issue":"2","key":"10.3233\/SAT-231505_ref21","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","article-title":"On the power of clause-learning SAT solvers as resolution engines","volume":"175","author":"Pipatsrisawat","year":"2011","journal-title":"Artif. Intell."},{"key":"10.3233\/SAT-231505_ref22","unstructured":"P.\u00a0Pudl\u00e1k and R.\u00a0Impagliazzo, A lower bound for DLL algorithms for SAT, in: Proc. 11th Symposium on Discrete Algorithms (SODA), 2000, pp.\u00a0128\u2013136."},{"key":"10.3233\/SAT-231505_ref23","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s00037-001-8194-y","article-title":"A complexity gap for tree-resolution","volume":"10","author":"Riis","year":"2001","journal-title":"Computational Complexity"},{"key":"10.3233\/SAT-231505_ref24","doi-asserted-by":"crossref","unstructured":"A.\u00a0Van Gelder, Contributions to the theory of practical quantified Boolean formula solving, in: Proc. Principles and Practice of Constraint Programming (CP), 2012, pp.\u00a0647\u2013663.","DOI":"10.1007\/978-3-642-33558-7_47"}],"container-title":["Journal on Satisfiability, Boolean Modeling and Computation"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/SAT-231505","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T07:08:27Z","timestamp":1761548907000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/SAT-231505"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,29]]},"references-count":24,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2024,10,29]]}},"URL":"https:\/\/doi.org\/10.3233\/sat-231505","relation":{},"ISSN":["1574-0617"],"issn-type":[{"type":"electronic","value":"1574-0617"}],"subject":[],"published":{"date-parts":[[2024,10,29]]}}}