Pythonで2つのシンボリックブール式が等しいかどうかを判断する方法はありますか？

Question

私はSympyとブール式の等価性を決定しようとしてきたが、それは、より複雑な式

from sympy.abc import x, y 
from sympy.logic.boolalg import * 

print(Equivalent(x, x)) 
print(Equivalent(x, x & True)) 
print(Equivalent(x | y, y | x)) 
print(Equivalent(x | (x & y), x | y)) 
print(Equivalent(~x & ~y, ~(x | y))) 

結果の等価性を検出しないようだ。

>>>True 
>>>True 
>>>True 
>>>Equivalent(Or(x, y), Or(And(x, y), x)) 
>>>Equivalent(Not(Or(x, y)), And(Not(x), Not(y))) 

を決定する方法はあります2つのシンボリックブール式がPythonで等しいかどうか

Answer 1

sympy.simplify_logicおそらく？

>>> sympy.simplify_logic(Equivalent(Or(x, y), Or(And(x, y), x))) 
Or(Not(y), x) 
>>> sympy.simplify_logic(Equivalent(Not(Or(x, y)), And(Not(x), Not(y)))) 
True 

Answer 2

sympy.Equivalentには、別個の式の論理的等価性を検出するために必要なブール充足可能ソルバーがありません。あなたがTrueを得た場合には、Equivalentに渡されたオブジェクトが既にによる&と|によって実行される変換に構造的に同等であった：より複雑なケースで

In [7]: x|y 
Out[7]: Or(x, y) 

In [8]: y|x 
Out[8]: Or(x, y) 

In [9]: x&True 
Out[9]: x 

、あなただけのEquivalentのインスタンスを取得します。 Equivalent(x | (x & y), x | y)の出力は

In [19]: ~(x|y) 
Out[19]: And(Not(x), Not(y)) 

です

：私は上でテストしていたバージョンで

（0.7.2）、私はまた、このバージョン ~(x | y)にド・モルガンの法則を自動的に適用されるが、どうやらので、 Equivalent(~x & ~y, ~(x | y))のために真の取得しますそれは実際に同音異義語ではないので間違いなく正しい。 xが偽でyが真である場合、等価は成立しません。

Answer 3

equalsは私のために正常に動作します：一般的に

(x|(x&y)).equals(x|y) 
# False 

(~x&~y).equals(~(x|y)) 
# True 

は、equals彼らは互いに等しくなるまで、2つの式を変換しようとすると、それが失敗した場合にのみFalseを返します。したがって、==よりも正確です（ただし遅くなります）。