{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:41:25Z","timestamp":1777347685013,"version":"3.51.4"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2023,7,25]],"date-time":"2023-07-25T00:00:00Z","timestamp":1690243200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"U.S. National Science Foundation","doi-asserted-by":"crossref","award":["CCF-2108521"],"award-info":[{"award-number":["CCF-2108521"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2023,10,31]]},"abstract":"<jats:p>\n            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\n            <jats:italic>extended resolution<\/jats:italic>\n            logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability. Such a proof indicates that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it.\n          <\/jats:p>\n          <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 BDD-based solver, implemented by extending an existing BDD package, to several challenging Boolean satisfiability problems. Our results demonstrate scaling for parity formulas as well as the Urquhart, mutilated chessboard, and pigeonhole problems far beyond that of other proof-generating SAT solvers.<\/jats:p>","DOI":"10.1145\/3595295","type":"journal-article","created":{"date-parts":[[2023,5,22]],"date-time":"2023-05-22T12:03:21Z","timestamp":1684757001000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Generating Extended Resolution Proofs with a BDD-Based SAT Solver"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5024-6613","authenticated-orcid":false,"given":"Randal E.","family":"Bryant","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,7,25]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00395-5"},{"key":"e_1_3_2_3_2","volume-title":"An Introduction to Binary Decision Diagrams","author":"Andersen Henrik Reif","year":"1997","unstructured":"Henrik Reif Andersen. 1997. An Introduction to Binary Decision Diagrams. Technical Report. Technical University of Denmark."},{"key":"e_1_3_2_4_2","first-page":"8","volume-title":"Proc. of SAT Race 2019 \u2013 Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B)","author":"Biere Armin","year":"2019","unstructured":"Armin Biere. 2019. CaDiCaL at the SAT Race 2019. In Proc. of SAT Race 2019 \u2013 Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Vol. B-2019-1. University of Helsinki, 8\u20139."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_3_2_6_2","first-page":"51","volume-title":"Proc. of SAT Competition 2020\u2014Solver and Benchmark Descriptions (Department of Computer Science Report Series B)","author":"Biere Armin","year":"2020","unstructured":"Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. 2020. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In Proc. of SAT Competition 2020\u2014Solver and Benchmark Descriptions (Department of Computer Science Report Series B), Vol. B-2020-1. University of Helsinki, 51\u201353."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_7"},{"key":"e_1_3_2_10_2","volume-title":"Formal Methods in Computer-Aided Design (FMCAD\u201922)","author":"Bryant Randal E.","year":"2022","unstructured":"Randal E. Bryant. 2022. TBUDDY: A proof-generating BDD package. In Formal Methods in Computer-Aided Design (FMCAD\u201922)."},{"key":"e_1_3_2_11_2","first-page":"76","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201922) (LNCS)","author":"Bryant Randal E.","year":"2022","unstructured":"Randal E. Bryant, Armin Biere, and Marijn J. H. Heule. 2022. Clausal proofs for pseudo-Boolean reasoning. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201922) (LNCS), Vol. 12651. 76\u201393."},{"key":"e_1_3_2_12_2","first-page":"433","volume-title":"Conference on Automated Deduction (CADE\u201921) (LNAI)","volume":"12699","author":"Bryant Randal E.","year":"2021","unstructured":"Randal E. Bryant and Marijn J. H. Heule. 2021. Dual proof generation for quantified Boolean formulas with a BDD-based solver. In Conference on Automated Deduction (CADE\u201921) (LNAI), Vol. 12699. 433\u2013449."},{"key":"e_1_3_2_13_2","first-page":"76","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part I (LNCS)","author":"Bryant Randal E.","year":"2021","unstructured":"Randal E. Bryant and Marijn J. H. Heule. 2021. Generating extended resolution proofs with a BDD-based SAT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part I (LNCS), Vol. 12651. 76\u201393."},{"key":"e_1_3_2_14_2","unstructured":"Randal E. Bryant and Mate Soos. 2022. Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination. (2022)."},{"key":"e_1_3_2_15_2","volume-title":"VLSI91","author":"Burch Jerry R.","year":"1991","unstructured":"Jerry R. Burch, Edmund M. Clarke, and David E. Long. 1991. Symbolic model checking with partitioned transition relations. In VLSI91."},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_3_2_17_2","first-page":"449","volume-title":"Conference on Automated Deduction (CADE\u201900) (LNCS)","volume":"1831","author":"Chatalic Philippe","year":"2000","unstructured":"Philippe Chatalic and Laurent Simon. 2000. ZRes: The old Davis-Putnam procedure meets ZBDD. In Conference on Automated Deduction (CADE\u201900) (LNCS), Vol. 1831. 449\u2013454."},{"key":"e_1_3_2_18_2","first-page":"1","volume-title":"Theory and Applications of Satisfiability Testing (SAT\u201920) (LNCS)","author":"Chew Leroy","year":"2020","unstructured":"Leroy Chew and Marijn J. H. Heule. 2020. Sorting parity encodings by reusing variables. In Theory and Applications of Satisfiability Testing (SAT\u201920) (LNCS), Vol. 12178. 1\u201310."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1008335.1008338"},{"key":"e_1_3_2_20_2","first-page":"220","volume-title":"Conference on Automated Deduction (CADE\u201917) (LNCS)","volume":"10395","author":"Cruz-Filipe Lu\u00eds","year":"2017","unstructured":"Lu\u00eds Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider-Kamp. 2017. Efficient certified RAT verification. In Conference on Automated Deduction (CADE\u201917) (LNCS), Vol. 10395. 220\u2013236."},{"key":"e_1_3_2_21_2","first-page":"118","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (LNCS)","author":"Cruz-Filipe Lu\u00eds","year":"2017","unstructured":"Lu\u00eds Cruz-Filipe, Jo\u00e3o P. Marques-Silva, and Peter Schneider-Kamp. 2017. Efficient certified resolution proof checking. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (LNCS), Vol. 10205. 118\u2013135."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00059-4"},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/978-3-540-24605-3_30","volume-title":"Theory and Applications of Satisfiability Testing (SAT) (LNCS)","author":"Franco John","year":"2004","unstructured":"John Franco, Michal Kouril, John Schlipf, Jeffrey Ward, Sean Weaver, Michael Dransfield, and W. Mark Vanfleet. 2004. SBSAT: A state-based, BDD-based satisfiability solver. In Theory and Applications of Satisfiability Testing (SAT) (LNCS), Vol. 2919. 398\u2013410."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90040-4"},{"key":"e_1_3_2_26_2","first-page":"886","volume-title":"Design, Automation and Test in Europe (DATE\u201903)","author":"Goldberg Evgueni I.","year":"2003","unstructured":"Evgueni I. Goldberg and Yakov Novikov. 2003. Verification of proofs of unsatisfiability for CNF formulas. In Design, Automation and Test in Europe (DATE\u201903). 886\u2013891."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(02)00403-1"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_3_2_29_2","series-title":"Math. Logic and Foundations","volume-title":"All about Proofs, Proofs for All (APPA\u201915)","author":"Heule Marijn J. H.","year":"2015","unstructured":"Marijn J. H. Heule and Armin Biere. 2015. Proofs for satisfiability problems. In All about Proofs, Proofs for All (APPA\u201915). Math. Logic and Foundations, Vol. 55. College Pub."},{"key":"e_1_3_2_30_2","first-page":"345","volume-title":"Conference on Automated Deduction (CADE\u201913) (LNCS)","volume":"7898","author":"Heule Marijn J. H.","year":"2013","unstructured":"Marijn J. H. Heule, Warren A. Hunt, Jr., and Nathan D. Wetzler. 2013. Verifying refutations with extended resolution. In Conference on Automated Deduction (CADE\u201913) (LNCS), Vol. 7898. 345\u2013359."},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0273-0979-06-01126-8"},{"key":"e_1_3_2_32_2","first-page":"54","volume-title":"Theory and Applications of Satisfiability Testing (SAT\u201906) (LNCS)","author":"Jussila Toni","year":"2006","unstructured":"Toni Jussila, Carsten Sinz, and Armin Biere. 2006. Extended resolution proofs for symbolic SAT solving with quantification. In Theory and Applications of Satisfiability Testing (SAT\u201906) (LNCS), Vol. 4121. 54\u201360."},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(99)00037-2"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09525-z"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(02)00407-9"},{"issue":"4","key":"e_1_3_2_36_2","first-page":"71","article-title":"Explicit construction of concentrators","volume":"9","author":"Margulis Gregori A.","year":"1973","unstructured":"Gregori A. Margulis. 1973. Explicit construction of concentrators. Probl. Perdachi Info (Problems in Information Transmission) 9, 4 (1973), 71\u201380.","journal-title":"Probl. Perdachi Info (Problems in Information Transmission)"},{"key":"e_1_3_2_37_2","first-page":"131","volume-title":"Handbook of Satisfiability","author":"Marques-Silva Jo\u00e3o","year":"2009","unstructured":"Jo\u00e3o Marques-Silva, Ines Lynce, and Sharad Malik. 2009. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability. IOS Press, 131\u2013153."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1038\/218019a0"},{"key":"e_1_3_2_39_2","first-page":"52","volume-title":"Design Automation Conference (DAC\u201990)","author":"Minato Shin-Ichi","year":"1990","unstructured":"Shin-Ichi Minato, Nagisa Ishiura, and Shuzo Yajima. 1990. Shared binary decision diagrams with attributed edges for efficient Boolean function manipulation. In Design Automation Conference (DAC\u201990). 52\u201357."},{"key":"e_1_3_2_40_2","first-page":"235","volume-title":"Theory and Applications of Satisfiability Testing (SAT\u201905) (LNCS)","author":"Pan Guoqiang","year":"2005","unstructured":"Guoqiang Pan and Moshe Y. Vardi. 2005. Search vs. symbolic techniques in satisfiability solving. In Theory and Applications of Satisfiability Testing (SAT\u201905) (LNCS), Vol. 3542. 235\u2013250."},{"key":"e_1_3_2_41_2","first-page":"65","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201917)","author":"Philipp Tobias","year":"2017","unstructured":"Tobias Philipp and Adri\u00e1n Rebola-Pardo. 2017. Towards a semantics of unsatisfiability proofs with inprocessing. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201917). 65\u201384."},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-005-0424-6"},{"key":"e_1_3_2_44_2","first-page":"827","volume-title":"Principles and Practice of Constraint Programming (CP\u201905) (LNCS)","author":"Sinz Carsten","year":"2005","unstructured":"Carsten Sinz. 2005. Towards an optimal CNF encoding of Boolean cardinality constraints. In Principles and Practice of Constraint Programming (CP\u201905) (LNCS), Vol. 3709. 827\u2013831."},{"key":"e_1_3_2_45_2","first-page":"600","volume-title":"Computer Science Symposium in Russia (CSR\u201906) (LNCS)","author":"Sinz Carsten","year":"2006","unstructured":"Carsten Sinz and Armin Biere. 2006. Extended resolution proofs for conjoining BDDs. In Computer Science Symposium in Russia (CSR\u201906) (LNCS), Vol. 3967. 600\u2013611."},{"key":"e_1_3_2_46_2","first-page":"223","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part II (LNCS)","author":"Tan Yong Kiam","year":"2021","unstructured":"Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. 2021. cake_lpr: Verified propagation redundancy checking in CakeML. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part II (LNCS), Vol. 12652. 223\u2013241."},{"key":"e_1_3_2_47_2","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970","author":"Tseitin Gregori S.","year":"1983","unstructured":"Gregori S. Tseitin. 1983. On the complexity of derivation in propositional calculus. In Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970. Springer, 466\u2013483."},{"key":"e_1_3_2_48_2","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/BFb0016843","volume-title":"Constraints in Computational Logics (LNCS)","author":"Uribe Tom\u00e1s E.","year":"1994","unstructured":"Tom\u00e1s E. Uribe and Mark E. Stickel. 1994. Ordered binary decision diagrams and the Davis-Putnam procedure. In Constraints in Computational Logics (LNCS), Vol. 845. 34\u201349."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-012-9322-x"},{"issue":"2","key":"e_1_3_2_51_2","first-page":"89","article-title":"Extending existential quantification in conjunctions of BDDs","volume":"1","author":"Weaver Sean","year":"2006","unstructured":"Sean Weaver, John V. Franco, and John S. Schlipf. 2006. Extending existential quantification in conjunctions of BDDs. JSAT 1, 2 (2006), 89\u2013110.","journal-title":"JSAT"},{"key":"e_1_3_2_52_2","first-page":"422","volume-title":"Theory and Applications of Satisfiability Testing (SAT\u201914) (LNCS)","author":"Wetzler Nathan D.","year":"2014","unstructured":"Nathan D. Wetzler, Marijn J. H. Heule, and Warren A. Hunt Jr.2014. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Theory and Applications of Satisfiability Testing (SAT\u201914) (LNCS), Vol. 8561. 422\u2013429."},{"key":"e_1_3_2_53_2","first-page":"880","volume-title":"Design, Automation and Test in Europe (DATE\u201903)","author":"Zhang Lintao","year":"2003","unstructured":"Lintao Zhang and Sharad Malik. 2003. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Design, Automation and Test in Europe (DATE\u201903). 880\u2013885."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3595295","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3595295","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:08Z","timestamp":1750182548000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3595295"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,25]]},"references-count":52,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,10,31]]}},"alternative-id":["10.1145\/3595295"],"URL":"https:\/\/doi.org\/10.1145\/3595295","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,7,25]]},"assertion":[{"value":"2021-04-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-04-25","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-07-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}