CODEWITHSUNDEEP
pythonsympyboolean-logic
sascha
sascha

Reputation: 33532

sympy + logic module: assert(is_cnf(to_cnf(expr, simplify=True))) fails

I'm trying to use sympy to help me parse some logic-related text-files (after additional string-processing: e.g. generation of numbered x-vars like x0, x1...) and i don't understand the following behaviour:

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

This looks really bad!

Without simplification:

This somewhat looks like a "i will never be able to minimize that so i don't try it" thing, without any feedback.

Did i miss something? Is my usage correct (i assumed sympys parsing able to work with my numbered variables).

(Let's ignore the more theoretical side for now -> exponential blow-up; feasibility of simplification)

Upvotes: 0

Views: 289

Answers (1)

smichr
smichr

Reputation: 19115

The to_cnf function with simplify=True calls simplify_logic without passing the force=True flag setting. Since the expresssion has more than 8 variables a conversion to cnf is not attempted and the routine does not check to see if the simplified result is in cnf form. A simple patch is

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):

Then (if you want to try simplify the result) you have to call simplify_logic with force=True.

Upvotes: 1

Related Questions