{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T06:39:12Z","timestamp":1768286352175,"version":"3.49.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720155","type":"print"},{"value":"9783030720162","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,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"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>In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the<jats:italic>extended resolution<\/jats:italic>logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability. Such proofs indicate that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it.<\/jats:p><jats:p>We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a prototype solver to obtain polynomially sized proofs on benchmarks for the mutilated chessboard and pigeonhole problems\u2014ones that are very challenging for search-based SAT solvers.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_5","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"76-93","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Generating Extended Resolution Proofs with a BDD-Based SAT Solver"],"prefix":"10.1007","author":[{"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M.: Mutilated chessboard problem is exponentially hard for resolution. Theoretical Computer Science 310(1-3), 513\u2013525 (Jan 2004)","DOI":"10.1016\/S0304-3975(03)00395-5"},{"key":"5_CR2","unstructured":"Andersen, H.R.: An introduction to binary decision diagrams. Tech. rep., Technical University of Denmark (October 1997)"},{"key":"5_CR3","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling, and Treengeling entering the SAT competition 2020 (2020), unpublished"},{"key":"5_CR4","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers 35(8), 677\u2013691 (1986)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys 24(3), 293\u2013318 (September 1992)","DOI":"10.1145\/136035.136043"},{"key":"5_CR6","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":"5_CR7","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. Information and Computation 98(2), 142\u2013170 (1992)","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: A short proof of the pigeon hole principle using extended resolution. SIGACT News 8(4), 28\u201332 (1976)","DOI":"10.1145\/1008335.1008338"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: Automated Deduction (CADE). LNCS, vol. 10395, pp. 220\u2013236 (2017)","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 10205, pp. 118\u2013135 (2017)","DOI":"10.1007\/978-3-662-54577-5_7"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","DOI":"10.1145\/321033.321034"},{"key":"5_CR12","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":"5_CR13","doi-asserted-by":"crossref","unstructured":"Franco, J., Kouril, M., Schlipf, J., Ward, J., Weaver, S., Dransfield, M., Vanfleet, W.M.: SBSAT: a state-based, BDD-based satisfiability solver. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a02919, pp. 398\u2013410 (2004)","DOI":"10.1007\/978-3-540-24605-3_30"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Zantema, H.: Resolution and binary decision diagrams cannot simulate each other polynomially. Discrete Applied Mathematics 130(2), 157\u2013171 (2003)","DOI":"10.1016\/S0166-218X(02)00403-1"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Haken, A.: The intractability of resolution. Theoretical Computer Science 39, 297\u2013308 (1985)","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"5_CR16","unstructured":"Heule, M.J.H., Biere, A.: Proofs for satisfiability problems. In: All about Proofs, Proofs for All (APPA), Math. Logic and Foundations, vol.\u00a055. College Pub. (2015)"},{"key":"5_CR17","unstructured":"Heule, M.J.H., Biere, A.: What a difference a variable makes. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 10806, pp. 75\u201392 (2018)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A., Kaufmann, M., Wetzler, N.D.: Efficient, verified checking of propositional proofs. In: Interactive Theorem Proving. LNCS, vol. 10499, pp. 269\u2013284 (2017)","DOI":"10.1007\/978-3-319-66107-0_18"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Clausal proofs of mutilated chessboards. In: NASA Formal Methods. LNCS, vol. 11460, pp. 204\u2013210 (2019)","DOI":"10.1007\/978-3-030-20652-9_13"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Seidl, M., Biere, A.: PRuning through satisfaction. In: Haifa Verification Conference (HVC). LNCS, vol. 10629, pp. 179\u2013194 (2017)","DOI":"10.1007\/978-3-319-70389-3_12"},{"key":"5_CR21","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.\u00a04121, pp. 54\u201360 (2006)","DOI":"10.1007\/11814948_8"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 96-97, 149\u2013176 (1999)","DOI":"10.1016\/S0166-218X(99)00037-2"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. Journal of Automated Reasoning 64, 513\u2013532 (2020)","DOI":"10.1007\/s10817-019-09525-z"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Minato, S.I., Ishiura, N., Yajima, S.: Shared binary decision diagrams with attributed edges for efficient Boolean function manipulation. In: 27th ACM\/IEEE Design Automation Conference. pp. 52\u201357 (June 1990)","DOI":"10.1145\/123186.123225"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Pan, G., Vardi, M.Y.: Search vs.\u00a0symbolic techniques in satisfiability solving. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a03542, pp. 235\u2013250 (2005)","DOI":"10.1007\/11527695_19"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (January 1965)","DOI":"10.1145\/321250.321253"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints. In: Principles and Practice of Constraint Programming (CP). LNCS, vol.\u00a03709, pp. 827\u2013831 (2005)","DOI":"10.1007\/11564751_73"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Computer Science Symposium in Russia (CSR). LNCS, vol.\u00a03967, pp. 600\u2013611 (2006)","DOI":"10.1007\/11753728_60"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Tan, Y.K., Heule, M.J.H., Myreen, M.O.: cake\\_lpr: Verified propagation redundancy checking in CakeML. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2021)","DOI":"10.1007\/978-3-030-72013-1_12"},{"key":"5_CR30","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"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Uribe, T.E., Stickel, M.E.: Ordered binary decision diagrams and the Davis-Putnam procedure. In: Constraints in Computational Logics. LNCS, vol.\u00a0845, pp. 34\u201349 (1994)","DOI":"10.1007\/BFb0016843"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Wetzler, N.D., Heule, M.J.H., Hunt\u00a0Jr., W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a08561, pp. 422\u2013429 (2014)","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"5_CR33","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe (DATE) Volume 1. p. 10880. IEEE Computer Society (2003)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,29]],"date-time":"2021-04-29T20:34:42Z","timestamp":1619728482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_5","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":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","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":"141","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":"41","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":"21","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":"29% - 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":"12","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":"The conference changed to an online format due to the COVID-19 pandemic","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)"}}]}}