ALLQBF Solving by Computational Learning

摘要: In the last years, search-based QBF solvers have become essential for many applications in formal methods domain. The exploitation of their reasoning efficiency has however been restricted to which a "satisfiable/unsatisfiable" answer or one model an open quantified Boolean formula suffices as outcome, whereas compact representation all models is required could not be tackled with so far. In this paper, we describe how computational learning provides remedy problem. Our algorithms employ solver and learn set given problem CNF (conjunctive normal form), DNF (disjunctive CDNF (conjunction DNFs) representation. We evaluate our approach experimentally using benchmarks from synthesis finite-state systems temporal logic monitor computation.