References & Citations
Computer Science > Logic in Computer Science
Title: Generating Extended Resolution Proofs with a BDD-Based SAT Solver
(Submitted on 3 May 2021 (v1), last revised 27 Mar 2023 (this version, v4))
Abstract: 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 extended resolution logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability for a set of clauses. 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.
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 modifying an existing BDD package, to several challenging Boolean satisfiability problems. Our resultsdemonstrate scaling for parity formulas, as well as the Urquhart, mutilated chessboard, and pigeonhole problems far beyond that of other proof-generating SAT solvers.
Submission history
From: Randal E. Bryant [view email][v1] Mon, 3 May 2021 14:09:21 GMT (42kb)
[v2] Mon, 14 Jun 2021 14:48:31 GMT (42kb)
[v3] Tue, 13 Sep 2022 11:35:26 GMT (45kb)
[v4] Mon, 27 Mar 2023 20:37:50 GMT (83kb)
Link back to: arXiv, form interface, contact.