pydepqbf 0.0.2

作者：

很多python绑定代码和文档都是从pycosat中提取出来的 <；https://pypi.python.org/pypi/pycosat>；

depqbf归florian lonsing所有<；http://lonsing.github.io/depqbf/>；

pydepqbf python模块与depqbf在同一术语下分布。

摘要

DepQBF是一个有效的 QBF求解器 由弗洛里安·朗辛用纯C语言写的。 这个包在C级别上为depqbf提供了高效的Python绑定， 即，当导入pydepqbf时，depqbf解算器成为 python进程本身。

用法

pydepqbf模块有一个函数：solve。

函数solve返回包含两个元素的元组。这个 第一个元素是一个整数，即qdpll_result_sat或 qdpll_result_unsat或qdpll_result_unknown。第二要素 包含输入问题的部分证书。如果最外层 （最左边的）量词块是一个非终结符。 量化，则部分证书是 此块的变量（对于不可满足的qbfs和universal是对偶的 最外层块的变量，如果该块是通用的 量化）。如果 可满足的qbf是普遍量化的，或者如果最外层的块 一个不可满足的QBF是存在量化的。

示例

让我们考虑以下问题，用 qdimacsQDIMACS 格式：

p cnf 5 3
a 1 2 0
e 3 4 0
-1 -3 0
1 2 4 0
1 -4 0

这里，我们有4个变量和3个子句，第一个子句是 （不是x₁或不是x₃）。 在python中，每个子句都是 最方便地表示为整数列表。很自然，它使 将每个解也表示为整数列表，其中 对应于布尔值（+表示真和-表示假）和 绝对值对应于i^th变量：

>>> from pydepqbf import solve, QDPLL_QTYPE_FORALL, QDPLL_QTYPE_EXISTS
>>> quantifiers = ((QDPLL_QTYPE_FORALL, (1, 2)), (QDPLL_QTYPE_EXISTS, (3, 4)))
>>> clauses = ((-1, -3), (1, 2, 4), (1, -4))
>>> solve(quantifiers, clauses)
(20, [-1, -2])

结果对的第一个元素是20（定义为 qdpll_result_unsat in the pydepqbf package）和partial 证书转换为：x₁=x₂=false。