PyQBF: A Python Framework for Solving Quantified Boolean Formulas

Over the last years many solvers for quantified Boolean formulas (QBFs) have been developed. While most of these solvers support QDIMACS as a standard input format, exchanging a QBF solver within a reasoning framework is often a challenging task. Many solvers do not provide an API but they can only be used via their executable. Further, incremental solving is only supported to a limited extent.

We present PyQBF, a Python-based framework that provides a uniform programmatic interface to state-of-the-art QBF solvers. In this paper, we introduce the general architecture of PyQBF, describe the supported features and give a detailed example that illustrates how our framework can be used to implement an enumerative QBF solution counter as well as to solve a bounded model checking problem using a non-CNF representation. Our extensive experimental evaluation shows the efficiency of PyQBF. The experiments indicate that there is only little overhead compared to direct usage of the solvers.