Generating Extended Resolution Proofs with a BDD-Based SAT Solver
| Autor: | Randal E. Bryant, Marijn J. H. Heule |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science mutilated chessboard General Computer Science Logic pigeonhole problem Article Theoretical Computer Science Logic in Computer Science (cs.LO) Computational Mathematics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES binary decision diagrams extended resolution Hardware_LOGICDESIGN |
| Zdroj: | Tools and Algorithms for the Construction and Analysis of Systems |
| Popis: | 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. Extended version of paper published at TACAS 2021 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|