% -*- compile-command: "pdflatex --enable-write18 hw.11.tex" -*-
\documentclass[11pt]{tufte-handout}
\usepackage{times,graphicx,epstopdf,fancyhdr,amsfonts,amsthm,amsmath,url,xspace}
\usepackage[linesnumbered,ruled]{algorithm2e}
% \usepackage[left=.75in,top=.75in,right=.75in,bottom=.75in]{geometry}

\usepackage{qrcode, enumitem}

\usepackage{pgf}
\usepackage[outputdir=diagrams, extension=pgf, backend=pgf, input]{diagrams-latex}

\pagestyle{fancy}

\newcommand{\ie}{\emph{i.e.}\xspace}
\newcommand{\term}[1]{\emph{#1}}

\newtheorem{claim}{Claim}
\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{observation}{Observation}

\theoremstyle{definition}
\newtheorem{question}{Question}

\begin{document}

\lhead{CSCI 280: Algorithms -- Spring 2016}
\chead{}
\rhead{Brent Yorgey}
\lfoot{Homework 11}
\cfoot{\thepage}
\rfoot{Due: 4:00pm, Friday, April 29}
\renewcommand{\headrulewidth}{0.4pt}
\renewcommand{\headwidth}{\textwidth}
\renewcommand{\footrulewidth}{0.4pt}

We have spent some time exploring some of the theoretical aspects of
NP-completeness, and a sampling of NP-complete problems. On this
assignment, you will explore the more practical side of
NP-completeness: what can you do when you really, actually need to
solve an NP-complete problem?

\section{What to turn in}

You should turn in two files:
\begin{itemize}
\item \verb|certificate.txt|, described in the section ``Coloring your
  graph'' below.
\item Whatever program(s) you used to help you generate
  \verb|certificate.txt|.
\end{itemize}

\section{Background: graph coloring}

Suppose we have an undirected graph $G = (V,E)$. Given some set of
colors $C$, a \emph{coloring} of $G$ is a function $\chi : V \to C$,
that is, an assignment of a color to each vertex.  A \emph{valid}
coloring is one for which no two adjacent vertices have the same
color; that is, $\chi(u) \neq \chi(v)$ for every $(u,v) \in E$.

For example, Figure~\ref{fig:example-four-coloring} shows a valid
coloring of a graph with $7$ vertices.  You can check that no two
adjacent vertices have the same color.

\begin{marginfigure}
\begin{diagram}[width=100]
  import GraphColoring

  dia = drawGraph exampleGraph exampleColoring False
\end{diagram}
\caption{A valid 4-coloring of a graph with 7
  vertices} \label{fig:example-four-coloring}
\end{marginfigure}

A \emph{$k$-coloring} is a valid coloring of a graph which uses at
most $k$ colors.  The example shown in
Figure~\ref{fig:example-four-coloring} is a $4$-coloring (and also a
$5$-coloring, and a $26$-coloring, and so on). A graph $G$ is called
\emph{$k$-colorable} if it has a valid $k$-coloring.  Finally, the
\emph{chromatic number} of a graph $G$ is the \emph{smallest} $k$ for
which $G$ is $k$-colorable.  The graph shown in
Figure~\ref{fig:example-four-coloring} actually has a chromatic number
of $3$---can you find a valid $3$-coloring?

Given a graph $G$ and a number $k$, the \textsc{Graph Coloring}
problem asks: is the graph $k$-colorable?  There are $k^n$ possible
colorings to check, so a brute force algorithm is definitely not going
to work.  In fact, this problem is NP-complete for
$k \geq 3$,\marginnote{For $k=2$, however, it can be solved
  efficiently---can you figure out how?} which can be proved by
reduction from \textsc{3-SAT}.  The proof has a similar flavor to the
reduction
$\text{\textsc{3-SAT}} \leq_P \text{\textsc{INDEPENDENT SET}}$ we did
in class: given a \textsc{3-SAT} instance, one builds a particular
graph out of ``gadgets'' which encodes the constraints given by the
3-SAT clauses, in such a way that a 3-coloring of the graph
corresponds to a valid truth assignment.  For details of the proof,
see, for example,
\url{https://www.cs.cmu.edu/~ckingsf/bioinfo-lectures/sat.pdf}.

\section{Defining your graph}

For this assignment you will work with your own personal graph.  Here
is how to determine your graph:
\begin{enumerate}
\item Pick a specific string to represent your name.  For example,
  mine might be \verb|"Brent Yorgey"| or \verb|"Brent A. Yorgey"| or
  \verb|"Dr. Yorgey"|---it does not matter what string you pick, as
  long as you specify it exactly.
\item Find the MD5 hash of your string, which should yield a 16-byte
  hash value.  For example, in Python, given your chosen string stored
  in a variable \verb|name|, one can write
\begin{verbatim}
import md5

hash_bytes = md5.new(name).digest()
\end{verbatim}
to compute the MD5 hash.  In Java, one can write something like
\begin{verbatim}
import java.security.*;

byte[] bytesOfMessage = name.getBytes("UTF-8");

MessageDigest md = MessageDigest.getInstance("MD5");
byte[] hash_bytes = md.digest(bytesOfMessage);
\end{verbatim}

\item The resulting 16-byte hash can of course be thought of as a
  sequence of 128 bits.  We can use a sequence of bits to encode an
  undirected, unweighted graph as follows. Each bit records the
  presence or absence of a single edge: a 1 bit means the edge is
  present, and 0 means it is absent.  We assume that the vertices of
  the graph are numbered from $0$ to $n-1$.
  \begin{itemize}
  \item The index-0 bit, that is, the \emph{least significant} or
    \emph{last} bit, corresponds to the edge $(1,0)$.
  \item The bit at index 1, i.e. the second-to-last bit, corresponds
    to $(2,0)$, and the bit at index 2 corresponds to $(2,1)$.
  \item The next three bits correspond to $(3,0)$, $(3,1)$, and
    $(3,2)$.
  \end{itemize}
  The general pattern is that the first
  $1 + 2 + 3 + \dots + k = k(k+1)/2$ bits (counting from the
  \emph{end} of the bit string) correspond to all the possible edges
  involving vertices numbered $0$ through $k$; the next $k+1$ bits
  after that correspond to edges from vertex $k+1$ to all the smaller
  vertices, starting with vertex $0$.

  For example, we need $(4\cdot 5)/2 = 10$ bits to encode a graph with
  $5$ vertices; the graph shown in Figure~\ref{fig:five} is encoded by
  $0010001101$. The last bit (a $1$) indicates that there is an edge from
  vertex $1$ to vertex $0$; the second-to-last bit (a $0$) indicates
  that there is no edge from $2$ to $0$; and so on.

  \begin{marginfigure}[-0.5in]
    \begin{diagram}[width=100]
      import GraphColoring
      dia = drawGraph (bitsGraph 5 (0x8d :: Int)) allBlack True # frame 0.1
    \end{diagram}
    \caption{The graph encoded by $0010001101$.} \label{fig:five}
  \end{marginfigure}

  In general, to determine whether vertices $i$ and $j$ are connected,
  first sort them so $i > j$, and then look at the bit with index
  $i(i-1)/2 + j$.

  Since $16(16-1)/2 = 120 < 128$ (but $17(17-1)/2 = 136 > 128$), your
  128-bit hash value defines a particular undirected graph with $16$
  nodes. The final 8 bits of your hash value are not used.

  Note that there is an annoying mismatch between the way we are
  numbering the bits (starting from the right) and the way the
  individual bytes in an array or string are numbered (starting
  from the left).  To make things easier on yourself, after computing
  the MD5 hash you may want to reverse the list/array of bytes, so
  that the last byte will be at index 0, the second-to-last at index
  1, and so on.  Then bit $j$ will be the $(j \bmod 8)$th bit in the
  $\lfloor j / 8 \rfloor$th byte.  Alternately, you can just turn your
  list of bytes into a list of bits, and then reverse the entire list.

  As an example, my graph (generated from the string %
  \verb|Brent Yorgey|) is shown in Figure~\ref{fig:brent}.
  \begin{figure}
    \centering
    \begin{diagram}[width=200]
      import GraphColoring
      dia = drawGraph (mkGraph "Brent Yorgey") allBlack True # frame 0.1
    \end{diagram}
    \caption{The graph generated by ``Brent Yorgey'', corresponding
      to the hash ad 02 2f e3 f6 88 00 b6 f1 db 37 a8 f8 e1 4b 10}
    \label{fig:brent}
  \end{figure}
\end{enumerate}
For example, the final $10$ in the hexadecimal representation of the
hash corresponds to the bits $00010000$, which correspond to edges in
the graph as follows: \medskip

\begin{tabular}{cccccccc}
  0 &0 &0&1&0&0&0&0 \\
  (4,1) & (4,0)& (3,2)&(3,1)&(3,0)&(2,1)& (2,0) & (1,0)
\end{tabular} \medskip

As you can see, there is indeed an edge between vertices $1$ and $3$
in the graph, and no edges between any of the other indicated pairs of
vertices.
To make sure you understand how a hash value determines a graph, you
can spot-check other edges for yourself: pick a pair of vertices and
check that the corresponding bit in the hash value is what you expect.

\section{Coloring your graph}

The question you now need to answer is: what is the chromatic number
of your graph?  Most randomly chosen graphs with $16$ vertices have
chromatic number $5$, so that wouldn't be a bad guess, but of course
it could in theory be as small as $1$ (if your graph has no edges) or
as large as $16$ (if your graph includes every possible edge).
Empirically, it seems likely that at least one of you will have a
graph with chromatic number $6$.  In any case, guessing the right
chromatic number would not be enough anyway: in addition to
determining the chromatic number $k$, you should construct an actual
valid $k$-coloring, which can serve as an efficiently-checkable
\emph{certificate} that your graph is indeed
$k$-colorable.\marginnote{On the other hand, coming up with an
  efficiently-checkable certificate proving that your graph is
  \emph{not} $(k-1)$-colorable is quite a different story, and is
  likely to be impossible, though no one knows for sure.}

Ultimately, you should turn in a file named \verb|certificate.txt|
containing three lines:
\begin{enumerate}
\item The first line should contain the exact string you chose to
  generate your graph.
\item The second line should contain a single number, the chromatic
  number $k$ of your graph.
\item The third line should contain 16 characters specifying a valid
  coloring for the vertices $0 \dots 15$ in your graph.  It does not
  matter which characters you use, but there should be exactly $k$
  different characters, one standing for each color.
\end{enumerate}

For example, my \verb|certificate.txt| looks like this:
\begin{verbatim}
Brent Yorgey
5
eeedcddbabaccebd
\end{verbatim}

You can check that assigning the same color to the first three
vertices, a different color to the next vertex, and so on, is indeed a
valid 5-coloring of the graph generated by the string
\verb|Brent Yorgey|, as shown in Figure~\ref{fig:brent-coloring}.
\begin{figure}
  \centering
  \begin{diagram}[width=200]
    import GraphColoring
    dia = drawGraph (mkGraph "Brent Yorgey") (mkColoring "eeedcddbabaccebd") True # frame 0.1
  \end{diagram}
  \caption{A $5$-coloring of the ``Brent Yorgey'' graph}
  \label{fig:brent-coloring}
\end{figure}

At this point you might wonder how you are supposed to come up with a
coloring for your graph.  Even with the relatively small value
$n = 16$, a brute force algorithm might have to check, for example, up
to $5^{16} = 152587890625$ potential $5$-colorings.  One might try a
greedy strategy: for each vertex from $0 \dots n-1$, pick the smallest
color that is unused by any of the previous vertices it is connected
to.  But as you can see if you try it, this does not really work.  For
example, this greedy algorithm on my graph produces the (non-optimal)
$6$-coloring shown in Figure~\ref{fig:brent-greedy}. Notice how vertex
$14$ is given a sixth color (brown), since by the time it is reached,
it has at least one neighbor with each of 5 different colors.

\begin{figure}
  \centering
  \begin{diagram}[width=200]
    import GraphColoring
    brent = mkGraph "Brent Yorgey"
    dia = drawGraph brent (colourize (greedyColoring brent)) True # frame 0.1
  \end{diagram}
  \caption{A non-optimal greedy coloring of the ``Brent Yorgey'' graph}
  \label{fig:brent-greedy}
\end{figure}

In fact, we will use a tried-and-true technique for attacking
computationally hard problems like this: reduce the problem to SAT, and
hand it off to a \emph{SAT solver}, a program specifically designed to
solve SAT instances.  Even though all such programs (that we know of)
take exponential time in the \emph{worst} case, they are astonishingly
efficient in the general case.

\section{Using the Yices SAT solver}

For this assignment, you will use a SAT solver called Yices, available
at \url{http://yices.csl.sri.com/}.  There are many solvers available;
I chose Yices simply because it is freely available on multiple
platforms and easy to get started with.  (If you want to try a
different one for some reason, you are welcome to.)

Download the latest version of Yices (2.4.2 as of this writing) for
your OS and unzip it somewhere.  In the \verb|bin/| folder you should
find several executables, one of which is \verb|yices-sat|.  This is
the SAT solver that comes with Yices. (In fact, Yices is not
\emph{just} a SAT solver, but actually something called an ``SMT
solver'', which is much more general and powerful than a SAT solver; ask me if you
are interested in the details.)

The format expected by \verb|yices-sat| is described at
\url{http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html}. The short
version is that the first line should contain
\begin{verbatim}
p cnf n k
\end{verbatim}
where the text \verb|p cnf| occurs literally, and \verb|n| and
\verb|k| are replaced by the number of variables and the number of
clauses, respectively.  For example, \verb|p cnf 7 20| would denote a
SAT instance with $7$ variables and $20$ clauses.

The next \verb|k| lines should describe the clauses.  Each line
consists of a list of integers, separated by spaces, with an extra $0$
at the end. The integers indicate variables, numbered $1 \dots n$,
with an integer $i$ corresponding to $x_i$ and $-i$ corresponding to
$\overline{x_i}$.  For example, to encode the clause $(x_1 \lor
\overline{x_3} \lor x_7 \lor \overline{x_4})$ one would write
\begin{verbatim}
1 -3 7 -4 0
\end{verbatim}
As a complete example, suppose we have $4$ variables $x_1 \dots x_4$
and the clauses \[ (x_1 \lor x_4), (x_2 \lor \overline{x_3} \lor
\overline{x_4}), (\overline{x_1} \lor x_3 \lor x_4). \] We would
encode this as the file
\begin{verbatim}
p cnf 4 3
1 4 0
2 -3 -4 0
-1 3 4 0
\end{verbatim}
Suppose this was saved in a file called \verb|example.cnf|.  Then we
can give it as input to \verb|yices-sat| just by giving the file name
as an argument at the command line:
\begin{verbatim}
$ yices-sat example.cnf
sat
\end{verbatim}
(Note that \verb|$|
indicates the command prompt, and should not be typed.)  Yices returns
immediately and tells us the clauses are satisfiable.  To see the
actual assignment it came up with, pass it the \verb|-m| option:
\begin{verbatim}
$ yices-sat -m example.cnf
sat
-1 -2 -3 4 0
\end{verbatim}
It tells us that a satisfying assignment consists of setting $x_1$,
$x_2$, and $x_3$ to $F$, and $x_4$ to $T$.

On the other hand, given the input file
\begin{verbatim}
p cnf 2 4
1 2 0
1 -2 0
-1 2 0
-1 -2 0
\end{verbatim}
\verb|yices-sat| prints \verb|unsat|, telling us that the set of
clauses is not satisfiable (as you can easily verify).

\section{Reducing to SAT}

You will need to write a program that reduces $k$-colorability of your
graph to a SAT instance,\marginnote{\emph{Hint:}\quad\qrcode{Use\ n*k\
    Boolean\ variables,\ one\ for\ each\ combination\ of\ vertex\ and\
    color.}} and outputs an appropriate input file for
\verb|yices-sat|.  You can then try each value of $k = 1, 2, \dots$
until you find the smallest one for which the corresponding instance
is satisfiable. (In general one could of course use binary search, but
for such small values of $k$ it is hardly worth the effort.)  Then use
the satisfying assignment generated by Yices to construct a valid
$k$-coloring of your graph.
\end{document}
