Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations (Q2058378): Difference between revisions

@@ Property / describes a project that uses @@
+QRATPre+
@@ Property / describes a project that uses: QRATPre+ / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Bloqqer
@@ Property / describes a project that uses: Bloqqer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+QUBOS
@@ Property / describes a project that uses: QUBOS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+RAReQS
@@ Property / describes a project that uses: RAReQS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CAQE
@@ Property / describes a project that uses: CAQE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+sQueezeBF
@@ Property / describes a project that uses: sQueezeBF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+semprop
@@ Property / describes a project that uses: semprop / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+DepQBF
@@ Property / describes a project that uses: DepQBF / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10703-021-00371-7
+Normal rank
@@ Property / OpenAlex ID @@
+W3195087575
@@ Property / OpenAlex ID: W3195087575 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q113902759
@@ Property / Wikidata QID: Q113902759 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4427904
@@ Property / cites work: Q4427904 / rank @@
+Normal rank
@@ Property / cites work @@
+QBF: Challenges and Solutions
@@ Property / cites work: 2QBF: Challenges and Solutions / rank @@
+Normal rank
@@ Property / cites work @@
+SAT race 2015
@@ Property / cites work: SAT race 2015 / rank @@
+Normal rank
@@ Property / cites work @@
+On Unification of QBF Resolution-Based Calculi
@@ Property / cites work: On Unification of QBF Resolution-Based Calculi / rank @@
+Normal rank
@@ Property / cites work @@
+Blocked Clause Elimination for QBF
@@ Property / cites work: Blocked Clause Elimination for QBF / rank @@
+Normal rank
@@ Property / cites work @@
+SAT-Based Synthesis Methods for Safety Specs
@@ Property / cites work: SAT-Based Synthesis Methods for Safety Specs / rank @@
+Normal rank
@@ Property / cites work @@
+Stable-unstable semantics: Beyond NP with normal logic programs
+Normal rank
@@ Property / cites work @@
+Bounded Universal Expansion for Preprocessing QBF
@@ Property / cites work: Bounded Universal Expansion for Preprocessing QBF / rank @@
+Normal rank
@@ Property / cites work @@
+Structural Synthesis for GXW Specifications
@@ Property / cites work: Structural Synthesis for GXW Specifications / rank @@
+Normal rank
@@ Property / cites work @@
+Counterexample-guided abstraction refinement for symbolic model checking
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Conformant planning as a case study of incremental QBF solving
+Normal rank
@@ Property / cites work @@
+Encodings of Bounded Synthesis
@@ Property / cites work: Encodings of Bounded Synthesis / rank @@
+Normal rank
@@ Property / cites work @@
+Detecting Unrealizability of Distributed Fault-tolerant Systems
+Normal rank
@@ Property / cites work @@
+sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
+Normal rank
@@ Property / cites work @@
+Clause Elimination for SAT and QSAT
@@ Property / cites work: Clause Elimination for SAT and QSAT / rank @@
+Normal rank
@@ Property / cites work @@
+Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
+Normal rank
@@ Property / cites work @@
+Solving QBF with counterexample guided refinement
@@ Property / cites work: Solving QBF with counterexample guided refinement / rank @@
+Normal rank
@@ Property / cites work @@
+Solving QBF with Counterexample Guided Refinement
@@ Property / cites work: Solving QBF with Counterexample Guided Refinement / rank @@
+Normal rank
@@ Property / cites work @@
+On Propositional QBF Expansions and Q-Resolution
@@ Property / cites work: On Propositional QBF Expansions and Q-Resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Expansion-based QBF solving versus Q-resolution
@@ Property / cites work: Expansion-based QBF solving versus Q-resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Abstraction-Based Algorithm for 2QBF
@@ Property / cites work: Abstraction-Based Algorithm for 2QBF / rank @@
+Normal rank
@@ Property / cites work @@
+Resolution for quantified Boolean formulas
@@ Property / cites work: Resolution for quantified Boolean formulas / rank @@
+Normal rank
@@ Property / cites work @@
+A Non-prenex, Non-clausal QBF Solver with Game-State Learning
+Normal rank
@@ Property / cites work @@
+Q4412858
@@ Property / cites work: Q4412858 / rank @@
+Normal rank
@@ Property / cites work @@
+DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
+Normal rank
@@ Property / cites work @@
+QRATPre+: effective QBF preprocessing via strong redundancy properties
+Normal rank
@@ Property / cites work @@
+Dependency learning for QBF
@@ Property / cites work: Dependency learning for QBF / rank @@
+Normal rank
@@ Property / cites work @@
+Non-prenex QBF Solving Using Abstraction
@@ Property / cites work: Non-prenex QBF Solving Using Abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+On expansion and resolution in CEGAR based QBF solving
+Normal rank
@@ Property / cites work @@
+QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
+Normal rank
@@ Property / cites work @@
+QBF Encoding of Temporal Properties and QBF-Based Verification
+Normal rank