Generating Extended Resolution Proofs with a BDD-Based SAT Solver
From MaRDI portal
Publication:6082228
DOI10.1145/3595295MaRDI QIDQ6082228
Randal E. Bryant, Marijn J. H. Heule
Publication date: 3 November 2023
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Boolean satisfiabilitybinary decision diagramsextended resolutionpigeonhole problemmutilated chessboardUrquhart formulas
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Producing and verifying extremely large propositional refutations
- The intractability of resolution
- Explicit constructions of linear-sized superconcentrators
- Symbolic model checking: \(10^{20}\) states and beyond
- Resolution and binary decision diagrams cannot simulate each other polynomially
- Equivalent literal propagation in the DLL procedure
- Mutilated chessboard problem is exponentially hard for resolution
- On a generalization of extended resolution
- Bucket elimination: A unifying framework for reasoning
- Generating extended resolution proofs with a BDD-based SAT solver
- Dual proof generation for quantified Boolean formulas with a BDD-based solver
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
- Efficient certified RAT verification
- Sorting parity encodings by reusing variables
- Binary Decision Diagrams
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Extended Resolution Proofs for Conjoining BDDs
- Expander graphs and their applications
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- Graph-Based Algorithms for Boolean Function Manipulation
- Towards a Semantics of Unsatisfiability Proofs with Inprocessing
- The Complexity of Propositional Proofs
- Verifying Refutations with Extended Resolution
- Ordered Binary Decision Diagrams and the Davis-Putnam procedure
- Theory and Applications of Satisfiability Testing
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
- Theory and Applications of Satisfiability Testing
- Extended Resolution Proofs for Symbolic SAT Solving with Quantification
- Efficient verified (UN)SAT certificate checking
