Model-Based Transformations for Quantified Boolean Formulas

Share
Author
Bubeck, U.
Pub. date
May 2010
Pages
226
Binding
softcover
Volume
329 of Dissertations in Artificial Intelligence
ISBN print
978-1-60750-545-7
Subject
Artificial Intelligence, Computer & Communication Sciences, Computer Science
€50 / US$73 Excl. VAT
Order Model-Based Transformations for Quantified Boolean Formulas ISBN @ €50.00

A popular approach for solving difficult decision problems in many areas, for example planning or verification, is to encode them as propositional formulas and to apply one of the powerful SAT solvers available today. Quantified Boolean formulas (QBF) generalize propositional logic by allowing universal and existential quantifiers over propositional variables. This permits very natural encodings which are often significantly more compact than their propositional counterparts, but also more difficult to solve.


The goal of this work is to support effective use of quantification by examining close relationships between formula structure and quantifier expressiveness. Useful subclasses with lower complexity are considered, in particular quantified Horn formulas and interesting generalizations thereof. From a theoretical and a practical point of view, this work presents efficient formula transformations and a pre-processing approach which allows the elimination of weak quantifiers from given QBF formulas in order to improve the performance of QBF solvers.