Solving QBF with Counterexample Guided Refinement
From MaRDI portal
Publication:2843327
DOI10.1007/978-3-642-31612-8_10zbMath1273.68178OpenAlexW1503377936MaRDI QIDQ2843327
William Klieber, Mikoláš Janota, Edmund M. Clarke, João P. Marques-Silva
Publication date: 12 August 2013
Published in: Theory and Applications of Satisfiability Testing – SAT 2012 (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.422.9685
Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
Quantified maximum satisfiability ⋮ An approximation framework for solvers and decision procedures ⋮ The QBF Gallery: behind the scenes ⋮ QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving ⋮ Propositional SAT Solving ⋮ Solving dependency quantified Boolean formulas using quantifier localization ⋮ Conformant planning as a case study of incremental QBF solving ⋮ Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem ⋮ Lower Bound Techniques for QBF Proof Systems ⋮ Long-distance Q-resolution with dependency schemes ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Synchronous counting and computational algorithm design ⋮ Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models ⋮ True crafted formula families for benchmarking quantified satisfiability solvers ⋮ Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable ⋮ Complexity-sensitive decision procedures for abstract argumentation ⋮ Refutation-based synthesis in SMT ⋮ Incremental Determinization ⋮ Non-prenex QBF Solving Using Abstraction ⋮ 2QBF: Challenges and Solutions ⋮ Long Distance Q-Resolution with Dependency Schemes ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) ⋮ Expansion-based QBF solving versus Q-resolution ⋮ How QBF expansion makes strategy extraction hard ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ GhostQ ⋮ Solving QBF with counterexample guided refinement ⋮ Hardness and optimality in QBF proof systems modulo NP
Uses Software
