\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[plain,linesnumbered]{algorithm2e} %algo2e for compatibility

\class{CSE 235H}         %Class Name
\test{SAT Homework 03}          %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, February 20, 2023} \hfill Written by Daniel Geschwender
\line(1,0){430}\\

\flushleft{\large{\textbf{Name~1}} (Print) \line(1,0){100}}\hfill{\large{\textbf{CSE Login} \line(1,0){100}}}
\flushleft{\large{\textbf{Name~2}} (Print) \line(1,0){100}}\hfill{\large{\textbf{CSE Login} \line(1,0){100}}}



 \vspace{0.5cm}

 \begin{large}

 \begin{center}
 \begin{tabular}{|l|c|r||c|}\hline
 Problem & Page & Points & Score\\ \hline
 A & - & 3 &  \\ \hline
 B & - & 3 &  \\ \hline
 C & - & 4 &  \\ \hline
 \multicolumn{2}{|l|}{Typesetting (bonus)}& 1 & \\ \hline
 \multicolumn{2}{|l|}{Total}& 10 & \\ \hline
 \end{tabular}
 \end{center}
 \end{large}

 \vspace{0.5cm}
 \begin{small}

\begin{instructions} Follow instructions \textit{carefully}, failure to do so may result in points being deducted.
\begin{itemize}

\item
This homework is one of the `honors' component of this course.  It
should not take more than two (2) hours to complete.  If it does,
please let us know.

\item
The homework must be submitted on paper. Homework \textit{neatly}
formatted in \LaTeX will receive a 10 percent bonus. When formatting
in \LaTeX , submit both the .tex and .pdf files via handin, in
addition to the hard copy. You will not receive the bonus points if
you work with a partner (see below).

\item
Clearly label each problem and submit answers \textit{in order}.

\item
Staple this cover page to the front of your assignment for easier grading.

\item
Late submissions will \textit{not\/} be accepted.

\item
When you are asked to prove something, you must give a formal,
rigorous, and complete a proof as possible. Each step in your proof
must contain explanation that would allow us to understand what
theorem/logic you have applied to arrive at that step.

\item
You are to work individually and all work should be your own. Check
partner policy below.

\item
The CSE academic dishonesty policy is in effect (see
\url{http://cse.unl.edu/ugrad/resources/academic_integrity.php}).
\end{itemize}
\end{instructions}

\textbf{Partner Policy} You may work in pairs as long as follow
the guidelines below:
\begin{enumerate}
\item
You must work \textit{all} problems \textit{together}. You may not
simply partition the work between you.

\item
You must use \LaTeX and you may divide the typing duties however you wish.

\item
You may not discuss the problems with other groups or individuals.

\item
Hand in only one hard copy with both authors' names.
\end{enumerate}
 \end{small}


\clearpage


\noindent{\bf Homework set-up:}
\begin{itemize}
\item
Install MiniSAT on your CSE account.

\item
Follow the instructions provided in the recitation slides.

\item
SATLIB benchmarks can be found at
\centerline{
\url{http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html}.}

\item Results from running MiniSAT on a problem instance are output to a file specified by the user:
\centerline{./minisat [options] \textless
 input-file\textgreater ~\textless result-output-file\textgreater}

\item
{\em Alert\/}: Some instances may have extra lines that cannot be parsed by MiniSAT. Delete any line starting with `\%' and all following lines.

\end{itemize}
\vspace{\baselineskip}

\textbf{Problem A:}
\begin{itemize}
\item
Select a {\em satisfiable\/} benchmark instance from the SATLIB website.

\item
 Run the instance through MiniSAT.

\item
Submit the generated output as well as the contents of the
results file.
\end{itemize}
\vspace{\baselineskip}


\textbf{Problem B:}
\begin{itemize}
\item
Select an {\em unsatisfiable\/} benchmark instance from the SATLIB
website.

\item
Run the instance through MiniSAT.

\item
Submit the generated output as well as the contents of the
results file.

\end{itemize}
\vspace{\baselineskip}


\textbf{Problem C:}
\begin{itemize}
\item
Select a benchmark from the SATLIB website.
\item
Read its description page.
\item
Briefly describe, in your own words, what the benchmark is modeling.
\end{itemize}

\end{document}
