PyQBF: A Python Framework for Solving Quantified Boolean Formulas
Mark Peyrer, Maximilian Heisinger, Martina Seidl · Formal Aspects of Computing · 2025
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 article, 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 with direct usage of the solvers.