\documentclass[12pt]{article}
\usepackage{fullpage-old} \usepackage{fancyhdr}
\usepackage{amsmath}    \usepackage{amsfonts}   \usepackage{amssymb}
\usepackage{graphics}   \usepackage{epsfig}     \usepackage{wrapfig}
\usepackage{enumitem}
\usepackage{alltt}

\lhead{} \cfoot[]{Page \thepage{}}%{ of 1}
\pagestyle{fancy} \renewcommand{\headrulewidth}{0pt}
\fancypagestyle{plain}{ \renewcommand{\headrulewidth}{0pt} }
\parskip 1ex
\parindent 0mm

\newcommand*{\ii}[1]{\textit{\it #1\/}}
\def\mi{\mathit}
\def\ttt{\texttt}
\def\ss{\hspace{1pt}}

% Logical operators
\def\andl{\wedge}
\def\orl{\vee}
\def\xorl{\oplus}
\def\notl{\neg}

\newcommand{\sub}[2]{#1_{#2}}

\begin{document}

%{\flushright Name: \rule{15em}{0.25pt} \par} 
\vspace{-2ex}
{\center \Large FLAC Project --- Using SAT to Solve Sudoku\par}
\vspace{2ex}

%\begin{wrapfigure}{r}{3.3in}
%\vspace{-3ex}
%\includegraphics[scale=1.2]{hw2-fig.pdf}
%\end{wrapfigure}

Although SAT is an NP-complete problem in general, certain kinds of large SAT
instances can be solved in a reasonable amount of time.  In this project, you
will use a SAT solver to solve Sudoku puzzles.

\hspace{-0.5em}\begin{tabular}{p{0.5\textwidth}p{0.5\textwidth}}
Most existing SAT solvers require the input formula to be in Conjunctive Normal Form
(CNF).  The most commonly used input format is the DIMACS format, whose structure is as shown at the right:
&
\vspace{-0.75cm}
\begin{center}
\fbox{\parbox{2.5in}{
\ttt{p cnf \ii{NumVars} \ii{NumClauses} \\
\(\sub{Clause}{1}\) \\
\(\sub{Clause}{2}\) \\
\(\vdots\) \\
\(\sub{Clause}{n}\) 
}}}
\end{center}
\end{tabular}

\hspace{-0.5em}\begin{tabular}{p{0.5\textwidth}p{0.5\textwidth}}
The variables are assumed to be numbered from 1 to $\ii{NumVars}$.  The $i^{\rm th}$ variable
is represented by the positive integer $i$; the negation of this variable is
represented by the negative integer $-i$.  A clause is represented by listing
the literals in the clause, separated by spaces, followed by a zero
(``\ttt{0}'').  For example, the below CNF formula
is represented in DIMACS as shown at the right.
&
\begin{center}
\fbox{\parbox{2.5in}{
\ttt{%
p cnf 4 5 \\
1 0 \\
2 -3 0 \\
-4 -1 0 \\
-1 -2 3 4 0 \\
-2 4 0
}}}
\end{center}
\end{tabular}
$$x_1 \andl (x_2 \orl \notl x_3) \andl (\notl x_4 \orl \notl x_1) 
\andl (\notl x_1 \orl \notl x_2 \orl x_3 \orl x_4) \andl (\notl x_2 \orl x_4)$$

For more information about DIMACS, see:
$$\verb+http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps+$$

For this assignment we will use the MiniSAT solver, which was the fastest SAT
solver in the SAT Competition in 2005 and 2006.  You can download and build
MiniSAT on the Andrew machines (\ttt{unix.andrew.cmu.edu} via ssh or PuTTY) as follows:

\begin{center}
\fbox{\parbox{4.5in}{
\ttt{%
wget http://minisat.se/downloads/minisat2-070721.zip \\
unzip minisat2-070721.zip \\
cd minisat/core \\
make
}}}
\end{center}

You can run MiniSat by the following command:
$$\verb+~+\ttt{/minisat/core/minisat \ii{InputFile} \ii{OutputFile}}$$
If the input formula is unsatisfiable, then MiniSat writes ``\ttt{UNSAT}'' to the output file.
If the formula is satisfiable, then it writes ``\ttt{SAT}'' and a satisfying assignment.

\textbf{Exercise:} Download \verb+http://www.cs.cmu.edu/~emc/flac09/sample-cnfs.zip+
and run MiniSat on these files.

\textbf{Sudoku.} Sudoku is played on an  $n \!\times\! n$ board, where $n$ is a perfect square.
Some cells are prefilled with numbers from 1 to $n$; the rest are blank.  The board is subdivided
into $\sqrt{n} \times \sqrt{n}$ blocks.  The goal is to fill each cell with a number in such a way that each number from 1 to $n$ occurs exactly once in each row, each column, and each block.  The prefilled squares are such that there is a unique solution.

For this assignment, you will write a program which does the following: (1) read a Sudoku puzzle from
an input file, (2) encode the Sudoku puzzle as a CNF formula in DIMACS format, (3)
use MiniSat to find a satisfying assignment to the CNF formula, (4) read the satisfying
assignment produced by MiniSat to generate the solution to the input Sukodu problem.
The input and output formats for Sudoku puzzles will be as follows (where 0
indicates that a square is empty):

\begin{center}
\begin{minipage}{3.5in}
\begin{alltt}
{\Large{Sample Input}}     {\Large{Sample Output}}
0 6 0 1 0 4 0 5 0     9 6 3 1 7 4 2 5 8 
0 0 8 3 0 5 6 0 0     1 7 8 3 2 5 6 4 9 
2 0 0 0 0 0 0 0 1     2 5 4 6 8 9 7 3 1 
8 0 0 4 0 7 0 0 6     8 2 1 4 3 7 5 9 6 
0 0 6 0 0 0 3 0 0     4 9 6 8 5 2 3 1 7 
7 0 0 9 0 1 0 0 4     7 3 5 9 6 1 8 2 4 
5 0 0 0 0 0 0 0 2     5 8 9 7 1 3 4 6 2 
0 0 7 2 0 6 9 0 0     3 1 7 2 4 6 9 8 5 
0 4 0 5 0 8 0 7 0     6 4 2 5 9 8 1 7 3 
\end{alltt}
\end{minipage}
\end{center}

Due the limited time you have, we recommend using the naive encoding with $n^3$ boolean variables and $O(n^4)$ clauses.  Let the boolean variable $x_{r,c,d}$ be true iff the number $d$ is in the cell at row $r$, column $c$.
Encode the following constraints, along with the prefilled cells:
\\- Exactly one number appears in each cell.
\\- Each number appears exactly once in each row.
\\- Each number appears exactly once in each column.
\\- Each number appears exactly once in each block.
\\Hint: Encode ``exactly one'' as ``at least one and at most one''.  See slides for more details.

Your solver will
take five command-line arguments, as follows:
$$\ttt{./solver \ii{InputPuzzle} \ii{OutputSoln} \ii{MiniSatExec} \ii{TempToSat} \ii{TempFromSat}}$$
where \ii{MiniSatExec} is the filename of the MiniSAT executable (e.g., 
``\verb+~/minisat/core/minisat+''), 
\ii{TempToSat} is the name of the temporary DIMACS file that your solver will produce,
and \ii{TempFromSat} is the solution that MiniSAT will generate.

We suggest writing your solver in C/C++ (compiled by GCC) or Python 2.5.  Other
possible languages include Java 1.5 (J2SE 5.0), Ruby 1.8.6, and OCaml 3.08.  If
you would like to use another language, please email the TAs to see if it
would be available on the test machine.  

Benchmarks and a sample program skeleton are at
\verb+www.cs.cmu.edu/~emc/flac09/bench.zip+ and \ttt{skel.py}.  
The output of your program on the benchmark inputs must match the provided
benchmark solutions exactly, except for possible minor differences in
whitespace (we will compare with \ttt{diff -Bbs}).

\end{document}
