\documentclass{scrartcl}
\usepackage[margin=1in, left=0.5in, right=0.5in]{geometry}
\usepackage[utf8]{inputenc}
\usepackage[francais]{babel}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{fancyhdr}
\usepackage{mathtools}
\fancyhead[R]{\textsc{Langage formels, calculabilité et complexité}}
\fancyhead[L]{TD8} % except the center
\fancyfoot{} % except the center
\fancyfoot[L]{louis.jachiet@ens.fr}
\fancyfoot[C]{https://louis.jachiet.com/tps.html}
\fancyfoot[R]{December the 7th 2017}
\newcommand{\DP}{\mathcal{P}}
\newcommand{\NP}{\mathcal{NP}}
\newcommand{\coNP}{\mbox{co-}\mathcal{NP}}
\newcommand{\B}{\mathcal{B}}
\newcommand{\X}{\mathcal{X}}
\newcommand{\I}{\mathcal{I}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\R}{\mathcal{R}}
\newcommand{\Ls}{{\mathcal{L}_\Sigma}}
\newcommand{\Lc}{{\mathcal{L}}}
\newcommand{\ml}{\mu_{\mathcal{L}}}
\newcommand{\Mn}{M_n(\Ls)}
\newcommand{\Vn}{{M_{n,1}(\Ls)}}
\newcommand{\tr}[1]{\xrightarrow{#1}}
\newcommand{\td}{\tilde{\delta}}
\newcommand{\norm}[1]{\left\lvert#1\right\rvert}
\newcommand{\code}[1]{{\langle}{#1}{\rangle}}
\renewcommand{\headrulewidth}{0.4pt}
\renewcommand{\footrulewidth}{0.4pt}
\usepackage{exsheets}[2014/09/14] % v0.16 or newer
\SetupExSheets{
  headings = runin ,
  headings-format = \large\bfseries\sffamily ,
  subtitle-format = \large\bfseries\sffamily ,
%  counter-within = section ,
%  counter-format = se.qu\IfQuestionSubtitleT{:} ,
%solution/print = true
}
\newtheorem{defi}{Definition}

\newcommand\myeq{\stackrel{\mathclap{\normalfont\mbox{def}}}{=}}

\newcommand*\fo[1]{\tikz[baseline=(char.base)]{
                \node[shape=circle,draw,inner sep=2pt] (char) {#1};}}
\usepackage{tikz}
\usetikzlibrary{automata,positioning,trees}

\author{}
%\date{}
\title{TD8 : Langages formels, calculabilité et complexité}

\begin{document}
\pagestyle{fancy}

\section{Reducing from 3-SAT to CNF-SAT}


A formula \emph{CNF} (for \emph{Conjunctive Normal Form}) is a set of
variables $x_1, \dots, x_n$ and a set of clauses $C_1, \dots, C_k$
where each clause is a disjunction of literals (a literal is either
a variable $x$ of its negation $\lnot x$). For all $1\leq j \leq k$,
we have $C_j = \bigvee_i v^j_i$ where $v^j_i = x_l$ or $v^j_i=\lnot
x_l$ for a given $l$.

A CNF formula is satisfiable if it exists an assignation of the
variables $x_1, \dots, x_n$ to true ($\top$) or false ($\bot$) such
that each clause is satisfied (i.e. for each clause, at least one of
these literals is true). From a logical point of view, a CNF formula
is a formula of the form: $\exists x_1, \dots x_n\in \{\top,\bot\}^n:
{\bigwedge_j \left( \bigvee_{i} v^j_i \right)}$.

\begin{defi}
The \emph{CNF-SAT} problem is to decide whether a CNF formula is
satisfiable.
\end{defi}


\begin{defi}
The $k$\emph{-SAT} problem is to decide the satisfiability of a CNF
formula where each clause has to have at most $k$ literals.
\end{defi}


\begin{question} 
Show that the \emph{CNF-SAT} and \emph{$k$-SAT} problems (for all
$k\in\mathbb{N}$)) are $\NP$.
\end{question}

\begin{question}
Show that the formula $(v_1\lor v_2\lor v_3\lor v_4)$ is satisfiable
if and only if $(v_1\lor v_2\lor l) \land (\lnot l \lor v_3\lor v_4)$
is satisfiable (where $l$ is a fresh variable, \textit{i.e.} $l$ does
not appear in any of the $v_1, \dots, v_4$).
\end{question}

\begin{question}
  Show that $3$-SAT is $\NP$-complete. Start from CNF-SAT (which is
  $\NP$-complete) and show that for each CNF formula $\varphi$ we can
  find $\varphi'$ satisfiable iff $\varphi$ also is with $|\varphi'|$
  polynomial in $|\varphi|$ and where each clause of $\varphi'$
  contains at most $3$ literals.
\end{question}

\begin{defi}
  A DNF formula (for \emph{Disjunctive Normal Form}) is a set of
  variables $x_1, \dots, x_n$ and a disjunction of clauses where each
  clause is a conjunction of literals. A DNF formula is thus
  equivalent to $\exists x_1, \dots, x_n\in\{\bot,\top\}^n:\lor_j
  (\land_i v_i^j)$
\end{defi}

\begin{question}
Is the DNF-SAT (satisfiability of DNF formula) in $\NP$? in $\coNP$?
in $\DP$?
\end{question}

\section{Reducing from 3-SAT to 3-coloring}

\begin{defi}
  Given a graph $G=(V,E)$, $G$ is $k$-coloriable if we can color its
  nodes with $k$ colors such that no two neighboring nodes have the
  same color. Formally $\exists (c:V\rightarrow \{1,\dots,k\})~\forall
  (i,j)\in E~: c(i)\neq c(j) $.
\end{defi}

\begin{question}
Show that for each $k$ fixed, the $k$-coloriability is $\NP$.
\end{question}

\begin{question}
Show that if the $k+1$-coloriability problem is in $\DP$ then so is
the $k$-coloriability problem.
\end{question}

Let us show that $3$-SAT can be reduced to $3$-coloriage. First let us
introduce a few gadgets.

\subsection{Color gadget}

We will make sure that the colors in our graph represent either true
($\top$), false ($\bot$) or ground $G$. To encode these colors, our
first gadget is to include in the graph the graph drawn below. After
that we will often plug nodes to $G$ or $\bot$ to forbid colors in
nodes. This gadget is only present once in the graph.
\begin{center}
\begin{tikzpicture}[shorten >=1pt,node distance=1cm,on grid,auto,scale=0.6, every node/.style={scale=0.6}]
    \node[state] (V)   {$\top$};
    \node[state] (F) [right=of V] {$\bot$};
    \node[state] (G) [below right=0.75cm and 0.5cm of V] {$G$};
    \path[-]
    (V) edge  (F)
    (F) edge (G)
    (G) edge (V) ;
\end{tikzpicture}
\end{center}


\subsection{Literal gadget}
For each variable $x_i$ we create two nodes: $x_i$ and $\lnot x_i$
that we will connected to each other and to $G$ as represented below:
\begin{center}
\begin{tikzpicture}[shorten >=1pt,scale=0.6, every node/.style={scale=0.6},node distance=2cm,on grid,auto]
    \node[state] (x)   {$x_i$};
    \node[state] (n) [below=0.75cm of x] {$\lnot x_i$};
    \node[state] (G) [below left=0.325cm and 1.75cm of x] {$G$};
    \path[-]
    (x) edge  (n)
    (n) edge (G)
    (G) edge (x) ;
\end{tikzpicture}
\end{center}



\subsection{OR gadget}

Suppose that $a$ and $b$ represent boolean values (we can enforce that
by plugging them into $G$), the OR gadget is the following (the $G$
node is the one of the color gadget) :
\begin{center}
\begin{tikzpicture}[shorten >=1pt,scale=0.6, every node/.style={scale=0.6},node distance=1cm,on grid,auto]
    \node[state] (R)  {$R$};
    \node[state] (G)  [below left=1cm and 3cm of R] {$G$};
    \node[state] (a1) [below left=1.cm and 0.5cm of R]  {$\widetilde{a}$};
    \node[state] (b1) [right=of a1] {$\widetilde{b}$};
    \node[state] (a) [below=of a1]  {$a$};
    \node[state] (b) [right=of a] {$b$};
    \path[-]
    (a) edge  (a1)
    (a1) edge (R)
    (b) edge  (b1)
    (b1) edge (R)
    (a1) edge (b1)
    (G) edge (R) 
    (G) edge (a) 
    (G) edge [bend right=60] (b) ;
\end{tikzpicture}
\end{center}

\begin{question}
  Show that in any valid coloring, the color of $R$ is the color of
  $a$ or $b$. And, if we limit the problem to this subgraph then it
  can be colored with either the color of $a$ or $b$.
\end{question}

  
\begin{question}
  Find a gadget that performs the OR between three boolean values $a$,
  $b$, $c$ (represented as nodes colored either $\top$ or $\bot$).
\end{question}

\subsection{Packing everything}
\begin{question}
  For each clause, design a gadget to verify it.
\end{question}

\begin{question}
Provide a polynomial reduction from $3$-SAT to $3$-coloring.
\end{question}

\section{Miscellaneous}


\begin{question}
In which classes ($\DP$? $\NP$? $\coNP$?) is the $2$-coloring problem?
\end{question}

\begin{question}
Show that SAT can be reduced to $3$-SAT (i.e the satisfiability of
formula composed of $\lor$, $\land$, $\lnot$ and variables).
\end{question}

\begin{question}
In which classes is the $2$-SAT problem?
\end{question}

\section{Cliques}

\begin{defi}
  The clique problem is to decide whether a given graph contains a
  $k$-clique ($k$ nodes all direct neighbors of each others).
\end{defi}

\begin{question}
  Show that the clique problem is $\NP$-complete.

  \emph{Suggestion: find a reduction with 3-SAT. Given $\bigvee_j
    (\bigwedge_i v^j_i)$ we create a node for each $v^j_i$ (when a
    literal appears in several clauses we include it several times).}
\end{question}

\end{document}

