Generating extended resolution proofs with a BDD-based SAT solver
From MaRDI portal
Publication:2044191
DOI10.1007/978-3-030-72016-2_5zbMath1467.68203arXiv2105.00885OpenAlexW3136791784MaRDI QIDQ2044191
Marijn J. H. Heule, Randal E. Bryant
Publication date: 4 August 2021
Full work available at URL: https://arxiv.org/abs/2105.00885
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)
Related Items (4)
Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Non-clausal redundancy properties ⋮ Dual proof generation for quantified Boolean formulas with a BDD-based solver
Cites Work
- Unnamed Item
- Unnamed Item
- The intractability of resolution
- Symbolic model checking: \(10^{20}\) states and beyond
- Resolution and binary decision diagrams cannot simulate each other polynomially
- Efficient, verified checking of propositional proofs
- Mutilated chessboard problem is exponentially hard for resolution
- On a generalization of extended resolution
- Bucket elimination: A unifying framework for reasoning
- What a difference a variable makes
- Efficient certified RAT verification
- Binary Decision Diagrams
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Extended Resolution Proofs for Conjoining BDDs
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- Graph-Based Algorithms for Boolean Function Manipulation
- 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
This page was built for publication: Generating extended resolution proofs with a BDD-based SAT solver
