\newcommand{\ig}[1]{}

% For the Exam Version:
% \documentclass[10pt]{exam}
\documentclass[10pt,letterpaper]{myexam}
\usepackage[letterpaper]{geometry}
\usepackage{epsfig}
\usepackage{url}
\usepackage{amsmath,amssymb}
\usepackage{caption}
\usepackage[plain,linesnumbered]{algorithm2e} %algo2e for compatibility

\class{CSE 235H}         %Class Name
\test{SAT Homework 06}          %Test Name
\semester{Spring 2023}  %Semester

\setlength{\parindent}{0pt} %No indentation of paragraphs
\newcommand{\comment}[1]{}  %For large section of comments

% exam class Optional commands
% \bracketedpoints
\boxedpoints
\addpoints          %Add up points across entire document

% Page Style
\pagestyle{headandfoot}

\firstpageheader{{\bf\Large \class}}
{{\bf\Large \test}}
{{\bf\Large \semester}}
\runningheader{\class}{\test}{\semester}
\runningheadrule %horizontal rule on page 2+

\firstpagefooter{}{Page \thepage\ of \numpages}{}
\runningfooter{}{Page \thepage\ of \numpages}{}

\begin{document}
\textbf{Due: Monday, March 27, 2023} \hfill Written by Daniel Geschwender
\line(1,0){430}\\

\textbf{Programmatically Generating the PL sentence of a Sudoku in CNF   (Part 3 of 3):}\\
The goal of this homework is to write a simple program to generate
the text file, in the DIMACS CNF `format,' of a Sudoku instance.
The homework is broken
into three parts as follows:
\begin{itemize}

\item {\it Part 1}: Manually write a simple CNF file in the DIMACS
format; solve with MiniSAT; and write code to generate the first set
of clauses that model a Sudoku puzzle.

\item {\it Part 2}: Write code to generate a CNF file expressing all
the rules of an empty Sudoku board and solve with MiniSAT. Your program
must produce all of the DIMACS comments and the parameter line. Copying 
the output of your program and manually entering the DIMACS comments and 
the parameter line is considered modifying results and will not be accepted.

\item {\it Part 3}: Write code to parse a string representing a
partially filled instance of Sudoku. Add the corresponding clauses
to the CNF file and solve with MiniSAT.
\end{itemize}
In this homework, you have to do only Part~3.
\vfill
\textbf{Grading Rubric for Part 3:}
\begin{large}
\begin{center}
\begin{tabular}{|lr|}
\hline
{\bf To Do} & {\bf Points} \\ \hline
Problem A: Code is clear & 2 \\ \hline
Problem A: Code is commented & 1 \\ \hline
Problem A: Program generates the correct clauses & 6  \\ \hline
Problem A: \#variables and \#clauses counts are correct & (1 bonus)  \\ \hline
Problem B: CNF files are properly formatted DIMACS CNF & 3  \\ \hline
Problem B: MiniSAT successfully runs on all three CNF files  & 3  \\ \hline
\hline\hline
Total:    & 15 \\
\hline
\end{tabular}
\end{center}
\end{large}
\vfill

\textbf{General Instructions:}
\begin{itemize}

\item The program must be written in Java and compile and run on
Webgrader (\url{cse.unl.edu/~cse235h/grade/}).

\item Your program must use standard input (stdin)
and standard output (stdout).

\item The model should follow the Sudoku CNF formulation from the
textbook (see page 36) and reproduced below.

\item The generated output should conform to the DIMACS
CNF file specifications described below.

\item Submit your code and all accompanying files
via handin. Please submit a hard copy of all files (including this page). All submitted files must match
the filenames specified in the assignment. Webgrader will use the
files submitted through handin and requires exact filenames.

\item This homework must be completed individually.  \LaTeX~bonus and partner policy do {\em not\/} apply.

\end{itemize}

\clearpage


\textbf{The Sudoku CNF Formulation:}\\
We will adopt the following formulation of the Sudoku problem to generate the CNF file:
\begin{itemize}

\item
The proposition $p(i,j,n)$ indicates that the cell in row $i$ and
column $j$ is given value $n$. In the CNF file, represent $p(i,j,n)$
by $ijn$. (e.g., $\neg p(3,8,7)$ corresponds to -387 in the CNF file)

\item
Every row contains every number:
\begin{equation}
\bigwedge\limits_{i=1}^{9} \bigwedge\limits_{n=1}^{9} \bigvee\limits_{j=1}^{9} p(i,j,n)
\end{equation}
\item
Every column contains every number:
\begin{equation}
\bigwedge\limits_{j=1}^{9} \bigwedge\limits_{n=1}^{9} \bigvee\limits_{i=1}^{9} p(i,j,n)
\end{equation}
\item
Every 3x3 block contains every number:
\begin{equation}
\bigwedge\limits_{r=0}^{2} \bigwedge\limits_{s=0}^{2} \bigwedge\limits_{n=1}^{9} \bigvee\limits_{i=1}^{3} \bigvee\limits_{j=1}^{3} p(3r+i,3s+j,n)
\end{equation}
\item
No cell contains more than one number:
\begin{equation}
\bigwedge\limits_{i=1}^{9} \bigwedge\limits_{j=1}^{9} \bigwedge\limits_{n=1}^{8}  \bigwedge\limits_{m=n+1}^{9} (\neg p(i,j,n) \vee \neg p(i,j,m))
\end{equation}
\end{itemize}

\textbf{DIMACS CNF Format Specification:}
\begin{itemize}
\item
Comment lines begin with the character `c'.

