{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:06:32Z","timestamp":1743066392202,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"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_28","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"399-416","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Proof Complexity of Symbolic QBF Reasoning"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Mengel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Friedrich","family":"Slivovsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-30201-8_9","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"A Atserias","year":"2004","unstructured":"Atserias, A., Kolaitis, P.G., Vardi, M.Y.: Constraint propagation as a proof system. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 77\u201391. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30201-8_9"},{"issue":"1","key":"28_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. Formal Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-319-09284-3_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"V Balabanov","year":"2014","unstructured":"Balabanov, V., Widl, M., Jiang, J.-H.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 154\u2013169. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_12"},{"issue":"3","key":"28_CR4","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/s00224-019-09940-0","volume":"64","author":"O Beyersdorff","year":"2020","unstructured":"Beyersdorff, O., Blinkhorn, J.: Lower bound techniques for QBF expansion. Theory Comput. Syst. 64(3), 400\u2013421 (2020)","journal-title":"Theory Comput. Syst."},{"key":"28_CR5","unstructured":"Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: A semantic technique for hard random QBFs. Log. Methods Comput. Sci. 15(1) (2019)"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Hardness characterisations and size-width lower bounds for QBF resolution. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) LICS 2020: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Saarbr\u00fccken, Germany, 8\u201311 July 2020, pp. 209\u2013223. ACM (2020)","DOI":"10.1145\/3373718.3394793"},{"issue":"2","key":"28_CR7","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/3381881","volume":"67","author":"O Beyersdorff","year":"2020","unstructured":"Beyersdorff, O., Bonacina, I., Chew, L., Pich, J.: Frege systems for quantified boolean logic. J. ACM 67(2), 9:1\u20139:36 (2020)","journal-title":"J. ACM"},{"issue":"4","key":"28_CR8","doi-asserted-by":"publisher","first-page":"26:1","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:1\u201326:42 (2019)","journal-title":"ACM Trans. Comput. Theory"},{"key":"28_CR9","unstructured":"Biere, A.: Resolve and expand. In: SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, Vancouver, BC, Canada, 10\u201313 May 2004, Online Proceedings (2004)"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Bloem, R., Braud-Santoni, N., Hadzic, V., Egly, U., Lonsing, F., Seidl, M.: Expansion-based QBF solving without recursion. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, 30 October\u20132 November 2018, pp. 1\u201310. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603004"},{"issue":"8","key":"28_CR11","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"28_CR12","unstructured":"Buss, S., Itsykson, D., Knop, A., Sokolov, D.: Reordering rule makes OBDD proof systems stronger. In: Servedio, R.A. (ed.) 33rd Computational Complexity Conference, CCC 2018, San Diego, CA, USA, 22\u201324 June 2018, vol. 102 of LIPIcs, pp. 16:1\u201316:24. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2018)"},{"key":"28_CR13","unstructured":"Capelli, F., Mengel, S.: Tractable QBF by knowledge compilation. In: Niedermeier, R., Paul, C. (eds.) 36th International Symposium on Theoretical Aspects of Computer Science, STACS 2019, 13\u201316 March 2019, vol. 126 of LIPIcs, pp. 18:1\u201318:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"28_CR14","unstructured":"Chattopadhyay, A., Mahajan, M., Mande, N.S., Saurabh, N.: Lower bounds for linear decision lists. Chic. J. Theor. Comput. Sci. 2020 (2020)"},{"issue":"1","key":"28_CR15","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"key":"28_CR16","unstructured":"Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: Walsh, T. (ed.) IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, 16\u201322 July 2011, pp. 819\u2013826. IJCAI\/AAAI (2011)"},{"key":"28_CR17","unstructured":"Dell, H., Komusiewicz, C., Talmon, N., Weller, M.: The PACE 2017 parameterized algorithms and computational experiments challenge: the second iteration. In: Lokshtanov, D., Nishimura, N. (eds.) 12th International Symposium on Parameterized and Exact Computation, IPEC 2017, Vienna, Austria, 6\u20138 September 2017, vol. 89 of LIPIcs, pp. 30:1\u201330:12. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017)"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Dudek, J.M., Phan, V., Vardi, M.Y.: ADDMC: weighted model counting with algebraic decision diagrams. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, 7\u201312 February 2020, pp. 1468\u20131476. AAAI Press (2020)","DOI":"10.1609\/aaai.v34i02.5505"},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-45221-5_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"U Egly","year":"2013","unstructured":"Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: proof generation and strategy extraction in search-based QBF solving. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 291\u2013308. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_21"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11591191_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A Ferrara","year":"2005","unstructured":"Ferrara, A., Pan, G., Vardi, M.Y.: Treewidth in verification: local vs. global. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 489\u2013503. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11591191_34"},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/978-3-642-33558-7_47","volume-title":"Principles and Practice of Constraint Programming","author":"A van Gelder","year":"2012","unstructured":"van Gelder, A.: Contributions to the theory of practical quantified boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, pp. 647\u2013663. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33558-7_47"},{"issue":"4","key":"28_CR22","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1090\/S0273-0979-06-01126-8","volume":"43","author":"S Hoory","year":"2006","unstructured":"Hoory, S., Linial, N., Wigderson, A.: Expander graphs and their applications. Bull. Am. Math. Soc. 43(4), 439\u2013561 (2006)","journal-title":"Bull. Am. Math. Soc."},{"key":"28_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-98334-9_13","volume-title":"Principles and Practice of Constraint Programming","author":"HH Hoos","year":"2018","unstructured":"Hoos, H.H., Peitl, T., Slivovsky, F., Szeider, S.: Portfolio-based algorithm selection for circuit QBFs. In: Hooker, J. (ed.) CP 2018. LNCS, vol. 11008, pp. 195\u2013209. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98334-9_13"},{"key":"28_CR24","doi-asserted-by":"crossref","unstructured":"Impagliazzo, R., Williams, R.: Communication complexity with synchronized clocks. In: Proceedings of the 25th Annual IEEE Conference on Computational Complexity, CCC 2010, Cambridge, Massachusetts, USA, 9\u201312 June 2010, pp. 259\u2013269. IEEE Computer Society (2010)","DOI":"10.1109\/CCC.2010.32"},{"key":"28_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2016.01.004","volume":"234","author":"M Janota","year":"2016","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1\u201325 (2016)","journal-title":"Artif. Intell."},{"key":"28_CR26","unstructured":"Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25\u201331 July 2015, pp. 325\u2013331. AAAI Press (2015)"},{"issue":"1","key":"28_CR27","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":"28_CR28","volume-title":"Communication Complexity","author":"K Eyal","year":"1997","unstructured":"Eyal, K., Noam, N.: Communication Complexity. Cambridge University Press, Cambridge (1997)"},{"issue":"2\u20133","key":"28_CR29","first-page":"71","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: Depqbf: a dependency-aware QBF solver. J. Satisf. Boolean Model. Comput. 7(2\u20133), 71\u201376 (2010)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"28_CR30","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":"28_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-30201-8_34","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"G Pan","year":"2004","unstructured":"Pan, G., Vardi, M.Y.: Symbolic decision procedures for QBF. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 453\u2013467. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30201-8_34"},{"key":"28_CR32","doi-asserted-by":"crossref","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."},{"key":"28_CR33","unstructured":"Pipatsrisawat, K., Darwiche, A.: New compilation languages based on structured decomposability. In: Fox, D., Gomes, C.P. (eds.) Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, 13\u201317 July 2008, pp. 517\u2013522. AAAI Press (2008)"},{"issue":"1","key":"28_CR34","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/s10601-008-9051-2","volume":"14","author":"L Pulina","year":"2009","unstructured":"Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified boolean formulas. Constraints An. Int. J. 14(1), 80\u2013116 (2009)","journal-title":"Constraints An. Int. J."},{"key":"28_CR35","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, 27\u201330 September 2015, pp. 136\u2013143. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"issue":"3","key":"28_CR36","first-page":"229","volume":"2","author":"L Ronald","year":"1987","unstructured":"Ronald, L.: Rivest. Learning decision lists. Mach. Learn. 2(3), 229\u2013246 (1987)","journal-title":"Mach. Learn."},{"key":"28_CR37","unstructured":"Somenzi, F.: CUDD: CU decision diagram package-release 2.4. 0. University of Colorado at Boulder (2009)"},{"key":"28_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-319-40970-2_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"L Tentrup","year":"2016","unstructured":"Tentrup, L.: Non-prenex QBF solving using abstraction. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 393\u2013401. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_24"},{"key":"28_CR39","doi-asserted-by":"crossref","unstructured":"Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM (2000)","DOI":"10.1137\/1.9780898719789"},{"key":"28_CR40","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Pileggi, L.T., Kuehlmann, A. (eds.) Proceedings of the 2002 IEEE\/ACM International Conference on Computer-aided Design, ICCAD 2002, San Jose, California, USA, 10\u201314 November 2002, pp. 442\u2013449. ACM\/IEEE Computer Society (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_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T09:45:09Z","timestamp":1672652709000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_28","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"}}]}}