pycosat 0.6.6

用法

pycosat模块包含两个函数：solve和itersolve，这两个函数都接受一个子句的迭代器作为参数。每个子句本身也是一个整数迭代器（非零整数）。

函数solve返回以下之一

• 一个解（整数列表）

• 字符串“UNSAT”（当子句不可满足时）

• 字符串“UNKNOWN”（当在传播限制内无法确定解决方案时）

函数itersolve返回一个解的迭代器。当指定传播限制时，耗尽迭代器可能不会生成所有可能的解决方案。

这两个函数都接受以下关键字参数

• prop_limit：传播限制（整数）

• vars：变量数量（整数）

• verbose：详细程度（整数）

示例

让我们考虑以下子句，使用DIMACS cnf格式表示

p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

这里，我们有5个变量和3个子句，第一个子句是（x₁ 或 not x₅ 或 x₄）。请注意，变量x₂在任何一个子句中都没有被使用，这意味着对于每个x₂ = True的解，我们也必须有一个x₂ = False的解。在Python中，每个子句最方便的表示方法是一个整数列表。自然地，将每个解也表示为整数列表是有意义的，其中符号对应于布尔值（+表示True，-表示False），绝对值对应于第i个变量

>>> import pycosat
>>> cnf = [[1, -5, 4], [-1, 5, 3, 4], [-3, -4]]
>>> pycosat.solve(cnf)
[1, -2, -3, -4, 5]

这个解翻译为：x₁ = x₅ = True，x₂ = x₃ = x₄ = False

要找到所有解，请使用itersolve

>>> for sol in pycosat.itersolve(cnf):
...     print sol
...
[1, -2, -3, -4, 5]
[1, -2, -3, 4, -5]
[1, -2, -3, 4, 5]
...
>>> len(list(pycosat.itersolve(cnf)))
18

在这个例子中，总共有18个可能的解，因为子句中没有指定x₂，所以这个数字必须是一个偶数。

由于itersolve返回一个迭代器，这使得它在许多类型的操作中非常优雅且高效。例如，使用标准库中的itertools模块，以下是构建（最多）3个解列表的方法

>>> import itertools
>>> list(itertools.islice(pycosat.itersolve(cnf), 3))
[[1, -2, -3, -4, 5], [1, -2, -3, 4, -5], [1, -2, -3, 4, 5]]

itersolve的实现

如何从一个解找到另一个解？答案是惊人的简单。只需将已找到的解的逆作为新的子句添加。这个新的子句确保搜索另一个解，因为它排除了已找到的解。以下是在terms of solve中基本上是纯Python实现的itersolve

def py_itersolve(clauses): # don't use this function!
    while True:            # (it is only here to explain things)
        sol = pycosat.solve(clauses)
        if isinstance(sol, list):
            yield sol
            clauses.append([-x for x in sol])
        else: # no more solutions -- stop iteration
            return

这个实现有几个问题。首先，它相当慢，因为pycosat.solve需要一次又一次地转换子句列表。其次，调用py_itersolve后，子句列表将被修改。在pycosat中，itersolve在C级别实现，利用picosat C接口（这使得它比上述简单的Python实现快得多）。