def reduceCnf(cnf):
output = Cnf()<EOL>for x in cnf.dis:<EOL><INDENT>dont_add = False<EOL>for y in x:<EOL><INDENT>for z in x:<EOL><INDENT>if z == -y:<EOL><INDENT>dont_add = True<EOL>break<EOL><DEDENT><DEDENT>if dont_add: break<EOL><DEDENT>if dont_add: continue<EOL>if x not in output.dis:<EOL><INDENT>output.dis |= frozenset([x])<EOL><DEDENT><DEDENT>return output<EOL>
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)