Mark Peyrer, Maximilian Heisinger, Martina Seidl,
"PyQBF: A Python Framework for Solving Quantified Boolean Formulas"
: Integrated Formal Methods, 19th International Conference (IFM 2024), Serie Lecture Notes in Computer Science, Vol. 15234, Springer, Cham, Seite(n) 279?287, 11-2024, ISBN: 978-3-031-76553-7
Original Titel:
PyQBF: A Python Framework for Solving Quantified Boolean Formulas
Sprache des Titels:
Englisch
Original Buchtitel:
Integrated Formal Methods, 19th International Conference (IFM 2024)
Original Kurzfassung:
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.
Forschungs-