{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T17:51:29Z","timestamp":1743011489969,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"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_2","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T21:02:31Z","timestamp":1561755751000},"page":"19-35","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Short Proofs in QBF Expansion"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leroy","family":"Chew","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Judith","family":"Clymo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meena","family":"Mahajan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"issue":"1","key":"2_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. Formal Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Formal Methods Syst. Des."},{"issue":"1\u20134","key":"2_CR2","doi-asserted-by":"crossref","first-page":"133","DOI":"10.3233\/SAT190055","volume":"5","author":"M Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: QBF-based formal verification: experience and perspectives. J. Satisfiability Boolean Model. Comput. (JSAT) 5(1\u20134), 133\u2013191 (2008)","journal-title":"J. Satisfiability Boolean Model. Comput. (JSAT)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Bonacina, I., Chew, L.: Lower bounds: from circuits to QBF proof systems. In: Proceedings of the ACM Conference on Innovations in Theoretical Computer Science (ITCS 2016), pp. 249\u2013260. ACM (2016)","DOI":"10.1145\/2840728.2840740"},{"key":"2_CR4","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Proceedings of the Symposium on Theoretical Aspects of Computer Science, pp. 76\u201389. LIPIcs Series (2015)"},{"issue":"1","key":"2_CR5","doi-asserted-by":"crossref","first-page":"1:1","DOI":"10.1145\/3157053","volume":"19","author":"O Beyersdorff","year":"2018","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), 1:1\u20131:26 (2018). (preliminary version in STACS 2016)","journal-title":"ACM Trans. Comput. Logic"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/j.ic.2018.08.002","volume":"262","author":"O Beyersdorff","year":"2018","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Understanding cutting planes for QBFs. Inf. Comput. 262, 141\u2013161 (2018)","journal-title":"Inf. Comput."},{"issue":"18","key":"2_CR7","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1016\/j.ipl.2013.06.002","volume":"113","author":"O Beyersdorff","year":"2013","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: A characterization of tree-like resolution size. Inf. Process. Lett. 113(18), 666\u2013671 (2013)","journal-title":"Inf. Process. Lett."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Pich, J.: Understanding Gentzen and Frege systems for QBF. In: Proceedings of the ACM\/IEEE Symposium on Logic in Computer Science (LICS 2016) (2016)","DOI":"10.1145\/2933575.2933597"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-319-66263-3_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"J Blinkhorn","year":"2017","unstructured":"Blinkhorn, J., Beyersdorff, O.: Shortening QBF proofs with dependency schemes. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 263\u2013280. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_17"},{"issue":"7","key":"2_CR10","doi-asserted-by":"publisher","first-page":"906","DOI":"10.1016\/j.apal.2011.09.009","volume":"163","author":"SR Buss","year":"2012","unstructured":"Buss, S.R.: Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic 163(7), 906\u2013917 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1","key":"2_CR11","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. Logic 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Logic"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10472-016-9501-2","volume":"80","author":"U Egly","year":"2017","unstructured":"Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving. Ann. Math. Artif. Intell. 80(1), 21\u201345 (2017)","journal-title":"Ann. Math. Artif. Intell."},{"key":"2_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":"2_CR14","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":"2_CR15","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":"2_CR16","unstructured":"Kleine B\u00fcning, H., Bubeck, U.: Theory of quantified Boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 735\u2013760. IOS Press (2009)"},{"issue":"1","key":"2_CR17","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":"2_CR18","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":"2_CR19","unstructured":"Kontchakov, R., et al.: Minimal module extraction from DL-lite ontologies using QBF solvers. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), pp. 836\u2013841. AAAI Press (2009)"},{"key":"2_CR20","unstructured":"Lonsing, F.: Dependency schemes and search-based QBF solving: theory and practice. Ph.D. thesis, Johannes Kepler University (2012)"},{"issue":"2\u20133","key":"2_CR21","first-page":"71","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. JSAT 7(2\u20133), 71\u201376 (2010)","journal-title":"JSAT"},{"key":"2_CR22","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"},{"issue":"3","key":"2_CR23","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/2815493.2815497","volume":"2","author":"J Nordstr\u00f6m","year":"2015","unstructured":"Nordstr\u00f6m, J.: On the interplay between proof complexity and SAT solving. SIGLOG News 2(3), 19\u201344 (2015)","journal-title":"SIGLOG News"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, pp. 136\u2013143. FMCAD Inc. (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"issue":"3","key":"2_CR25","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/2578043","volume":"57","author":"MY Vardi","year":"2014","unstructured":"Vardi, M.Y.: Boolean satisfiability: theory and engineering. Commun. ACM 57(3), 5 (2014)","journal-title":"Commun. ACM"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: 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 2019"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24258-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,8]],"date-time":"2021-01-08T14:52:50Z","timestamp":1610117570000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24258-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242572","9783030242589"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24258-9_2","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)"}}]}}