{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:34:23Z","timestamp":1743129263340,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030802226"},{"type":"electronic","value":"9783030802233"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_5","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"47-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Lower Bounds for QCDCL via Formula Gauge"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"B\u00f6hm","sequence":"first","affiliation":[]},{"given":"Olaf","family":"Beyersdorff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"issue":"1","key":"5_CR1","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":"5_CR2","doi-asserted-by":"crossref","unstructured":"Balabanov, V., Widl, M., Jiang, J.H.R.: QBF resolution systems and their proof complexities. In: Proceedings of Theory and Applications of Satisfiability Testing (SAT), pp. 154\u2013169 (2014)","DOI":"10.1007\/978-3-319-09284-3_12"},{"key":"5_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":"5_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 - resolution made simple. J. ACM 48(2), 149\u2013169 (2001)","journal-title":"J. ACM"},{"key":"5_CR5","unstructured":"Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. Logical Methods Comput. Sci 15(1), 13:1\u201313:39 (2019)"},{"key":"5_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 ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 209\u2013223. ACM (2020)","DOI":"10.1145\/3373718.3394793"},{"key":"5_CR7","unstructured":"Beyersdorff, O., B\u00f6hm, B.: Understanding the relative strength of QBF CDCL solvers and QBF resolution. In: Proceedings of Innovations in Theoretical Computer Science (ITCS), pp. 12:1\u201312:20 (2021)"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Bonacina, I., Chew, L., Pich, J.: Frege systems for quantified Boolean logic. J. ACM 67(2), 1\u201336 (2020)","DOI":"10.1145\/3381881"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theor. 11(4), 26:1\u201326:42 (2019)","DOI":"10.1145\/3352155"},{"key":"5_CR10","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Feasible interpolation for QBF resolution calculi. Logical Methods Comput. Sci. 13, 7:1\u20137:20 (2017)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Are short proofs narrow? QBF resolution is not so simple. ACM Trans. Comput. Logic 19, 1\u201326 (2018)","DOI":"10.1145\/3157053"},{"key":"5_CR12","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":"5_CR13","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. ACM Trans. Comput. Theor. 12(2), 1\u201327 (2020)","DOI":"10.1145\/3378665"},{"key":"5_CR14","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, 2nd edn. IOS press, Frontiers in Artificial Intelligence and Applications (2021)","DOI":"10.3233\/FAIA201015"},{"key":"5_CR15","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":"5_CR16","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 Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp. 291\u2013308 (2013)","DOI":"10.1007\/978-3-642-45221-5_21"},{"key":"5_CR17","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":"5_CR18","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":"5_CR19","doi-asserted-by":"crossref","unstructured":"Janota, M.: On Q-Resolution and CDCL QBF solving. In: Proceedings of International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 402\u2013418 (2016)","DOI":"10.1007\/978-3-319-40970-2_25"},{"key":"5_CR20","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":"5_CR21","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":"5_CR22","doi-asserted-by":"crossref","unstructured":"Kraj\u00ed\u010dek, J.: Proof complexity, Encyclopedia of Mathematics and Its Applications, vol. 170. Cambridge University Press (2019)","DOI":"10.1017\/9781108242066"},{"key":"5_CR23","unstructured":"Lonsing, F.: Dependency Schemes and Search-Based QBF Solving: Theory and Practice. Ph.D. thesis, Johannes Kepler University Linz (2012)"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In: Proceedings of International Conference on Automated Deduction (CADE), pp. 371\u2013384 (2017)","DOI":"10.1007\/978-3-319-63046-5_23"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-319-98334-9_19","volume-title":"Principles and Practice of Constraint Programming","author":"F Lonsing","year":"2018","unstructured":"Lonsing, F., Egly, U.: Evaluating QBF solvers: quantifier alternations matter. In: Hooker, J. (ed.) CP 2018. LNCS, vol. 11008, pp. 276\u2013294. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98334-9_19"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-319-40970-2_27","volume-title":"Theory and Applications of Satisfiability Testing","author":"F Lonsing","year":"2016","unstructured":"Lonsing, F., Egly, U., Seidl, M.: Q-resolution with generalized axioms. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 435\u2013452. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_27"},{"key":"5_CR27","unstructured":"Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability. IOS Press (2009)"},{"key":"5_CR28","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":"5_CR29","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":"5_CR30","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":"5_CR31","doi-asserted-by":"crossref","unstructured":"Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified Boolean formulas. In: Proceedings of IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pp. 78\u201384 (2019)","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"5_CR32","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":"5_CR33","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 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 279\u2013285 (2001)","DOI":"10.1145\/774572.774637"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Proceedings of IEEE\/ACM International Conference on Computer-aided Design (ICCAD), pp. 442\u2013449 (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T23:29:01Z","timestamp":1625182141000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}