You could use the Riss3g Coprocessor of Norbert Manthey to simplify your CNF
.
The SAT
solver minisat 2 allows to store the preprocessed CNF
in a file.
Lingeling, a SAT
solver from Austria has an option "-s"
to simplify CNF
clauses.
To convert a Boolean expression into a simplified CNF
, you could use bc2cnf.