pdf

hw1/hw1.tex

@@ -3,8 +3,9 @@
 \usepackage[english]{babel}
 \usepackage{amsthm, amssymb, amsmath, amsfonts, extramarks}
 \usepackage{gen, color}
+\usepackage{graphicx}
 
-\title{Homework Assignment 6}
+\title{\vspace{-2cm}Homework Assignment 6}
 
 \author{Bailey Wickham \& Alex MacLean\\ CSC530}
 
@@ -96,7 +97,6 @@ \section{Propositional Logic and Normal Forms}
 The case for $\phi = \phi_1 \lor \phi_2$ follows similarly.
 
 \item \textbf{Conclusion:} By induction, every interpretation $I$ and $I'$ such that $\emph{pos}(I, \phi) \subseteq \emph{pos}(I', \phi)$, if $I \models \phi$, then $I' \models \phi$.
-
 \end{proof}
 \end{solution}
 
@@ -122,12 +122,17 @@ \section{Propositional Logic and Normal Forms}
 
 \begin{solution}
 	\begin{proof}
-		...
+		If there exists an interpretation $I$, such that $I \models \phi$, then an interpretation $I'$ such that $I' \models \hat{\phi}$ can always be constructed from it. This can be accomplished by setting the literals in $I'$ to there values in $I$ and setting the fresh auxiliary variables generated by the algorithm to the truth values the clauses they represent in $I \models \phi$. This works because the clauses that the auxiliary variables are being substituted into will evaluate to the same truth values as they do in $\phi$ and the implication clauses added to the CNF will all be true because $\top \rightarrow \top \equiv \top$ and $\bot \rightarrow \bot \equiv \top$.
+
+		\item The reverse is also true, if there exists an interpretation $I$, such that $I \models \hat{\phi}$, then an interpretation $I'$ such that $I' \models \phi$ can always be constructed from it. This can be accomplished by simply removing the auxiliary variables from $I$. This new interpretation will always satisfy $\phi$ because if the truth value of the clause is the same as the one assigned to the auxiliary variable then substituting it in will not change anything. Since the auxiliary variable implies the clause it is substituted for the only other possibility is that the auxiliary variable is $\bot$ while the cause evaluates to $\top$. Since the auxiliary variables will only occur in conjunctions and disjunctions substituting $\bot$ for $\top$ in an expression that evaluates to $\top$ cannot possibly cause it to evaluate to $\bot$.
+
+		\item Therefore if $\phi$ is satisfiable then $\hat{\phi}$ is also satisfiable and vice versa so $\hat{\phi}$ is satisfiable if and only if $\phi$ is satisfiable.
 	\end{proof}
 \end{solution}
 
 \end{enumerate}
 
+\pagebreak
 
 \section{SAT solving (20 points)}\label{solving}
 
@@ -162,11 +167,68 @@ \section{SAT solving (20 points)}\label{solving}
 	To produce the abstract trace, create an abstract trace  entry (``Level'') whenever the decision level changes in the detailed trace due to a new decision or backtracking. When filling out the entry template, use the literal names from the detailed trace. For example, the solver will represent the literal $\neg x_1$ as \texttt{-1}. Use GraphViz to visualize the implication graph at a given level. The \texttt{impl-graph.dot} file shows an example of how to specify implication graphs with GraphViz. Use the LaTeX \texttt{\textbackslash includegraphics} command to insert the resulting graph images into your \texttt{hw1.pdf} file.
 
 
+\begin{solution}
+	\begin{itemize}
+\item \textbf{Level} 1
+\begin{itemize}
+	\item \textbf{Decision:} 1
+	\item \textbf{BCP:} 3
+	\item \textbf{Conflict Clause:} NA
+	\item \textbf{Implication Graph:} 
+	\begin{figure}[h!]
+		\begin{center}
+			\includegraphics[scale=0.75]{sat-images/graph1}
+		\end{center}
+	\end{figure}
+\end{itemize}
 
+\pagebreak
 
+\item \textbf{Level} 2
+\begin{itemize}
+	\item \textbf{Decision:} 2
+	\item \textbf{BCP:} -4
+	\item \textbf{Conflict Clause:} 4 -2 -3 learned -3 -2
+	\item \textbf{Implication Graph:}
+	\begin{figure}[h!]
+		\begin{center}
+			\includegraphics[scale=0.75]{sat-images/graph2}
+		\end{center}
+	\end{figure}
+\end{itemize}
+
+\item \textbf{Level} 1
+\begin{itemize}
+	\item \textbf{Decision:} NA
+	\item \textbf{BCP:} -2, 4
+	\item \textbf{Conflict Clause:} -4 2 -1 learned -1
+	\item \textbf{Implication Graph:}
+	\begin{figure}[h!]
+		\begin{center}
+			\includegraphics[scale=0.75]{sat-images/graph3}
+		\end{center}
+	\end{figure}
+\end{itemize}
+
+\item \textbf{Level} 0
+\begin{itemize}
+	\item \textbf{Decision:} NA
+	\item \textbf{BCP:} -1, 3, 4, -2
+	\item \textbf{Conflict Clause:} NA
+	\item \textbf{Implication Graph:} 
+	\begin{figure}[h!]
+		\begin{center}
+			\includegraphics[scale=0.75]{sat-images/graph4}
+		\end{center}
+	\end{figure}
+\end{itemize}
+	\end{itemize}
+\end{solution}
 
 \end{enumerate}
 
+\pagebreak
+
 \section{Graph Coloring with SAT (40 points)}\label{coloring}
 
 A graph is \emph{k-colorable} if there is an assignment of $k$ colors to its vertices such that no two adjacent vertices have the same color.  Deciding if such a coloring exists is a classic NP-complete problem with many practical applications, such as register allocation in compilers.  In this problem, you will develop a CNF encoding for graph coloring and apply them to graphs from various application domains, including course scheduling, N-queens puzzles, and register allocation for real code.
@@ -248,6 +310,7 @@ \section{Graph Coloring with SAT (40 points)}\label{coloring}
 
 \end{enumerate}
 
+
 \section{Optimal Graph Coloring with Variations on SAT (10 points)}\label{varsat}
 
 

hw1/sat-images/graph1.dot

@@ -3,6 +3,9 @@ digraph ImplicationGraph {
   rankdir=LR;
   margin=0;
 
+  node [color=blue, fontcolor=blue]
+  edge [color=blue, fontcolor=blue]
+
   n1 [label="1@1"];
   n2 [label="3@1"];
 

hw1/sat-images/graph2.dot

@@ -3,6 +3,9 @@ digraph ImplicationGraph {
   rankdir=LR;
   margin=0;
 
+  node [color=blue, fontcolor=blue]
+  edge [color=blue, fontcolor=blue]
+
   n1 [label="1@1"];
   n2 [label="3@1"];
   n3 [label="2@2"];

hw1/sat-images/graph3.dot

@@ -3,6 +3,9 @@ digraph ImplicationGraph {
   rankdir=LR;
   margin=0;
 
+  node [color=blue, fontcolor=blue]
+  edge [color=blue, fontcolor=blue]
+
   n1 [label="1@1"];
   n2 [label="3@1"];
   n3 [label="-2@1"];

hw1/sat-images/graph4.dot

@@ -3,6 +3,9 @@ digraph ImplicationGraph {
   rankdir=LR;
   margin=0;
 
+  node [color=blue, fontcolor=blue]
+  edge [color=blue, fontcolor=blue]
+
   n1 [label="-1@0"];
   n2 [label="-2@0"];
   n3 [label="3@0"];