Portfolio-based algorithm selection for circuit QBFs

Abstract

Quantified Boolean Formulas (QBFs) are a generalization of propositional formulae that admits succinct encodings of verification and synthesis problems. Given that modern QBF solvers are based on different architectures with complementary performance characteristics, a portfolio-based approach to QBF solving is particularly promising. While general QBFs can be converted to prenex conjunctive normal form (PCNF) with small overhead, this transformation has been known to adversely affect performance. This issue has prompted the development of several solvers for circuit QBFs in recent years. We define a natural set of features of circuit QBFs and show that they can be used to construct portfolio-based algorithm selectors of state-of-the-art circuit QBF solvers that are close to the virtual best solver. We further demonstrate that most of this performance can be achieved using surprisingly small subsets of cheaply computable and intuitive features.