{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T06:00:51Z","timestamp":1768284051587,"version":"3.49.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030798758","type":"print"},{"value":"9783030798765","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Existing proof-generating quantified Boolean formula (QBF) solvers must construct a different type of proof depending on whether the formula is false (refutation) or true (satisfaction). We show that a QBF solver based on ordered binary decision diagrams (BDDs) can emit a single <jats:italic>dual proof<\/jats:italic> as it operates, supporting either outcome. This form consists of a sequence of equivalence-preserving clause addition and deletion steps in an extended resolution framework. For a false formula, the proof terminates with the empty clause, indicating conflict. For a true one, it terminates with all clauses deleted, indicating tautology. Both the length of the proof and the time required to check it are proportional to the total number of BDD operations performed. We evaluate our solver using a scalable benchmark based on a two-player tiling game.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_25","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"433-449","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5024-6613","authenticated-orcid":false,"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"25_CR1","unstructured":"Andersen, H.R.: An introduction to binary decision diagrams. Tech. rep., Technical University of Denmark (October 1997)"},{"key":"25_CR2","unstructured":"Berlekamp, E.R., Conway, J.H., Guy, R.K.: Winning Ways for your Mathematical Plays:, vol. 1, 2nd edn. CRC Press (2001)"},{"key":"25_CR3","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: Extension variables in QBF resolution. In: AAAI Workshop on Beyond NP (2016)"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A.: Resolve and expand. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 3542, pp. 59\u201370 (2005)","DOI":"10.1007\/11527695_5"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Conference on Automated Deduction (CADE). LNCS, vol. 6803, pp. 101\u2013115. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_10"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers 35(8), 677\u2013691 (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys 24(3), 293\u2013318 (1992)","DOI":"10.1145\/136035.136043"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Binary decision diagrams. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 191\u2013217. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_7"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Heule, M.J.H.: Generating extended resolution proofs with a BDD-based SAT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2021)","DOI":"10.26226\/morressier.604907f41a80aac83ca25ceb"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Dechter, R.: Bucket elimination: A unifying framework for reasoning. Artificial Intelligence 113(1\u20132), 41\u201385 (1999)","DOI":"10.1016\/S0004-3702(99)00059-4"},{"key":"25_CR11","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman (1979)"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause\/term resolution and learning in the evaluation of quantified Boolean formulas. Journal of AI Research 26, 371\u2013416 (2006)","DOI":"10.1613\/jair.1959"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: International Joint Conference on Automated Reasoning (IJCAR). LNCS, vol. 8562, pp. 91\u2013106 (2014)","DOI":"10.1007\/978-3-319-08587-6_7"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF. Journal of Automated Reasoning 58, 97\u2013125 (2017)","DOI":"10.1007\/s10817-016-9390-4"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Janota, M., Klieber, W., Marques-Silva, J.a.P., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artificial Intelligence 234, 1\u201325 (2016)","DOI":"10.1016\/j.artint.2016.01.004"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 4121, pp. 54\u201360 (2006)","DOI":"10.1007\/11814948_8"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Jussila, T., Sinz, C., Biere, A., Kr\u00f6ning, D., Wintersteiger, C.M.: A first step towards a unified proof checker for QBF. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 4501, pp. 201\u2013714 (2007)","DOI":"10.1007\/978-3-540-72788-0_21"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Kleine B\u00fcning, H., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified Boolean formulas. Information and Computation 117(1), 12\u201318 (1995)","DOI":"10.1006\/inco.1995.1025"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Klieber, W.: GhostQ system description. Journal on Satisfiability, Boolean Modeling, and Computation 11, 65\u201372 (2019)","DOI":"10.3233\/SAT190117"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In: Conference on Automated Deduction (CADE). LNCS, vol. 10395, pp. 371\u2013384 (2017)","DOI":"10.1007\/978-3-319-63046-5_23"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Narizzano, M., Peschiera, C., Pulina, L., Tacchella, A.: Evaluating and certifying QBFs: A comparison of state-of-the-art tools. AI Communications 22(4), 191\u2013210 (2009)","DOI":"10.3233\/AIC-2009-0468"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 7317, pp. 430\u2013435 (2012)","DOI":"10.1007\/978-3-642-31612-8_33"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Olivo, O., Emerson, E.A.: A more efficient BDD-based QBF solver. In: Principles and Practice of Constraint Programming (CP). LNCS, vol. 6876, pp. 675\u2013690 (2011)","DOI":"10.1007\/978-3-642-23786-7_51"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Pan, G., Vardi, M.Y.: Symbolic decision procedures for QBF. In: Principles and Practice of Constraint Programming (CP). LNCS, vol. 3258, pp. 453\u2013467 (2004)","DOI":"10.1007\/978-3-540-30201-8_34"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Polynomial-time validation of QCDCL certificates. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 10929, pp. 253\u2013269 (2018)","DOI":"10.1007\/978-3-319-94144-8_16"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Computer Science Symposium in Russia (CSR). LNCS, vol. 3967, pp. 600\u2013611 (2006)","DOI":"10.1007\/11753728_60"},{"key":"25_CR27","unstructured":"Sloane, N.J.A., The OEIS Foundation: The on-line encyclopedia of integer sequences (2012), http:\/\/oeis.org\/A215721, sequence A215721"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970. pp. 466\u2013483. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1_28"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:33:54Z","timestamp":1625650434000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"0","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":"38% - 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":"5","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)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}