Generating Extended Resolution Proofs with a BDD-Based SAT Solver

TL;DR

This paper extends BDD-based SAT solvers to generate extended resolution proofs with arbitrary existential quantification, enabling verification of unsatisfiability for complex problems more effectively than previous methods.

Contribution

It introduces a method to incorporate arbitrary existential quantification into BDD-based SAT solvers, enhancing their proof-generating capabilities for complex formulas.

Findings

Successfully applied to challenging SAT problems

Demonstrated scalability for parity and combinatorial problems

Produced checkable proofs of unsatisfiability for complex formulas

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.