Extended Resolution Proofs for Conjoining BDDs
From MaRDI portal
Publication:3434726
DOI10.1007/11753728_60zbMath1185.68635OpenAlexW1800789167MaRDI QIDQ3434726
Publication date: 2 May 2007
Published in: Computer Science – Theory and Applications (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11753728_60
Related Items (15)
On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Extended clause learning ⋮ A finite state intersection approach to propositional satisfiability ⋮ Simulating strong practical proof systems with extended resolution ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Producing and verifying extremely large propositional refutations ⋮ Variable and Clause Ordering in an FSA Approach to Propositional Satisfiability ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ Generating extended resolution proofs with a BDD-based SAT solver ⋮ Efficient verified (UN)SAT certificate checking ⋮ Non-clausal redundancy properties ⋮ Dual proof generation for quantified Boolean formulas with a BDD-based solver ⋮ Dynamic Symmetry Breaking by Simulating Zykov Contraction ⋮ DRAT Proofs for XOR Reasoning
Uses Software
This page was built for publication: Extended Resolution Proofs for Conjoining BDDs
