Abstract
We describe a novel decision procedure for Quantified Boolean Formulas (QBFs) which aims to unleash the hidden potential of quantified reasoning in applications. The Skolem theorem acts like a glue holding several ingredients together: BDD-based representations for boolean functions, search-based QBF decision procedure, and compilation-to-SAT techniques, among the others. To leverage all these techniques at once we show how to evaluate QBFs by symbolically reasoning on a compact representation for the propositional expansion of the skolemized problem. We also report about a first implementation of the procedure, which yields very interesting experimental results. © Springer-Verlag Berlin Heidelberg 2005.
Cite
CITATION STYLE
Benedetti, M. (2005). Evaluating QBFs via symbolic skolemization. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3452 LNAI, pp. 285–300). Springer Verlag. https://doi.org/10.1007/978-3-540-32275-7_20
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
