Variable Dependencies of Quantified Boolean Formulas

Abstract. The satisfiability problem of Quantified Boolean Formulas (QBF) offers succinct encodings for hard problems arising in areas such as formal verification and planning. This research project explores new ways to leverage independence of variables for QBF. The nesting of existential and universal quantifiers in Quantified Boolean Formulas can generate variable dependencies that are a serious obstacle to lifting successful techniques from propositional satisfiability to QBF. In some cases one can identify a variable dependency as spurious and conclude that the corresponding variables are in fact independent. This information can be used to significantly improve the performance of decision procedures, but deciding whether variables are independent is a highly intractable problem in itself. The aim of this project is three-fold: (A) to advance the state of the art in detecting variable independence by developing new theory and improved algorithms for currently used methods; (B) to nd new approaches to detecting and harnessing variable independence; (C) to extend the scope of successful techniques from QBF to more general problems.

A generic logical language for encoding combinatorial problems paired with an efficient decision procedure has several advantages over the design of problem-specific algorithms. Development time is reduced as users need only come up with an encoding, and advances in decision procedures translate to improved algorithms for free. Conversely, the development of decision procedures is spurred by a constant stream of instances stemming from new applications. The recent progress in decision procedures (so-called SAT solvers) for the satisfiability problem of propositional logic has been largely due to such a virtuous cycle. SAT solvers have become so efficient that many hard combinatorial problems can be solved in practice simply by encoding them in propositional logic. However, for certain problems, the size of the resulting formula increases exponentially with the original problem description so that only small instances can be solved by reduction to SAT. This issue has prompted research into decision procedures for more succinct logical languages such as Quantified Boolean Formulas (QBFs). The nesting of universal and existential quantifiers in QBFs induces dependencies among variables: the value of a variable has to be chosen depending on the value of another variable. Decision algorithms need to respect variable dependencies to ensure soundness, but this typically decreases their performance. In certain cases dependencies can be identified as spurious. Dependency analysis is concer- ned with detecting spurious dependencies to give QBF solvers more freedom and improve their performance. As part of the project, we were able to develop new techniques for dependency analysis such as dependency learning. Unlike previous approaches that identify spurious dependencies during preprocessing, dependency learning allows for the detection of spurious dependencies in a QBF solver at runtime. Experiments show that this leads to many dependencies being recognized as spurious, which cannot be identified during preprocessing. Moreover, the resulting decision procedure enjoys favorable properties that must be given up when using standard techniques for variable dependency analysis. We implemented dependency learning in a system called QUTE, which has established itself as one of the best state-of-the-art solvers over the course of several annual QBF solving competitions.