Working on report

1 files changed, 38 insertions, 26 deletions

diff --git a/Practical1/report/algorithm.tex b/Practical1/report/algorithm.tex
index 7ce0fdd..f6272e4 100644
--- a/Practical1/report/algorithm.tex
+++ b/Practical1/report/algorithm.tex
@@ -45,7 +45,7 @@ But this latter recurrence is clearly more efficient for \emph{large} $d(v)$. Th
     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{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.
+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, since the maximum degree of any vertex in our graph is $4$, we will be able to apply \autoref{eq:with-two-neighbours} instead, since $d(v)$ will have been decreased by one to at most $3$.
 
 This gives us \autoref{alg:with-best-vertex}, which combines \autoref{eq:basic-structure} and \ref{eq:with-two-neighbours}.
 
@@ -111,27 +111,27 @@ For the case that $d(v)=2$ we write $w,w'$ for the neighbours of $v$.
         \REQUIRE $G=(V,E)$
         \IF{$G$ has multiple strongly connected components}
             \STATE $C\gets$ some strongly connected component
-            \RETURN $\ms(C) + \ms(G\ex C)$ \COMMENT{\autoref{lem:components}}
-        \ELSIF{$|G|=1$}
-            \RETURN $|G|$ \COMMENT{\autoref{lem:base-case}}
+            \RETURN $\ms(C) + \ms(G\ex C)$ \COMMENT{\autoref{lem:components}}\label{alg:ms:case-component}
+        \ELSIF{$|G|\le1$}
+            \RETURN $|G|$ \COMMENT{\autoref{lem:base-case}}\label{alg:ms:case-g1}
         \ELSE
             \STATE $v\gets v\in V$ with minimal $d(v)$
             \STATE $w\gets w\in N(v)$ with maximal $d(w)$
             \IF{$d(v)=1$}
-                \RETURN $1+\ms(G\ex\iN(v))$ \COMMENT{\autoref{lem:robson-ms-d1}}
+                \RETURN $1+\ms(G\ex\iN(v))$ \COMMENT{\autoref{lem:robson-ms-d1}}\label{alg:ms:case-d1}
             \ELSIF{$d(v)=2$}
                 \STATE $w'\gets$ the other neighbour of $v$
                 \IF{$e(w,w')$}
-                    \RETURN $1+\ms(G\ex\iN(v))$ \COMMENT{\autoref{lem:robson-ms-d2-edge}}
+                    \RETURN $1+\ms(G\ex\iN(v))$ \COMMENT{\autoref{lem:robson-ms-d2-edge}}\label{alg:ms:case-d2-edge}
                 \ELSE
-                    \RETURN $\max(2+\ms(G\ex\iN(w)\ex\iN(w')), 1+\ms^2(G\ex\iN(v),N^2(v)))$ \COMMENT{\autoref{lem:robson-ms-d2-noedge}}
+                    \RETURN $\max(2+\ms(G\ex\iN(w)\ex\iN(w')), 1+\ms^2(G\ex\iN(v),N^2(v)))$ \COMMENT{\autoref{lem:robson-ms-d2-noedge}}\label{alg:ms:case-d2-noedge}
                 \ENDIF
             \ELSIF{$d(v)=3$}
-                \RETURN $\max(\ms^2(G\ex v,N(v)), 1+\ms(G\ex\iN(v)))$ \COMMENT{\autoref{eq:with-two-neighbours}}
+                \RETURN $\max(\ms^2(G\ex v,N(v)), 1+\ms(G\ex\iN(v)))$ \COMMENT{\autoref{eq:with-two-neighbours}}\label{alg:ms:case-d3}
             \ELSIF{$v>w$}
-                \RETURN $\ms(G\ex w)$ \COMMENT{\autoref{lem:dominance}}
+                \RETURN $\ms(G\ex w)$ \COMMENT{\autoref{lem:dominance}}\label{alg:ms:case-dominance}
             \ELSE
-                \RETURN $\max(\ms(G\ex w), 1+\ms(G\ex\iN(w)))$ \COMMENT{\autoref{eq:basic-structure}}
+                \RETURN $\max(\ms(G\ex w), 1+\ms(G\ex\iN(w)))$ \COMMENT{\autoref{eq:basic-structure}}\label{alg:ms:case-otherwise}
             \ENDIF
         \ENDIF
     \end{algorithmic}
@@ -145,6 +145,10 @@ For the case that $d(v)=2$ we write $w,w'$ for the neighbours of $v$.
     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}
 
+\begin{thmproof}[ms-terminates]{theorem}{\autoref{alg:ms} terminates with every input, if $\ms^2$ terminates with a smaller input.}
+    There is a base case on line \ref{alg:ms:case-g1} which is not recursive and handles the graphs with the lowest $k$ possible orders ($k=2$). In every other case, the same algorithm is run on a smaller input (or $\ms^2$ on a smaller input), so inductively the algorithm terminates with any input.
+\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$.
@@ -180,39 +184,39 @@ We will write $s_1,s_2,\dots$ for the elements of $S$.
     \label{alg:ms2}
     \begin{algorithmic}[1]
         \REQUIRE $G=(V,E), S\subseteq V$
-        \IF{$|S|=1$}
-            \RETURN $0$ \COMMENT{\autoref{lem:helper-1}}
+        \IF{$|S|\le1$}
+        \RETURN $0$ \COMMENT{\autoref{lem:helper-1}}\label{alg:ms2:case-s1}
         \ELSIF{$|S|=2$}
             \IF{$e(s_1,s_2)$}
-                \RETURN $0$ \COMMENT{\autoref{lem:helper-2-edge}}
+                \RETURN $0$ \COMMENT{\autoref{lem:helper-2-edge}}\label{alg:ms2:case-s2-edge}
             \ELSE
-                \RETURN $2+\ms(G\ex\iN(s_1)\ex\iN(s_2))$ \COMMENT{\autoref{lem:helper-2-noedge}}
+                \RETURN $2+\ms(G\ex\iN(s_1)\ex\iN(s_2))$ \COMMENT{\autoref{lem:helper-2-noedge}}\label{alg:ms2:case-s2-noedge}
             \ENDIF
         \ELSIF{$|S|=3$}
             \IF{$\exists_i[d(s_i)=0]$}
-                \RETURN $1+\ms^1(G\ex s_i,S\ex s_i)$ \COMMENT{Special case of \autoref{lem:components}}
+                \RETURN $1+\ms^1(G\ex s_i,S\ex s_i)$ \COMMENT{Special case of \autoref{lem:components}}\label{alg:ms2:case-s3-d0}
             \ELSIF{$s_1,s_2,s_3$ form a three-cycle}
-                \RETURN $0$ \COMMENT{Impossible to pick two vertices from a three-cycle}
+                \RETURN $0$ \COMMENT{Impossible to pick two vertices from a three-cycle}\label{alg:ms2:case-s3-cycle}
             \ELSIF{$\exists_{i,j,k}[i\neq k \land e(s_i,s_j) \land e(s_i,s_k)]$}
-                \RETURN $2 + \ms(G\ex\iN(s_j)\ex\iN(s_k))$ \COMMENT{Impossible to choose $s_i$ and another vertex, so we have to choose $s_j$ and $s_k$}
+                \RETURN $2 + \ms(G\ex\iN(s_j)\ex\iN(s_k))$ \COMMENT{Impossible to choose $s_i$ and another vertex, so we have to choose $s_j$ and $s_k$}\label{alg:ms2:case-s3-path}
             \ELSIF{$\exists_{i,j}[e(s_i,s_j)]$}
                 \STATE $s_k\gets S\ex s_1\ex s_j$
-                \RETURN $1 + \ms^1(G\ex\iN(s_k), S\ex s_k)$ \COMMENT{Impossible to choose $s_i$ and $s_j$, so we choose $s_k$ and one of $s_i,s_j$}
+                    \RETURN $1 + \ms^1(G\ex\iN(s_k), S\ex s_k)$ \COMMENT{Impossible to choose $s_i$ and $s_j$, so we choose $s_k$ and one of $s_i,s_j$}\label{alg:ms2:case-s3-edge}
             \ELSIF{$\exists_{i,j}[N(s_i)\cap N(s_j)\neq\emptyset]$}
-                \RETURN $\ms^2(G\ex(N(s_i)\cap N(s_j)), S)$ \COMMENT{m.i.s. contains either $s_i$ or $s_j$, so not their common neighbours}
+                \RETURN $\ms^2(G\ex(N(s_i)\cap N(s_j)), S)$ \COMMENT{m.i.s. contains either $s_i$ or $s_j$, so not their common neighbours}\label{alg:ms2:case-s3-intersection}
             \ELSIF{$\exists_i[d(s_i)=1]$}
-                \RETURN $1+\ms^1(G\ex\iN(s_i),S\ex s_i)$ \COMMENT{Special case of \autoref{lem:one-neighbour}}
+                \RETURN $1+\ms^1(G\ex\iN(s_i),S\ex s_i)$ \COMMENT{Special case of \autoref{lem:one-neighbour}}\label{alg:ms2:case-s3-d1}
             \ELSE
-                \RETURN $\max(1+\ms^1(G\ex\iN(s_1),S\ex s_1), 2 + \ms^2(G\ex\iN(s_2)\ex\iN(s_3)\ex s_1, N(s_1)))$ \COMMENT{Either the m.i.s. does contain $s_1$, and one of $s_2,s_3$, or it doesn't. In the latter case, it must contain $s_2,s_3$, and at least two on $s_1$'s neighbours, using an argument similar to \autoref{lem:two-neighbours}. Robson misses the `$2+$' for this second case, but from the writing it is clear that it should be included.}
+                \RETURN $\max(1+\ms^1(G\ex\iN(s_1),S\ex s_1), 2 + \ms^2(G\ex\iN(s_2)\ex\iN(s_3)\ex s_1, N(s_1)))$ \COMMENT{Either the m.i.s. does contain $s_1$, and one of $s_2,s_3$, or it doesn't. In the latter case, it must contain $s_2,s_3$, and at least two on $s_1$'s neighbours, using an argument similar to \autoref{lem:two-neighbours}. Robson misses the `$2+$' for this second case, but from the writing it is clear that it should be included.}\label{alg:ms2:case-s3-otherwise}
             \ENDIF
         \ELSIF{$|S|=4$}
             \IF{$\lnot\exists_i[d(s_i)\leq3]$}
-                \RETURN $\max(1+\ms(G\ex\iN(s_1)),\ms^2(G\ex s_1,S\ex s_1))$ \COMMENT{m.i.s. either does or doesn't contain $s_1$}
+                \RETURN $\max(1+\ms(G\ex\iN(s_1)),\ms^2(G\ex s_1,S\ex s_1))$ \COMMENT{m.i.s. either does or doesn't contain $s_1$}\label{alg:ms2:case-s4-no-dle3}
             \ELSE
-            \RETURN $\ms(G)$ \COMMENT{More efficient than the $\max$ in this case; \autoref{lem:helper-general}}
+                \RETURN $\ms(G)$ \COMMENT{More efficient than the $\max$ in this case; \autoref{lem:helper-general}}\label{alg:ms2:case-s4-dle3}
             \ENDIF
         \ELSE
-            \RETURN $\ms(G)$ \COMMENT{No clever optimisation found; \autoref{lem:helper-general}}
+            \RETURN $\ms(G)$ \COMMENT{No clever optimisation found; \autoref{lem:helper-general}}\label{alg:ms2:case-otherwise}
         \ENDIF
     \end{algorithmic}
 \end{algorithm}
@@ -221,6 +225,10 @@ We will write $s_1,s_2,\dots$ for the elements of $S$.
     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}
 
+\begin{thmproof}[ms2-terminates]{theorem}{\autoref{alg:ms2} terminates for any input, if $\ms$ and $\ms^1$ terminate with a smaller input.}
+    There are base cases for the smallest cases, $|S|$-wise, that terminate directly. Every other case terminates directly or reduces to termination of $\ms$ on a smaller input $|G|$-wise, $\ms^1$ on a smaller input $|G|$-wise, or $\ms^2$ on a smaller input $|G|$ or $|S|$-wise. By induction, the algorithm terminates with any input.
+\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.
@@ -248,10 +256,10 @@ If the conditions of \autoref{lem:helper-ms1-2-2} are met, write $w_1,w_2$ for t
 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!]
-    \caption{Finding the size of the m.i.s. of a graph, given that it should contain one node from a certain subgraph}
+    \caption{Finding the size of the m.i.s. of a graph, given that it should contain one node from a certain subgraph with two nodes}
     \label{alg:ms1}
     \begin{algorithmic}[1]
-        \REQUIRE $G=(V,E), S\subseteq V, d(s_1)\leq d(s_2)$
+        \REQUIRE $G=(V,E), S\subseteq V, S=\{s_1,s_2\}, d(s_1)\leq d(s_2)$
         \IF{$d(s_1)\leq1$}
             \RETURN $\ms(G)$ \COMMENT{\autoref{lem:helper-general}} \label{alg:ms1:case-d1}
         \ELSIF{$e(s_1,s_2)$}
@@ -281,5 +289,9 @@ This leads us to a slightly adapted version of $\ms^2$ that we can use for $\ms^
     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}
 
+\begin{thmproof}[ms1-terminates]{theorem}{\autoref{alg:ms1} terminates with any input if the second argument has size $2$.}
+    Inductively by \autoref{thm:ms-terminates} and \ref{thm:ms2-terminates}.
+\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.