Crash with .to_cnf() on large expressions

[addoolit]

Ran into a problem where python hangs (I'm guessing trying to use too much memory, and segfault, but can't be sure) when I'm trying to take a large-ish expression (output of espresso_exprs()) and convert it to CNF with .to_cnf(). I've recreated a situation where this happened below (pyeda.__version__ == '0.28.0'):

E1 = expr('E1')
B0 = expr('B0')
B1 = expr('B1')
B2 = expr('B2')
B3 = expr('B3')
S0 = expr('S0')
S1 = expr('S1')
S2 = expr('S2')
S3 = expr('S3')
S4 = expr('S4')

ex = Or(And(~E0, ~E1, S1, ~B1, B3), And(~E0, ~E1, ~B0, ~B1, B3), 
    And(~E0, ~E1, ~S0, S3, S4), And(~E0, ~E1, ~B0, ~S2, S4), 
    And(~E0, ~E1, ~B0, S3, S4), And(~E0, ~E1, ~S0, S3, B3), 
    And(~E0, ~E1, S1, ~B1, S4), And(~E0, ~E1, ~B0, ~B1, S4), 
    And(~E0, ~E1, ~B0, S3, B3), And(~E0, ~E1, ~S0, ~S2, B3), 
    And(~E0, ~E1, ~S0, ~B1, B3), And(~E0, ~E1, ~S0, ~B1, S4), 
    And(~E0, ~E1, S1, S3, B3), And(~E0, ~E1, ~S0, ~S2, S4), 
    And(~E0, ~E1, S1, S3, S4), And(~E0, ~E1, S1, ~S2, B3), 
    And(~E0, ~E1, S1, ~S2, S4), And(~E0, ~E1, ~B0, ~S2, B3))
ex = ex.to_cnf()

In my own code, the expressions were all DNF, so I was able to break the problem down into smaller pieces by iterating through .xs, OR'ing the current expression with the result of the previous iteration, and doing .to_cnf() on this smaller partial expression before continuing. I'm not very versed on how to optimize things, but it's an approach that may be worth considering adding to the code to handle larger expressions.

[Komplication]

Experiencing the same issue with larger functions and seems to be related to the number of operations included rather than the number of variables. When converting to CNF, machines lock up and a complete power cycle is required. Using PyEda 0.28.0. with Linux 5.3.0-46-generic, with Intel© Core™ i7 CPU X 980 @ 3.33GHz × 6, with 12 GiB RAM.

An example that will crash when converting to CNF, but runs fine otherwise.

from pyeda.inter import *

A = exprvar('A')
B = exprvar('B')
C = exprvar('C')
D = exprvar('D')
E = exprvar('E')
F = exprvar('F')
G = exprvar('G')
H = exprvar('H')
I = exprvar('I')
J = exprvar('J')
K = exprvar('K')
L = exprvar('L')
M = exprvar('M')
N = exprvar('N')
O = exprvar('O')
P = exprvar('P')
Q = exprvar('Q')
R = exprvar('R')
S = exprvar('S')
T = exprvar('T')
U = exprvar('U')
V = exprvar('V')
W = exprvar('W')
X = exprvar('X')
Y = exprvar('Y')
Z = exprvar('Z')
AA = exprvar('AA')
AB = exprvar('AB')
AC = exprvar('AC')
AD = exprvar('AD')
AE = exprvar('AE')
AF = exprvar('AF')
AG = exprvar('AG')
AH = exprvar('AH')
AI = exprvar('AI')
AJ = exprvar('AJ')
AK = exprvar('AK')
AL = exprvar('AL')
AM = exprvar('AM')
AN = exprvar('AN')
AO = exprvar('AO')
AP = exprvar('AP')
AQ = exprvar('AQ')
AR = exprvar('AR')
AS = exprvar('AS')
AT = exprvar('AT')
AU = exprvar('AU')
AV = exprvar('AV')
AW = exprvar('AW')
AX = exprvar('AX')
AY = exprvar('AY')
AZ = exprvar('AZ')
BA = exprvar('BA')
BB = exprvar('BB')
BC = exprvar('BC')
BD = exprvar('BD')
BE = exprvar('BE')
BF = exprvar('BF')
BG = exprvar('BG')
BH = exprvar('BH')
BI = exprvar('BI')
BJ = exprvar('BJ')
BK = exprvar('BK')
BL = exprvar('BL')
BM = exprvar('BM')
BN = exprvar('BN')
BO = exprvar('BO')
BP = exprvar('BP')
BQ = exprvar('BQ')
BR = exprvar('BR')
BS = exprvar('BS')
BT = exprvar('BT')
BU = exprvar('BU')
BV = exprvar('BV')
BW = exprvar('BW')
BX = exprvar('BX')
BY = exprvar('BY')
BZ = exprvar('BZ')
CA = exprvar('CA')
CB = exprvar('CB')
CC = exprvar('CC')
CD = exprvar('CD')
CE = exprvar('CE')
CF = exprvar('CF')
CG = exprvar('CG')
CH = exprvar('CH')

