Labelled CNF Conversion and its Improvement

The CNF classical conversion is expensive although it preserves the equivalence. However, CNF labelled conversion maintains the equi-satisfiability, i.e., if the original formula is SAT, then so is the converted version.

The idea is to label a part of formula as a new variable and convert only the labelled ones, which we can derive it now.

$$\phi \leftrightarrow \phi [(p \wedge q) | B] \wedge CNF_{label} (B \leftrightarrow (p \wedge q))$$

where

$$\begin{align*} &CNF_{label} (B \leftrightarrow (p \wedge q)) \\ =& (\neg B \vee (p \wedge q)) \wedge (\neg (p \wedge q) \vee B) \\ =& (\neg B \vee p) \wedge (\neg B \vee q) \wedge (B \vee \neg p \vee \neg q)) \end{align*}$$

The same applies for disjunction, implication and double implication.

Improved version

By utilizing the results we had in last post (polarity), we can simplify the $CNF_{label}$ procedure. For instance, if $p \wedge q$ occurs positively, we only proceed with $CNF_{label} (B \rightarrow (p \wedge q))$, on negative occurrence, we instead use $CNF_{label} ((p \wedge q) \rightarrow B)$

An example

Convert the following using improved $CNF_{label}$. Credit: R. Sebastiani.

$$(A_1 \wedge A_2) \vee (A_3 \wedge \neg A_4) \vee (\neg A_1 \wedge \neg A_3) \vee (A_2 \wedge \neg A_4)$$

We start considering the whole formula as a sole variable $B$. And the rest conjunctions are $B_1$,$B_2$, $\cdots$, i.e.

$$\overbrace{\underbrace{(A_1 \wedge A_2)}_{B_1} \vee \underbrace{(A_3 \wedge \neg A_4)}_{B_2} \vee \underbrace{(\neg A_1 \wedge \neg A_3)}_{B_3} \vee \underbrace{(A_2 \wedge \neg A_4)}_{B_4}}^{B}$$

Finally, $B_i$s all occur positively, then we only use one-side implication. i.e.

$$\begin{align*} &B \wedge (B \rightarrow (B_1 \vee B_2 \vee B_3 \vee B_4)) \\ & \wedge (B_1 \rightarrow (A_1 \wedge A_2)) \\ & \wedge \cdots \end{align*}$$