Certified DQBF solving by definition extraction (Q2118343): Difference between revisions

@@ Property / describes a project that uses @@
+CaDiCaL
@@ Property / describes a project that uses: CaDiCaL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+iProver
@@ Property / describes a project that uses: iProver / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PySAT
@@ Property / describes a project that uses: PySAT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HQSpre
@@ Property / describes a project that uses: HQSpre / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3183677195
@@ Property / OpenAlex ID: W3183677195 / rank @@
+Normal rank
@@ Property / cites work @@
+What's hard about Boolean functional synthesis?
@@ Property / cites work: What's hard about Boolean functional synthesis? / rank @@
+Normal rank
@@ Property / cites work @@
+Lower bounds for multiplayer noncooperative games of incomplete information
+Normal rank
@@ Property / cites work @@
+Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
+Normal rank
@@ Property / cites work @@
+Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
+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 @@
+Dependency Quantified Horn Formulas: Models and Complexity
+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 @@
+Encodings of Bounded Synthesis
@@ Property / cites work: Encodings of Bounded Synthesis / rank @@
+Normal rank
@@ Property / cites work @@
+Fast DQBF Refutation
@@ Property / cites work: Fast DQBF Refutation / rank @@
+Normal rank
@@ Property / cites work @@
+PySAT: a Python toolkit for prototyping with SAT oracles
+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 @@
+A theory of formal synthesis via inductive learning
+Normal rank
@@ Property / cites work @@
+iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
+Normal rank
@@ Property / cites work @@
+The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
+Normal rank
@@ Property / cites work @@
+A resolution-style proof system for DQBF
@@ Property / cites work: A resolution-style proof system for DQBF / rank @@
+Normal rank
@@ Property / cites work @@
+Incremental Determinization
@@ Property / cites work: Incremental Determinization / rank @@
+Normal rank
@@ Property / cites work @@
+Q2786915
@@ Property / cites work: Q2786915 / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation-based semantic gate extraction and its applications to QBF preprocessing
+Normal rank
@@ Property / cites work @@
+Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
+Normal rank
@@ Property / cites work @@
+Q4131648
@@ Property / cites work: Q4131648 / rank @@
+Normal rank
@@ Property / cites work @@
+CAQE and QuAbS: Abstraction Based QBF Solvers
@@ Property / cites work: CAQE and QuAbS: Abstraction Based QBF Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Clausal abstraction for DQBF
@@ Property / cites work: Clausal abstraction for DQBF / rank @@
+Normal rank
@@ Property / cites work @@
+Fast interpolating BMC
@@ Property / cites work: Fast interpolating BMC / rank @@
+Normal rank
@@ Property / cites work @@
+From DQBF to QBF by dependency elimination
@@ Property / cites work: From DQBF to QBF by dependency elimination / rank @@
+Normal rank
@@ Property / cites work @@
+The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1
+Normal rank
@@ Property / cites work @@
+Dependency Schemes for DQBF
@@ Property / cites work: Dependency Schemes for DQBF / rank @@
+Normal rank