\usepackagepifont \definecolorfakeaaltobluelRGB00,141,229 \definecoloraaltoblueRGB00,101,189 \definecoloraaltoredRGB237,41,57 \definecolorMyBoxBackgroundrgb0.98,0.98,1.0 \definecolorMyBoxBorderrgb0.90,0.90,1.0 \definecolorbackgroundredrgb1.0,0.98,0.98 \definecolorshadowredrgb1.0,0.90,0.90 \newcommand{\subheading}[1]{\large{\usebeamercolor[fg]{frametitle}\sc #1}} %\newtcbox{\mybox}[1][red]{on line,arc=0pt,outer arc=0pt,colback=#1!10!white,colframe=#1!50!black,boxsep=0pt,left=1pt,right=1pt,top=2pt,bottom=2pt,boxrule=0pt,bottomrule=1pt,toprule=1pt} %\newtcbox{\mybox}[1][MyBoxBackground]{on line,arc=0pt,outer arc=0pt,colback=#1!10!white,colframe=#1!50!black,boxsep=0pt,left=1pt,right=1pt,top=2pt,bottom=2pt,boxrule=0pt,bottomrule=1pt,toprule=1pt} \newtcolorbox{MyBoxTitled}[1]{colback=MyBoxBackground!100!black,colframe=MyBoxBorder!100!black,boxsep=2pt,left=0pt,right=0pt,top=2pt,bottom=0pt,%enhanced,%\) \( coltitle=red!25!black,title=#1,boxrule=1pt} \newtcolorbox{MyBox}[1][]{colback=MyBoxBackground!100!black,colframe=MyBoxBorder!100!black,boxsep=0pt,left=2pt,right=0pt,top=0pt,bottom=0pt,%enhanced,%\) \( coltitle=red!25!black,boxrule=1pt,#1} \newenvironment{EqnBox}[1]{\begin{adjustbox}{valign=t}\begin{minipage}{#1}\begin{MyBox}[colback=backgroundred!100!black,colframe=shadowred!100!black]}{\end{MyBox}\end{minipage}\end{adjustbox}} \newenvironment{topbox}[1]{\begin{adjustbox}{valign=t}\begin{minipage}{#1}}{\end{minipage}\end{adjustbox}} \newcommand{\Blue}[1]{{\color{aaltoblue}#1}} \newcommand{\Red}[1]{{\color{aaltored}#1}} %\newcommand{\Emph}[1]{\emph{\color{aaltoblue}#1}} \newcommand{\Emph}[1]{\emph{\usebeamercolor[fg]{structure} #1}} %\newcommand{\Emp}{\usebeamercolor[fg]{structure}} \newcommand{\Emp}{\color{aaltored}} \newcommand{\TextDef}[1]{{\bf\usebeamercolor[fg]{structure} #1}} \newcommand{\todo}[1]{\textbf{\Red{\Pointer #1}}} \newcommand{\TODO}[1]{\todo{#1}} \newcommand{\Pointer}{\raisebox{-1ex}{\huge\ding{43}}\ } %\newcommand{\Follows}{\Pointer} \newcommand{\Follows}{\color{flagblue}\rightsquigarrow} \newcommand{\Property}{{\color{italygreen}\bf Property}} % % Common math definitions % \newcommand{\Set}[1]{\{#1\}} \newcommand{\Setdef}[2]{\{{#1}\mid{#2}\}} \newcommand{\PSet}[1]{\mathcal{P}(#1)} \newcommand{\Pair}[2]{(#1,#2)} \newcommand{\Card}[1]{{\vert{#1}\vert}} \newcommand{\Tuple}[1]{(#1)} \newcommand{\Seq}[1]{[#1]} \newcommand{\bbZ}{\mathbb{Z}} \newcommand{\Ints}{\mathbb{Z}} \newcommand{\Reals}{\mathbb{R}} \newcommand{\bbQ}{\mathbb{Q}} \newcommand{\Rats}{\bbQ} \newcommand{\False}{\textsf{F}} \newcommand{\True}{\textsf{T}} \newcommand{\Implies}{\rightarrow} \newcommand{\Iff}{\leftrightarrow} %\newcommand{\Implies}{\Rightarrow} %\newcommand{\Iff}{\Leftrightarrow} \newcommand{\Xor}{\oplus} \newcommand{\Equiv}{\equiv} \newcommand{\Oh}[1]{O(#1)} %\newcommand{\Theta}[1]{\Theta(#1)} \newcommand{\PHP}[2]{\mathrm{php}_{#1,#2}} \newcommand{\PH}[2]{\mathit{x}_{#1,#2}} \newcommand{\NP}{\textbf{NP}} \newcommand{\coNP}{\textbf{co-NP}} \newcommand{\bnfdef}{\mathrel{\textup{::=}}} \newcommand{\bnfor}{\mathrel{\mid}}
\newcommand{\Vars}{X} \newcommand{\VarsOf}[1]{\mathop{vars}(#1)} \newcommand{\Bool}{\Bbb{B}} \newcommand{\FF}{\bot} % Formula "False" \newcommand{\TF}{\top} % Formula "True" %\newcommand{\FF}{\mathbf{F}} % Formula "True" %\newcommand{\TF}{\mathbf{T}} % Formula "False" \newcommand{\LHS}{\alpha} \newcommand{\RHS}{\beta} \newcommand{\EHS}{\gamma} \newcommand{\Res}[2]{{#1} \otimes {#2}} \newcommand{\Gates}{{\mathcal G}} \newcommand{\Eqns}{{\mathcal D}} \newcommand{\Circuit}{{\mathcal C}} \newcommand{\GDef}{\mathrel{\mathrm{:=}}} \newcommand{\Gate}{g} \newcommand{\GateL}{g'} \newcommand{\GateR}{g''} \newcommand{\GateVar}[1]{v_{#1}} \newcommand{\ORf}{\mathbf{or}} \newcommand{\ANDf}{\mathbf{and}} \newcommand{\NOTf}{\mathbf{not}} \newcommand{\OR}[1]{\mathbf{or}(#1)} \newcommand{\AND}[1]{\mathbf{and}(#1)} \newcommand{\NOT}[1]{\mathbf{not}(#1)} \newcommand{\FG}{\mathbf{f}} % Input gate "False" \newcommand{\TG}{\mathbf{t}} % Input gate "True" \newcommand{\Tseitin}[1]{\mathop{\textrm{cnf}}(#1)} \newcommand{\Trans}{\mathrel{\rightsquigarrow}} \newcommand{\SUD}[3]{x_{#1,#2,#3}} \newcommand{\SUDClues}{H} \newcommand{\PseudoDPLL}{\mathop{\mathit{dpll}}} \newcommand{\PseudoAsgn}{\mathrel{\leftarrow}} \newcommand{\PseudoUnsat}{\mathbf{unsat}} \newcommand{\PseudoSat}{\mathbf{sat}} \newcommand{\TA}{\tau} \newcommand{\Undef}{\mathit{undef}} %\newcommand{\PseudoPropagate}{\textit{propagate}}

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}