diff --git a/hw1/hw1.pdf b/hw1/hw1.pdf index be3dca3..e4b2051 100644 Binary files a/hw1/hw1.pdf and b/hw1/hw1.pdf differ diff --git a/hw1/hw1.tex b/hw1/hw1.tex index a400ad8..88ca907 100644 --- a/hw1/hw1.tex +++ b/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} diff --git a/hw1/sat-images/graph1.dot b/hw1/sat-images/graph1.dot index 65f8864..a5aab7d 100644 --- a/hw1/sat-images/graph1.dot +++ b/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"]; diff --git a/hw1/sat-images/graph1.pdf b/hw1/sat-images/graph1.pdf new file mode 100644 index 0000000..7e32906 Binary files /dev/null and b/hw1/sat-images/graph1.pdf differ diff --git a/hw1/sat-images/graph2.dot b/hw1/sat-images/graph2.dot index b6f89d1..e3eccfe 100644 --- a/hw1/sat-images/graph2.dot +++ b/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"]; diff --git a/hw1/sat-images/graph2.pdf b/hw1/sat-images/graph2.pdf new file mode 100644 index 0000000..8e9c3e6 Binary files /dev/null and b/hw1/sat-images/graph2.pdf differ diff --git a/hw1/sat-images/graph3.dot b/hw1/sat-images/graph3.dot index 6235719..c44298d 100644 --- a/hw1/sat-images/graph3.dot +++ b/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"]; diff --git a/hw1/sat-images/graph3.pdf b/hw1/sat-images/graph3.pdf new file mode 100644 index 0000000..e53f4b3 Binary files /dev/null and b/hw1/sat-images/graph3.pdf differ diff --git a/hw1/sat-images/graph4.dot b/hw1/sat-images/graph4.dot index b2596c4..4fd16d7 100644 --- a/hw1/sat-images/graph4.dot +++ b/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"]; diff --git a/hw1/sat-images/graph4.pdf b/hw1/sat-images/graph4.pdf new file mode 100644 index 0000000..ed5861c Binary files /dev/null and b/hw1/sat-images/graph4.pdf differ