
Florian Lonsing 


Dissertation
 Florian Lonsing. Dependency Schemes and SearchBased QBF Solving: Theory and
Practice. PhD Thesis. Johannes Kepler University, Linz, Austria. 2012
 Advisor: Univ.Prof. Dr. Armin Biere
 CoAdvisor: 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
NPcomplete and PSPACEcomplete, 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 searchbased 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 miniscoping 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 searchbased 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.
Downloads
 Dissertation: PDF
 Talk
slides: PDF
 More information on the QBF solver DepQBF can be found here.