DNF — The Disjunctive Normal Form¶

The disjunctive normal form is the dual of CNF. We define a cube to be a conjunction \((l_1 \land l_2 \land ... \land l_n)\) of literals. A cube is contradictory if it contains a literal and its negation. A formula is in disjunctive normal form (DNF) if it is a disjunction of cubes.

Example

The formula \((a \land \neg b) \lor (\neg a \land \neg b \land c)\) is in DNF.

Checking whether a DNF formula is satisfiable is easy: as the formula is a disjunction of cubes, each non-contradictory cube corresponds to one or more satisfying truth assignments.

Example

The DNF formula \((a \land \neg b) \lor (\neg a \land \neg b \land c)\) over the three variables \(\Set{a,b,c}\) has three satisfying truth assignments:

The cube \((a \land \neg b)\) corresponds to \(\Set{a \mapsto \True, b \mapsto \False, c \mapsto \False}\) and \(\Set{a \mapsto \True, b \mapsto \False, c \mapsto \True}\).
The cube \((\neg a \land \neg b \land c)\) corresponds to \(\Set{a \mapsto \False, b \mapsto \False, c \mapsto \True}\).

However, this fact does not make SAT solving trivial: translating a formula to DNF can require exponential time and space in the worst case.

Example

Consider the parity formula \(x_1 \Xor x_2 \Xor \ldots \Xor x_n\). Its minimal DNF consists of \(2^{n-1}\) cubes of length \(n\). For instance, when \(n = 3\), the DNF of \(x_1 \Xor x_2 \Xor x_3\) is

\begin{eqnarray*} (\neg x_1 \land \neg x_2 \land x_3) &{\lor}&\\ (\neg x_1 \land x_2 \land \neg x_3) &{\lor}&\\ (x_1 \land \neg x_2 \land \neg x_3) &{\lor}&\\ (x_1 \land x_2 \land x_3) \end{eqnarray*}

As with CNF (recall the section CNF Translations), a formula can be translated to DNF by local rewriting rules:

removing other binary operands but disjunction and conjunction,
pushing negations next to variables, and
pushing disjunctions outside of conjunctions with the rule \({\EHS \land (\LHS \lor \RHS)} \Trans {(\EHS \land \LHS) \lor (\EHS \land \RHS)}\)

For small formulas, the DNF can also be directly read from the truth table by observing that a cube \((l_1 \land ... \land l_k)\) “includes” all the rows in which \(l_1,...,l_k\) are all true.

Example

Consider the formula \((a \land b) \Xor c\) with the truth table below.

\[\begin{array}{ccc|c|c@{}} a & b & c & (a \land b) & (a \land b) \Xor c \\ \hline \False & \False & \False & \False & \False \\ \False & \False & \True & \False & \True \\ \False & \True & \False & \False & \False \\ \False & \True & \True & \False & \True \\ \True & \False & \False & \False & \False \\ \True & \False & \True & \False & \True \\ \True & \True & \False & \True & \True \\ \True & \True & \True & \True & \False \\ \end{array}\]

Now the cube \((\neg a \land \neg b \land c)\) includes the second row in which \(a\) and \(b\) are false and \(c\) is true. Including all the rows, and only those, in which \((a \land b) \Xor c\) is \(\True\) by adding cubes, we get the DNF formula

\begin{equation} (\neg a \land \neg b \land c) \lor (\neg a \land b \land c) \lor (a \land \neg b \land c) \lor (a \land b \land \neg c) \end{equation}