\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 05}          %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 20, 2023} \hfill Written by Daniel Geschwender
\line(1,0){430}\\

\textbf{Programmatically Generating the PL sentence of a Sudoku in CNF   (Part 2 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~2.
\vfill
\textbf{Grading Rubric for Part 2:}
\begin{large}
\begin{center}
\begin{tabular}{|lr|}
\hline
{\bf To Do} & {\bf Points} \\ \hline
Problem A: Code is clear and commented & 2 \\ \hline
Problem A: Code is commented & 1 \\ \hline
Problem A: Program generates the correct clauses & 6  \\ \hline
Problem A: Output is properly formatted DIMACS CNF file & 3  \\ \hline
Problem B: MiniSAT finds a valid solution  & 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 2}
\end{center}

\textbf{Problem~A:}\\ Modify your program from Part I (\textbf{GenerateSudoku.java}) to generate a
complete CNF file to model an empty Sudoku grid. You will need to
write loops to generate the remaining sets of Sudoku clauses (i.e.,
Expressions~(2), (3), and~(4)). Use loops similar to those used to
generate the first set of clauses (i.e., Expression~(1)). Pay
attention to differences in the indices, negations, and clause
termination location. The code should produce output resembling
Figure~\ref{fig:clauses2}, Figure~\ref{fig:clauses3}, and
Figure~\ref{fig:clauses4}.\\

Your code should produce output that is properly formatted in the
DIMACS CNF format. It should include a comment header briefly
describing the problem, a problem line, and comment lines indicating
each of the four sets of clauses. Figure~\ref{fig:cnfStructure} shows
required structure for the CNF file.

\vspace{\baselineskip}
\begin{minipage}{.45\textwidth}
\begin{verbatim}
111 211 311 411 511 611 711 811 911 0
112 212 312 412 512 612 712 812 912 0
113 213 313 413 513 613 713 813 913 0
114 214 314 414 514 614 714 814 914 0
115 215 315 415 515 615 715 815 915 0
116 216 316 416 516 616 716 816 916 0
117 217 317 417 517 617 717 817 917 0
118 218 318 418 518 618 718 818 918 0
119 219 319 419 519 619 719 819 919 0
121 221 321 421 521 621 721 821 921 0
122 222 322 422 522 622 722 822 922 0
123 223 323 423 523 623 723 823 923 0
\end{verbatim}
\centerline{\vdots}
\captionof{figure}{Expected output for Expression~(2).}
\label{fig:clauses2}

\end{minipage}%
\hfill
\begin{minipage}{.45\textwidth}
\begin{verbatim}
111 121 131 211 221 231 311 321 331 0
112 122 132 212 222 232 312 322 332 0
113 123 133 213 223 233 313 323 333 0
114 124 134 214 224 234 314 324 334 0
115 125 135 215 225 235 315 325 335 0
116 126 136 216 226 236 316 326 336 0
117 127 137 217 227 237 317 327 337 0
118 128 138 218 228 238 318 328 338 0
119 129 139 219 229 239 319 329 339 0
141 151 161 241 251 261 341 351 361 0
142 152 162 242 252 262 342 352 362 0
143 153 163 243 253 263 343 353 363 0
\end{verbatim}
\centerline{\vdots}
\captionof{figure}{Expected output for Expression~(3).}
\label{fig:clauses3}

\end{minipage}

\vspace{\baselineskip}

\begin{minipage}{.45\textwidth}
\begin{verbatim}
-111 -112 0
-111 -113 0
-111 -114 0
-111 -115 0
-111 -116 0
-111 -117 0
-111 -118 0
-111 -119 0
-112 -113 0
-112 -114 0
-112 -115 0
-112 -116 0
\end{verbatim}
~~~~~~~~\vdots
\captionof{figure}{Expected output for Expression~(4).}
\label{fig:clauses4}
\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)>
\end{verbatim}
\captionof{figure}{Structure of Sudoku CNF file.}
\label{fig:cnfStructure}
\end{minipage}

\vspace{\baselineskip}

\textbf{Problem~B:}\\
Execute the following steps:
\begin{enumerate}
\item Use your code to generate a CNF file (\textbf{emptySudoku.cnf}). To write
to a file from stdout, you can use the output redirection operator ($>$):
{\tt java GenerateSudoku > emptySudoku.cnf}

\item
Take your generated Sudoku CNF file and solve it using MiniSAT. (An
`empty' Sudoku board can be solved by MiniSAT.)

\item
Obtain the results file from MiniSAT. (\textbf{emptySudokuResults.txt})

\item
Submit your file and check Webgrader. The Webgrader script will verify
the correctness of your solution and display the filled Sudoku board.
\end{enumerate}


\vspace{\baselineskip}

\textbf{Files to Submit to Handin:} \\
\begin{itemize}
\item Your code (\textbf{GenerateSudoku.java})
\item Your generated Sudoku CNF file (\textbf{emptySudoku.cnf})
\item The MiniSAT results file (\textbf{emptySudokuResults.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}

