University of Limerick Institutional Repository

Solving QBF with counterexample guided refinement

DSpace Repository

Show simple item record Janota, Mikolas Klieber, William Marques-Silva, Joao Clarke, Edmund 2013-01-02T14:52:09Z 2013-01-02T14:52:09Z 2012
dc.description peer-reviewed en_US
dc.description.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. en_US
dc.language.iso eng en_US
dc.publisher Springer en_US
dc.relation.ispartofseries The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012). Lecture Notes in Computer Science;7317, pp. 114-128
dc.rights The original publication is available at en_US
dc.subject CEGAR en_US
dc.subject software engineering en_US
dc.subject algorithms en_US
dc.title Solving QBF with counterexample guided refinement en_US
dc.type info:eu-repo/semantics/conferenceObject en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.contributor.sponsor FCT en_US
dc.contributor.sponsor SFI en_US
dc.relation.projectid ATTEST (CMU-PT/ELE/0009/2009) en_US
dc.relation.projectid POLARIS (PTDC/EIA-CCO/123051/2010) en_US
dc.relation.projectid BEACON (09/IN.1/I2618) en_US
dc.rights.accessrights info:eu-repo/semantics/openAccess en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


My Account