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

DOI10.1007/978-3-030-79876-5_25OpenAlexW3178381410MaRDI QIDQ2055876FDOQ2055876

Authors: 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

Recommendations

• Generating extended resolution proofs with a BDD-based SAT solver
• Theory and Applications of Satisfiability Testing
• A First Step Towards a Unified Proof Checker for QBF
• Unified QBF certification and its applications
• Principles and Practice of Constraint Programming – CP 2004

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Blocked clause elimination for QBF
• Theory and Applications of Satisfiability Testing
• Graph-Based Algorithms for Boolean Function Manipulation
• Title not available (Why is that?)
• Resolution for quantified Boolean formulas
• Solving QBF with counterexample guided refinement
• On Unification of QBF Resolution-Based Calculi
• Principles and Practice of Constraint Programming – CP 2004
• Winning ways for your mathematical plays. Vol. 1.
• Extended Resolution Proofs for Symbolic SAT Solving with Quantification
• A unified proof system for QBF preprocessing
• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
• Bucket elimination: A unifying framework for reasoning
• Extended Resolution Proofs for Conjoining BDDs
• Title not available (Why is that?)
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• A First Step Towards a Unified Proof Checker for QBF
• Polynomial-time validation of QCDCL certificates
• Generating extended resolution proofs with a BDD-based SAT solver
• Binary decision diagrams
• Solution validation and extraction for QBF preprocessing
• Evaluating and certifying QBFs: a comparison of state-of-the-art tools
• GhostQ. System description
• GhostQ

Cited In (5)

• Generating Extended Resolution Proofs with a BDD-Based SAT Solver
• Moving definition variables in quantified Boolean formulas
• Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms
• Never trust your solver: certification for SAT and QBF
• True crafted formula families for benchmarking quantified satisfiability solvers

Uses Software

• OEIS
• DepQBF
• GhostQ

This page was built for publication: Dual proof generation for quantified Boolean formulas with a BDD-based solver

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055876)