How can I recast a CNF expression to 3-CNF?

Question

I have a CNF expression like this and I want recast it to 3-CNF:

(a+b+c+d)(~a)(~b+d)(a+b+~d)

Does anyone know how I can do that?

Answer 1

A 3-CNF is a Conjunctive Normal Form where all clauses have three or less literals. To obtain such a form for your expression, you could translate the expression into a nested Boolean expression where all operators (and, or) have two operands:

t1a = (a+b)
t1b = (c+d)
t1 = t1a + t1b
t2 = (~a)
t3 = (~b+d)
t4a = (a+b)
t4 = t4a + ~d
t5a = t1 t2
t5b = t3 t4
t5 = t5a t5b

You can directly translate this nested expression into a set of 3-CNF clauses.

Minimized solution:

(~a)(~b + d)(b + ~d)(c + d)  

as suggested by WolframAlpha is a 3-CNF of your expression as it does not contain longer clauses.

For small cases, you could fill a truth table. Look at all rows with output 0 and find minterms covering all these rows. If you then invert all literals in the minterms, you have a CNF. In case clauses have more than 3 literals, they can be broken up into two or more shorter clauses by introducing intermediate variables. The widely used procedure for that is called Tseitin Transformation or Tseitin Encoding.