{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:36:31Z","timestamp":1743089791869,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030242572"},{"type":"electronic","value":"9783030242589"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-24258-9_23","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T21:02:31Z","timestamp":1561755751000},"page":"319-335","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Proof Complexity of Fragments of Long-Distance Q-Resolution"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Peitl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Friedrich","family":"Slivovsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"issue":"1","key":"23_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., Roland Jiang, J.-H.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Balabanov, V., Jiang, J.H.R., Janota, M., Widl, M.: Efficient extraction of QBF (counter) models from long-distance resolution proofs. In: Bonet, B., Koenig, S., (eds.) Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 25\u201330 January 2015, Austin, Texas, USA., pp. 3694\u20133701. AAAI Press (2015)","DOI":"10.1609\/aaai.v29i1.9750"},{"key":"23_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"},{"key":"23_CR4","unstructured":"Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. Log. Methods Comput. Sci. 15(1), 13:1\u201313:39 (2019)"},{"key":"23_CR5","unstructured":"Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Building strategies into QBF proofs. In: 36th International Symposium on Theoretical Aspects of Computer Science, STACS 2019, 13\u201316 March (2019), Berlin, Germany, pp. 14:1\u201314:18 (2019)"},{"key":"23_CR6","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Mayr, E.W., Ollinger, N. (eds.) 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, 4\u20137 March 2015, Garching, Germany, vol. 30 of LIPIcs, pp. 76\u201389. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"23_CR7","unstructured":"Biere, A.: Resolve and expand. In: Proceedings of SAT 2004 Seventh International Conference on Theory and Applications of Satisfiability Testing, 10\u201313 May 2004, Vancouver, BC, Canada, pp. 59\u201370 (2004)"},{"key":"23_CR8","unstructured":"Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds) Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pp. 457\u2013481. IOS Press (2009)"},{"key":"23_CR9","unstructured":"Bj\u00f8rner, N., Janota, M., Klieber, W.: On conflicts and strategies in QBF. In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A., (eds.) 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, EPiC Series in Computing, LPAR 2015, Suva, Fiji, 24\u201328 November 2015, vol. 35 pp. 28\u201341. EasyChair (2015)"},{"issue":"2","key":"23_CR10","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S0020-0190(98)00042-8","volume":"66","author":"B Bollig","year":"1998","unstructured":"Bollig, B., Wegener, I.: A very simple function that requires exponential size read-once branching programs. Inf. Process. Lett. 66(2), 53\u201357 (1998)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"23_CR11","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1015019416843","volume":"28","author":"M Cadoli","year":"2002","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate Quantified Boolean Formulae and its experimental evaluation. J. Automat. Reason. 28(2), 101\u2013142 (2002)","journal-title":"J. Automat. Reason."},{"key":"23_CR12","unstructured":"Chew, L.N.: QBF proof complexity. Ph.D. thesis, University of Leeds, UK (2017)"},{"key":"23_CR13","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":"23_CR14","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":"23_CR15","doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: Handbook of Knowledge Representation, volume 3 of Foundations of Artificial Intelligence, pp. 89\u2013134. Elsevier (2008)","DOI":"10.1016\/S1574-6526(07)03002-7"},{"key":"23_CR16","volume-title":"Computational Limitations of Small-depth Circuits","author":"J H\u00e5stad","year":"1987","unstructured":"H\u00e5stad, J.: Computational Limitations of Small-depth Circuits. MIT Press, Cambridge, MA, USA (1987)"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M Janota","year":"2012","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114\u2013128. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_10"},{"key":"23_CR18","unstructured":"Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Yang, Q., Wooldridge, M. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pp. 325\u2013331. AAAI Press (2015)"},{"key":"23_CR19","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."},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-319-40970-2_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"M Janota","year":"2016","unstructured":"Janota, M.: On Q-resolution and CDCL QBF solving. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 402\u2013418. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_25"},{"issue":"1","key":"23_CR21","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"HK B\u00fcning","year":"1995","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-14186-7_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"W Klieber","year":"2010","unstructured":"Klieber, W., Sapra, S., Gao, S., Clarke, E.: A non-prenex, non-clausal QBF solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 128\u2013142. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_12"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39071-5_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"F Lonsing","year":"2013","unstructured":"Lonsing, F., Egly, U., Van Gelder, A.: Efficient clause learning for quantified boolean formulas via QBF pseudo unit propagation. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 100\u2013115. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_9"},{"issue":"4","key":"23_CR24","first-page":"765","volume":"169","author":"I Nechiporuk","year":"1966","unstructured":"Nechiporuk, I.: A Boolean function. Dokl. Akad. Nauk SSSR 169(4), 765\u2013766 (1966)","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"23_CR25","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1613\/jair.1.11529","volume":"65","author":"Tom\u00e1\u0161 Peitl","year":"2019","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. J. Artif. Intell. Res. 65, 181\u2013208 (2019)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Kaivola, R., Wahl, R. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2015, pp. 136\u2013143. IEEE Computer Society (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"key":"23_CR27","unstructured":"Rintanen, J.: Planning and SAT. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pp. 483\u2013504. IOS Press (2009)"},{"issue":"3","key":"23_CR28","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":"23_CR29","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: Proceedings of Theory of Computing, pp. 1\u20139. ACM (1973)","DOI":"10.1145\/800125.804029"},{"key":"23_CR30","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":"23_CR31","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning. Classical Papers on Computer Science","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning. Classical Papers on Computer Science, pp. 466\u2013483. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_28 . Zap. Nauchn. Sem. Leningrad Otd. Mat. Inst. Akad. Nauk SSSR, 8:23\u201341, 1968. Russian. English translation"},{"key":"23_CR32","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 Gelder van","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":"11","key":"23_CR33","doi-asserted-by":"publisher","first-page":"2021","DOI":"10.1109\/JPROC.2015.2455034","volume":"103","author":"Y Vizel","year":"2015","unstructured":"Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. Proc. IEEE 103(11), 2021\u20132035 (2015)","journal-title":"Proc. IEEE"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM (2000)","DOI":"10.1137\/1.9780898719789"},{"key":"23_CR35","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 2019"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24258-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,22]],"date-time":"2022-09-22T10:33:27Z","timestamp":1663842807000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24258-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242572","9783030242589"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24258-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"29 June 2019","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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sat2019.tecnico.ulisboa.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}