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 tautologies. For example, anything with
A -A in it will always evaluate to true. Regardless of what else is in the clause.
then the possible answers are
(A=true, B=true) and
B has no effect and the two clauses can be collapsed to simply
These are the most basic simplification processes. Various papers describe more advanced transformations, but these are beyond me for now.