satispy/cnf.py
def reduceCnf(cnf):
    """
    I just found a remarkably large bug in my SAT solver and found an
    interesting solution.
    Remove all b | -b
    (-b | b) & (b | -a) & (-b | a) & (a | -a)
    becomes
    (b | -a) & (-b | a)

    Remove all (-e) & (-e)
    (-e | a) & (-e | a) & (-e | a) & (-e | a)
    becomes
    (-e | a)
    (-b | b | c) becomes nothing, not (c)
    """
    output = Cnf()
    for x in cnf.dis:
        dont_add = False
        for y in x:
            for z in x:
                if z == -y:
                    dont_add = True
                    break
            if dont_add: break
        if dont_add: continue
        # TODO: Is this necessary anymore? Probably not. Do statistical analysis.
        if x not in output.dis:
            output.dis |= frozenset([x])
    return output
def reduceCnf(cnf):
    """
    I just found a remarkably large bug in my SAT solver and found an
    interesting solution.
    Remove all b | -b
    (-b | b) & (b | -a) & (-b | a) & (a | -a)
    becomes
    (b | -a) & (-b | a)

    Remove all (-e) & (-e)
    (-e | a) & (-e | a) & (-e | a) & (-e | a)
    becomes
    (-e | a)
    (-b | b | c) becomes nothing, not (c)
    """
    output = Cnf()
    for x in cnf.dis:
        dont_add = False
        for y in x:
            for z in x:
                if z == -y:
                    dont_add = True
                    break
            if dont_add: break
        if dont_add: continue
        # TODO: Is this necessary anymore? Probably not. Do statistical analysis.
        if x not in output.dis:
            output.dis |= frozenset([x])
    return output
I just found a remarkably large bug in my SAT solver and found an
    interesting solution.
    Remove all b | -b
    (-b | b) & (b | -a) & (-b | a) & (a | -a)
    becomes
    (b | -a) & (-b | a)

    Remove all (-e) & (-e)
    (-e | a) & (-e | a) & (-e | a) & (-e | a)
    becomes
    (-e | a)
    (-b | b | c) becomes nothing, not (c)