We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Generating Extended Resolution Proofs with a BDD-Based SAT Solver

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 prototype solver to several problems that are very challenging for search-based SAT solvers, obtaining polynomially sized proofs on benchmarks for parity formulas, as well as the Urquhart, mutilated chessboard, and pigeonhole problems.
Comments: Extended version of paper published at TACAS 2021
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2105.00885 [cs.LO]
  (or arXiv:2105.00885v2 [cs.LO] for this version)

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)

Link back to: arXiv, form interface, contact.