$$ $$ $$ $\text{usepackage}pifont$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $\text{You can't use 'macro parameter character \#' in math mode}$ $\text{You can't use 'macro parameter character \#' in math mode}$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$

$$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$

$$ $$ $$

CNF Translations

As mentioned earlier, each formula can be translated into a logically equivalent formula in the conjunctive normal form. We next show three methods to do this. The first two only use the variables occurring in the original formula and are, in the worst case, of exponential size in the size of the original formula. The third method introduces auxiliary variables and is of linear size.

Method 1: Applying local rewriting rules

One can transform an arbitrary formula into an equivalent CNF formula by applying a sequence of local transformations:

1. Eliminate other binary connectives but conjunction and disjunction by applying the following rules:

   • ​ $\alpha \oplus \beta$ $⇝$ $(\alpha \wedge \mathrm{\neg }\beta )\vee (\mathrm{\neg }\alpha \wedge \beta )$

   • ​ $\alpha \to \beta$ $⇝$ $(\mathrm{\neg }\alpha \vee \beta )$

   • ​ $\alpha \leftrightarrow \beta$ $⇝$ $(\mathrm{\neg }\alpha \wedge \mathrm{\neg }\beta )\vee (\alpha \wedge \beta )$

2. Move negations next to variables

   • ​ $\mathrm{\neg }(\mathrm{\neg }\alpha )⇝\alpha$

   • ​ $\mathrm{\neg }(\alpha \wedge \beta )⇝(\mathrm{\neg }\alpha )\vee (\mathrm{\neg }\beta )$

   • ​ $\mathrm{\neg }(\alpha \vee \beta )⇝(\mathrm{\neg }\alpha )\wedge (\mathrm{\neg }\beta )$

3. Move conjunctions outside of disjunctions:

   • ​ $\alpha \vee ({\beta }_1\wedge ...\wedge {\beta }_k)⇝(\alpha \vee {\beta }_1)\wedge ...\wedge (\alpha \vee {\beta }_k)$

Note that simplification could, and should, be performed whenever possible by applying, for instance, the following rules:

• ​ $x\vee \mathrm{\neg }x⇝\mathrm{\top }$

• ​ $\mathrm{\top }\vee \beta ⇝\mathrm{\top }$

• ​ $\mathrm{\top }\wedge \beta ⇝\beta$

Example

Translating the formula $(a\wedge b)\oplus c$ to CNF by the procedure above gives us

1. first $(a\wedge b\wedge \mathrm{\neg }c)\vee (\mathrm{\neg }(a\wedge b)\wedge c)$,

2. then $(a\wedge b\wedge \mathrm{\neg }c)\vee ((\mathrm{\neg }a\vee \mathrm{\neg }b)\wedge c)$, and

3. and finally

   • ​ $((a\wedge b\wedge \mathrm{\neg }c)\vee (\mathrm{\neg }a\vee \mathrm{\neg }b))\wedge ((a\wedge b\wedge \mathrm{\neg }c)\vee c)$,

   • ​ $(a\vee \mathrm{\neg }a\vee \mathrm{\neg }b)\wedge (b\vee \mathrm{\neg }a\vee \mathrm{\neg }b)\wedge (\mathrm{\neg }c\vee \mathrm{\neg }a\vee \mathrm{\neg }b)\wedge (a\vee c)\wedge (b\vee c)\wedge (\mathrm{\neg }c\vee c)$, and

   • ​ $(\mathrm{\neg }c\vee \mathrm{\neg }a\vee \mathrm{\neg }b)\wedge (a\vee c)\wedge (b\vee c)$

In the worst case, the above translation results in exponentially larger CNF formulas. For instance, for the formula

$$(x_1\wedge y_1)\vee (x_2\wedge y_2)\vee ...\vee (x_n\wedge y_n)$$

the equivalent CNF formula

$$\underset{z_1\in \{x_1,y_1\},...,z_n\in \{x_n,y_n\}}{\bigwedge }(z_1\vee z_2\vee ...\vee z_n)$$

has $2^n$ clauses. As a concrete example with $n=3$, the CNF of $(x_1\wedge y_1)\vee (x_2\wedge y_2)\vee (x_3\wedge y_3)$ is

$$\begin{array}{l}(x_1\vee x_2\vee x_3)\wedge (x_1\vee x_2\vee y_3)\wedge \\ (x_1\vee y_2\vee x_3)\wedge (x_1\vee y_2\vee y_3)\wedge \\ (y_1\vee x_2\vee x_3)\wedge (y_1\vee x_2\vee y_3)\wedge \\ (y_1\vee y_2\vee x_3)\wedge (y_1\vee y_2\vee y_3)\end{array}$$

Method 2: Deriving CNF from truth tables

For small formulas, CNF can be directly read from the truth table for the formula. This is based on the observation that

• ​ a clause $(l_1\vee ..\vee l_k)$ is equivalent to $\mathrm{\neg }(\mathrm{\neg }{l}_1\wedge ...\wedge \mathrm{\neg }{l}_k)$ and

• ​ thus, in CNF, “excludes” the rows in the truth table in which $l_1,...,l_k$ are all false.

Example

The truth table for the formula $(a\wedge b)\oplus c$ is shown below.

$$\begin{array}{ccccc}a& b& c& (a\wedge b)& (a\wedge b)\oplus c\\ \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}\\ \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{T}}\\ \mathsf{\text{F}}& \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}\\ \mathsf{\text{F}}& \mathsf{\text{T}}& \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{T}}\\ \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}\\ \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{T}}\\ \mathsf{\text{T}}& \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{T}}& \mathsf{\text{T}}\\ \mathsf{\text{T}}& \mathsf{\text{T}}& \mathsf{\text{T}}& \mathsf{\text{T}}& \mathsf{\text{F}}\end{array}$$

