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.
hdavid16
commented
7 months ago
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.