有没有办法确定Python中两个符号布尔表达式是否相等？

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

有没有办法确定Python中两个符号布尔表达式是否相等？

Answer 1

equals对我来说很好：

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

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

一般来说，equals尝试转换这两个表达式，直到它们彼此相等，并且只有在失败时才返回False。因此它比==更准确（但也更慢）。

Answer 2

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 3

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的实例。

在我正在测试的版本（0.7.2）上，我也为Equivalent(~x & ~y, ~(x | y))获得了True，显然是因为这个版本自动将De Morgan的定律应用于~(x | y)：

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

Equivalent(x | (x & y), x | y)的输出绝对正确，因为这实际上不是重言式。当x为假且y为真时，等价不成立。