sympy+逻辑模块:assert(is_cnf(to_cnf(expr，simple=True))失败

Question

我试图使用sympy来帮助我解析一些与逻辑相关的文本文件(经过额外的字符串处理：例如生成编号的x-vars，如x0, x1...(，但我不理解以下行为：

in_ = '( ( x1 & x2 & x3 & x4 & x5 & x6 & x7 & x8 & x9 )  |  ( x1 & x2 & x3 & x4 & x5 & x6 & x7 & x10 & x9 )  |  ( x1 & x11 & x3 & x12 & x5 & x13 & x14 & x15 & x9 ) ) '
from sympy.parsing.sympy_parser import parse_expr
from sympy.logic.boolalg import to_cnf, is_cnf
parsed = parse_expr(in_, evaluate=False)
cnf_candidate = to_cnf(parsed, simplify=True)  # broken with simp=True; works with simp=False
cnf_status = is_cnf(cnf_candidate)
print(parsed)
print(cnf_candidate)
print(cnf_status)
assert cnf_status 
> (x1 & x10 & x2 & x3 & x4 & x5 & x6 & x7 & x9) | (x1 & x11 & x12 & x13 & x14 & x15 & x3 & x5 & x9) 
(x1 & x2 & x3 & x4 & x5 & x6 & x7 & x8 & x9)
> (x1 & x10 & x2 & x3 & x4 & x5 & x6 & x7 & x9) | (x1 & x11 & x12 & x13 & x14 & x15 & x3 & x5 & x9) | 
(x1 & x2 & x3 & x4 & x5 & x6 & x7 & x8 & x9)
> False
> AssertionError

这看起来真的很糟糕！

• to_cnf并没有真正产生cnf，也没有警告我(使用simplify=True(

无需简化：

• 它工作，输出显示预期的指数爆炸

这看起来有点像"我永远无法将其最小化，所以我不会尝试">事情，没有任何反馈。

我错过什么了吗？我的用法正确吗(我假设sympys解析能够使用我的编号变量(。

(让我们暂时忽略更理论的一面->指数爆炸；简化的可行性(

Answer 1

带有simplify=True的to_cnf函数在不传递force=True标志设置的情况下调用simplify_logic。由于表达式有8个以上的变量，因此不会尝试转换为cnf，例程也不会检查简化的结果是否为cnf形式。一个简单的补丁是

diff --git a/sympy/logic/boolalg.py b/sympy/logic/boolalg.py
index dd734ce..d544ea7 100644
--- a/sympy/logic/boolalg.py
+++ b/sympy/logic/boolalg.py
@@ -1714,7 +1714,9 @@ def to_cnf(expr, simplify=False):
return expr
if simplify:
-        return simplify_logic(expr, 'cnf', True)
+        new = simplify_logic(expr, 'cnf', True)
+        if is_cnf(new):
+            return new
# Don't convert unless we have to
if is_cnf(expr):

然后(如果你想尝试简化结果(，你必须用force=True调用simplify_logic。