bastikr / boolean.py

Implements boolean algebra in one module.
BSD 2-Clause "Simplified" License
76 stars 34 forks source link

Exponential blowup when normalizing #106

Closed olliemath closed 2 years ago

olliemath commented 3 years ago

This is the sister issue to https://github.com/bastikr/boolean.py/pull/105

The following normalizes to a&c&f&g. However currently cnf never returns (left long enough it uses up all 32G of memory on my laptop and is killed):

        a & (
            (b & c & d & e & f & g)
            | (c & d & f & g & i & j)
            | (c & f & g & h & i & j)
            | (c & f & g & i & j & k)
            | (c & d & f & g & i & n & p)
            | (c & e & f & g & i & m & x)
            | (c & e & f & g & l & o & w)
            | (c & e & f & g & q & s & t)
            | (c & f & g & i & m & n & r)
            | (c & f & g & l & n & o & r)
            | (c & d & f & g & i & l & o & u)
            | (c & e & f & g & i & p & y & ~v)
            | (c & f & g & i & j & z & ~(c & f & g & i & j & k))
            | (
                c & f & g & t
                & ~(b & c & d & e & f & g)
                & ~(c & d & f & g & i & j)
                & ~(c & f & g & h & i & j)
                & ~(c & f & g & i & j & k)
                & ~(c & d & f & g & i & n & p)
                & ~(c & e & f & g & i & m & x)
                & ~(c & e & f & g & l & o & w)
                & ~(c & e & f & g & q & s & t)
                & ~(c & f & g & i & m & n & r)
                & ~(c & f & g & l & n & o & r)
                & ~(c & d & f & g & i & l & o & u)
                & ~(c & e & f & g & i & p & y & ~v)
                & ~(c & f & g & i & j & z & ~(c & f & g & i & j & k))
            )
            | (
                c & f & g & ~t
                & ~(b & c & d & e & f & g)
                & ~(c & d & f & g & i & j)
                & ~(c & f & g & h & i & j)
                & ~(c & f & g & i & j & k)
                & ~(c & d & f & g & i & n & p)
                & ~(c & e & f & g & i & m & x)
                & ~(c & e & f & g & l & o & w)
                & ~(c & e & f & g & q & s & t)
                & ~(c & f & g & i & m & n & r)
                & ~(c & f & g & l & n & o & r)
                & ~(c & d & f & g & i & l & o & u)
                & ~(c & e & f & g & i & p & y & ~v)
                & ~(c & f & g & i & j & z & ~(c & f & g & i & j & k))
            )
        )