Clausal notation for formulas in CNF

In various situations, it is easier to use another notation for formulas in conjunctive normal form (CNF) which has the set as its base data structure. This set will represent the set of all clauses in the formula. Since a set has no ordering a formula in this notation does not represent a unique formula (like the prefix and mostly the infix or human-readable notation do) but a set of equivalent formulas.

Starting point

In general, in a conjunction $\bigwedge_{i<n} \varphi_i$ we can, while keeping equivalence,

• rearrange the $\varphi_i$s,
• add copies of any $\varphi_i$,
• remove other occurrences of any of the $\varphi_i$s.

Example $\bigwedge(X_0, \neg X_1, \neg X_1, X_2) \SemEquiv \bigwedge(\neg X_1, X_0, X_2, X_0)$.

The following lemma makes a formal statement about this.

Lemma Let $\varphi$ and $\psi$ be formulas where $\varphi = \bigwedge_{i < m} \varphi_i$ and $\psi = \bigwedge_{j<n} \psi_j$ with $\varphi_i \in \text{PVars}$ and $\psi_j \in \text{PVars}$ for every $i < m$ and $j<n$. Then $\varphi \SemEquiv \psi$ if, and only if, $\text{vars}(\varphi) = \text{vars}(\psi)$.

This, together with the substitution lemma, justifies the following notation for $\bigvee$ and $\bigwedge$. When $\Phi$ is a finite set of formulas, then $\bigwedge \Phi$ stands for any formula $\bigwedge_{i < n} \varphi_i$ such that $\{\varphi_i \colon i < n\} = \Phi$. The same applies to $\bigvee$.

Example We may write $\bigwedge \{X_0, \neg X_1 \vee X_1\}$ instead of $\bigwedge(X_0, \neg X_1 \vee X_1, X_0)$.

This also justifies the following notation. When $M$ is a finite set of finite sets of formulas, then $$\bigwedge\bigvee M$$ stands for any formula $$\bigwedge_{i<m}\bigvee_{j<n_i}\varphi_i^j$$ such that $M = \{\{\varphi_i^j \colon j < n_i\} \colon i < m\}$.

Example We may write $\bigwedge\bigvee \{\{X_0, X_1 \wedge X_2\}, \{X_2, \neg \neg X_4\}\}$ instead of $\bigwedge(\bigvee(X_0, X_1 \wedge X_2), \bigvee(X_2, \neg \neg X_4))$.

Formal definition

A formula is in clausal notation for CNF if it is of the form $\bigwedge\bigvee M$ where $M$ is a finite set of finite sets of literals.

In other words, a formula is in conjunctive normal form when it can be written as $\bigwedge\bigvee M$ for a finite set $M$ of finite sets of literals.

Example 2-colorability of the triangle can be modelled by the formula \begin{align} (X_0 \vee X_1) \wedge (\neg X_0 \vee \neg X_1) \wedge (X_1 \vee X_2) \wedge (\neg X_1 \vee \neg X_2) \wedge (X_2 \vee X_0) \wedge (\neg X_2 \vee \neg X_0) \enspace. \end{align} The clausal notation for this formula is \begin{align} \bigwedge \bigvee\{\{X_0, X_1\}, \{\neg X_0, \neg X_1\}, \{X_1, X_2\}, \{\neg X_1, \neg X_2\}, \{X_2, X_0\}, \{\neg X_2, \neg X_0\}\} \enspace. \end{align}

Often the prefix $\bigwedge\bigvee$ is ommitted in contexts where one deals only with formulas in CNF.