Qute: A Dependency Learning QBF Solver
Quantified Boolean Formulas, or QBFs, augment propositional formulas with existential and universal quantification over truth values. QBFs can succinctly encode problems arising in areas such as formal verification and synthesis.
For instance, if \(\phi(X, Y)\) specifies a system's desired input/output behavior (with inputs \(X\) and outputs \(Y\)), the QBF \(\Phi = \forall X \exists Y \phi (X, Y)\) is true if there is a system implementing this specification. In general, the value of a variable \(y \in Y\) can depend on the values of all variables \(x \in X\), but in practice \(y\) often depends only on a small subset of \(X\). Such information on variable dependencies can significantly reduce the search space that QBF solvers must consider, but unfortunately deciding whether \(y\) depends on \(x\) is as hard as evaluating a QBF. Some solvers rely on so-called dependency schemes to over-approximate the set of variable dependencies, but the resulting approximation tends to be coarse and frequently coincides with the set of syntactic dependencies.
As part of our project on variable dependencies of QBFs we developed Qute, a QBF solver that obtains information on variable dependencies on the fly. Qute assumes that variable \(y\) is independent of variable \(x\) until it runs into a problem that suggests otherwise, in which case the pair \((x, y)\) is added to a database of dependencies that must be observed. Experiments show that Qute typically only learns a small fraction of a formula's syntactic dependencies, which results in improved propagation and a more freedom for decision heuristics.
Awards
Qute placed 3rd in the PCNF track of QBFEVAL'17.
Download
Qute is open source and available from GitHub. Qute is written in C++11 and requires Boost (Version >= 1.60).
Team
Friedrich Slivovsky, Tomas Peitl, and Stefan Szeider
Developers
Friedrich Slivovsky and Tomas Peitl
Publications
1 result
