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}