Dual proof generation for quantified Boolean formulas with a BDD-based solver
type: Item
instance of: scholarly article
title: Dual proof generation for quantified Boolean formulas with a BDD-based solver
DOI: 10.1007/978-3-030-79876-5_25
author: Randal E. Bryant
author: Marijn J. H. Heule
publication date: 2021-12-01T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7437093
cites work: GhostQ
cites work: Winning ways for your mathematical plays. Vol. 1.
cites work: On Unification of QBF Resolution-Based Calculi
cites work: Theory and Applications of Satisfiability Testing
cites work: Blocked Clause Elimination for QBF
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: Binary Decision Diagrams
cites work: Generating extended resolution proofs with a BDD-based SAT solver
cites work: Bucket elimination: A unifying framework for reasoning
cites work: Q4198056
cites work: Q3624018
cites work: A Unified Proof System for QBF Preprocessing
cites work: Solution validation and extraction for QBF preprocessing
cites work: Solving QBF with counterexample guided refinement
cites work: Extended Resolution Proofs for Symbolic SAT Solving with Quantification
cites work: A First Step Towards a Unified Proof Checker for QBF
cites work: Resolution for quantified Boolean formulas
cites work: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
cites work: Evaluating and certifying QBFs: A comparison of state-of-the-art tools
cites work: Principles and Practice of Constraint Programming – CP 2004
cites work: Polynomial-time validation of QCDCL certificates
cites work: Extended Resolution Proofs for Conjoining BDDs
cites work: Q3682462
describes a project that uses: GhostQ
describes a project that uses: DepQBF
describes a project that uses: OEIS
MaRDI profile type: Publication
full work available at URL: 978-3-030-79876-5 25
OpenAlex ID: W3178381410
description: scientific article; zbMATH DE number 7437093