Correctness proofs

1 files changed, 66 insertions, 40 deletions

diff --git a/Practical1/report/algorithm.tex b/Practical1/report/algorithm.tex
index 6a079ea..7ce0fdd 100644
--- a/Practical1/report/algorithm.tex
+++ b/Practical1/report/algorithm.tex
@@ -5,13 +5,17 @@
 \label{sec:algorithm:basic-structure}
 The basic structure of the algorithm is fairly simple. For any graph $G=(V,E)$, we pick a vertex $v\in V$. Either that vertex is in an m.i.s. (and none of its neighbours), or it is not. This gives the recurrence: \refeq[basic-structure]{\ms(G) = \max(1 + \ms(G\ex \iN(v)), \ms(G\ex v)).} The rest of the algorithm will be optimising this basic structure by cleverly choosing $v$ and pruning the search tree.
 
-\begin{lemmaproof}[one-neighbour]{For a graph $G=(V,E)$ and vertex $v\in V$, if $v$ is not in an m.i.s. there is a neighbour $w\in N(v)$ which is in an m.i.s.}
+\begin{thmproof}[base-case]{lemma}{For a graph $G$ with $|G|\leq1$, we have $\ms(G)=|G|$.}
+    For both the cases $|G|=0$ and $|G|=1$, $G$ is an m.i.s. of itself.
+\end{thmproof}
+
+\begin{thmproof}[one-neighbour]{lemma}{For a graph $G=(V,E)$ and vertex $v\in V$, if $v$ is not in an m.i.s. there is a neighbour $w\in N(v)$ which is in an m.i.s.}
     By contradiction. Suppose there were an m.i.s. $ms_1$ that does not contain $v$ or one of its neighbours. Then we may create a new m.i.s. $ms_2=ms_1\with v$. We then have $|ms_2| = |ms_1|+1 > |ms_1|$. Therefore, $ms_1$ was not maximal.
-\end{lemmaproof}
+\end{thmproof}
 
-\begin{lemmaproof}[two-neighbours]{For a graph $G=(V,E)$ and vertex $v\in V$, there is an m.i.s. with $v$, or there is an m.i.s. with two distinct elements $w_1,w_2\in N(v)$.}
+\begin{thmproof}[two-neighbours]{lemma}{For a graph $G=(V,E)$ and vertex $v\in V$, there is an m.i.s. with $v$, or there is an m.i.s. with two distinct elements $w_1,w_2\in N(v)$.}
     By contradiction. If $v$ is in an m.i.s., we're done. If $v$ is not in an m.i.s., we know by \autoref{lem:one-neighbour} that there is a $w_1\in N(v)$ that is, say in m.i.s. $ms$. Suppose there were no other neighbour $w_2\in N(v), w_2\neq w_1$ with $w_2\in ms$. Then $ms\ex w_1\with v$ is also an m.i.s., and it does contain $v$.
-\end{lemmaproof}
+\end{thmproof}
 
 At this point we define, as Robson \cite{robson}, the function $\ms^n(G,S)$ which is the $\ms(G)$ given that the m.i.s. should contain at least $n$ elements of $S$.
 
