SymPy to_cnf() 的评估结果为 False

Question

我正在尝试采用布尔表达式并使用to_cnf()将其转换为合取范式。

我的布尔表达式相当复杂，所以我在调试时遇到问题。我无法使用任何简单的布尔表达式重现输出CNF: False。什么可能导致to_cnf输出 False？

#TEST 1
from sympy import symbols
from sympy.logic.boolalg import to_cnf
from sympy.logic import simplify_logic
ls = symbols('a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z')
z = "~(~(~(ls[11] | ~(~(~(~(ls[5]) | ~(ls[3])) | ls[15] & ls[18]) & ~(~(~(ls[5]) | ~(ls[3])) & ls[15])) & ls[17]) & ~(ls[11] & ~(~(~(~(ls[5]) | ~(ls[3])) | ls[15] & ls[18]) & ~(~(~(ls[5]) | ~(ls[3])) & ls[15]))) & ~(ls[14] | ls[7] | ls[1])) & ~(~(~(ls[14]) | ls[7] | ls[1]) & ~(ls[11]) | ls[17] & ~(ls[18]) | ls[15] & ~(ls[3]) | ls[5] | ~(ls[18]) & ls[15] | ~(ls[11]) & ls[17]) | ~(~(ls[4]) & ls[12] | ~(~(ls[4]) | ls[12])) & ~(ls[14]) | ls[1] | ~(ls[7]) | ~(ls[17]) | ~(ls[15]) | ~(ls[5]) & ~(ls[7]) | ls[14] | ~(ls[1]) | ls[12] & ~(~(ls[12] | ls[15] | ls[5] | ls[17]) & ~(ls[14] | ls[1] | ~(ls[7])) | ~(ls[4]) & ls[12] | ~(~(ls[4]) | ls[12]) & ~(~(ls[1]) | ~(ls[14]))) & ~(~(~(ls[15] | ls[5]) | ls[14] | ls[1] | ~(ls[7]) & ~(ls[4]) | ~(ls[1]) | ls[7] & ~(ls[17]) | ls[14] | ls[1] | ~(ls[7]) & ~(ls[14]) | ls[1] | ~(ls[7]) | ~(~(ls[17]) | ~(ls[15]) | ~(ls[5]))) & ls[12]) & ~(~(~(ls[11]) | ls[17] & ~(ls[18]) | ls[15] & ~(ls[3]) | ls[5] | ~(ls[18]) & ls[15] | ~(ls[11]) & ls[17]) & ~(~(ls[14]) | ls[7] | ls[1])) & ~(~(ls[14] | ls[7] | ls[1]) & ~(~(ls[11] | ~(~(~(~(ls[5]) | ~(ls[3])) | ls[15] & ls[18]) & ~(~(~(ls[5]) | ~(ls[3])) & ls[15])) & ls[17]) & ~(ls[11] & ~(~(~(~(ls[5]) | ~(ls[3])) | ls[15] & ls[18]) & ~(~(~(ls[5]) | ~(ls[3])) & ls[15]))))) | ~(ls[4]) & ls[12] | ~(~(ls[4]) | ls[12]))"
print(eval(z))
z = to_cnf(eval(z))
print(z)

测试 1 的输出

Eval:  ~(b | o | ~b | ~h | ~p | ~r | (m & ~e) | (~f & ~h) | ~(m | ~e) | (~o & ~((m & ~e) | ~(m | ~e))) | (~(f | (p & ~d) | (p & ~s) | (r & ~l) | (r & ~s) | (~l & ~(b | h | ~o))) & ~(~(b | h | o) & ~(l & ~(~(p & ~(~d | ~f)) & ~((p & s) | ~(~d | ~f)))) & ~(l | (r & ~(~(p & ~(~d | ~f)) & ~((p & s) | ~(~d | ~f))))))) | (m & ~(~(b | h | ~o) & ~(f | ~l | (p & ~d) | (p & ~s) | (r & ~l) | (r & ~s))) & ~((m & ~e) | (~(m | ~e) & ~(~b | ~o)) | (~(b | o | ~h) & ~(f | m | p | r))) & ~(m & ~(b | o | ~b | ~h | (h & ~r) | ~(f | p) | (~e & ~h) | (~h & ~o) | ~(~f | ~p | ~r))) & ~(~(b | h | o) & ~(~(l & ~(~(p & ~(~d | ~f)) & ~((p & s) | ~(~d | ~f)))) & ~(l | (r & ~(~(p & ~(~d | ~f)) & ~((p & s) | ~(~d | ~f)))))))))
CNF:  False

如果我用像 z = ls[0] | ls[1] 这样简单的东西替换 z，一切都按预期工作。

#TEST 2
from sympy import symbols
from sympy.logic.boolalg import to_cnf
from sympy.logic import simplify_logic
ls = symbols('a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z')
z = "ls[0] | ls[1]"
print("Eval: ",eval(z))
z = to_cnf(eval(z))
print("CNF: ", z)

测试 2 的输出

Eval:  a | b
CNF:  a | b

Answer 1

例如，逻辑表达式可以简化为 False。

>>> x = symbols('x')
>>> simplify_logic(x & ~x)
False

也许你的表达也是如此？SymPy的当前开发版本也这么认为：

>>> z = simplify_logic(eval(z), form='cnf')
>>> z
False

与 SymPy 1.1.1 不同，to_cnf(eval(z))返回 False，当前的开发版本(可通过从 GitHub 克隆获得(在漫长的等待后评估行z = to_cnf(eval(z))(您可以同时散步(。我在这里不包括输出，因为它远远超过了帖子长度限制。

>>> len(str(z))
1013494

但考虑到一个符号与自我否定相结合的频率，我并没有忽视 False 是正确的简化答案的可能性。