Clausal Normal Form (Propositional Formula)

logic propositional-logic

Definition

Clausal Normal Form

The clausal normal form of a propositional formula $A$ is a set of clauses $S$ such that $S$ is equisatisfiable with $A$.

This is weaker than conjunctive normal form, which requires logical equivalence and can cause exponential blow-up. Clausal normal form avoids this by using naming to introduce new atoms for subformulas.

Definitional Transformation

Naive Definitional Transformation

Naive Definitional Transformation

This algorithm converts a formula $A$ into a set of clauses $S$ such that $S$ is a clausal normal form of $A$.

If $A$ has the form $C_1\wedge \cdots \wedge C_n$, where $n\ge 1$ and each $C_i$ is a clause, then $S\stackrel{\text{def}}{=}\{C_1,\dots ,C_n\}$. Otherwise, introduce a name for each subformula $B$ of $A$ such that $B$ is not a literal and use this name instead of the formula.

In detail:

1. If $A$ is already a conjunction of clauses, return the corresponding set of clauses.
2. Otherwise, for each non-literal subformula $B$ of $A$, introduce a new atom $n$ and add the defining equivalence $n\leftrightarrow B$.
3. Replace $B$ by $n$ in $A$.
4. The resulting set $\{A^{\prime }\}\cup \{\text{definitions}\}$ is equisatisfiable with $A$.
5. Transform each definition into clauses using standard rewrite rules.

This runs in time almost linear in the size of $A$.

Definitional transformation step by step

Let

$$A=\neg (((p\to q)\wedge (p\wedge q\to r))\to (p\to r)).$$

We name every non-literal subformula, working from the largest to the smallest.

The process is easiest to follow on the parse tree. Each internal node gets the name that will later be used in its defining equivalence:

Step 1 — The whole formula.
The outermost connective is $\neg$. We name the body of the negation $n_2$, and let $n_1$ stand for the whole formula:

$$n_1\leftrightarrow \neg n_2.$$

Step 2 — The implication inside.
The subformula $n_2$ is an implication whose antecedent is a conjunction and whose consequent is another implication. We name these two parts $n_3$ and $n_7$:

$$n_2\leftrightarrow (n_3\to n_7).$$

Step 3 — The conjunction and the inner implication.
The conjunction $n_3$ has two conjuncts: an implication $p\to q$ and another implication $p\wedge q\to r$. We name the first $n_4$. For the second, its antecedent $p\wedge q$ is not a literal, so we name it $n_6$ and let $n_5$ stand for the whole implication:

$$n_3\leftrightarrow (n_4\wedge n_5),n_5\leftrightarrow (n_6\to r),n_6\leftrightarrow (p\wedge q).$$

Step 4 — The remaining implications.
The two implications that now contain only literals are $p\to q$ and $p\to r$. We name them $n_4$ and $n_7$ respectively:

$$n_4\leftrightarrow (p\to q),n_7\leftrightarrow (p\to r).$$

Step 5 — Convert every definition to clauses.
Each equivalence is expanded using the standard rewrite rules. For instance, $n_1\leftrightarrow \neg n_2$ becomes $(\neg n_1\vee \neg n_2)\wedge (n_1\vee n_2)$, and $n_4\leftrightarrow (p\to q)$ becomes $(\neg n_4\vee \neg p\vee q)\wedge (p\vee n_4)\wedge (\neg q\vee n_4)$.

The full list is:

name	subformula	definition	clauses
$n_1$	$\neg ((p\to q)\wedge (p\wedge q\to r)\to (p\to r))$	$n_1\leftrightarrow \neg n_2$	$\neg n_1\vee \neg n_2$, $n_1\vee n_2$
$n_2$	$(p\to q)\wedge (p\wedge q\to r)\to (p\to r)$	$n_2\leftrightarrow (n_3\to n_7)$	$\neg n_2\vee \neg n_3\vee n_7$, $n_3\vee n_2$, $\neg n_7\vee n_2$
$n_3$	$(p\to q)\wedge (p\wedge q\to r)$	$n_3\leftrightarrow (n_4\wedge n_5)$	$\neg n_3\vee n_4$, $\neg n_3\vee n_5$, $\neg n_4\vee \neg n_5\vee n_3$
$n_4$	$p\to q$	$n_4\leftrightarrow (p\to q)$	$\neg n_4\vee \neg p\vee q$, $p\vee n_4$, $\neg q\vee n_4$
$n_5$	$p\wedge q\to r$	$n_5\leftrightarrow (n_6\to r)$	$\neg n_5\vee \neg n_6\vee r$, $n_6\vee n_5$, $\neg r\vee n_5$
$n_6$	$p\wedge q$	$n_6\leftrightarrow (p\wedge q)$	$\neg n_6\vee p$, $\neg n_6\vee q$, $\neg p\vee \neg q\vee n_6$
$n_7$	$p\to r$	$n_7\leftrightarrow (p\to r)$	$\neg n_7\vee \neg p\vee r$, $p\vee n_7$, $\neg r\vee n_7$

The clausal normal form of $A$ is the set of all clauses in the rightmost column.

Polarity-based Definitional Transformation

Polarity-based Definitional Transformation

In the naive transformation, every definition is an equivalence

$$n\leftrightarrow B.$$

This produces two clauses for each direction. When all occurrences of $B$ in the formula have the same polarity, one of those directions is redundant and can be dropped.

• If $B$ occurs only positively, use $n\to B$ instead of $n\leftrightarrow B$.
• If $B$ occurs only negatively, use $B\to n$ instead of $n\leftrightarrow B$.

This yields fewer clauses while preserving equisatisfiability.

Naming on positive polarity

Let $S$ be a set of formulas. Let $B$ be a formula occurring only positively in $S$. Let $n$ be an atom not occurring in $S$ and not occurring in $B$.

Let $S^{\prime }$ be obtained from $S$ by replacing every occurrence of $B$ by $n$. Then $S$ is satisfiable if and only if $S^{\prime }\cup \{n\to B\}$ is satisfiable.

Naming on negative polarity

Let $S$ be a set of formulas. Let $B$ be a formula occurring only negatively in $S$. Let $n$ be an atom not occurring in $S$ and not occurring in $B$.

Let $S^{\prime }$ be obtained from $S$ by replacing every occurrence of $B$ by $n$. Then $S$ is satisfiable if and only if $S^{\prime }\cup \{B\to n\}$ is satisfiable.

Relation to Conjunctive Normal Form

CNF vs. clausal normal form

Conjunctive normal form preserves logical equivalence but may produce an exponentially larger formula.

Clausal normal form preserves only equisatisfiability, but the transformation is efficient and the resulting set of clauses is at most linearly larger.

Examples

Nested equivalence

Let

$$A=p_1\leftrightarrow (p_2\leftrightarrow (p_3\leftrightarrow p_4)).$$

A direct CNF transformation expands each $\leftrightarrow$ into two clauses and distributes, yielding exponentially many clauses.

Instead, use naming. Introduce new atoms:

$$\begin{array}{rl}{n}_1& \leftrightarrow (p_3\leftrightarrow p_4),\\ n_2& \leftrightarrow (p_2\leftrightarrow n_1).\end{array}$$

The renamed formula is:

$$A^{\prime }=p_1\leftrightarrow n_2.$$

The clausal normal form is the set of clauses obtained from $A^{\prime }$, $n_1\leftrightarrow (p_3\leftrightarrow p_4)$, and $n_2\leftrightarrow (p_2\leftrightarrow n_1)$. Each piece is small, and the total size is linear in the size of $A$.