PyQBF: A Python Framework for Solving Quantified Boolean Formulas (short paper)
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
International Conference on Integrated Formal Methods (iFM 2024)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
Over the last years many solvers for quantified Boolean for-
mulas (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 uni-
form 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 solu-
tion 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.
Forschungs-