\item
A problem line must be included before any clauses. The problem line
uses the following format: {\tt p cnf \textless\# variables\textgreater ~\textless\# clauses\textgreater}.

\item
Each clause is given by a line of non-null numbers, separated by
spaces, and ending with a `0'. The numbers correspond to variables. A
negative number represents a negated variable in the clause.
\end{itemize}

\textbf{Note on MiniSAT Variables:}\\ Because of the way the variables
are specified in our Sudoku model, there are gaps in the numbering of
the variables. MiniSAT will see that the highest variable is 999 and
will assume that there are 999 variables.  This is a `feature' of
MiniSAT.  The solution generated by MiniSAT will include all the
variables in 1$\ldots$999. The additional variables (1$\ldots$110,
120, 130, etc.) should simply be ignored.

\clearpage

\begin{center}
\large\textbf{Tasks for Part 3}
\end{center}

\textbf{Problem~A:}\\ Modify the program you wrote for Part~2 (\textbf{GenerateSudoku.java}) by adding to it the following two functionalities:
\begin{enumerate}
\item
Reading and parsing a Sudoku instance from an input file
\item
Generating clauses corresponding to the filled cells and adding them
to the clauses that model the Sudoku constraints.
\end{enumerate}

Follow the guidelines below:
\begin{itemize}
\item
The input file will consist of a single line of exactly 81
characters. Each character corresponds to a cell of the Sudoku
board. A digit (1--9) indicates that the cell is filled with the given
value. A `.' character indicates the cell is initially empty. The
board is expressed in {\em row-major\/} order (i.e., the first nine
characters correspond to the first row, the second nine characters
correspond to the second row, etc.).  Figure~\ref{fig:input} shows an
example input file (File `example.txt' from
\url{cse.unl.edu/~cse235h/files/SudokuInstances.tar.gz}).\\

\begin{small}
\begin{verbatim}
4.....8.5.3..........7......2.....6.....8.4......1.......6.3.7.5..2.....1.4......
\end{verbatim}
\captionof{figure}{Format of the Sudoku instance input file.}
\label{fig:input}
\end{small}

\item
Each filled cell requires a unit clause representing the assignment of
the given value to the corresponding cell.  Figure~\ref{fig:output}
shows the clauses generated from the example input file.\\

\begin{small}
\begin{minipage}{.45\textwidth}
\begin{verbatim}
114 0
178 0
195 0
223 0
347 0
422 0
486 0
558 0
574 0
651 0
746 0
763 0
787 0
815 0
842 0
911 0
934 0
\end{verbatim}
\captionof{figure}{Expected output after parsing the input file from Figure~\ref{fig:input}.}
\label{fig:output}

\end{minipage}%
\hfill
\begin{minipage}{.45\textwidth}
\begin{verbatim}
c <Description of problem>
p cnf <#variables> <#clauses>
c <Description of clauses>
<Clauses from Expression (1)>
c <Description of clauses>
<Clauses from Expression (2)>
c <Description of clauses>
<Clauses from Expression (3)>
c <Description of clauses>
<Clauses from Expression (4)>
c <Description of clauses>
<Clauses generated from input file>
\end{verbatim}
\captionof{figure}{Structure of Sudoku CNF file.}
\label{fig:format}
\end{minipage}
\end{small}

\item
Your program must read the file from standard input. The sample
GenerateSudoku.java
(\url{cse.unl.edu/~cse235h/files/GenerateSudoku.java}) provides an
example. To read from a file (and write to a file) using
stdin/stdout on the command line, use the input/output redirection
operators ($<$,$>$):
\begin{verbatim}
java GenerateSudoku < example.txt > example.cnf
\end{verbatim}

\item
The complete output from your program should be a properly
formatted CNF file resembling Figure~\ref{fig:format}.

\item
MiniSAT will run
on a file with incorrect counts of \# of variables and \# of clauses
but will report a warning. Having correct counts is worth one~(1)
bonus point.
\end{itemize}


\vspace{\baselineskip}

\textbf{Problem~B:}\\
Execute the following steps:
\begin{enumerate}
\item
Download the provided Sudoku instances
(\url{cse.unl.edu/~cse235h/files/SudokuInstances.tar.gz}). This folder
contains four instances:
\begin{enumerate}
\item
The instance given in Figure~\ref{fig:input}

\item
An easy Sudoku instance

\item
An unsatisfiable
Sudoku instance

\item
The Escargot Sudoku instance, one of the most
difficult Sudoku puzzles (\url{www.sudokuwiki.org/Escargot}).
\end{enumerate}

\item
Use your code to generate CNF files (\textbf{easy.cnf},\textbf{unsat.cnf},\textbf{aiEscargot.cnf}) for each of the last three instances {\em excluding\/} the example.

\item
Run each of the three CNF files through MiniSAT. For each CNF, save
the MiniSAT results files (\textbf{easyResults.txt},\textbf{unsatResults.txt},\textbf{aiEscargotResults.txt}).
\end{enumerate}

\vspace{\baselineskip}

\textbf{Files to Submit to Handin:} \\
\begin{itemize}
\item Your code (\textbf{GenerateSudoku.java})
\item Three generated Sudoku CNF files (\textbf{easy.cnf},\textbf{unsat.cnf},\textbf{aiEscargot.cnf})
\item Three MiniSAT results files (\textbf{easyResults.txt},\textbf{unsatResults.txt},\textbf{aiEscargotResults.txt})
\end{itemize}

\textbf{Running on Webgrader:} \\
After submitting your files on Handin, you can run the Webgrader to
verify your submission. You can access the Webgrader at
\url{cse.unl.edu/~cse235h/grade/}. The Webgrader script will print the
contents of all required files, compile your code (using `javac
-J-Xmx256m GenerateSudoku.java'), run your code (using `java -Xmx256m
GenerateSudoku'), and print the program output.

\end{document}

