python - SAT验证器python

Question

我正在使用 python 和 Sympy。

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

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

Answer 1

你可以在纯 python 中通过 2 种方式来做到这一点（使用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模块：

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))

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