Dual proof generation for quantified Boolean formulas with a BDD-based solver
From MaRDI portal
Publication:2055876
DOI10.1007/978-3-030-79876-5_25OpenAlexW3178381410MaRDI QIDQ2055876
Randal E. Bryant, Marijn J. H. Heule
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_25
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Never trust your solver: certification for SAT and QBF
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Solving QBF with counterexample guided refinement
- Polynomial-time validation of QCDCL certificates
- Resolution for quantified Boolean formulas
- Bucket elimination: A unifying framework for reasoning
- Generating extended resolution proofs with a BDD-based SAT solver
- Solution validation and extraction for QBF preprocessing
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- On Unification of QBF Resolution-Based Calculi
- Binary Decision Diagrams
- A Unified Proof System for QBF Preprocessing
- Evaluating and certifying QBFs: A comparison of state-of-the-art tools
- Extended Resolution Proofs for Conjoining BDDs
- A First Step Towards a Unified Proof Checker for QBF
- Graph-Based Algorithms for Boolean Function Manipulation
- GhostQ
- Blocked Clause Elimination for QBF
- Theory and Applications of Satisfiability Testing
- Extended Resolution Proofs for Symbolic SAT Solving with Quantification
- Principles and Practice of Constraint Programming – CP 2004
- GhostQ
