Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
type: Item
instance of: scholarly article
title: Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
author: Roderick Bloem
author: Nicolas Braud-Santoni
author: Vedad Hadzic
author: Uwe Egly
author: Florian Lonsing
author: Martina Seidl
published in: Formal Methods in System Design
publication date: 2021-12-08T00:00:00Z
Mathematics Subject Classification ID: 68-XX
zbMATH DE Number: 7440320
zbMATH Keywords: quantified Boolean formulas
zbMATH Keywords: decision procedures
zbMATH Keywords: CEGAR
describes a project that uses: QESTO
describes a project that uses: HQSpre
describes a project that uses: QRATPre+
describes a project that uses: Bloqqer
describes a project that uses: QUBOS
describes a project that uses: RAReQS
describes a project that uses: CAQE
describes a project that uses: sQueezeBF
describes a project that uses: semprop
describes a project that uses: DepQBF
MaRDI profile type: Publication
full work available at URL: s10703-021-00371-7
OpenAlex ID: W3195087575
Wikidata QID: Q113902759
cites work: Q4427904
cites work: 2QBF: Challenges and Solutions
cites work: SAT race 2015
cites work: On Unification of QBF Resolution-Based Calculi
cites work: Blocked Clause Elimination for QBF
cites work: SAT-Based Synthesis Methods for Safety Specs
cites work: Stable-unstable semantics: Beyond NP with normal logic programs
cites work: Bounded Universal Expansion for Preprocessing QBF
cites work: Structural Synthesis for GXW Specifications
cites work: Counterexample-guided abstraction refinement for symbolic model checking
cites work: Theory and Applications of Satisfiability Testing
cites work: Conformant planning as a case study of incremental QBF solving
cites work: Encodings of Bounded Synthesis
cites work: Detecting Unrealizability of Distributed Fault-tolerant Systems
cites work: sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
cites work: Clause Elimination for SAT and QSAT
cites work: Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
cites work: Solving QBF with counterexample guided refinement
cites work: Solving QBF with Counterexample Guided Refinement
cites work: On Propositional QBF Expansions and Q-Resolution
cites work: Expansion-based QBF solving versus Q-resolution
cites work: Abstraction-Based Algorithm for 2QBF
cites work: Resolution for quantified Boolean formulas
cites work: A Non-prenex, Non-clausal QBF Solver with Game-State Learning
cites work: Q4412858
cites work: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
cites work: QRATPre+: effective QBF preprocessing via strong redundancy properties
cites work: Dependency learning for QBF
cites work: Non-prenex QBF Solving Using Abstraction
cites work: On expansion and resolution in CEGAR based QBF solving
cites work: QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
cites work: QBF Encoding of Temporal Properties and QBF-Based Verification
DOI: 10.1007/S10703-021-00371-7
description: scientific article; zbMATH DE number 7440320