\(%\usepackage{color}\) \(%\usepackage{tcolorbox}\) \(%\tcbuselibrary{skins}\) \(\usepackage{pifont}\) \(\) \(\definecolor{fakeaaltobluel}{RGB}{00,141,229} % 0065BD\) \(\definecolor{aaltoblue}{RGB}{00,101,189} % 0065BD\) \(\definecolor{aaltored}{RGB}{237,41,57} % ED2939\) \(\) \(\definecolor{MyBoxBackground}{rgb}{0.98,0.98,1.0}\) \(\definecolor{MyBoxBorder}{rgb}{0.90,0.90,1.0}\) \(\definecolor{backgroundred}{rgb}{1.0,0.98,0.98}\) \(\definecolor{shadowred}{rgb}{1.0,0.90,0.90}\) \(\) \(%\newcommand{\subheading}[1]{\textbf{\large\color{fakeaaltobluel}#1}}\) \(\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}}\)

\(\newcommand{\VA}{p}\) \(\newcommand{\VB}{q}\) \(\newcommand{\TVar}[1]{v_{#1}}\)

CNF Translations

As mentioned earlier, each formula can be translated into a logically equivalent formula in the conjunctive normal form. We next show three methods to do this. The first two only use the variables occurring in the original formula and are, in the worst case, of exponential size in the size of the original formula. The third method introduces auxiliary variables and is of linear size.

Method 1: Applying local rewriting rules

One can transform an arbitrary formula into an equivalent CNF formula by applying a sequence of local transformations:

1. Eliminate other binary connectives but conjunction and disjunction by applying the following rules:

   • ​ \( \LHS \Xor \RHS \) \( \Trans \) \( (\LHS \land \neg \RHS) \lor (\neg \LHS \land \RHS) \)

   • ​ \( \LHS \Implies \RHS \) \( \Trans \) \( (\neg \LHS \lor \RHS) \)

   • ​ \( \LHS \Iff \RHS \) \( \Trans \) \( (\neg \LHS \land \neg \RHS) \lor (\LHS \land \RHS) \)

2. Move negations next to variables

   • ​ \( \neg(\neg \LHS) \Trans \LHS \)

   • ​ \( \neg(\LHS \land \RHS) \Trans {(\neg \LHS) \lor (\neg \RHS)} \)

   • ​ \( \neg(\LHS \lor \RHS) \Trans {(\neg \LHS) \land (\neg \RHS)} \)

3. Move conjunctions outside of disjunctions:

   • ​ \( {\LHS \lor (\RHS_1 \land … \land \RHS_k)} \Trans {(\LHS \lor \RHS_1) \land … \land (\LHS \lor \RHS_k)} \)

Note that simplification could, and should, be performed whenever possible by applying, for instance, the following rules:

• ​ \( x \lor \neg x \Trans \TF \)

• ​ \( \TF \lor \RHS \Trans \TF \)

• ​ \( \TF \land \RHS \Trans \RHS \)

Example

Translating the formula \( (a \land b) \Xor c \) to CNF by the procedure above gives us

1. first \( (a \land b \land \neg c) \lor (\neg(a \land b) \land c) \),

2. then \( (a \land b \land \neg c) \lor ((\neg a \lor \neg b) \land c) \), and

3. and finally

   • ​ \( ((a \land b \land \neg c) \lor (\neg a \lor \neg b))\ \ \land\ \ ((a \land b \land \neg c) \lor c) \),

   • ​ \( (a \lor \neg a \lor \neg b) \land (b \lor \neg a \lor \neg b) \land (\neg c \lor \neg a \lor \neg b) \land (a \lor c) \land (b \lor c) \land (\neg c \lor c) \), and

   • ​ \( (\neg c \lor \neg a \lor \neg b) \land (a \lor c) \land (b \lor c) \)

In the worst case, the above translation results in exponentially larger CNF formulas. For instance, for the formula \[(x_1 \land y_1) \lor (x_2 \land y_2) \lor … \lor (x_n \land y_n)\] the CNF formula \[\bigwedge_{z_1 \in \Set{x_1,y_1},…,z_n \in \Set{x_n,y_n}} (z_1 \lor z_2 \lor … \lor z_n)\] has \( 2^n \) clauses. As a concrete example with \( n = 3 \), the CNF of \( (x_1 \land y_1) \lor (x_2 \land y_2) \lor (x_3 \land y_3) \) is \begin{array}{l} (x_1 \lor x_2 \lor x_3) \land (x_1 \lor x_2 \lor y_3) \land\\\\ (x_1 \lor y_2 \lor x_3) \land (x_1 \lor y_2 \lor y_3) \land\\\\ (y_1 \lor x_2 \lor x_3) \land (y_1 \lor x_2 \lor y_3) \land\\\\ (y_1 \lor y_2 \lor x_3) \land (y_1 \lor y_2 \lor y_3) \end{array}

Method 2: Deriving CNF from truth tables

For small formulas, CNF can be directly read from the truth table for the formula. This is based on the observation that

• ​ a clause \( (l_1 \lor .. \lor l_k) \) is equivalent to \( \neg(\neg l_1 \land … \land \neg l_k) \) and

• ​ thus, in CNF, “excludes” the rows in the truth table in which \( l_1,…,l_k \) are all false.

Example

The truth table for the formula \( (a \land b) \Xor c \) is shown 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 clause \( (a \lor b \lor c) \), which is equivalent to \( \neg(\neg a \land \neg b \land \neg c) \), forbids the all-false truth assignment in the first row. Excluding each row in which \( (a \land b) \Xor c \) is \( \False \) by adding a clause, we get the CNF formula \begin{eqnarray*} (a \lor b \lor c) \land (a \lor \neg b \lor c) \land \\\\ (\neg a \lor b \lor c) \land (\neg a \lor \neg b \lor \neg c). \end{eqnarray*} This is equivalent to the formula \( (\neg c \lor \neg a \lor \neg b) \land (a \lor c) \land (b \lor c) \) obtained in the example of the previous method above.

Method 3: The Tseitin-translation

This methods uses auxiliary, “fresh” variables that do not occur in the original formula to encode the semantics of the sub-formulas. The resulting CNF formula is of linear size in the size of the original formula.

Take a formula \( \phi \). For each non-variable sub-formula \( \EHS \), introduce a fresh auxiliary variable \( \TVar{\EHS} \). For each variable \( x \), let \( \TVar{x} = x \). We then encode the semantics of each sub-formula \( \EHS \) by the following rules: \[\begin{array}{@{}c|l@{}} \EHS & \text{Encoding clauses} \\\\ \hline \neg \LHS & (\neg\TVar{\EHS} \lor \neg\TVar{\LHS}) \land (\TVar{\EHS} \lor \TVar{\LHS}) \\\\ \LHS \land \RHS & (\neg\TVar{\EHS} \lor \TVar{\LHS}) \land (\neg\TVar{\EHS} \lor \TVar{\RHS}) \land (\TVar{\EHS} \lor \neg\TVar{\LHS} \lor \neg\TVar{\RHS}) \\\\ \LHS \lor \RHS & (\TVar{\EHS} \lor \neg\TVar{\LHS}) \land (\TVar{\EHS} \lor \neg\TVar{\RHS}) \land (\neg\TVar{\EHS} \lor \TVar{\LHS} \lor \TVar{\RHS}) \\\\ \LHS \Xor \RHS & (\neg\TVar{\EHS} \lor \neg\TVar{\LHS} \lor \neg\TVar{\RHS}) \land (\neg\TVar{\EHS} \lor \TVar{\LHS} \lor \TVar{\RHS}) \land (\TVar{\EHS} \lor \neg\TVar{\LHS} \lor \TVar{\RHS}) \land (\TVar{\EHS} \lor \TVar{\LHS} \lor \neg\TVar{\RHS}) \\\\ \LHS \Implies \RHS & (\TVar{\EHS} \lor \TVar{\LHS}) \land (\TVar{\EHS} \lor \neg\TVar{\RHS}) \land (\neg\TVar{\EHS} \lor \neg\TVar{\LHS} \lor \TVar{\RHS}) \\\\ \LHS \Iff \RHS & (\neg\TVar{\EHS} \lor \neg\TVar{\LHS} \lor \TVar{\RHS}) \land (\neg\TVar{\EHS} \lor \TVar{\LHS} \lor \neg\TVar{\RHS}) \land (\TVar{\EHS} \lor \neg\TVar{\LHS} \lor \neg\TVar{\RHS}) \land (\TVar{\EHS} \lor \TVar{\LHS} \lor \TVar{\RHS}) \end{array}\] For intuition, consider the case \( \EHS = \LHS \land \RHS \). The clauses correspond to the implications: \[(\TVar{\EHS} \Implies \TVar{\LHS}) \land (\TVar{\EHS} \Implies \TVar{\RHS}) \land (\neg \TVar{\EHS} \Implies (\neg\TVar{\LHS} \lor \neg\TVar{\RHS}))\] or, equivalently, \[(\neg \TVar{\LHS} \Implies \neg\TVar{\EHS}) \land (\neg\TVar{\RHS} \Implies \neg\TVar{\EHS}) \land (\TVar{\LHS} \land \TVar{\RHS} \Implies \TVar{\EHS})\] From these it is easier to see that the clauses do encode the semantics of the sub-formulas correctly.

Finally, to force that the whole formula \( \phi \) should evaluate to true, we add the unary clause \( (\TVar{\phi}) \) to the CNF formula.

Example

Consider again the formula \[(a \land b) \Xor c\] For notational convenience, let \( \VA = \TVar{(a \land b) \Xor c} \) and \( \VB = \TVar{(a \land b)} \). The CNF translation is: \begin{eqnarray*} && (\neg\VB \lor a) \land (\neg\VB \lor b) \land (\VB \lor \neg a \lor \neg b) \land {} \\\\ && (\neg\VA \lor \neg\VB \lor \neg c) \land (\neg\VA \lor \VB \lor c) \land (\VA \lor \neg\VB \lor c) \land (\VA \lor \VB \lor \neg c) \land {} \\\\ && (\VA) \end{eqnarray*}

The satisfying truth assignments of \( \phi \) and its Tseitin-translated formula are in one-to-one correspondence.

Example

Again, consider the formula \( \phi \) and its Tseitin translation \( \phi’ \): \begin{eqnarray*} \phi &=& (a \land b) \Xor c\\\\ \phi’ &=& (\neg\VB \lor a) \land (\neg\VB \lor b) \land (\VB \lor \neg a \lor \neg b) \land {} \\\\ && (\neg\VA \lor \neg\VB \lor \neg c) \land (\neg\VA \lor \VB \lor c) \land (\VA \lor \neg\VB \lor c) \land (\VA \lor \VB \lor \neg c) \land {} \\\\ && (\VA) \end{eqnarray*}

1. The assignment \( \TA = \Set{a\mapsto\True,b\mapsto\False,c\mapsto\True} \) satisfies \( \phi \).

   Its extension \( \TA’ = \Set{a\mapsto\True,b\mapsto\False,c\mapsto\True,\VA\mapsto\True,\VB\mapsto\False} \) satisfies \( \phi’ \).

2. The assignment \( \TA = \Set{a\mapsto\True,b\mapsto\False,c\mapsto\False} \) does not satisfy \( \phi \).

   There is no extension of \( \Set{a\mapsto\True,b\mapsto\False,c\mapsto\False} \) that satisfies \( \phi’ \).