我们在当前的任务中遇到了挑战，我们需要将现有的逻辑表达式修改/最小化为另一个新的逻辑表达式。但结果应该是一样的。
例如：要求转换
(1 AND (2 OR 9 OR 10) AND (3 OR 4 OR 5) AND (6 OR 7) AND 8) OR (1 AND (2 OR 9 OR 10) AND (11 OR 12) AND 8)
进入
1 AND (2 OR 9 OR 10) AND 8 AND (((3 OR 4 OR 5) AND (6 OR 7)) OR 11 OR 12)
并查看它们是否在每个数字的（T 或 F）的各种组合中评估为相同。
我需要为几乎 100 多个表达式进行相同的活动。因此，我正在寻找一种工具来帮助加快速度。
根据前面的评论，这里是一个 Python 实现的示例，以蛮力方式检查两个条件是否相等。我基本上只是测试输入逻辑值的所有可能组合。这导致操作。例如，在我的电脑上大约需要 3 秒. 对于较低的值当然要快得多，这可能是最常发生的情况。
import numpy as np
def exp1(x):
return (x[0,:] & (x[1,:] | x[8,:] | x[9,:]) & \
(x[2,:] | x[3,:] | x[4,:]) & \
(x[5,:] | x[6,:]) & x[7,:]) | \
(x[0,:] & (x[1,:] | x[8,:] | x[9,:]) & \
(x[10,:] | x[11,:]) & x[7,:])
def exp2(x):
return x[0,:] & (x[1,:] | x[8,:] | x[9,:]) & x[7,:] & \
(((x[2,:] | x[3,:] | x[4,:]) & \
(x[5,:] | x[6,:])) | x[10,:] | x[11,:])
# for other logical operations in Python:
# https://numpy.org/doc/stable/reference/arrays.ndarray.html#arithmetic-matrix-multiplication-and-comparison-operations
def compareBoolConditions(exp1,exp2,n):
## 1 - generate all possible combinations
# from itertools import product
# comb = np.array(tuple(product(np.array([True, False]), repeat=n))).T
## 1 - 2nd solution
comb = np.array(np.meshgrid( *[[True, False] for i in range(n)] ) , order='F').T.reshape(-1,n)
## 1 - 3rd solution
# see https://stackoverflow.com/questions/1208118/using-numpy-to-build-an-array-of-all-combinations-of-two-arrays
## 2 - vectorized check
if np.all( exp1(comb) == exp2(comb) ):
print('equivalent conditions')
else:
print('conditions are not equivalent')
compareBoolConditions(exp1, exp2, 12)
我找到了多种生成组合的解决方案，因此根据问题的大小，您可能想要测试并选择更快的一个。
这不完全是一种工具，而是一种以图形方式比较逻辑表达式的便捷方法。使用电路来表示您的布尔表达式：每个电阻器可以是开门 (F) 或闭门 (T)，并联电阻表示 OR，串联电阻表示 AND。然后，检查对应于两个给定逻辑表达式的两个电路（图中的顶部和底部）可以识别它们是等效的。
如果我没记错的话，每个公式都有一个唯一的规范合取范式，并且对于每个可能的真值表，您可以从一组变量中创建一个相应的规范 CNF。因此，如果两个表达式具有相同的 CNF，则它们是等价的。
因此，如果您能找到一种将公式表达为 CNF（这是一个相当简单的算法）的方法，然后找到一种适当地对输出项进行排序的方法，则可以进行字符串等价检查。这将有效地解决许多情况，尽管有些逻辑表达式的 CNF 表示比输入呈指数级大，因此它不是万能药。
一个 Python 示例：
import re
from sympy.logic.boolalg import to_cnf
#Your inputs
str1 = "(1 AND (2 OR 9 OR 10) AND (3 OR 4 OR 5) AND (6 OR 7) AND 8) OR (1 AND (2 OR 9 OR 10) AND (11 OR 12) AND 8)"
str2 = "1 AND (2 OR 9 OR 10) AND 8 AND (((3 OR 4 OR 5) AND (6 OR 7)) OR 11 OR 12)"
#Convert numbers to something we can use as a variable
str1 = re.sub(r"\b([0-9]+)\b", r"x\1", str1)
str2 = re.sub(r"\b([0-9]+)\b", r"x\1", str2)
#Convert logic to something SymPy will recognize
str1 = str1.replace("AND", "&").replace("OR", "|")
str2 = str2.replace("AND", "&").replace("OR", "|")
#Check equivalence
print("Equivalent?", str(to_cnf(str1))==str(to_cnf(str2)))
```