f1 = ((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|AA|AB|AC)&(AD|AE|AF|AG)&(AH)&(AI|AJ)&(AK|AL|AM)&(AN|AO|AP|AQ|AR|AS|AT)&(AU|AV|AW|AX|AY|AZ|BA|BB|BC|BD|BE|BF|BG|BH|BI|BJ|BK|BL|BM|BN|BO|BP|BQ|BR|BS|BT|BU|BV|BW|BX|BY|BZ|CA|CB|CC|CD|CE|CF|CG|CH))|((A|B&(C)&(E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z|AA|AB|AC)&(AD|AE|AF|AG)&(AH)&(AI|AJ)&(AK|AL|AM)&(AN|AO|AP|AQ|AR|AS|AT)&(AV|AW)&(AU|AX|AY|AZ|BA|D|BB|BC|BD|BE|BF|BG|BH|BI|BJ|BK|BL|BM|BN|BO|BP|BQ|BR|BS|BT|BU|BV|BW|BX|BY|BZ|CA|CB|CC|CD|CE|CF|CG|CH))|((A|B)&(C)&(BK|BL|BM|BN|BO|BP)&(AU)&(BB|BC|BD|BE|BF|BG|BH|BI|BJ|BU|BV|BW|BX|BY|BZ|CA|CB|CC|CD|CF)&(AX|AZ)&(AY|BA)&(CE)&(BQ)&(AV|AW|D|AK|AN|AI|AO|AJ|AH|AP|AL|BR|AQ|E|F|BS|BT|G|H|AR|AM|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z|AA|AS|AT|AB|AD|AE|AF|AG|AC|CG|CH))|((A|B)&(C)&(AU)&(AX|AZ)&(AY|BA)&(CE)&(BQ)&(AI|AJ|BR)&(AV|AW|D|AK|AN|BB|BC|BD|BE|BF|AO|BG|BH|BI|BJ|AH|AP|AL|BK|BL|BM|BN|BO|BP|AQ|E|F|BS|BT|G|H|BU|AR|BV|AM|BW|BX|BY|BZ|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z|AA|AS|AT|CA|AB|AD|AE|AF|AG|CB|CC|CD|CF|AC|CG|CH))|((A|B)&(C)&(AX|AZ)&(AY|BA)&(CE)&(BQ)&(AI|AJ|BR)&(CG|CH)&(AU|AV|AW|D|AK|AN|BB|BC|BD|BE|BF|AO|BG|BH|BI|BJ|AH|AP|AL|BK|BL|BM|BN|BO|BP|AQ|E|F|BS|BT|G|H|BU|AR|BV|AM|BW|BX|BY|BZ|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z|AA|AS|AT|CA|AB|AD|AE|AF|AG|CB|CC|CD|CF|AC))|((A|B)&(C)&(AY|BA)&(CE)&(BQ)&(AI|AJ|BR)&(CG|CH)&(BS)&(AU|AV|AW|AX|AZ|D|AK|AN|BB|BC|BD|BE|BF|AO|BG|BH|BI|BJ|AH|AP|AL|BK|BL|BM|BN|BO|BP|AQ|E|F|BT|G|H|BU|AR|BV|AM|BW|BX|BY|BZ|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z|AA|AS|AT|CA|AB|AD|AE|AF|AG|CB|CC|CD|CF|AC))|((A|B)&(C)&(CE)&(BQ)&(AI|AJ|BR)&(CG|CH)&(BS)&(BT)&(AU|AV|AW|AX|AY|AZ|BA|D|AK|AN|BB|BC|BD|BE|BF|AO|BG|BH|BI|BJ|AH|AP|AL|BK|BL|BM|BN|BO|BP|AQ|E|F|G|H|BU|AR|BV|AM|BW|BX|BY|BZ|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z|AA|AS|AT|CA|AB|AD|AE|AF|AG|CB|CC|CD|CF|AC))

f1m, = espresso_exprs(f1.to_dnf())
f1m = f1m.to_cnf()

[heikkiorsila]

I may have the same issue when converting to cnf. I valgrinded the problem to:

==4396== Jump to the invalid address stated on the next line
==4396==    at 0x0: ???
==4396==    by 0x6811D78: BX_Array_Del (array.c:52)
==4396==    by 0x68121A0: _op_del (boolexpr.c:230)
==4396==    by 0x6817B1F: _bx_simplify (simple.c:570)
==4396==    by 0x6817B1F: _bx_simplify (simple.c:560)
==4396==    by 0x6815B19: _distribute (flatten.c:87)
==4396==    by 0x6815D50: _to_cnf.part.0 (flatten.c:303)
==4396==    by 0x68161E7: _to_cnf (flatten.c:346)
==4396==    by 0x68161E7: BX_ToCNF (flatten.c:340)
==4396==    by 0x6819045: ExprNode_to_cnf (exprnodemodule.c:797)
==4396==    by 0x52506D: ??? (in /usr/bin/python3.8)
==4396==    by 0x509570: _PyEval_EvalFrameDefault (in /usr/bin/python3.8)
==4396==    by 0x51E8F6: _PyFunction_Vectorcall (in /usr/bin/python3.8)
==4396==    by 0x509570: _PyEval_EvalFrameDefault (in /usr/bin/python3.8)
==4396==  Address 0x0 is not stack'd, malloc'd or (recently) free'd
==4396== 
==4396== 
==4396== Process terminating with default action of signal 11 (SIGSEGV)
==4396==  Bad permissions for mapped region at address 0x0
==4396==    at 0x0: ???
==4396==    by 0x6811D78: BX_Array_Del (array.c:52)
==4396==    by 0x68121A0: _op_del (boolexpr.c:230)
==4396==    by 0x6817B1F: _bx_simplify (simple.c:570)
==4396==    by 0x6817B1F: _bx_simplify (simple.c:560)
==4396==    by 0x6815B19: _distribute (flatten.c:87)
==4396==    by 0x6815D50: _to_cnf.part.0 (flatten.c:303)
==4396==    by 0x68161E7: _to_cnf (flatten.c:346)
==4396==    by 0x68161E7: BX_ToCNF (flatten.c:340)
==4396==    by 0x6819045: ExprNode_to_cnf (exprnodemodule.c:797)
==4396==    by 0x52506D: ??? (in /usr/bin/python3.8)
==4396==    by 0x509570: _PyEval_EvalFrameDefault (in /usr/bin/python3.8)
==4396==    by 0x51E8F6: _PyFunction_Vectorcall (in /usr/bin/python3.8)
==4396==    by 0x509570: _PyEval_EvalFrameDefault (in /usr/bin/python3.8)

[heikkiorsila]

I may have the same issue when converting to cnf. I valgrinded the problem to:
...

I didn't use espresso at all. I used truthtable, truthtable2expr and then .to_cnf() method:

t = truthtable(X, value
f = truthtable2expr(t)
expr = f.to_cnf()

In my case this turned out to be two problems:

1. The cause for invalid jump address was corrupt memory. After marking memory unusable in kernel the invalid jump address problem disappeared.
2. The problem occured because ".to_cnf()" uses exponential memory in some cases even for relatively simple expressions. In my case a simple expression is a truth table for 4-bit function mapping to a binary value.

"to_cnf()" algorithm could be improved. My workaround was to use Python's Sympy library to convert to cnf/dnf rather than pyeda.