University of Limerick Institutional Repository

Solving QBF with counterexample guided refinement

DSpace Repository

Show simple item record

dc.contributor.author Janota, Mikolas
dc.contributor.author Klieber, William
dc.contributor.author Marques-Silva, Joao
dc.contributor.author Clarke, Edmund
dc.date.accessioned 2013-01-02T14:52:09Z
dc.date.available 2013-01-02T14:52:09Z
dc.date.issued 2012
dc.identifier.uri http://hdl.handle.net/10344/2770
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.relation.uri http://dx.doi.org/10.1007/978-3-642-31612-8_10
dc.rights The original publication is available at www.springerlink.com 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


Browse

My Account

Statistics