Now the clause $(a\vee b\vee c)$, which is equivalent to $\mathrm{\neg }(\mathrm{\neg }a\wedge \mathrm{\neg }b\wedge \mathrm{\neg }c)$, forbids the all-false truth assignment in the first row. Excluding each row in which $(a\wedge b)\oplus c$ is $\mathsf{\text{F}}$ by adding a clause, we get the CNF formula

$$\begin{array}{r}(a\vee b\vee c)\wedge (a\vee \mathrm{\neg }b\vee c)\wedge \\ (\mathrm{\neg }a\vee b\vee c)\wedge (\mathrm{\neg }a\vee \mathrm{\neg }b\vee \mathrm{\neg }c).\end{array}$$

This is equivalent to the formula $(\mathrm{\neg }c\vee \mathrm{\neg }a\vee \mathrm{\neg }b)\wedge (a\vee c)\wedge (b\vee c)$ obtained in the example of the previous method above.

Method 3: The Tseitin-translation

This methods uses auxiliary, “fresh” variables that do not occur in the original formula to encode the semantics of the sub-formulas. The resulting CNF formula is of linear size in the size of the original formula.

Take a formula $\varphi$. For each non-variable sub-formula $\gamma$, introduce a fresh auxiliary variable $v_{\gamma }$. For each variable $x$, let $v_x=x$. We then encode the semantics of each sub-formula $\gamma$ by the following rules:

$$\begin{array}{cl}\gamma & \text{Encoding clauses}\\ \mathrm{\neg }\alpha & (\mathrm{\neg }{v}_{\gamma }\vee \mathrm{\neg }{v}_{\alpha })\wedge (v_{\gamma }\vee v_{\alpha })\\ \alpha \wedge \beta & (\mathrm{\neg }{v}_{\gamma }\vee v_{\alpha })\wedge (\mathrm{\neg }{v}_{\gamma }\vee v_{\beta })\wedge (v_{\gamma }\vee \mathrm{\neg }{v}_{\alpha }\vee \mathrm{\neg }{v}_{\beta })\\ \alpha \vee \beta & (v_{\gamma }\vee \mathrm{\neg }{v}_{\alpha })\wedge (v_{\gamma }\vee \mathrm{\neg }{v}_{\beta })\wedge (\mathrm{\neg }{v}_{\gamma }\vee v_{\alpha }\vee v_{\beta })\\ \alpha \oplus \beta & (\mathrm{\neg }{v}_{\gamma }\vee \mathrm{\neg }{v}_{\alpha }\vee \mathrm{\neg }{v}_{\beta })\wedge (\mathrm{\neg }{v}_{\gamma }\vee v_{\alpha }\vee v_{\beta })\wedge (v_{\gamma }\vee \mathrm{\neg }{v}_{\alpha }\vee v_{\beta })\wedge (v_{\gamma }\vee v_{\alpha }\vee \mathrm{\neg }{v}_{\beta })\\ \alpha \to \beta & (v_{\gamma }\vee v_{\alpha })\wedge (v_{\gamma }\vee \mathrm{\neg }{v}_{\beta })\wedge (\mathrm{\neg }{v}_{\gamma }\vee \mathrm{\neg }{v}_{\alpha }\vee v_{\beta })\\ \alpha \leftrightarrow \beta & (\mathrm{\neg }{v}_{\gamma }\vee \mathrm{\neg }{v}_{\alpha }\vee v_{\beta })\wedge (\mathrm{\neg }{v}_{\gamma }\vee v_{\alpha }\vee \mathrm{\neg }{v}_{\beta })\wedge (v_{\gamma }\vee \mathrm{\neg }{v}_{\alpha }\vee \mathrm{\neg }{v}_{\beta })\wedge (v_{\gamma }\vee v_{\alpha }\vee v_{\beta })\end{array}$$

