University of Limerick
Browse
Janota_2012_QBF.pdf (587.8 kB)

Solving QBF with counterexample guided refinement

Download (587.8 kB)
conference contribution
posted on 2013-01-02, 14:52 authored by Mikolas Janota, William Klieber, Joao Marques-Silva, Edmund Clarke
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.

History

Publication

The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012). Lecture Notes in Computer Science;7317, pp. 114-128

Publisher

Springer

Note

peer-reviewed

Other Funding information

FCT, SFI

Rights

The original publication is available at www.springerlink.com

Language

English

Usage metrics

    University of Limerick

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC