ALLQBF Solving by Computational Learning
Bernd Becker, Rüdiger Ehlers, Matthew Lewis, and Paolo Marin
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.
10th International Symposium on Automated Technology for Verification and Analysis (ATVA 2012).
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.