Evaluating QBFs via Symbolic Skolemization

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.

• Type: Conference
• Year: 2004
• Where: LPAR
• Authors: Marco Benedetti
• Keywords: Boolean Formulas, Decision Procedure, LPAR 2004, QBF Decision Procedure