Solving QBF with counterexample guided refinement

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

zbMATH Keywords

expansioncounterexample guided abstraction refinement (CEGAR)QBF

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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

• MiniSat
• sQueezeBF
• Quaffle
• Bloqqer
• Nenofex
• QUBOS
• DepQBF
• CirQit2
• QUBE
• semprop
• Mjollnir
• sKizzo

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