Remove terms that cancel out. If there are two clauses
Often I'll be trying to make a new sort of generalized SAT pattern. Usually this consists of a combination of brute-force enumeration and logical deduction, with a smattering of test cases on the corners.
One helpful tool consumes a verbose brute force CNF and returns a more minimal expression without redundancy. Patterns become much more visible after such a cleanup, helped along by pretty-printing the CNF in tidy columns.
BE AWARE: Every sat solver already does this step internally and much much faster. There is no reason to use this code in the solving pipeline - it is for exploration and experimentation.
source at github, simplify.py
Remove duplicate clauses. If it was correct the first time, it'll still be correct later.
Remove tautologies. For example, anything with
A -A in it will always evaluate to true. Regardless of what else is in the clause.
A B A -B
then the possible answers are
(A=true, B=true) and
B has no effect and the two clauses can be collapsed to simply
Remove perfect supersets. In the case of
A B C A B
the state of
C has no effect. The entire
A B C clause can be safely eliminated.
These are the most basic simplification processes. Various papers describe more advanced transformations, but these are beyond me for now.