Generating extended resolution proofs with a BDD-based SAT solver

DOI10.1007/978-3-030-72016-2_5MaRDI QIDQ2044191zbMATH OpenOpenAlexFDO

Authors Randal E. Bryant, Marijn J. H. Heule

Publication date 4 August 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2105.00885

zbMATH Keywords

binary decision diagramsextended resolutionmutilated chessboardpigeonhole problem

Mathematics Subject Classification ID

Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Recommendations

• Extended Resolution Proofs for Conjoining BDDs
• Extended Resolution Proofs for Symbolic SAT Solving with Quantification
• Extended resolution simulates binary decision diagrams
• Mechanical verification of SAT refutations with extended resolution
• Verifying Refutations with Extended Resolution

Cites work

• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• Binary decision diagrams
• Bucket elimination: A unifying framework for reasoning
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Efficient certified RAT verification
• Efficient verified (UN)SAT certificate checking
• Efficient, verified checking of propositional proofs
• Extended Resolution Proofs for Conjoining BDDs
• Extended Resolution Proofs for Symbolic SAT Solving with Quantification
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 3904558 (Why is no real title available?)
• scientific article; zbMATH DE number 7178357 (Why is no real title available?)
• Mutilated chessboard problem is exponentially hard for resolution
• On a generalization of extended resolution
• Ordered binary decision diagrams and the Davis-Putnam procedure
• Resolution and binary decision diagrams cannot simulate each other polynomially
• Symbolic model checking: \(10^{20}\) states and beyond
• The intractability of resolution
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
• What a difference a variable makes

Cited in

(10)

• Non-clausal redundancy properties
• Dual proof generation for quantified Boolean formulas with a BDD-based solver
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• Extended resolution simulates binary decision diagrams
• Extended Resolution Proofs for Conjoining BDDs
• Extending existential quantification in conjuctions of BDDs
• Extended Resolution Proofs for Symbolic SAT Solving with Quantification
• Generating Extended Resolution Proofs with a BDD-Based SAT Solver
• Clausal proofs for pseudo-Boolean reasoning
• Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms

This page was built for publication: Generating extended resolution proofs with a BDD-based SAT solver

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2044191)