\documentclass{article}
\usepackage{epsfig}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%% General formatting parameters %%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\parskip=.080in
\setlength{\evensidemargin}{0.in}
\setlength{\oddsidemargin}{0.in}
\setlength{\textwidth}{6.612in}
\setlength{\topmargin}{0.in}
\setlength{\textheight}{8.8in}
\setlength{\headheight}{0in}
\setlength{\headsep}{0in}
\setlength{\topsep}{0in}
\setlength{\itemsep}{0in}
\renewcommand{\baselinestretch}{1.2}
\newcommand{\smallsection}[1]{{\smallskip\bf #1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%% Non-mathematical macros %%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\larry}{{$\calL^3$}}
\newcommand{\marek}{\mbox{${\cal M}\!{\cal C}\!h$}}
\newcommand{\ie}{{\em i.e.}}
\newcommand{\etal}{\mbox{\em et al.\/} }
\newcommand{\tH}{{\rm th}}
\newcommand{\eg}{{\em e.g.}}
\newcommand{\etc}{{\em etc.}}
\newcommand{\case}[1]{{\smallskip\noindent{\bf Case #1:\/}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%% Caligraphic letters %%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\calA}{{\cal A}}
\newcommand{\calB}{{\cal B}}
\newcommand{\calC}{{\cal C}}
\newcommand{\calD}{{\cal D}}
\newcommand{\calE}{{\cal E}}
\newcommand{\calF}{{\cal F}}
\newcommand{\calG}{{\cal G}}
\newcommand{\calH}{{\cal H}}
\newcommand{\calI}{{\cal I}}
\newcommand{\calJ}{{\cal J}}
\newcommand{\calK}{{\cal K}}
\newcommand{\calL}{{\cal L}}
\newcommand{\calM}{{\cal M}}
\newcommand{\calN}{{\cal N}}
\newcommand{\calO}{{\cal O}}
\newcommand{\calP}{{\cal P}}
\newcommand{\calQ}{{\cal Q}}
\newcommand{\calR}{{\cal R}}
\newcommand{\calS}{{\cal S}}
\newcommand{\calT}{{\cal T}}
\newcommand{\calU}{{\cal U}}
\newcommand{\calV}{{\cal V}}
\newcommand{\calW}{{\cal W}}
\newcommand{\calX}{{\cal X}}
\newcommand{\calY}{{\cal Y}}
\newcommand{\calZ}{{\cal Z}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%% Delimiters %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\angled}[1]{{\left\langle #1\right\rangle}}
\newcommand{\barred}[1]{{\left|#1\right|}}
\newcommand{\braced}[1]{{\left\{#1\right\}}}
\newcommand{\brackd}[1]{{\left[#1\right]}}
\newcommand{\parend}[1]{{\left(#1\right)}}
\newcommand{\spaced}[1]{{\ #1\ }}
\newcommand{\dummydot}{{\/\cdot\/}}
\newcommand{\mytimes}{{\!\times\!}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%% something-ed letters %%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\barx}{{\bar{x}}}
\newcommand{\bary}{{\bar{y}}}
\newcommand{\cstar}{{c^\ast}}
\newcommand{\phistar}{{\phi^\ast}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%% Strategy and problems names %%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\adv}{{\it adv}}
\newcommand{\MSS}{{\rm MSS}}
\newcommand{\PRP}[1]{{#1\!-\!\mbox{\rm PRP}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%% Sets and constants %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\Domain}{\mbox{\sf Dom\,}}
\newcommand{\reals}{{\rm I\!R}}
\newcommand{\naturals}{ \mbox{\rm I\hspace{-3pt}N} }
\newcommand{\Det}{{\mbox{\sf Det}}}
\newcommand{\distrib}{{\rm I\!D}}
\newcommand{\half}{{\scriptstyle{1\over 2}}}
\newcommand{\Rand}{{\mbox{\sf Rand}}}
\newcommand{\nats}{{\rm I\!N}}
\newcommand{\posreals}{{\rm I\!R^+}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%% Functions and Operators %%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\becomes}{\mbox{$:=$}}
\newcommand{\bdistrib}{{\rm I\!B}}
\newcommand{\cost}{\mbox{\it cost\/}}
\newcommand{\To}{{\Rightarrow}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%% Environments %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newtheorem{theorem}{Theorem}
\newtheorem{observation}{Observation}
\newtheorem{lemma}{Lemma}
\newtheorem{conjecture}{Conjecture}
\newtheorem{corollary}{Corollary}
\newtheorem{remark}{Remark}
\newtheorem{fact}{Fact}
\newenvironment{proof}{{\it Proof:\/}}{$\Box$\vskip 0.1in}
\newenvironment{example}[1]{{%
        \vskip 0.1in \noindent
        {\bf Example~{#1}:\ }%
    }}%
    {$\Diamond$\vskip 0.1in}
\newenvironment{claim}[1]%
  {{\vskip 0.1in\noindent \bf Claim~#1:\ }}%
  {\vskip 0.1in}

\newcommand{\sfparagraph}[1]%
   {\vskip 0.1in\noindent{\sf #1}}

\newenvironment{mydescription}%
        {%
           \begin{list}{}%
             {%
                \setlength{\topsep}{0pt}%
                \setlength{\parsep}{0pt}%
                \setlength{\partopsep}{0pt}%
                \setlength{\itemsep}{0pt}%
                \setlength{\itemindent}{0pt}%
                \setlength{\labelwidth}{0.2in}%
                \setlength{\leftmargin}{0.3in}%
                \setlength{\rightmargin}{0.3in}%
            }%
        }%
        {\end{list}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\margincomment}[1]%
    {{%
      \marginpar{{\tiny\begin{minipage}{0.5in}
                       \begin{flushleft}
                          {#1}
                       \end{flushleft}
                       \end{minipage}
                }}
    }}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%% maly %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\maly}[1]{{\scriptscriptstyle#1}}
\newcommand{\malyz}{{\maly{0}}}
\newcommand{\malyone}{{\maly{1}}}
\newcommand{\malytwo}{{\maly{2}}}
\newcommand{\smallX}{{\scriptscriptstyle X}}
\newcommand{\smallY}{{\scriptscriptstyle Y}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%% fill-in blanks %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\u{\_\_}
\def\uu{\u\u}
\def\uuu{\uu\uu}
\def\uuuu{\uuu\uuu}
\def\uuuuu{\uuuu\uuuu}
\def\uuuuuu{\uuuuu\uuuuu}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\spcd}[1]{{\ #1\ }}
\newcommand{\romn}[1]{{\mbox{\rm #1}}}
\newcommand{\spacedromn}[1]{\spcd{\romn{#1}}}

\newcommand{\leftbracedtwo}[2]{\left\{\begin{array}{l}
                                        #1 \\ #2
                                    \end{array}\right.
                           }

\renewcommand{\labelenumi}{\arabic{enumi}. }
\renewcommand{\labelenumii}{(\roman{enumii})}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
%\thispagestyle{empty}
%\setcounter{page}{0}
\section*{CS456 UNLV Spring Semester 2018}
\subsection*{Reduction of SAT to 3-CNF-SAT}

The internet contains pages that explain how SAT can be reduced to 3-SAT.
In this handout, I will give a brief explanation of a reduction, illustrated
by a small example.

Suppose you are given a Boolean expression $E$.  Our goal is to construct
a Boolean Expression $E'$ in conjunctive normal form such that $E$ and $E'$
are equisatisfiable, and such that the length of $E'$ is at most a polynomial
function of the length of $E$.  We outline the construction below.

\begin{itemize}
\item
First, eliminate all operators except conjunction, disjunction, and negation,
{\em i.e.,} which we write as *, +, and !.
For example, $u\Rightarrow v$ is replaced by the equisatisfiable formula
$!u+v$, $u=v$ by $(u+!v)*(v+!u)$, and $u\ne v$ by $(u+v)*(!u+!v)$.
Any other Boolean operator can similarly be eliminated.

\item
Then, draw a parse tree for $e$, where there is a leaf for each operator
and each variable, and an internal node for each larger sub-expression of $e$.
Then replace each internal node by a new variable.  These new variables must
be distinct, and none can be the same as a variable in the original formula.

\item
Then, for every internal node, write the Boolean formula which sets its
variable equal to the expression given by its children.
Replace each such equality by an equivalent conjunction
of CNF clauses, and let $E'$ be the conjunction of all those clauses.
\end{itemize}

Here is an example.  Let $E$ be the Boolean expression $!(x*y)+z*!x$.
We need a variable for each subexpression of $E$.   We introduce variables
$a,b,c,d,e$, where $a$ represents $x*y$, $b$ represents
$!x$, $c$ represents $!(x*y)$, $d$ represent $z*!x$, and $e$ represents
$!(x*y)+z*!x$.  We then draw the parse tree for $E$:

\vskip 0.2in
\centerline{\epsfig{file = parse.eps,width = 2 in}}
\vskip 0.2in

Given an assignment of the original variables $x$, $y$, and $z$,
we place the assigned Boolean values (either true
or false) at the leaves, and then evaluate bottom-up.
The root is then true if and only if the assignment is satisfying.

The following Boolean expression states that the nodes of the tree are
properly evaluated and that the root is true.
The expression is satisfiable if and only if $E$ is satisfiable.

$$ e*(e=c*d)*(c=!a)*(a=x*y)*(d=z*b)*(b=!x)$$

To obtain conjunction normal form, we replace each clause by an equisatisfiable
CNF formula using the following rules:

\begin{enumerate}
\item
Replace $u=!v$ by $(u+v)*(!u+!v)$.
\item
Replace $u=v+w$ by $(u+!v)*(u+!w)*(!u+v+w)$.
\item
Replace $u=v*w$ by $(!u+v)*(!u+w)*(u+!v+!w)$.
\end{enumerate}
We then obtain the CNF formula $E'$:
$$e*(e+!c)*(e+!d)*(!e+c+d)*(c+a!*(!c+!a)*
      (!a+x)*(!a+y)*(a+!x+!y)*(!d+z)*(!d+b)*(d+!z+!b)*(b+x)*(!b+!x)$$

$E$ and $E'$ are equisatisfiable.
Finally, we can then put $E'$ into 3-CNF form by ``padding" each clause with
redundant terms, as needed.  For example, we can replace $e$ by $(e+e+e)$,
$(!e+c)$ by $(!e+c+c)$, {\em etc.}

\end{document}