For intuition, consider the case $\gamma =\alpha \wedge \beta$. The clauses correspond to the implications:

$$(v_{\gamma }\to v_{\alpha })\wedge (v_{\gamma }\to v_{\beta })\wedge (\mathrm{\neg }{v}_{\gamma }\to (\mathrm{\neg }{v}_{\alpha }\vee \mathrm{\neg }{v}_{\beta }))$$

or, equivalently,

$$(\mathrm{\neg }{v}_{\alpha }\to \mathrm{\neg }{v}_{\gamma })\wedge (\mathrm{\neg }{v}_{\beta }\to \mathrm{\neg }{v}_{\gamma })\wedge (v_{\alpha }\wedge v_{\beta }\to v_{\gamma })$$

From these it is easier to see that the clauses do encode the semantics of the sub-formulas correctly.

Finally, to force that the whole formula $\varphi$ should evaluate to true, we add the unary clause $(v_{\varphi })$ to the CNF formula.

Example

Consider again the formula

$$(a\wedge b)\oplus c$$

For notational convenience, let $p=v_{(a\wedge b)\oplus c}$ and $q=v_{(a\wedge b)}$. The CNF translation is:

$$\begin{array}{rcl}& & (\mathrm{\neg }q\vee a)\wedge (\mathrm{\neg }q\vee b)\wedge (q\vee \mathrm{\neg }a\vee \mathrm{\neg }b)\wedge \\ & & (\mathrm{\neg }p\vee \mathrm{\neg }q\vee \mathrm{\neg }c)\wedge (\mathrm{\neg }p\vee q\vee c)\wedge (p\vee \mathrm{\neg }q\vee c)\wedge (p\vee q\vee \mathrm{\neg }c)\wedge \\ & & (p)\end{array}$$

The satisfying truth assignments of $\varphi$ and its Tseitin-translated formula are in one-to-one correspondence.

Example

Again, consider the formula $\varphi$ and its Tseitin translation ${\varphi }^{\prime }$:

$$\begin{array}{rcl}\varphi & =& (a\wedge b)\oplus c\\ {\varphi }^{\prime }& =& (\mathrm{\neg }q\vee a)\wedge (\mathrm{\neg }q\vee b)\wedge (q\vee \mathrm{\neg }a\vee \mathrm{\neg }b)\wedge \\ & & (\mathrm{\neg }p\vee \mathrm{\neg }q\vee \mathrm{\neg }c)\wedge (\mathrm{\neg }p\vee q\vee c)\wedge (p\vee \mathrm{\neg }q\vee c)\wedge (p\vee q\vee \mathrm{\neg }c)\wedge \\ & & (p)\end{array}$$

1. The assignment $\tau =\{a\mapsto \mathsf{\text{T}},b\mapsto \mathsf{\text{F}},c\mapsto \mathsf{\text{T}}\}$ satisfies $\varphi$.

   Its extension ${\tau }^{\prime }=\{a\mapsto \mathsf{\text{T}},b\mapsto \mathsf{\text{F}},c\mapsto \mathsf{\text{T}},p\mapsto \mathsf{\text{T}},q\mapsto \mathsf{\text{F}}\}$ satisfies ${\varphi }^{\prime }$.

2. The assignment $\tau =\{a\mapsto \mathsf{\text{T}},b\mapsto \mathsf{\text{F}},c\mapsto \mathsf{\text{F}}\}$ does not satisfy $\varphi$.

   There is no extension of $\{a\mapsto \mathsf{\text{T}},b\mapsto \mathsf{\text{F}},c\mapsto \mathsf{\text{F}}\}$ that satisfies ${\varphi }^{\prime }$.