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.
