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

DOI10.1007/978-3-030-79876-5_25MaRDI QIDQ2055876zbMATH OpenOpenAlexFDO

Authors Randal E. Bryant, Marijn J. H. Heule

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

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)

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

Cites work

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

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

Describes a project that uses

Uses Software

• GhostQ
• DepQBF
• OEIS

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)