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

\textbf{Programmatically Generating the PL sentence of a Sudoku in CNF   (Part 1 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~1.
\vfill
\textbf{Grading Rubric for Part 1:}
\begin{large}
\begin{center}
\begin{tabular}{lrc}
Dessert problem CNF file is properly formatted & 3& \\
MiniSAT gives correct solution when run on the dessert CNF file & 3& \\
Code is clear & 2& \\
Code is commented & 1& \\
Program generates the correct output & 6 & \\
\hline
Total:    & 15
\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 I}
\end{center}

\textbf{Problem~A:}\\
Consider the following dessert problem:
\begin{quote}
There are four choices of desserts: ice cream, fruit bowl, cake, pie.
Exactly one dessert must be selected (i.e., one and only one).
\end{quote}
\begin{eqnarray}
& & (iceCream\lor fruitBowl \lor cake \lor pie) \nonumber\\
&\land &(\neg iceCream \lor \neg fruitBowl) \nonumber\\
&\land &(\neg iceCream \lor \neg cake) \nonumber\\
&\land &(\neg iceCream \lor \neg pie) \nonumber\\
&\land &(\neg fruitBowl \lor \neg cake) \nonumber\\
&\land &(\neg fruitBowl \lor \neg pie) \nonumber\\
&\land &(\neg cake \lor \neg pie) \nonumber\
\end{eqnarray}
Manually write a DIMACS file (\textbf{dessert.cnf}) of the CNF sentence that model the
desserts problem described above.
\begin{itemize}
\item
Add a comment line to the file to
describe your variables.
\item
Make sure you include the problem line.
\item
Run
MiniSAT on the file that you wrote, store the MiniSAT results with the
solution in an output file (\textbf{results.txt}).
\end{itemize}

\textbf{Problem~B:}\\
Write a program (\textbf{GenerateSudoku.java}) to generate the first
set of clauses describing the Sudoku rules(Expression~(1)). Use the pseudocode shown in Algorithm~\ref{algo:printCNF} to help structure your program. Notice the correspondence between the loops and the iterated conjunction/disjunction operators. The code should produce output resembling Figure~\ref{fig:output}. Comment/problem lines are  {\em not} required at this point. The output does {\em not} yet need to be run on MiniSAT.

\vspace{\baselineskip}
\begin{minipage}{.45\textwidth}
\begin{algorithm}[H]
\DontPrintSemicolon
\SetAlgoLined
\SetAlgoVlined
\ForEach{$i \in [1 \dots 9]$}
{
\ForEach{$n \in [1 \dots 9]$}
{
\ForEach{$j \in [1 \dots 9]$}
{
\textbf{print} `` ''$+i+j+n$
}
\textbf{print} `` 0\textbackslash n''
}
}
\caption{Loop structure for printing clauses in DIMACS CNF format. Note: the `+' symbol represents a string concatenation operator.}
\label{algo:printCNF}
\end{algorithm}


\end{minipage}%
\hfill
\begin{minipage}{.45\textwidth}

\begin{verbatim}
111 121 131 141 151 161 171 181 191 0
112 122 132 142 152 162 172 182 192 0
113 123 133 143 153 163 173 183 193 0
114 124 134 144 154 164 174 184 194 0
115 125 135 145 155 165 175 185 195 0
116 126 136 146 156 166 176 186 196 0
117 127 137 147 157 167 177 187 197 0
118 128 138 148 158 168 178 188 198 0
119 129 139 149 159 169 179 189 199 0
211 221 231 241 251 261 271 281 291 0
212 222 232 242 252 262 272 282 292 0
213 223 233 243 253 263 273 283 293 0
\end{verbatim}
\vdots
\captionof{figure}{A sample of the expected output.}
\label{fig:output}

\end{minipage}

\clearpage

\textbf{Files to Submit to Handin:} \\
\begin{itemize}
\item The dessert problem CNF file (\textbf{dessert.cnf})
\item The MiniSAT results file for the dessert problem (\textbf{results.txt})
\item Your code (\textbf{GenerateSudoku.java})
\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}

