Name
Abstract | ||
|---|---|---|
In the last years, search-based QBF solvers have become essential for many applications in the formal methods domain. The exploitation of their reasoning efficiency has however been restricted to applications in which a "satisfiable/unsatisfiable" answer or one model of an open quantified Boolean formula suffices as an outcome, whereas applications in which a compact representation of all models is required could not be tackled with QBF solvers so far. In this paper, we describe how computational learning provides a remedy to this problem. Our algorithms employ a search-based QBF solver and learn the set of all models of a given open QBF problem in a CNF (conjunctive normal form), DNF (disjunctive normal form), or CDNF (conjunction of DNFs) representation. We evaluate our approach experimentally using benchmarks from synthesis of finite-state systems from temporal logic and monitor computation. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-33386-6_29 | ATVA |
Keywords | Field | DocType |
open qbf problem,search-based qbf solver,computational learning,boolean formula suffices,compact representation,disjunctive normal form,conjunctive normal form,formal methods domain,finite-state system,search-based qbf solvers | Discrete mathematics,Computer science,Disjunctive normal form,Theoretical computer science,Conjunctive normal form,Solver,Formal methods,Temporal logic,True quantified Boolean formula,Computation | Conference |
Citations | PageRank | References |
6 | 0.48 | 16 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bernd Becker | 1 | 6 | 0.48 |
| Rüdiger Ehlers | 2 | 236 | 21.00 |
| Matthew Lewis | 3 | 107 | 6.37 |
| Paolo Marin | 4 | 67 | 6.83 |