Loading...
Solving QBF with counterexample guided refinement
Date
2012
Abstract
We propose two novel approaches for using Counterexample- Guided Abstraction Re nement (CEGAR) in Quanti ed Boolean Formula (QBF) solvers. The rst approach develops a recursive algorithm whose search is driven by CEGAR (rather than by DPLL). The second approach employs CEGAR as an additional learning technique in an existing DPLL-based QBF solver. Experimental evaluation of the implemented prototypes shows that the CEGAR-driven solver outperforms existing solvers on a number of families in the QBF-LIB and that the DPLL solver bene ts from the additional type of learning. Thus this article opens two promising avenues in QBF: CEGAR-driven solvers as an alternative to existing approaches and a novel type of learning in DPLL.
Supervisor
Description
peer-reviewed
Publisher
Springer
Citation
The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012). Lecture Notes in Computer Science;7317, pp. 114-128
Files
Loading...
Janota_2012_QBF.pdf
Adobe PDF, 587.8 KB
Keywords
ULRR Identifiers
Funding code
Funding Information
FCT, Science Foundation Ireland (SFI)