From DNF to CNF

Question

What is the most efficient way to switch from DNF to CNF?.

Answer 1

A method with complete enumeration of 2^n terms is described here.

A suitable tool would be bc2cnf (http://users.ics.aalto.fi/tjunttil/bcsat/). To use bc2cnf, you'd have to express the DNF terms as "AND gates" in bc2cnf syntax.

Example for a EXOR function with four inputs and eight DNF minterms:

BC1.1
_m1 := !A & !B & !C &  D;
_m2 := !A & !B &  C & !D;
_m4 := !A &  B & !C & !D;
_m7 := !A &  B &  C &  D;
_m8 :=  A & !B & !C & !D;
_m11 := A & !B &  C &  D;
_m13 := A &  B & !C &  D;
_m14 := A &  B &  C & !D;
_F := _m1 | _m2 | _m4 | _m7 | _m8 | _m11 | _m13 | _m14;
ASSIGN _F;