@@ -21,13 +25,13 @@ Based on \autoref{lem:one-neighbour} and \ref{lem:two-neighbours} we may then re
 \label{sec:algorithm:good-v}
 Until now, we have assumed that we have some vertex $v$. Let us now discuss how to pick a `good' $v$, i.e. one that allows for the most efficient use of \autoref{eq:basic-structure} and \ref{eq:with-two-neighbours}.
 
-\begin{lemmaproof}[basic-structure-high-degree]{It is most efficient to use \autoref{eq:basic-structure} with a $v$ with large $d(v)$.}
+\begin{thmproof}[basic-structure-high-degree]{lemma}{It is most efficient to use \autoref{eq:basic-structure} with a $v$ with large $d(v)$.}
     The left-hand side, $\ms(G\ex\iN(v))$, will run faster with large $d(v)$, because it will run on a smaller graph. For the right-hand side it doesn't matter.
-\end{lemmaproof}
+\end{thmproof}
 
-\begin{lemmaproof}[two-neighbours-low-degree]{It is most efficient to use \autoref{eq:with-two-neighbours} with a $v$ with small $d(v)$.}
+\begin{thmproof}[two-neighbours-low-degree]{lemma}{It is most efficient to use \autoref{eq:with-two-neighbours} with a $v$ with small $d(v)$.}
     A straightforward implementation of $\ms^2(G\ex v,N(v))$ will consider all pairs of vertices in $N(v)$, which is quadratic. In the left-hand side, $\ms(G\ex\iN(v))$ is only linearly faster with large $d(v)$. Therefore, we should prefer small $d(v)$.
-\end{lemmaproof}
+\end{thmproof}
 
 In general, we'd like to use \autoref{eq:with-two-neighbours}, because the right-hand side of the $\max$ is more restricted than in \autoref{eq:basic-structure}. However, if we have a $v$ with large $d(v)$, this may not be the case. 
 
@@ -37,9 +41,9 @@ But this latter recurrence is clearly more efficient for \emph{large} $d(v)$. Th
 
 \subsubsection{Dominance}
 \label{sec:algorithm:good-v:dominance}
-\begin{lemmaproof}[dominance]{If in graph $G$ with vertices $v,w$ we have $v>w$, we know that $\ms(G)=\ms(G\ex w)$.}
+\begin{thmproof}[dominance]{lemma}{If in graph $G$ with vertices $v,w$ we have $v>w$, we know that $\ms(G)=\ms(G\ex w)$.}
     If there is an m.i.s. $ms$ with $w\in ms$, $ms\ex w\with v$ is an m.i.s. as well.
-\end{lemmaproof}
+\end{thmproof}
 
 If we then take $w$ instead of $v$ and use \autoref{eq:basic-structure}, it may be the case that $v>w$. In this case, we may bypass \autoref{eq:basic-structure} by applying the recurrence $\ms(G)=\ms(G\ex w)$ of \autoref{lem:dominance}. After this, it may be the case that we can apply \autoref{eq:with-two-neighbours} instead, since $d(v)$ will have been decreased by one.
 
@@ -51,13 +55,13 @@ This gives us \autoref{alg:with-best-vertex}, which combines \autoref{eq:basic-s
     \begin{algorithmic}[1]
         \REQUIRE $G=(V,E)$
         \IF{$|G|=1$}
-            \RETURN $|G|$ \COMMENT{Recursive base case}
+            \RETURN $|G|$ \COMMENT{\autoref{lem:base-case}}
         \ELSE
             \STATE $v\gets v\in V$ with minimal $d(v)$
             \IF{$d(v)$ is small enough}
                 \RETURN $\max(1+\ms(G\ex\iN(v)), \ms^2(G\ex v,N(v)))$ \COMMENT{\autoref{eq:with-two-neighbours}}
             \ELSIF{$v$ dominates $w$}
-                \RETURN $\ms(G\ex w)$
+                \RETURN $\ms(G\ex w)$ \COMMENT{\autoref{lem:dominance}}
             \ELSE
                 \STATE $w\gets w\in N(v)$ with maximal $d(w)$
                 \RETURN $\max(1+\ms(G\ex\iN(w)), \ms(G\ex w))$ \COMMENT{\autoref{eq:basic-structure}}
@@ -66,13 +70,17 @@ This gives us \autoref{alg:with-best-vertex}, which combines \autoref{eq:basic-s
     \end{algorithmic}
 \end{algorithm}
 
+\begin{thmproof}[first-ms-correct]{theorem}{\autoref{alg:with-best-vertex} is a correct implementation of the $\ms$ function.}
+    This follows from \autoref{lem:base-case} and \ref{lem:dominance} and \autoref{eq:basic-structure} and \ref{eq:with-two-neighbours}.
+\end{thmproof}
+
 \subsection{Strongly connected components}
 \label{sec:algorithm:components}
-\begin{lemmaproof}[components]{The size of the m.i.s. of a graph is equal to the sum of the sizes of the m.i.s. of all its strongly connected components.}
+\begin{thmproof}[components]{lemma}{The size of the m.i.s. of a graph is equal to the sum of the sizes of the m.i.s. of all its strongly connected components.}
     The union of the m.i.s. of the strongly connected components is an m.i.s. of the graph.
 
     If there were a larger m.i.s. in the graph, there has to be a $v$ in a strongly connected component $C$ in that m.i.s. which is not in the m.i.s. of $C$. If we can add $v$ to the m.i.s. of $C$, that m.i.s. wasn't maximal. If we cannot, then the larger m.i.s. of the whole graph cannot be an independent set.
-\end{lemmaproof}
+\end{thmproof}
 
 Based on \autoref{lem:components} we may write \refeq[with-components]{\ms(G)=\sum_{c\in C} \ms(c),} where $C$ is the set of strongly connected components of $G$. It is not difficult to see that in case a graph has multiple strongly connected components, this recurrence is more efficient than \autoref{alg:with-best-vertex}.
 
@@ -80,19 +88,19 @@ Based on \autoref{lem:components} we may write \refeq[with-components]{\ms(G)=\s
 \label{sec:algorithm:further-optimisations}
 Although I have referred to Robson \cite{robson} and used his notation throughout this report, this is how far I got without his help. Robson then introduces a number of further optimisations. In this section, we use $G$ for the graph at hand and $v,w$ for the vertex with the lowest degree, and its neighbour with the highest degree, respectively.
 
-\begin{lemmaproof}[robson-ms-d1]{If $d(v)=1$, we know $\ms(G)=1+\ms(G\ex\iN(v))$.}
+\begin{thmproof}[robson-ms-d1]{lemma}{If $d(v)=1$, we know $\ms(G)=1+\ms(G\ex\iN(v))$.}
     By contradiction. By \autoref{lem:one-neighbour} we know that if $v$ is not in any m.i.s., then $w$ is in an m.i.s., say $ms$. But then $ms\ex w\with v$ is also independent, and has the same size.
-\end{lemmaproof}
+\end{thmproof}
 
 For the case that $d(v)=2$ we write $w,w'$ for the neighbours of $v$.
 
-\begin{lemmaproof}[robson-ms-d2-edge]{If $d(v)=2$ and $e(w,w')$, we know $\ms(G)=1+\ms(G\ex\iN(v))$.}
+\begin{thmproof}[robson-ms-d2-edge]{lemma}{If $d(v)=2$ and $e(w,w')$, we know $\ms(G)=1+\ms(G\ex\iN(v))$.}
     By \autoref{lem:two-neighbours} we know that an m.i.s. will either contain $v$ or both $w$ and $w'$. But since $e(w,w')$, the latter cannot happen. Therefore, it must contain $v$ and neither of its neighbours.
-\end{lemmaproof}
+\end{thmproof}
 
-\begin{lemmaproof}[robson-ms-d2-noedge]{If $d(v)=2$ and $\lnot e(w,w')$, we know $$\ms(G) = \max(2+\ms(G\ex\iN(w)\ex\iN(w')), 1 + \ms^2(G\ex\iN(v), N^2(v))).$$}
+\begin{thmproof}[robson-ms-d2-noedge]{lemma}{If $d(v)=2$ and $\lnot e(w,w')$, we know $$\ms(G) = \max(2+\ms(G\ex\iN(w)\ex\iN(w')), 1 + \ms^2(G\ex\iN(v), N^2(v))).$$}
     By \autoref{lem:two-neighbours}, an m.i.s. contains either $v$ or both $w,w'$. In the second case, we remove $w$ and $w'$ and their neighbourhoods from the graph (the left-hand side of $\max$). In the first case, the m.i.s. cannot contain $w$ or $w'$ but must contain two of their neighbours other than $v$. If not, and there is an m.i.s. $ms$ with at most one such neighbour, $u$, then $ms\ex v\ex u\with w\with w'$ is also independent, and has the same size. This gives the right-hand side.
-\end{lemmaproof}
+\end{thmproof}
 
 \autoref{alg:with-best-vertex} combined with \autoref{lem:components}, \ref{lem:robson-ms-d1}, \ref{lem:robson-ms-d2-edge} and \ref{lem:robson-ms-d2-noedge} gives us \autoref{alg:with-robsons-optimisations}.
 
@@ -105,7 +113,7 @@ For the case that $d(v)=2$ we write $w,w'$ for the neighbours of $v$.
             \STATE $C\gets$ some strongly connected component
             \RETURN $\ms(C) + \ms(G\ex C)$ \COMMENT{\autoref{lem:components}}
         \ELSIF{$|G|=1$}
-            \RETURN $|G|$ \COMMENT{Recursive base case}
+            \RETURN $|G|$ \COMMENT{\autoref{lem:base-case}}
         \ELSE
             \STATE $v\gets v\in V$ with minimal $d(v)$
             \STATE $w\gets w\in N(v)$ with maximal $d(w)$
@@ -129,33 +137,41 @@ For the case that $d(v)=2$ we write $w,w'$ for the neighbours of $v$.
     \end{algorithmic}
 \end{algorithm}
 
+\begin{thmproof}[ms-correct]{theorem}{\autoref{alg:ms} is a correct implementation of the $\ms$ function.}
+    This follows from \autoref{lem:base-case}, \ref{lem:dominance}, \ref{lem:components}, \ref{lem:robson-ms-d1}, \ref{lem:robson-ms-d2-edge} and \ref{lem:robson-ms-d2-noedge} and \autoref{eq:basic-structure} and \ref{eq:with-two-neighbours}.
+\end{thmproof}
+
+\begin{thmproof}[ms-efficiency]{theorem}{\autoref{alg:ms} is more efficient than \autoref{alg:with-best-vertex}, assuming that conditions are evaluated efficiently.}
+    The algorithm follows the same basic structure. In any case that \autoref{alg:ms} is different, it considers less cases (yet it is still correct by \autoref{thm:ms-correct}). Therefore, it can only be more efficient.
+\end{thmproof}
+
 \subsection{The helper function $\ms^n$}
 \label{sec:algorithm:helper-function}
 So far we have been using $\ms^n(G,S)$ as the size of the maximum independent set of $G$ given that it contains at least $n$ vertices in $S$. This section is devoted to arguing an efficient implementation of this helper function. In the above, we have only used $\ms^2$. Therefore, we do not need to go into details about the case $n\neq2$.
 
 We will write $s_1,s_2,\dots$ for the elements of $S$.
 
-\begin{lemmaproof}[helper-general]{In our algorithm, it always holds that $\ms^n(G,S)=\ms(G)$.}
+\begin{thmproof}[helper-general]{lemma}{In our algorithm, it always holds that $\ms^n(G,S)=\ms(G)$.}
     We only call $\ms^n$ when we know for sure that $n$ elements of $S$ are in an m.i.s. of $G$.
-\end{lemmaproof}
+\end{thmproof}
 
 \autoref{lem:helper-general} may be used as a default case, when no clever optimisation can be found.
 
-\begin{lemmaproof}[helper-1]{If $|S|<n$, we know $\ms^n(G,S)=0$.}
+\begin{thmproof}[helper-1]{lemma}{If $|S|<n$, we know $\ms^n(G,S)=0$.}
     It is impossible to pick $n$ edges from less than $n$.
-\end{lemmaproof}
+\end{thmproof}
 
-\begin{lemmaproof}[helper-2-edge]{If $|S|=2$ and $e(s_1,s_2)$, then $\ms^2(G,S)=0$.}
+\begin{thmproof}[helper-2-edge]{lemma}{If $|S|=2$ and $e(s_1,s_2)$, then $\ms^2(G,S)=0$.}
     The only possibility to choose two vertices from $S$, choosing $s_1$ and $s_2$ does not give us an independent set.
-\end{lemmaproof}
+\end{thmproof}
 
-\begin{lemmaproof}[helper-2-noedge]{If $|S|=2$ and $\lnot e(s_1,s_2)$, then $\ms^2(G,S)=2+\ms(G\ex\iN(s_1)\ex\iN(S_2)$.}
+\begin{thmproof}[helper-2-noedge]{lemma}{If $|S|=2$ and $\lnot e(s_1,s_2)$, then $\ms^2(G,S)=2+\ms(G\ex\iN(s_1)\ex\iN(S_2)$.}
     We only have to consider the one possibility of choosing $s_1$ and $s_2$. Then we may remove their inclusive neighbourhoods from the graph.
-\end{lemmaproof}
+\end{thmproof}
 
-\begin{lemmaproof}[helper-3-naive]{If $|S|=3$, we have $\ms^2(G,S)=\max(\ms^2(G,S\ex s_1), \ms^2(G,S\ex s_2), \ms^2(G,S\ex s_3)).$}
+\begin{thmproof}[helper-3-naive]{lemma}{If $|S|=3$, we have $\ms^2(G,S)=\max(\ms^2(G,S\ex s_1), \ms^2(G,S\ex s_2), \ms^2(G,S\ex s_3)).$}
     We only have to consider three possibilities.
-\end{lemmaproof}
+\end{thmproof}
 
 \autoref{lem:helper-general} through \ref{lem:helper-3-naive} were the results I achieved. Robson \cite{robson} adds some optimisations to the cases $|S|=3$ and $|S|=4$. As they are fairly straightforward, I will not discuss them here. They are included in \autoref{alg:ms2}, which combines our own results into one algorithm. Robson uses slightly different notation at some points, since he assumes $d(s_1)<d(s_2)$.
 
@@ -201,33 +217,37 @@ We will write $s_1,s_2,\dots$ for the elements of $S$.
     \end{algorithmic}
 \end{algorithm}
 
+\begin{thmproof}[ms2-correct]{theorem}{\autoref{alg:ms2} is a correct implementation of the $\ms^2$ function.}
+    This follows from \autoref{lem:helper-general} through \ref{lem:helper-2-noedge} and \autoref{lem:one-neighbour} and \ref{lem:components}. We have only made small efficiency enhancements that are clearly correct and are argued in the definition of the algorithm.
+\end{thmproof}
+
 \bigskip
 
 As the observant reader may have noticed, we use $\ms^1$ in the definition of $\ms^2$. We therefore also need to write an efficient algorithm to apply this function. Of course, \autoref{lem:helper-general} and \ref{lem:helper-1} apply to $\ms^1$ as well. Note, that we always call $\ms^1(\cdots,S)$ with $|S|=2$. We will therefore not give a complete algorithm $\ms^1$, but one that works in the necessary cases.
 
-\begin{lemmaproof}[helper-intersection]{If $N(s_1)\cap N(s_2)\neq\emptyset$, we know $\ms^1(G,S)=\ms^1(G\ex(N(s_1)\cap N(s_2)), S)$.}
+\begin{thmproof}[helper-intersection]{lemma}{If $N(s_1)\cap N(s_2)\neq\emptyset$, we know $\ms^1(G,S)=\ms^1(G\ex(N(s_1)\cap N(s_2)), S)$.}
     This was already used in \autoref{alg:ms2}, in the case of three states. The m.i.s. will contain either $s_1$ or $s_2$, therefore cannot contain the intersection of their neighbourhoods. Removing these vertices allows for early pruning.
-\end{lemmaproof}
+\end{thmproof}
 
 Robson adds further optimisations to this.
 
-\begin{lemmaproof}[helper-ms1-2-2]{If $d(s_1)=d(s_2)=2$ and $\lnot e(s_1,s_2)$, an m.i.s. containing one of $s_1,s_2$ will contain either $s_1$ or $N(s_1)\with\{s_2\}$.}
+\begin{thmproof}[helper-ms1-2-2]{lemma}{If $d(s_1)=d(s_2)=2$ and $\lnot e(s_1,s_2)$, an m.i.s. containing one of $s_1,s_2$ will contain either $s_1$ or $N(s_1)\with\{s_2\}$.}
     In the case that the m.i.s. contains $s_1$, we are done. If an m.i.s. $ms$ does not contain $s_1$ but $s_2$, it must contain $N(s_1)$, because otherwise $ms\ex N(s_1)\with s_1$ is an independent set of at least the same size.
-\end{lemmaproof}
+\end{thmproof}
 
 If the conditions of \autoref{lem:helper-ms1-2-2} are met, write $w_1,w_2$ for the two neighbours of $s_1$.
 
-\begin{lemmaproof}[helper-ms1-2-2-edge]{If the conditions of \autoref{lem:helper-ms1-2-2} are met and $e(w_1,w_2)$, we have $\ms^1(G,S)=1+\ms(G\ex s_1)$.}
+\begin{thmproof}[helper-ms1-2-2-edge]{lemma}{If the conditions of \autoref{lem:helper-ms1-2-2} are met and $e(w_1,w_2)$, we have $\ms^1(G,S)=1+\ms(G\ex s_1)$.}
     It cannot be the case that an m.i.s. will contain $N(s_1)$. \autoref{lem:helper-ms1-2-2} leaves this (choosing $s_1$) as only option.
-\end{lemmaproof}
+\end{thmproof}
 
-\begin{lemmaproof}[helper-ms1-2-2-dominance]{If the conditions of \autoref{lem:helper-ms1-2-2} are met and $N^2(s_1)\subset N(s_2)$, we have $\ms^1(G,S)=3+\ms(G\ex\iN(s_1)\ex\iN(s_2))$.}
+\begin{thmproof}[helper-ms1-2-2-dominance]{lemma}{If the conditions of \autoref{lem:helper-ms1-2-2} are met and $N^2(s_1)\subset N(s_2)$, we have $\ms^1(G,S)=3+\ms(G\ex\iN(s_1)\ex\iN(s_2))$.}
     Obviously, an m.i.s. $\iN(s_1)+\iN(s_2)$ that contains $s_1$ or $s_2$ cannot be larger than three. Furthermore, $\{w_1,w_2,s_2\}$ is an independent set and dominates every other independent set of the same size.
-\end{lemmaproof}
+\end{thmproof}
 
 This leads us to a slightly adapted version of $\ms^2$ that we can use for $\ms^1$. Pseudocode is given in \autoref{alg:ms1}.
 
-\begin{algorithm}[h]
+\begin{algorithm}[h!]
     \caption{Finding the size of the m.i.s. of a graph, given that it should contain one node from a certain subgraph}
     \label{alg:ms1}
     \begin{algorithmic}[1]
@@ -257,3 +277,9 @@ This leads us to a slightly adapted version of $\ms^2$ that we can use for $\ms^
     \end{algorithmic}
 \end{algorithm}
 
+\begin{thmproof}[ms1-correct]{theorem}{\autoref{alg:ms1} is a correct implementation of the $\ms^1$ function if the second argument has size $2$.}
+    This follows from \autoref{lem:helper-general} and \autoref{lem:helper-ms1-2-2} through \ref{lem:helper-ms1-2-2-dominance}. We have only made enhancements that are clearly correct and furthermore argued in the definition of the algorithm.
+\end{thmproof}
+
+If we assume to have implementations of the more obvious graph algorithms such as the neighbours of a vertex, we now have by \autoref{thm:ms-correct} a correct implementation of the maximum independent set problem.
+