Skip to content

Exponential blowup when normalizing #106

@olliemath

Description

@olliemath

This is the sister issue to #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))
            )
        )

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions