sympy + 逻辑模块:assert(is_cnf(to_cnf(expr, simplify=True))) 失败
sympy + logic module: assert(is_cnf(to_cnf(expr, simplify=True))) fails
我正在尝试使用 sympy 来帮助我解析一些与逻辑相关的文本文件(在进行额外的字符串处理后:例如生成 numbered 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
)。
没有简化:
- 有效,输出显示预期的指数爆炸
这有点像 "i will never be able to minimize that so i don't try it" 的事情,没有任何反馈。
我错过了什么吗?我的用法是否正确(我假设 sympys 解析能够使用我的编号变量)。
(让我们暂时忽略更理论的一面 -> 指数爆炸;简化的可行性)
具有 simplify=True
的 to_cnf
函数调用 simplify_logic
而不传递 force=True
标志设置。由于表达式有超过 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
。
我正在尝试使用 sympy 来帮助我解析一些与逻辑相关的文本文件(在进行额外的字符串处理后:例如生成 numbered 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
)。
没有简化:
- 有效,输出显示预期的指数爆炸
这有点像 "i will never be able to minimize that so i don't try it" 的事情,没有任何反馈。
我错过了什么吗?我的用法是否正确(我假设 sympys 解析能够使用我的编号变量)。
(让我们暂时忽略更理论的一面 -> 指数爆炸;简化的可行性)
具有 simplify=True
的 to_cnf
函数调用 simplify_logic
而不传递 force=True
标志设置。由于表达式有超过 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
。