\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{CSCE 235H}         %Class Name
\test{SAT Homework 07}          %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, April 3, 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 & - & 6 &  \\ \hline
 B & - & 3 &  \\ \hline
 C & - & 3 &  \\ \hline
 \multicolumn{2}{|l|}{Typesetting (bonus)}& 1 & \\ \hline
 \multicolumn{2}{|l|}{Total}& 12 & \\ \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

\textbf{Problem A:} Briefly describe, in two to four sentences and in
your {\em own\/} words, how each of the following mechanisms operate
within MiniSAT.  Consult the slides, the MiniSAT paper (\url{http://minisat.se/downloads/MiniSat.pdf}), or any other resource, online or from the
scientific literature. {\em Clearly\/} and {\em
  fully\/} cite your sources.  Importantly, your description must
express your own understanding: copy-paste content will not be accepted.
\begin{enumerate}
\item Unit propagation
\item Activity-based variable ordering (VSIDS heuristic)
\item Clause learning
\item Intelligent backtracking (conflict-driven backtracking)
\item Watched literals
\item Restarts
\end{enumerate}
\vspace{\baselineskip}

\textbf{Problem B:} Consider the following CNF formula:
\begin{eqnarray}
& & (\neg x_1 \lor \neg x_4 \lor \neg x_6) \nonumber\\
& \land &(x_2 \lor x_3 \lor x_5) \nonumber\\
& \land & (\neg x_1 \lor x_2 \lor x_6)  \nonumber\\
& \land &(x_4 \lor \neg x_5 \lor \neg x_6)  \nonumber
\end{eqnarray}
Report the following:
\begin{enumerate}
\item Assume the first assignment $x_1=1$ (as a decision).  Report the
  assignment trail (i.e., decision followed by all possible unit
  propagations) and give the implication graph.
\item Consider the second decision assignment $x_2=0$.  Update the
  assignments trail and implication graph.
\end{enumerate}
\vspace{\baselineskip}

\clearpage

\textbf{Problem C:} Using the assignment trail reported in
Figure~\ref{fig:trail1} and implication graph
of Figure~\ref{fig:implication}, answer the following questions. Note
that no CNF formula is provided; the clauses can be inferred from
the implication graph.
\begin{enumerate}
\item What clause causes the conflict?
\item What clause is learned as a result of this conflict?
\item To which assignment do we backtrack to and what new assignment do we make?
\end{enumerate}


\begin{minipage}{.45\textwidth}
\centering
\begin{tabular}{cl}
Decision Level & Assignment \\ \hline
1	& $x_1=0$ \\ \hline
2	& $x_2=1$ \\
	& $x_5=0$ \\ \hline
3	& $x_3=1$ \\
	& $x_4=1$ \\
	& $x_7=1$ \\ \hline
4	& $x_6=0$ \\
	& $x_8=0$ \\
	& $x_9=1$ \\
\end{tabular}
\captionof{figure}{The `trail' of current assignments}
\label{fig:trail1}

\end{minipage}%
\hfill
\begin{minipage}{.45\textwidth}
\centerline{\includegraphics[width=3in]{ImplicationGraph.pdf}}
  \captionof{figure}{An implication graph that has reached a conflict.}
  \label{fig:implication}
\end{minipage}


\end{document}
