{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:26:50Z","timestamp":1772119610167,"version":"3.50.1"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,9,27]],"date-time":"2023-09-27T00:00:00Z","timestamp":1695772800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,27]],"date-time":"2023-09-27T00:00:00Z","timestamp":1695772800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100007569","name":"Carl-Zeiss-Stiftung","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100007569","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["BE 4209\/3-1"],"award-info":[{"award-number":["BE 4209\/3-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100012957","name":"Friedrich-Schiller-Universit\u00e4t Jena","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100012957","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    QCDCL is one of the main algorithmic paradigms for solving quantified Boolean formulas (QBF). We design a new technique to show lower bounds for the running time in QCDCL algorithms. For this we model QCDCL by concisely defined proof systems and identify a new width measure for formulas, which we call\n                    <jats:italic>gauge<\/jats:italic>\n                    . We show that for a large class of QBFs, large (e.g. linear) gauge implies exponential lower bounds for QCDCL proof size. We illustrate our technique by computing the gauge for a number of sample QBFs, thereby providing new exponential lower bounds for QCDCL. Our technique is the first bespoke lower bound technique for QCDCL.\n                  <\/jats:p>","DOI":"10.1007\/s10817-023-09683-1","type":"journal-article","created":{"date-parts":[[2023,9,27]],"date-time":"2023-09-27T12:02:04Z","timestamp":1695816124000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Lower Bounds for QCDCL via Formula Gauge"],"prefix":"10.1007","volume":"67","author":[{"given":"Benjamin","family":"B\u00f6hm","sequence":"first","affiliation":[]},{"given":"Olaf","family":"Beyersdorff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,9,27]]},"reference":[{"key":"9683_CR1","doi-asserted-by":"crossref","unstructured":"Balabanov, V., Widl, M., Jiang, J.-H.R.: QBF resolution systems and their proof complexities. In: Proceedings of the Theory and Applications of Satisfiability Testing (SAT), pp. 154\u2013169 (2014)","DOI":"10.1007\/978-3-319-09284-3_12"},{"issue":"1","key":"9683_CR2","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. Form. Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"9683_CR3","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P Beame","year":"2004","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR) 22, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"issue":"2","key":"9683_CR4","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/375827.375835","volume":"48","author":"E Ben-Sasson","year":"2001","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow\u2014resolution made simple. J. ACM 48(2), 149\u2013169 (2001)","journal-title":"J. ACM"},{"key":"9683_CR5","unstructured":"Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. Logical Methods in Computer Science 15(1) (2019)"},{"key":"9683_CR6","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Hardness characterisations and size-width lower bounds for QBF resolution. In: Proceedings of the ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 209\u2013223 (2020)","DOI":"10.1145\/3373718.3394793"},{"key":"9683_CR7","unstructured":"Beyersdorff, O., B\u00f6hm, B.: Understanding the relative strength of QBF CDCL solvers and QBF resolution. In: Proceedings of the Innovations in Theoretical Computer Science (ITCS), pp. 12\u201311220 (2021)"},{"key":"9683_CR8","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Bonacina, I., Chew, L., Pich, J.: Frege systems for quantified Boolean logic. J. ACM 67(2) (2020)","DOI":"10.1145\/3381881"},{"key":"9683_CR9","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Are short proofs narrow? QBF resolution is not so simple. ACM Transactions on Computational Logic 19 (2018)","DOI":"10.1145\/3157053"},{"key":"9683_CR10","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Feasible interpolation for QBF resolution calculi. Logical Methods in Computer Science 13 (2017)"},{"key":"9683_CR11","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. ACM Transactions on Computation Theory 12(2) (2020)","DOI":"10.1145\/3378665"},{"key":"9683_CR12","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Janota, M., Lonsing, F., Seidl, M.: Quantified Boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, pp. 1177\u20131221. IOS Press, Amsterdam (2021)","DOI":"10.3233\/FAIA201015"},{"key":"9683_CR13","first-page":"353","volume-title":"Mathematics for Computation (M4C)","author":"O Beyersdorff","year":"2022","unstructured":"Beyersdorff, O.: Proof complexity of quantified Boolean logic\u2014a survey. In: Benini, M., Beyersdorff, O., Rathjen, M., Schuster, P. (eds.) Mathematics for Computation (M4C), pp. 353\u2013391. World Scientific, Singapore (2022)"},{"issue":"4","key":"9683_CR14","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/3352155","volume":"11","author":"O Beyersdorff","year":"2019","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory 11(4), 26\u201312642 (2019)","journal-title":"ACM Trans. Comput. Theory"},{"key":"9683_CR15","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.jcss.2016.11.011","volume":"104","author":"O Beyersdorff","year":"2019","unstructured":"Beyersdorff, O., Chew, L., Sreenivasaiah, K.: A game characterisation of tree-like Q-resolution size. J. Comput. Syst. Sci. 104, 82\u2013101 (2019)","journal-title":"J. Comput. Syst. Sci."},{"key":"9683_CR16","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-030-80223-3_5","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2021","author":"B B\u00f6hm","year":"2021","unstructured":"B\u00f6hm, B., Beyersdorff, O.: Lower bounds for QCDCL via formula gauge. In: Li, C.-M., Many\u00e0, F. (eds.) Theory and Applications of Satisfiability Testing\u2014SAT 2021, pp. 47\u201363. Springer, Cham (2021)"},{"key":"9683_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ipl.2018.05.005","volume":"138","author":"J Clymo","year":"2018","unstructured":"Clymo, J., Beyersdorff, O.: Relating size and width in variants of Q-resolution. Inf. Process. Lett. 138, 1\u20136 (2018)","journal-title":"Inf. Process. Lett."},{"key":"9683_CR18","doi-asserted-by":"crossref","unstructured":"Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: proof generation and strategy extraction in search-based QBF solving. In: Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp. 291\u2013308 (2013)","DOI":"10.1007\/978-3-642-45221-5_21"},{"key":"9683_CR19","doi-asserted-by":"publisher","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. J. Artif. Intell. Res. 26, 371\u2013416 (2006)","journal-title":"J. Artif. Intell. Res."},{"key":"9683_CR20","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"9683_CR21","doi-asserted-by":"crossref","unstructured":"Janota, M.: On Q-Resolution and CDCL QBF solving. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 402\u2013418 (2016)","DOI":"10.1007\/978-3-319-40970-2_25"},{"key":"9683_CR22","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.tcs.2015.01.048","volume":"577","author":"M Janota","year":"2015","unstructured":"Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577, 25\u201342 (2015)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9683_CR23","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. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"9683_CR24","unstructured":"Kraj\u00ed\u010dek, J.: Proof Complexity. Encyclopedia of Mathematics and Its Applications, vol. 170. Cambridge University Press, Cambridge (2019)"},{"key":"9683_CR25","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Egly, U., Seidl, M.: Q-resolution with generalized axioms. In: Proceedings of the Theory and Applications of Satisfiability Testing (SAT), pp. 435\u2013452 (2016)","DOI":"10.1007\/978-3-319-40970-2_27"},{"key":"9683_CR26","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In: Proceedings of the International Conference on Automated Deduction (CADE), pp. 371\u2013384 (2017)","DOI":"10.1007\/978-3-319-63046-5_23"},{"key":"9683_CR27","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Egly, U.: Evaluating QBF solvers: quantifier alternations matter. In: Proceedings of the Principles and Practice of Constraint Programming (CP), pp. 276\u2013294 (2018)","DOI":"10.1007\/978-3-319-98334-9_19"},{"key":"9683_CR28","unstructured":"Lonsing, F.: Dependency schemes and search-based QBF solving: theory and practice. PhD thesis, Johannes Kepler University Linz (2012)"},{"key":"9683_CR29","unstructured":"Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability. IOS Press, Amsterdam (2009)"},{"key":"9683_CR30","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1613\/jair.1.11529","volume":"65","author":"T Peitl","year":"2019","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. J. Artif. Intell. Res. 65, 180\u2013208 (2019)","journal-title":"J. Artif. Intell. Res."},{"issue":"2","key":"9683_CR31","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"key":"9683_CR32","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1016\/j.artint.2019.04.002","volume":"274","author":"L Pulina","year":"2019","unstructured":"Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (QBFEVAL\u201916 and QBFEVAL\u201917). Artif. Intell. 274, 224\u2013248 (2019)","journal-title":"Artif. Intell."},{"key":"9683_CR33","doi-asserted-by":"crossref","unstructured":"Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified Boolean formulas. In: Proceedings of the IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pp. 78\u201384 (2019)","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"9683_CR34","doi-asserted-by":"crossref","unstructured":"Vinyals, M.: Hard examples for common variable decision heuristics. In: Proceedings of the AAAI Conference on Artificial Intelligence (AAAI) (2020)","DOI":"10.1609\/aaai.v34i02.5527"},{"key":"9683_CR35","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in Boolean satisfiability solver. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 279\u2013285 (2001)","DOI":"10.1145\/774572.774637"},{"key":"9683_CR36","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Proceedings of the IEEE\/ACM International Conference on Computer-aided Design (ICCAD), pp. 442\u2013449 (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09683-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09683-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09683-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,9]],"date-time":"2023-12-09T04:06:53Z","timestamp":1702094813000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09683-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,27]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["9683"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09683-1","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-1796853\/v1","asserted-by":"object"}]},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,27]]},"assertion":[{"value":"26 June 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 August 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 September 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"35"}}