Extended Resolution Proofs for Conjoining BDDs
From MaRDI portal
Recommendations
- Generating extended resolution proofs with a BDD-based SAT solver
- Extended resolution simulates binary decision diagrams
- Extended Resolution Proofs for Symbolic SAT Solving with Quantification
- Resolution and binary decision diagrams cannot simulate each other polynomially
- scientific article; zbMATH DE number 2084326
Cited in
(26)- Resolution and binary decision diagrams cannot simulate each other polynomially
- Generating extended resolution proofs with a BDD-based SAT solver
- Non-clausal redundancy properties
- Dual proof generation for quantified Boolean formulas with a BDD-based solver
- Simulating strong practical proof systems with extended resolution
- Extended resolution simulates binary decision diagrams
- Functional encryption for inner product with full function privacy
- DRAT proofs for XOR reasoning
- scientific article; zbMATH DE number 2084326 (Why is no real title available?)
- On Extending Bounded Proofs to Inductive Proofs
- Dynamic Symmetry Breaking by Simulating Zykov Contraction
- A finite state intersection approach to propositional satisfiability
- Programming Combinations of Deduction and BDD-based Symbolic Calculation
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- Variable and clause ordering in an FSA approach to propositional satisfiability
- Proving with BDDs and control of information
- Extended Resolution Proofs for Symbolic SAT Solving with Quantification
- Efficient verified (UN)SAT certificate checking
- Generating Extended Resolution Proofs with a BDD-Based SAT Solver
- Extended clause learning
- Clausal proofs for pseudo-Boolean reasoning
- Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms
- Strategy extraction by interpolation
- Producing and verifying extremely large propositional refutations
- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
- Hiding propositional constants in BDDs.
This page was built for publication: Extended Resolution Proofs for Conjoining BDDs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3434726)
