如何检查两个布尔表达式是否相等

Question

我如何知道两个布尔表达式是否等价？

String expr1 = "(A or B) and C";
String expr2 = "C and (B or A)";
boolean equals = areExprsEquals(expr1, expr2);

我想我应该...

1. 解析表达式并将其存储在某些结构数据中
2. 减少 OR 组中的表达
3. 检查两个表达式是否具有相同的组

例如，通过第二步我得到：

Expr1
(A or B) and C
Converted to:
(A and C) or (B and C)

Expr2
C and (B or A)
Converted to:
(C and B) or (C and A)

现在我必须知道是否有相同的组。一种方法是获取每个组的哈希值：

经验1：

group 1: 
(A and C)
Order:
(A and C)
Hash:
md5("a&c")

group 2:
(B and C)
Order:
(B and C)
Hash:
md5("b&c")

经验2：

group 1: 
(C and B)
Order:
(B and C)
Hash:
md5("b&c")

group 2:
(C and A)
Order:
(A and C)
Hash:
md5("a&c")

所以：

expr1: md5( sort(md5("a&c"), md5("b&c") ))
expr2: md5( sort(md5("b&c"), md5("a&c") ))

我可以做每个组的md5，排序，expr哈希就是所有哈希的md5。

但问题是......我怎样才能减少exprs？有什么算法吗？这些表达式仅使用 AND 和 OR 运算符。

Answer 1

有什么算法吗？

理论答案：

• 您试图解决的问题是布尔可满足性问题，也称为 SAT。

• 它是NP 完全的。

• 这意味着，没有已知的算法¹总能在多项式时间内找到 SAT 问题的解决方案；即没有算法的最坏情况是O(N^C)或更优，其中C是常数，N 是 SAT 问题中的变量数量。

• 有一个明显的解决方案，那就是O(2^N)……对解决方案空间进行强力搜索。存在更好的算法；请参阅维基百科文章，但在最坏的情况下它们都是指数级的。

实用的解决方案：

• 对于非常小的东西N，暴力可能会给出可接受的性能。

• 使用现有的 SAT 求解器，请记住，理论表明它在最坏的情况下具有指数行为。

• 避免出现大型问题N……或对您的应用程序进行编码，以便求解器具有“时间限制”；即如果它不能在规定的时间内得到解决方案，它就会放弃。

^{1 - 如果证明P == NP，那么对于这个问题和其他 NP 完全问题可能会出现更好的算法。}