SAT验证器python

Question

我使用的是python和Sympy。

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

我如何有效地将这个表达式转换到其他库中，无论这个赋值是否满足规则，给定x，y，z和一个我将获得True/False的规则？

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

为了将症状函数转换为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))

希望这能像你所希望的那样加速你的问题。