Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations

DOI10.1007/s10703-021-00371-7OpenAlexW3195087575WikidataQ113902759 ScholiaQ113902759MaRDI QIDQ2058378

Roderick Bloem, Vedad Hadzic, Uwe Egly, Florian Lonsing, Nicolas Braud-Santoni, Martina Seidl

Publication date: 8 December 2021

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-021-00371-7

zbMATH Keywords

decision proceduresquantified Boolean formulasCEGAR

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (1)

Never trust your solver: certification for SAT and QBF

Uses Software

• sQueezeBF
• Bloqqer
• QUBOS
• DepQBF
• CAQE
• semprop
• HQSpre
• QRATPre+
• RAReQS
• QESTO

Cites Work

• Unnamed Item
• Unnamed Item
• Solving QBF with counterexample guided refinement
• SAT race 2015
• Dependency learning for QBF
• Resolution for quantified Boolean formulas
• On expansion and resolution in CEGAR based QBF solving
• QRATPre+: effective QBF preprocessing via strong redundancy properties
• Expansion-based QBF solving versus Q-resolution
• Conformant planning as a case study of incremental QBF solving
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Non-prenex QBF Solving Using Abstraction
• 2QBF: Challenges and Solutions
• Solving QBF with Counterexample Guided Refinement
• On Unification of QBF Resolution-Based Calculi
• SAT-Based Synthesis Methods for Safety Specs
• Clause Elimination for SAT and QSAT
• Abstraction-Based Algorithm for 2QBF
• Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
• QBF Encoding of Temporal Properties and QBF-Based Verification
• Detecting Unrealizability of Distributed Fault-tolerant Systems
• Encodings of Bounded Synthesis
• Counterexample-guided abstraction refinement for symbolic model checking
• QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
• Bounded Universal Expansion for Preprocessing QBF
• Stable-unstable semantics: Beyond NP with normal logic programs
• Structural Synthesis for GXW Specifications
• sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning
• Blocked Clause Elimination for QBF
• On Propositional QBF Expansions and Q-Resolution
• Theory and Applications of Satisfiability Testing

This page was built for publication: Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations