Dissertation
- Florian Lonsing. Dependency Schemes and Search-Based QBF Solving: Theory and Practice. PhD Thesis. Johannes Kepler University, Linz, Austria. 2012
- Advisor: Univ.-Prof. Dr. Armin Biere
- Co-Advisor: Assist.-Prof. Dr. Martina Seidl
- Second Reader: Ao. Univ.-Prof. Dr. Uwe Egly
- Defended: April 2012
Abstract
The logic of quantified Boolean formulae (QBF) extends propositional logic with universal quantification over propositional variables. The presence of universal quantifiers in QBF does not add expressiveness, but often allows for more compact encodings of problems. From a theoretical point of view, the decision problems of propositional logic (SAT) and QBF are NP-complete and PSPACE-complete, respectively. Compared to SAT, which successfully has been used for practical applications in model checking or formal verification, for example, empirical studies show that current approaches to QBF solving do not scale well in practice. The quantifier prefix of QBFs in prenex conjunctive normal form (PCNF) imposes a linear ordering on the variables. In general, the ordering of the prefix gives rise to dependencies between variables which are differently quantified. Variable dependencies restrict the freedom of QBF solvers and must be respected during semantical evaluation to avoid incorrect results. We consider dependency schemes, which were introduced in related work, to overcome the drawbacks of quantifier prefixes in PCNFs. A dependency scheme is a binary relation over the set of variables of a PCNF which expresses independence between variables. If two variables are independent then a search-based QBF solver can safely assign them in arbitrary order. Thus independence increases the freedom for QBF solvers. We analyze theoretical properties of different dependency schemes which can be computed by analyzing the syntactic structure of a PCNF. We show that the common approach of mini-scoping is not optimal among syntactic methods of dependency analysis. As an alternative, we introduce specific approaches to compute and represent the standard dependency scheme efficiently. As a byproduct, we obtain compact dependency graphs as a representation of arbitrary dependency schemes. A main contribution of this work is the combination of arbitrary dependency schemes and search-based QBF solvers relying on the QDPLL algorithm. This way, QDPLL can profit from independence of variables which otherwise is hidden by the quantifier prefix. We implemented the solver DepQBF which tightly integrates dependency schemes. Experimental results confirm the potential benefits for practical QBF solving in contrast to quantifier prefixes. Our results motivate further research on dependency schemes for applications in QBF solving.