pylgl 0.0.3

作者：

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

玲玲归Armin Biere所有<；http://fmv.jku.at/lingeling/>；

PYLGL的分布条件与LINGEN相同。

摘要

Lingeling是一个有效的 SAT求解器 由阿明·比埃尔用纯C语言写的。 这个包提供了高效的python绑定，可以在c级别徘徊， 即，当导入pylgl时，延迟解算器成为 python进程本身。为了便于部署，延迟的源文件 包括在这个项目中。这些文件有 从逗留版本BBE-6FE9691-170131中提取。

用法

pylgl模块有两个函数solve和itersolve， 两者都以一个可数从句作为论据。各条款 它本身表示为（非零）整数的iterable。

函数solve返回以下值之一：

• 一个解决方案（整数列表）
• 字符串“unsat”（当子句不可满足时）
• 字符串“未知”（当无法在 传播极限）

函数itersolve返回解决方案上的迭代器。当 指定了传播限制，用尽迭代器可能不会产生所有 可能的解决方案。

两个函数都采用以下关键字参数：

• vars：变量数（整数）
• verbose：详细级别（整数）
• simplify：启用简化（整数）
• seed：随机数生成器种子（整数）
• randec：启用随机决策顺序（整数）
• randecint：随机决策顺序间隔（整数）
• randphase：启用随机决策阶段（整数）
• randphaseint：随机决策阶段间隔（整数）

示例

让我们考虑下面的子句，用 迪马克一家 格式：

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

这里，我们有5个变量和3个子句，第一个子句是 （x₁或不x₅或x₄）。 注意，变量x₂不在任何子句中使用， 这意味着对于x₂=true的每个解，我们必须 还有一个x₂=false的解决方案。在python中，每个子句都是 最方便地表示为整数列表。很自然，它使 将每个解也表示为整数列表，其中 对应于布尔值（+表示真和-表示假）和 绝对值对应于i^th变量：

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

此解转化为：x₁=x₅=true， x₂=x₃=x₄=false

要查找所有解决方案，请使用itersolve：

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

在这个例子中，总共有18个可能的解决方案，必须 是偶数，因为x₂在子句中未指定。

itersolve返回迭代器，这使得它非常优雅 对许多类型的操作都很有效。例如，使用 标准库中的itertools模块 将构造一个（最多）3个解决方案的列表：

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

itersolve的实现

一个人如何从一个解决方案到另一个解决方案？ 答案出奇的简单。其中一个添加了 找到了作为新子句的解决方案。这个新条款保证了 搜索解决方案，因为它排除了已找到的解决方案。 这里基本上是itersolve的纯python实现 共solve：

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

这个实现有几个问题。首先，它相当缓慢 pylgl.solve必须反复转换子句列表 再一次。其次，在调用py_itersolve之后，子句列表将 被修改是的。在pylgl中，itersolve在c级实现， 使用延迟的C接口（这使得它更快 比上面天真的python实现）。