Solving QBF with counterexample guided refinement
From MaRDI portal
Publication:253964
DOI10.1016/j.artint.2016.01.004zbMath1351.68254OpenAlexW2233304325WikidataQ62047276 ScholiaQ62047276MaRDI QIDQ253964
Mikoláš Janota, William Klieber, Edmund M. Clarke, João P. Marques-Silva
Publication date: 8 March 2016
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.artint.2016.01.004
Related Items (24)
Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving ⋮ Proof complexity of modal resolution ⋮ Unnamed Item ⋮ Never trust your solver: certification for SAT and QBF ⋮ BOCoSy: Small but Powerful Symbolic Output-Feedback Control ⋮ Towards Uniform Certification in QBF ⋮ Computing smallest MUSes of quantified Boolean formulas ⋮ Unnamed Item ⋮ Encodings of Bounded Synthesis ⋮ Lower bound techniques for QBF expansion ⋮ Unnamed Item ⋮ New models for generating hard random Boolean formulas and disjunctive logic programs ⋮ Q-Resolution with Generalized Axioms ⋮ RAReQS ⋮ Dual proof generation for quantified Boolean formulas with a BDD-based solver ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ Unnamed Item ⋮ The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ GhostQ ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ QBFFam: a tool for generating QBF families from proof complexity ⋮ Proof complexity of symbolic QBF reasoning ⋮ Certified DQBF solving by definition extraction
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The QBF Gallery: behind the scenes
- Solving satisfiability problems with preferences
- A structure-preserving clause form translation
- The minimum equivalent DNF problem and shortest implicants
- Resolution for quantified Boolean formulas
- Expansion-based QBF solving versus Q-resolution
- Unified QBF certification and its applications
- Efficiently solving quantified bit-vector formulas
- Solving QBF with Counterexample Guided Refinement
- On Unification of QBF Resolution-Based Calculi
- Abstraction-Based Algorithm for 2QBF
- Failed Literal Detection for QBF
- Counterexample-guided abstraction refinement for symbolic model checking
- Nenofex: Expanding NNF for QBF Solving
- Using SAT in QBF
- Bounded Universal Expansion for Preprocessing QBF
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
- A Non-prenex, Non-clausal QBF Solver with Game-State Learning
- Exploiting Circuit Representations in QBF Solving
- Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription
- Blocked Clause Elimination for QBF
- Theory and Applications of Satisfiability Testing
- On Propositional QBF Expansions and Q-Resolution
- Experiments with Reduction Finding
- Quantified Maximum Satisfiability:
- Automated Deduction – CADE-20
- Logic for Programming, Artificial Intelligence, and Reasoning
- Binary Clause Reasoning in QBF
- Principles and Practice of Constraint Programming – CP 2004
This page was built for publication: Solving QBF with counterexample guided refinement
