SAT Verifier 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

あなたは（x=True/False, y=True/False, z=True/Falseで）2通りの方法で、純粋なPythonでそれを行うことができます。

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に変換するためです。 essionあなたは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)) 

希望...