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中的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 expr分裂國家，你可以嘗試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)) 

希望儘可能多地希望加快你的問題了......