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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

PyQBF: A Python Framework for Solving Quantified Boolean Formulas

  • Mark Peyrer,
  • Maximilian Heisinger,
  • Martina Seidl

摘要

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.