python - 比较大型 bool 表达式的等价性

Question

我正在尝试简化和比较非常大的 bool 表达式的等价性。我传统上使用 sympy 中的 simplify_logic 来简化表达式，然后比较两个字符串是否等价。这仅适用于表达式包含 8 个或更少元素的情况。如果我试图比较两个分别有 15 个以上元素的表达式，它就会挂起(因为它花费的时间呈指数增长)。是否有任何 Python 包或其他迂回方式来尝试和完成此任务？

使用随机示例更新

Exp1 = 'A|B&(C|D|E)&F|H|I|J|(K&L&M)|K'

Exp2 = 'A&B&C&(D|E|F|J|K|L)&M&K&O&P'

Exp1 == Exp2 ----> 假

这些显然不一样，只是我可能遇到的一些失控表达式的例子。为了理智起见，当我的实际情况每个表达式都是 10 个数字/字母的混合时，每个元素只有 1 个字母长。

Answer 1

测试 bool 表达式的等价性在计算上与求解 Boolean satisfiability problem 一样复杂.

为了在一个方向上减少，一个公式是可满足的当且仅当它不等同于公式 False。在另一个方向上，两个公式 A 和 B 等价当且仅当 (A and not B) or (not A and B)是不可满足的。

这个问题是 NP 完全问题，因此没有已知的解决方案可以在最坏的情况下有效地处理大型公式。但是，“大”是相对的； says Wikipedia :

Since the SAT problem is NP-complete, only algorithms with exponential worst-case complexity are known for it. In spite of this, efficient and scalable algorithms for SAT were developed during the 2000s and have contributed to dramatic advances in our ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints (i.e. clauses).

所以你的问题，只有几十个子句和几百个变量，应该是很可行的。维基百科推荐了一些算法:

There are two classes of high-performance algorithms for solving instances of SAT in practice: the conflict-driven clause learning algorithm, which can be viewed as a modern variant of the DPLL algorithm (well known implementations include Chaff and GRASP) and stochastic local search algorithms, such as WalkSAT.