SAT验证器python答案

【问题标题】：SAT verifier pythonSAT验证器python
【发布时间】：2017-02-03 10:16:58
【问题描述】：

我正在使用 python 和 Sympy。

我有以下格式的规则：Or(x,And(y,z))。不幸的是，Sympy subs 和 xreplace 函数没有提供足够快的实现来验证 x=False、y=True 和 z=True 是否满足上述规则。

如何有效地将这个表达式转换为给定 x,y,z 和规则的其他库，无论这个分配是否满足规则，我都会得到 True/False？

【问题讨论】：

【解决方案1】：

你可以在纯 python 中通过两种方式做到这一点（x=True/False, y=True/False, z=True/False）：

x or (y and z)

或（如0 == False, 1 == True）：

x | (y & z)

然后您可以使用以下方法遍历所有组合：

from itertools import product

for x, y, z in product((True, False), repeat=3):
    print(x, y, z)
    print(x or (y and z))
    print(x | (y & z))
    print()

为了将 sympy 函数转换为 python 表达式，您可以尝试lambdify module:

from sympy import lambdify, Or, And, var

x, y, z = var('x y z')
or_and = lambdify((x, y, z), Or(x, And(y, z)))
print(or_and(True, False, False))

希望能像您希望的那样加速您的问题...

【讨论】：

这些是很好的建议，但问题是如何有效地将 Sympy 中的表达式转换为您建议的新形式。
@JackStevens：好的，误会了，抱歉。添加了更新。希望有帮助。
感谢您的建议，看起来不错。我试图在我的代码中实现它，这导致了一个不同的问题，我发布了另一个 stackoverflow question for。