Look into Alternate CNF #59
Description
Alternate approaches exist for converting to CNF, which involve preserving clause satisfiability rather than clause equivalence. These approaches prevent exponential size increase in clauses and yield logically consistent results.
Paul Jackson and Daniel Sheridan. Clause form conversions
for boolean circuits. Theory and Applications of Satisfiability
Testing, page 183–198, 2005. doi:10.1007/11527695_15.