SKEDSOFT

CNF-conversion using gates: To contain the size explosion during the conversion of Boolean formulas to CNF or DNF, one can resort to a circuit-based representation of clauses. This keeps the sizes of formulas linear, but introduces a linear number of new intermediate variables. Theoretically, therefore, the exponential cost remains hidden. This is because during Boolean satisfiability, an exponential number of assignments can be sought for these new variables. In practice, however, we can often avoid suffering this cost.
We now illustrate the idea of CNF conversion using gates through an example. Consider converting the DNF expression xyzw pqrs to CNF. We build a circuit net-list as follows, by introducing temporary nodes
t1 through t7:
t1 = and(x,y) ; t2 = and(z,w) ; t3 = and(p,q) ; t4 = and(r,s)
t5 = and(t1,t2) ; t6 = and(t3,t4) ; t7 = or(t5,t6)
Now, we convert each gate to its own CNF representation. We now illustrate one conversion in detail:

• t1 = x ∧ y.
• Treat it as t1 ⇒ (x ∧ y) and (x ∧ y) ⇒ t1.
• The former is equivalent to (¬t1) ∨ (x ∧ y) which is equivalent to (¬t1 ∨ x) ∧ (¬t1 ∨ y).
• The latter is equivalent to (¬x∨¬y ∨ t1).
• Hence, t1 = x ∧ y can be represented through three clauses.

The following ML functions accomplish the conversion of AND gates and OR gates into clausal form (t1 = x ∧ y was an example of the former):

Using these ideas, the final result for the example xyzw pqrs is the following 15 variables (8 variables were in the original expression, and seven more – namely, t1 through t7 – were introduced) and 22 clauses (7 gates, each represented using 3 clauses each; the last clause is the unit clause t7 — encoded as variable number 15).