$$ $$ $$ $\text{usepackage}pifont$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $\text{You can't use 'macro parameter character \#' in math mode}$ $\text{You can't use 'macro parameter character \#' in math mode}$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$

$$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$ $$

DNF — The Disjunctive Normal Form

The disjunctive normal form is the dual of CNF. We define a cube to be a conjunction $(l_1\wedge l_2\wedge ...\wedge 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\wedge \mathrm{\neg }b)\vee (\mathrm{\neg }a\wedge \mathrm{\neg }b\wedge 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\wedge \mathrm{\neg }b)\vee (\mathrm{\neg }a\wedge \mathrm{\neg }b\wedge c)$ over the three variables $\{a,b,c\}$ has three satisfying truth assignments:

• ​ The cube $(a\wedge \mathrm{\neg }b)$ corresponds to $\{a\mapsto \mathsf{\text{T}},b\mapsto \mathsf{\text{F}},c\mapsto \mathsf{\text{F}}\}$ and $\{a\mapsto \mathsf{\text{T}},b\mapsto \mathsf{\text{F}},c\mapsto \mathsf{\text{T}}\}$.

• ​ The cube $(\mathrm{\neg }a\wedge \mathrm{\neg }b\wedge c)$ corresponds to $\{a\mapsto \mathsf{\text{F}},b\mapsto \mathsf{\text{F}},c\mapsto \mathsf{\text{T}}\}$.

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\oplus x_2\oplus \dots \oplus x_n$. Its minimal DNF consists of $2^{n-1}$ cubes of length $n$. For instance, when $n=3$, the DNF of $x_1\oplus x_2\oplus x_3$ is

$$\begin{array}{rcl}(\mathrm{\neg }{x}_1\wedge \mathrm{\neg }{x}_2\wedge x_3)& \vee & \\ (\mathrm{\neg }{x}_1\wedge x_2\wedge \mathrm{\neg }{x}_3)& \vee & \\ (x_1\wedge \mathrm{\neg }{x}_2\wedge \mathrm{\neg }{x}_3)& \vee & \\ (x_1\wedge x_2\wedge x_3)\end{array}$$

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 $\gamma \wedge (\alpha \vee \beta )⇝(\gamma \wedge \alpha )\vee (\gamma \wedge \beta )$

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

Example

Consider the formula $(a\wedge b)\oplus c$ with the truth table below.

$$\begin{array}{ccccc}a& b& c& (a\wedge b)& (a\wedge b)\oplus c\\ \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}\\ \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{T}}\\ \mathsf{\text{F}}& \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}\\ \mathsf{\text{F}}& \mathsf{\text{T}}& \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{T}}\\ \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}& \mathsf{\text{F}}\\ \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{T}}\\ \mathsf{\text{T}}& \mathsf{\text{T}}& \mathsf{\text{F}}& \mathsf{\text{T}}& \mathsf{\text{T}}\\ \mathsf{\text{T}}& \mathsf{\text{T}}& \mathsf{\text{T}}& \mathsf{\text{T}}& \mathsf{\text{F}}\end{array}$$

Now the cube $(\mathrm{\neg }a\wedge \mathrm{\neg }b\wedge 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\wedge b)\oplus c$ is $\mathsf{\text{T}}$ by adding cubes, we get the DNF formula

$$(\mathrm{\neg }a\wedge \mathrm{\neg }b\wedge c)\vee (\mathrm{\neg }a\wedge b\wedge c)\vee (a\wedge \mathrm{\neg }b\wedge c)\vee (a\wedge b\wedge \mathrm{\neg }c)$$