Using Sympy "to_nnf" and a MemoryError using eval()

Question

I am using Sympy to convert a Boolean function to negation normal form. This boolean function is read in as a string with a large, variable number of elements. In order to handle the different number of symbols dynamically, I first create a list of symbols and replace the variable names.

I end up with something like boolFunc = "~(ls[0] & ls[1])" where ls is a list of symbols (except len(ls) could be very large).

Then, I can convert the boolean Function using

boolFunc = str(to_nnf(eval(val), simplify=False))

This works great for smaller Boolean Functions (up to about len(ls) = 40), but fails once the Boolean functions get complicated enough (about len(ls) = 60). It appears that the issue is with eval().

s_push: parser stack overflow
Traceback (most recent call last):
  File "dualRail.py", line 187, in <module>
    eval(booleanFunction)
MemoryError

Does anyone know of a way to fix this issue either by getting rid of the need to use eval() somehow, or some other way?

I have found a possible solution here, but I want to modify the Python source code as a last resort.

Edit 1: I think the issue with eval is specifically deeply nested parenthesis. I also think there is a chance that some of these parenthesis are redundant. For example, in A | (B & C) the parenthesis are not needed. If I write an algorithm to remove these extra parenthesis (assuming one doesn't already exist), this might allow a larger sized Boolean function, but I'm not sure if it will be enough.

Edit 2: Here is a small example of what I am trying to do. I am using Python3.6

import re;
from sympy import symbols
from sympy.logic.boolalg import to_nnf

#This function works fine
boolean_function1 =  '(((((~(op[2])) & op[1]) & op[0]) & (~((~((((((((((((((((((A[1] & A[0]) & A[2]) & A[3]) & A[4]) & A[5]) & A[6]) & A[7]) & A[8]) & A[9]) & A[10]) & A[11]) & A[12]) & A[13]) & A[14]) & A[15]) & A[16]) & A[17]) & (~(A[18])))) & (~(A[18] & (~((((((((((((((((((A[1] & A[0]) & A[2]) & A[3]) & A[4]) & A[5]) & A[6]) & A[7]) & A[8]) & A[9]) & A[10]) & A[11]) & A[12]) & A[13]) & A[14]) & A[15]) & A[16]) & A[17])))))))) | (((~((~((~((~(((~(B[17])) | (~(A[17]))) & (~((~(((~(B[16])) | (~(A[16]))) & (~((~(((~(B[15])) | (~(A[15]))) & (~((~(((~(B[14])) | (~(A[14]))) & (~((~(((~(B[13])) | (~(A[13]))) & (~((~(((~(B[12])) | (~(A[12]))) & (~((~(((~(B[11])) | (~(A[11]))) & (~((~(((~(B[10])) | (~(A[10]))) & (~((~(((~(B[9])) | (~(A[9]))) & (~((~(((~(B[8])) | (~(A[8]))) & (~((~(((~(B[7])) | (~(A[7]))) & (~((~(((~(B[6])) | (~(A[6]))) & (~((~(((~(B[5])) | (~(A[5]))) & (~((~(((~(B[4])) | (~(A[4]))) & (~((~(((~(B[3])) | (~(A[3]))) & (~((~(((~(B[2])) | (~(A[2]))) & (~((~(((~(B[1])) | (~(A[1]))) & (~((A[0] & B[0]))))) & (~((~(B[1])) & (~(A[1])))))))) & (~((~(B[2])) & (~(A[2])))))))) & (~((~(B[3])) & (~(A[3])))))))) & (~((~(B[4])) & (~(A[4])))))))) & (~((~(B[5])) & (~(A[5])))))))) & (~((~(B[6])) & (~(A[6])))))))) & (~((~(B[7])) & (~(A[7])))))))) & (~((~(B[8])) & (~(A[8])))))))) & (~((~(B[9])) & (~(A[9])))))))) & (~((~(B[10])) & (~(A[10])))))))) & (~((~(B[11])) & (~(A[11])))))))) & (~((~(B[12])) & (~(A[12])))))))) & (~((~(B[13])) & (~(A[13])))))))) & (~((~(B[14])) & (~(A[14])))))))) & (~((~(B[15])) & (~(A[15])))))))) & (~((~(B[16])) & (~(A[16])))))))) & (~((~(B[17])) & (~(A[17])))))) & (((~(op[2])) & (~(op[1]))) & (~(op[0]))))) & (~((((~(op[2])) & (~(op[1]))) & op[0]) & (~(((((((((((((((((((((((((((((((((((((~(A[0])) & B[0]) | ((~(A[1])) & B[1])) & ((~(A[1])) | B[1])) | ((~(A[2])) & B[2])) & ((~(A[2])) | B[2])) | ((~(A[3])) & B[3])) & ((~(A[3])) | B[3])) | ((~(A[4])) & B[4])) & ((~(A[4])) | B[4])) | ((~(A[5])) & B[5])) & ((~(A[5])) | B[5])) | ((~(A[6])) & B[6])) & ((~(A[6])) | B[6])) | ((~(A[7])) & B[7])) & ((~(A[7])) | B[7])) | ((~(A[8])) & B[8])) & ((~(A[8])) | B[8])) | ((~(A[9])) & B[9])) & ((~(A[9])) | B[9])) | ((~(A[10])) & B[10])) & ((~(A[10])) | B[10])) | ((~(A[11])) & B[11])) & ((~(A[11])) | B[11])) | ((~(A[12])) & B[12])) & ((~(A[12])) | B[12])) | ((~(A[13])) & B[13])) & ((~(A[13])) | B[13])) | ((~(A[14])) & B[14])) & ((~(A[14])) | B[14])) | ((~(A[15])) & B[15])) & ((~(A[15])) | B[15])) | ((~(A[16])) & B[16])) & ((~(A[16])) | B[16])) | ((~(A[17])) & B[17])) & ((~(A[17])) | B[17])))))))) | (op[2] & op[0])) & (~((((~(A[18])) | B[18]) & (~(((~(A[18])) & B[18])))))))) | (~((~((~((~(((((((((((((((((((((((((((((((((((((~(A[0])) & B[0]) | ((~(A[1])) & B[1])) & ((~(A[1])) | B[1])) | ((~(A[2])) & B[2])) & ((~(A[2])) | B[2])) | ((~(A[3])) & B[3])) & ((~(A[3])) | B[3])) | ((~(A[4])) & B[4])) & ((~(A[4])) | B[4])) | ((~(A[5])) & B[5])) & ((~(A[5])) | B[5])) | ((~(A[6])) & B[6])) & ((~(A[6])) | B[6])) | ((~(A[7])) & B[7])) & ((~(A[7])) | B[7])) | ((~(A[8])) & B[8])) & ((~(A[8])) | B[8])) | ((~(A[9])) & B[9])) & ((~(A[9])) | B[9])) | ((~(A[10])) & B[10])) & ((~(A[10])) | B[10])) | ((~(A[11])) & B[11])) & ((~(A[11])) | B[11])) | ((~(A[12])) & B[12])) & ((~(A[12])) | B[12])) | ((~(A[13])) & B[13])) & ((~(A[13])) | B[13])) | ((~(A[14])) & B[14])) & ((~(A[14])) | B[14])) | ((~(A[15])) & B[15])) & ((~(A[15])) | B[15])) | ((~(A[16])) & B[16])) & ((~(A[16])) | B[16])) | ((~(A[17])) & B[17])) & ((~(A[17])) | B[17])) & (((~(op[2])) & (~(op[1]))) & op[0]))) & (~((((~(op[2])) & (~(op[1]))) & (~(op[0]))) & (~((~((~(((~(B[17])) | (~(A[17]))) & (~((~(((~(B[16])) | (~(A[16]))) & (~((~(((~(B[15])) | (~(A[15]))) & (~((~(((~(B[14])) | (~(A[14]))) & (~((~(((~(B[13])) | (~(A[13]))) & (~((~(((~(B[12])) | (~(A[12]))) & (~((~(((~(B[11])) | (~(A[11]))) & (~((~(((~(B[10])) | (~(A[10]))) & (~((~(((~(B[9])) | (~(A[9]))) & (~((~(((~(B[8])) | (~(A[8]))) & (~((~(((~(B[7])) | (~(A[7]))) & (~((~(((~(B[6])) | (~(A[6]))) & (~((~(((~(B[5])) | (~(A[5]))) & (~((~(((~(B[4])) | (~(A[4]))) & (~((~(((~(B[3])) | (~(A[3]))) & (~((~(((~(B[2])) | (~(A[2]))) & (~((~(((~(B[1])) | (~(A[1]))) & (~((A[0] & B[0]))))) & (~((~(B[1])) & (~(A[1])))))))) & (~((~(B[2])) & (~(A[2])))))))) & (~((~(B[3])) & (~(A[3])))))))) & (~((~(B[4])) & (~(A[4])))))))) & (~((~(B[5])) & (~(A[5])))))))) & (~((~(B[6])) & (~(A[6])))))))) & (~((~(B[7])) & (~(A[7])))))))) & (~((~(B[8])) & (~(A[8])))))))) & (~((~(B[9])) & (~(A[9])))))))) & (~((~(B[10])) & (~(A[10])))))))) & (~((~(B[11])) & (~(A[11])))))))) & (~((~(B[12])) & (~(A[12])))))))) & (~((~(B[13])) & (~(A[13])))))))) & (~((~(B[14])) & (~(A[14])))))))) & (~((~(B[15])) & (~(A[15])))))))) & (~((~(B[16])) & (~(A[16])))))))) & (~((~(B[17])) & (~(A[17])))))))))))) & (((~(A[18])) | B[18]) & (~(((~(A[18])) & B[18])))))) & (~((A[18] & B[18]) & ((~(op[1])) & op[2]))))) | (~((~(((A[18] & (~((((((((((((((((((~((A[1] | A[0]))) & (~(A[2]))) & (~(A[3]))) & (~(A[4]))) & (~(A[5]))) & (~(A[6]))) & (~(A[7]))) & (~(A[8]))) & (~(A[9]))) & (~(A[10]))) & (~(A[11]))) & (~(A[12]))) & (~(A[13]))) & (~(A[14]))) & (~(A[15]))) & (~(A[16]))) & (~(A[17])))))) | ((((((((((((((((((~((A[1] | A[0]))) & (~(A[2]))) & (~(A[3]))) & (~(A[4]))) & (~(A[5]))) & (~(A[6]))) & (~(A[7]))) & (~(A[8]))) & (~(A[9]))) & (~(A[10]))) & (~(A[11]))) & (~(A[12]))) & (~(A[13]))) & (~(A[14]))) & (~(A[15]))) & (~(A[16]))) & (~(A[17]))) & (~(A[18])))) & (((~(op[2])) & op[1]) & (~(op[0]))))) & (~((~(A[18])) & (op[1] & op[2] & (~(op[0])))))))'

#This function gives an error on eval()
boolean_function2 = '(((((~(op[2])) & op[1]) & op[0]) & (~((~((((((((((((((((((((A[1] & A[0]) & A[2]) & A[3]) & A[4]) & A[5]) & A[6]) & A[7]) & A[8]) & A[9]) & A[10]) & A[11]) & A[12]) & A[13]) & A[14]) & A[15]) & A[16]) & A[17]) & A[18]) & A[19]) & (~(A[20])))) & (~(A[20] & (~((((((((((((((((((((A[1] & A[0]) & A[2]) & A[3]) & A[4]) & A[5]) & A[6]) & A[7]) & A[8]) & A[9]) & A[10]) & A[11]) & A[12]) & A[13]) & A[14]) & A[15]) & A[16]) & A[17]) & A[18]) & A[19])))))))) | (((~((~((~((~(((~(B[19])) | (~(A[19]))) & (~((~(((~(B[18])) | (~(A[18]))) & (~((~(((~(B[17])) | (~(A[17]))) & (~((~(((~(B[16])) | (~(A[16]))) & (~((~(((~(B[15])) | (~(A[15]))) & (~((~(((~(B[14])) | (~(A[14]))) & (~((~(((~(B[13])) | (~(A[13]))) & (~((~(((~(B[12])) | (~(A[12]))) & (~((~(((~(B[11])) | (~(A[11]))) & (~((~(((~(B[10])) | (~(A[10]))) & (~((~(((~(B[9])) | (~(A[9]))) & (~((~(((~(B[8])) | (~(A[8]))) & (~((~(((~(B[7])) | (~(A[7]))) & (~((~(((~(B[6])) | (~(A[6]))) & (~((~(((~(B[5])) | (~(A[5]))) & (~((~(((~(B[4])) | (~(A[4]))) & (~((~(((~(B[3])) | (~(A[3]))) & (~((~(((~(B[2])) | (~(A[2]))) & (~((~(((~(B[1])) | (~(A[1]))) & (~((A[0] & B[0]))))) & (~((~(B[1])) & (~(A[1])))))))) & (~((~(B[2])) & (~(A[2])))))))) & (~((~(B[3])) & (~(A[3])))))))) & (~((~(B[4])) & (~(A[4])))))))) & (~((~(B[5])) & (~(A[5])))))))) & (~((~(B[6])) & (~(A[6])))))))) & (~((~(B[7])) & (~(A[7])))))))) & (~((~(B[8])) & (~(A[8])))))))) & (~((~(B[9])) & (~(A[9])))))))) & (~((~(B[10])) & (~(A[10])))))))) & (~((~(B[11])) & (~(A[11])))))))) & (~((~(B[12])) & (~(A[12])))))))) & (~((~(B[13])) & (~(A[13])))))))) & (~((~(B[14])) & (~(A[14])))))))) & (~((~(B[15])) & (~(A[15])))))))) & (~((~(B[16])) & (~(A[16])))))))) & (~((~(B[17])) & (~(A[17])))))))) & (~((~(B[18])) & (~(A[18])))))))) & (~((~(B[19])) & (~(A[19])))))) & (((~(op[2])) & (~(op[1]))) & (~(op[0]))))) & (~((((~(op[2])) & (~(op[1]))) & op[0]) & (~(((((((((((((((((((((((((((((((((((((((((~(A[0])) & B[0]) | ((~(A[1])) & B[1])) & ((~(A[1])) | B[1])) | ((~(A[2])) & B[2])) & ((~(A[2])) | B[2])) | ((~(A[3])) & B[3])) & ((~(A[3])) | B[3])) | ((~(A[4])) & B[4])) & ((~(A[4])) | B[4])) | ((~(A[5])) & B[5])) & ((~(A[5])) | B[5])) | ((~(A[6])) & B[6])) & ((~(A[6])) | B[6])) | ((~(A[7])) & B[7])) & ((~(A[7])) | B[7])) | ((~(A[8])) & B[8])) & ((~(A[8])) | B[8])) | ((~(A[9])) & B[9])) & ((~(A[9])) | B[9])) | ((~(A[10])) & B[10])) & ((~(A[10])) | B[10])) | ((~(A[11])) & B[11])) & ((~(A[11])) | B[11])) | ((~(A[12])) & B[12])) & ((~(A[12])) | B[12])) | ((~(A[13])) & B[13])) & ((~(A[13])) | B[13])) | ((~(A[14])) & B[14])) & ((~(A[14])) | B[14])) | ((~(A[15])) & B[15])) & ((~(A[15])) | B[15])) | ((~(A[16])) & B[16])) & ((~(A[16])) | B[16])) | ((~(A[17])) & B[17])) & ((~(A[17])) | B[17])) | ((~(A[18])) & B[18])) & ((~(A[18])) | B[18])) | ((~(A[19])) & B[19])) & ((~(A[19])) | B[19])))))))) | (op[2] & op[0])) & (~((((~(A[20])) | B[20]) & (~(((~(A[20])) & B[20])))))))) | (~((~((~((~(((((((((((((((((((((((((((((((((((((((((~(A[0])) & B[0]) | ((~(A[1])) & B[1])) & ((~(A[1])) | B[1])) | ((~(A[2])) & B[2])) & ((~(A[2])) | B[2])) | ((~(A[3])) & B[3])) & ((~(A[3])) | B[3])) | ((~(A[4])) & B[4])) & ((~(A[4])) | B[4])) | ((~(A[5])) & B[5])) & ((~(A[5])) | B[5])) | ((~(A[6])) & B[6])) & ((~(A[6])) | B[6])) | ((~(A[7])) & B[7])) & ((~(A[7])) | B[7])) | ((~(A[8])) & B[8])) & ((~(A[8])) | B[8])) | ((~(A[9])) & B[9])) & ((~(A[9])) | B[9])) | ((~(A[10])) & B[10])) & ((~(A[10])) | B[10])) | ((~(A[11])) & B[11])) & ((~(A[11])) | B[11])) | ((~(A[12])) & B[12])) & ((~(A[12])) | B[12])) | ((~(A[13])) & B[13])) & ((~(A[13])) | B[13])) | ((~(A[14])) & B[14])) & ((~(A[14])) | B[14])) | ((~(A[15])) & B[15])) & ((~(A[15])) | B[15])) | ((~(A[16])) & B[16])) & ((~(A[16])) | B[16])) | ((~(A[17])) & B[17])) & ((~(A[17])) | B[17])) | ((~(A[18])) & B[18])) & ((~(A[18])) | B[18])) | ((~(A[19])) & B[19])) & ((~(A[19])) | B[19])) & (((~(op[2])) & (~(op[1]))) & op[0]))) & (~((((~(op[2])) & (~(op[1]))) & (~(op[0]))) & (~((~((~(((~(B[19])) | (~(A[19]))) & (~((~(((~(B[18])) | (~(A[18]))) & (~((~(((~(B[17])) | (~(A[17]))) & (~((~(((~(B[16])) | (~(A[16]))) & (~((~(((~(B[15])) | (~(A[15]))) & (~((~(((~(B[14])) | (~(A[14]))) & (~((~(((~(B[13])) | (~(A[13]))) & (~((~(((~(B[12])) | (~(A[12]))) & (~((~(((~(B[11])) | (~(A[11]))) & (~((~(((~(B[10])) | (~(A[10]))) & (~((~(((~(B[9])) | (~(A[9]))) & (~((~(((~(B[8])) | (~(A[8]))) & (~((~(((~(B[7])) | (~(A[7]))) & (~((~(((~(B[6])) | (~(A[6]))) & (~((~(((~(B[5])) | (~(A[5]))) & (~((~(((~(B[4])) | (~(A[4]))) & (~((~(((~(B[3])) | (~(A[3]))) & (~((~(((~(B[2])) | (~(A[2]))) & (~((~(((~(B[1])) | (~(A[1]))) & (~((A[0] & B[0]))))) & (~((~(B[1])) & (~(A[1])))))))) & (~((~(B[2])) & (~(A[2])))))))) & (~((~(B[3])) & (~(A[3])))))))) & (~((~(B[4])) & (~(A[4])))))))) & (~((~(B[5])) & (~(A[5])))))))) & (~((~(B[6])) & (~(A[6])))))))) & (~((~(B[7])) & (~(A[7])))))))) & (~((~(B[8])) & (~(A[8])))))))) & (~((~(B[9])) & (~(A[9])))))))) & (~((~(B[10])) & (~(A[10])))))))) & (~((~(B[11])) & (~(A[11])))))))) & (~((~(B[12])) & (~(A[12])))))))) & (~((~(B[13])) & (~(A[13])))))))) & (~((~(B[14])) & (~(A[14])))))))) & (~((~(B[15])) & (~(A[15])))))))) & (~((~(B[16])) & (~(A[16])))))))) & (~((~(B[17])) & (~(A[17])))))))) & (~((~(B[18])) & (~(A[18])))))))) & (~((~(B[19])) & (~(A[19])))))))))))) & (((~(A[20])) | B[20]) & (~(((~(A[20])) & B[20])))))) & (~((A[20] & B[20]) & ((~(op[1])) & op[2]))))) | (~((~(((A[20] & (~((((((((((((((((((((~((A[1] | A[0]))) & (~(A[2]))) & (~(A[3]))) & (~(A[4]))) & (~(A[5]))) & (~(A[6]))) & (~(A[7]))) & (~(A[8]))) & (~(A[9]))) & (~(A[10]))) & (~(A[11]))) & (~(A[12]))) & (~(A[13]))) & (~(A[14]))) & (~(A[15]))) & (~(A[16]))) & (~(A[17]))) & (~(A[18]))) & (~(A[19])))))) | ((((((((((((((((((((~((A[1] | A[0]))) & (~(A[2]))) & (~(A[3]))) & (~(A[4]))) & (~(A[5]))) & (~(A[6]))) & (~(A[7]))) & (~(A[8]))) & (~(A[9]))) & (~(A[10]))) & (~(A[11]))) & (~(A[12]))) & (~(A[13]))) & (~(A[14]))) & (~(A[15]))) & (~(A[16]))) & (~(A[17]))) & (~(A[18]))) & (~(A[19]))) & (~(A[20])))) & (((~(op[2])) & op[1]) & (~(op[0]))))) & (~((~(A[20])) & (op[1] & op[2] & (~(op[0])))))))'

symbol_set = set(re.findall(r'((?:(?:[a-zA-Z_][\w$]*)|(?:\\.*?\ ))(?:[\[\]0-9])*)', boolean_function1))
symbol_set.update(re.findall(r'((?:(?:[a-zA-Z_][\w$]*)|(?:\\.*?\ ))(?:[\[\]0-9])*)', boolean_function2))
print(symbol_set)
#Convert each Boolean variable to 
ls = []
for i in range(0, len(symbol_set)):
    symbol_name = symbol_set.pop()
    ls.append(symbols(symbol_name))
    boolean_function1 = boolean_function1.replace(symbol_name, 'ls['+str(i)+']')
    boolean_function2 = boolean_function2.replace(symbol_name, 'ls['+str(i)+']')

print('TO_NNF #1', str(to_nnf(eval(boolean_function1), simplify=False)), '\n')
print('TO_NNF #2', str(to_nnf(eval(boolean_function2), simplify=False)), '\n')

@SFTP The number of boolean symbols is about 60, the length of the string is 9903 characters. I can try to come up with a unit test to reproduce the problem if you think it will help. — digitaLink, Mar 20 '18 at 21:08
@SFTP I added some example code to the post. Since the sympify command uses eval(), the error still occurs. — digitaLink, Mar 20 '18 at 21:40
So the issue isn't with SymPy of `nnf`, it's just that `eval` cannot handle this formula. This means you have to look for other ways to parse it. Writing own pre-parser to simplify the expression is one option; another is a boolean logic package such as [boolean](https://pypi.python.org/pypi/boolean.py/1.2). I have't tried it but at least it doesn't seem to rely on `eval`. — , Mar 21 '18 at 00:10
@SFTP I installed the boolean package and sure enough it doesn't rely on `eval`. I had to modify the parser in it a little bit, but it actually seems to work. It does not appear to have as many functions as sympy, but I think it will work for what I need. I will report back if I get it working. Thank you! — digitaLink, Mar 21 '18 at 20:12
Good to hear. It would be nice if an expression parsed with boolean could somehow be understood by SymPy. — , Mar 21 '18 at 20:15

Using Sympy "to_nnf" and a MemoryError using eval()

0 Answers0