Solving QBF with counterexample guided refinement (Q253964): Difference between revisions

@@ Property / DOI @@
-.1016/j.artint.2016.01.004
@@ Property / DOI: 10.1016/j.artint.2016.01.004 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+QUBE
@@ Property / describes a project that uses: QUBE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CirQit2
@@ Property / describes a project that uses: CirQit2 / 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.1016/j.artint.2016.01.004
+Normal rank
@@ Property / OpenAlex ID @@
+W2233304325
@@ Property / OpenAlex ID: W2233304325 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q62047276
@@ Property / Wikidata QID: Q62047276 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3620436
@@ Property / cites work: Q3620436 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic for Programming, Artificial Intelligence, and Reasoning
+Normal rank
@@ Property / cites work @@
+Nenofex: Expanding NNF for QBF Solving
@@ Property / cites work: Nenofex: Expanding NNF for QBF Solving / rank @@
+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 @@
+sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
+Normal rank
@@ Property / cites work @@
+Failed Literal Detection for QBF
@@ Property / cites work: Failed Literal Detection for QBF / rank @@
+Normal rank
@@ Property / cites work @@
+Binary Clause Reasoning in QBF
@@ Property / cites work: Binary Clause Reasoning in QBF / 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 @@
+Principles and Practice of Constraint Programming – CP 2004
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Counterexample-guided abstraction refinement for symbolic model checking
+Normal rank
@@ Property / cites work @@
+Q4412858
@@ Property / cites work: Q4412858 / 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 @@
+Solving QBF with Counterexample Guided Refinement
@@ Property / cites work: Solving QBF with Counterexample Guided Refinement / rank @@
+Normal rank
@@ Property / cites work @@
+Q5604434
@@ Property / cites work: Q5604434 / rank @@
+Normal rank
@@ Property / cites work @@
+A structure-preserving clause form translation
@@ Property / cites work: A structure-preserving clause form translation / rank @@
+Normal rank
@@ Property / cites work @@
+Q4298260
@@ Property / cites work: Q4298260 / 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 @@
+Solving satisfiability problems with preferences
@@ Property / cites work: Solving satisfiability problems with preferences / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809077
@@ Property / cites work: Q4809077 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804899
@@ Property / cites work: Q4804899 / rank @@
+Normal rank
@@ Property / cites work @@
+The minimum equivalent DNF problem and shortest implicants
+Normal rank
@@ Property / cites work @@
+A Non-prenex, Non-clausal QBF Solver with Game-State Learning
+Normal rank
@@ Property / cites work @@
+The QBF Gallery: behind the scenes
@@ Property / cites work: The QBF Gallery: behind the scenes / rank @@
+Normal rank
@@ Property / cites work @@
+Exploiting Circuit Representations in QBF Solving
@@ Property / cites work: Exploiting Circuit Representations in QBF Solving / rank @@
+Normal rank
@@ Property / cites work @@
+Efficiently solving quantified bit-vector formulas
+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 @@
+Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription
+Normal rank
@@ Property / cites work @@
+Using SAT in QBF
@@ Property / cites work: Using SAT in QBF / rank @@
+Normal rank
@@ Property / cites work @@
+Q3566747
@@ Property / cites work: Q3566747 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4427904
@@ Property / cites work: Q4427904 / rank @@
+Normal rank
@@ Property / cites work @@
+Experiments with Reduction Finding
@@ Property / cites work: Experiments with Reduction Finding / rank @@
+Normal rank
@@ Property / cites work @@
+Quantified Maximum Satisfiability:
@@ Property / cites work: Quantified Maximum Satisfiability: / 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 @@
+On Unification of QBF Resolution-Based Calculi
@@ Property / cites work: On Unification of QBF Resolution-Based Calculi / rank @@
+Normal rank
@@ Property / cites work @@
+Contributions to the Theory of Practical Quantified Boolean Formula Solving
+Normal rank
@@ Property / cites work @@
+Unified QBF certification and its applications
@@ Property / cites work: Unified QBF certification and its applications / 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 @@
+Q2954985
@@ Property / cites work: Q2954985 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / rank @@
+Normal rank
@@ Property / DOI @@
+.1016/J.ARTINT.2016.01.004
@@ Property / DOI: 10.1016/J.ARTINT.2016.01.004 / rank @@
+Normal rank