Dual proof generation for quantified Boolean formulas with a BDD-based solver

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

Mathematics Subject Classification ID

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

• OEIS
• DepQBF
• GhostQ

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