A Non-prenex, Non-clausal QBF Solver with Game-State Learning
From MaRDI portal
Publication:4930584
DOI10.1007/978-3-642-14186-7_12zbMath1306.68161OpenAlexW1562832747MaRDI QIDQ4930584
Sicun Gao, Samir Sapra, William Klieber, Edmund M. Clarke
Publication date: 29 September 2010
Published in: Theory and Applications of Satisfiability Testing – SAT 2010 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14186-7_12
Learning and adaptive systems in artificial intelligence (68T05) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items (19)
Quantified maximum satisfiability ⋮ The QBF Gallery: behind the scenes ⋮ QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving ⋮ Lower Bound Techniques for QBF Proof Systems ⋮ Long-distance Q-resolution with dependency schemes ⋮ Subsumption-linear Q-resolution for QBF theorem proving ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Building strategies into QBF proofs ⋮ Incremental Determinization ⋮ Non-prenex QBF Solving Using Abstraction ⋮ On Q-Resolution and CDCL QBF Solving ⋮ Q-Resolution with Generalized Axioms ⋮ 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) ⋮ GhostQ ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ Solving QBF with counterexample guided refinement
Uses Software
This page was built for publication: A Non-prenex, Non-clausal QBF Solver with Game-State Learning
