PyQBF: A Python Framework for Solving Quantified Boolean Formulas

PyQBF: A Python Framework for Solving Quantified Boolean Formulas

연구 분야: Software Development

학회: International Conference on Integrated Formal Methods

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 extend. 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. 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.