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}