Advanced dependency analysis for QBF

Abstract

The last two decades have seen the rise of extremely efficient solvers for the satisfiability problem of propositional logic (SAT). While SAT is, as an NP-complete problem, consid- ered theoretically intractable, the solvers have become so efficient that solving hard search and optimization problems from areas such as electronic design automation, software and hardware verification, or program synthesis via SAT encodings is now not only a feasible approach, but often the state of the art. Inspired by this success story, researchers started working on formalisms that could succinctly express an even wider range of problems than SAT can. One example, which we study, are quantified Boolean formulas (QBF). Quantified Boolean formulas generalize propositional logic with quantification, and the satisfiability problem for QBFs is PSPACE-complete. As a consequence of quantifier nesting in QBFs, dependencies between variables arise. In many cases, however, some dependencies that appear to be present syntactically, are spurious semantically. Dependency analysis is the process of identifying spurious dependencies and using that additional information to solve a QBF more efficiently. Prior to this thesis, the most general method for dependency analysis were dependency schemes. A dependency scheme is a mapping which takes a formula and returns a set of dependencies. The results in this thesis are related mainly to search-based QBF solvers that implement quantified con ict-driven constraint learning (QCDCL). The trace of a run of a QCDCL solver can be interpreted as a proof in long-distance Q-resolution. Our results can be summarized as follows: - we identify a sufficient condition for when a dependency scheme admits sound use and certificate extraction in QCDCL with long-distance Q-resolution; - we propose a new method for dependency analysis, called dependency learning, that is orthogonal to dependency schemes, and in which dependencies are computed dy- namically on the y as opposed to statically upfront; - we show that certificates extracted from long-distance Q-resolution proofs can be verified in polynomial time; - we report on an implementation of a portfolio for circuit QBFs, and identify a pair of key formula features that are excellent predictors of solver performance; - we present a dynamic implementation of the strongest known sound dependency scheme and demonstrate that dependency learning can be used together with de- pendency schemes; - we prove that two basic components of long-distance Q-resolution, universal reduction and merging, have incomparable strength, i.e., the proof systems without one of the rules are incomparable.