Clausal Normal Form

Clauses §

A Clause is a disjunction $L_1\vee ...\vee L_n,n>0$ of literals, where a literal is either an atom $A$ or its negation, $\neg A$.

Clausal Normal Form §

Unlike Conjunctive Normal Form, a formula and its representation in clausal normal form are not necessarily equivalent, but they must be equally satisfiable. This means that either $\{\}$ (satisfiable) or $\{\square \}$ (unsatisfiable) is a valid clausal normal form representation of every formula. However, determining which of these is correct for a given formula is computationally intensive as it is equivalent to checking for satisfiability. As such, we wish to find a clausal normal form for a formula which is not hard to construct. In order to achieve this, we introduce definitions. For every subformula, we introduce a definition for it and replace its occurrence with this new variable. For the example formula:

$$A\to B\vee C$$

there are two subformulae, the formula itself and $B\vee C$. We can introduce a definition for the top-level formula as

$$n_1\leftrightarrow A\to n_2$$

ensuring that the definition contains no more than two variables. In order to achieve this, we introduce a new definition for the right hand side of the implication, $n_2$. We do not need to introduce a definition for $A$ as this is already a literal. We must then define $n_2$ as:

$$n_2\leftrightarrow B\vee C$$

We can then transform these to clauses and state a clausal normal form for this example as:

$$\begin{array}{r}{n}_1\\ \\ \neg n_1\vee \neg A\vee n_2\\ n_1\vee A\\ n_1\vee \neg n_2\\ \\ \neg n_2\vee B\vee C\\ n_2\vee \neg B\\ n_2\vee \neg C\end{array}$$

Warning

It is important to remember to include the top-level definition as a single-variable clause (likely $n_1$), otherwise the resultant set of clauses will always be satisfiable.

For subformulae containing $\wedge$, $\to$ or $\leftrightarrow$, their definitions should be used to obtain a set of clauses for that subformula.

Optimised Clausal Normal Form §

We can reduce the number of clauses required through optimisation based on the Polarity of introduced variables.

If the subformula occurs positively in the original formula, then the left hand side of the bi-implication can be dropped. If the occurrence is negative, then the right hand side can be dropped. In the example above, $n_1$ occurs positively and as such can be defined as

$$n_1\to (A\to n_2)$$

This allows the clauses associated with the other side of the bi-implication to be removed from the clausal normal form representation. This would allow the omission of the following clauses from the above example:

$$\begin{array}{r}{n}_1\vee A\\ n_1\vee \neg n_2\end{array}$$