Generating Extended Resolution Proofs with a BDD-Based SAT Solver

DOI10.1145/3595295MaRDI QIDQ6082228zbMATH OpenWikidataFDO

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

Publication date 3 November 2023

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3595295

zbMATH Keywords

binary decision diagramsBoolean satisfiabilityextended resolutionmutilated chessboardpigeonhole problemUrquhart formulas

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• 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
• Dual proof generation for quantified Boolean formulas with a BDD-based solver
• Efficient certified RAT verification
• Efficient verified (UN)SAT certificate checking
• Equivalent literal propagation in the DLL procedure
• Expander graphs and their applications
• Explicit constructions of linear-sized superconcentrators
• Extended Resolution Proofs for Conjoining BDDs
• Extended Resolution Proofs for Symbolic SAT Solving with Quantification
• Extending existential quantification in conjuctions of BDDs
• Generating extended resolution proofs with a BDD-based SAT solver
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 1614715 (Why is no real title available?)
• scientific article; zbMATH DE number 3487716 (Why is no real title available?)
• scientific article; zbMATH DE number 2102695 (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
• Producing and verifying extremely large propositional refutations
• Resolution and binary decision diagrams cannot simulate each other polynomially
• Sorting parity encodings by reusing variables
• Symbolic model checking: \(10^{20}\) states and beyond
• The Complexity of Propositional Proofs
• The intractability of resolution
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Towards a Semantics of Unsatisfiability Proofs with Inprocessing
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
• Verifying Refutations with Extended Resolution

Cited in

(1)

• Extended resolution clause learning via dual implication points

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 Q6082228)