How to convert SAT formula to 3SAT format?

Viewed 196
1 Answers

If you have a clause C that has too few literals, it can be replaced by (C ∨ x) ∧ (C ∨ x′) where x is a fresh variable.

If you have a clause C that has too many literals, you can first split it as C = C0 ∨ C1, putting one half of the literals in C0 and the other half of the literals in C1, then return to conjunctive normal form by replacing C with (C0 ∨ x) ∧ (C1 ∨ x′).

Related