Add writings from 18th of January

thesis/sections/1_introduction.tex

@@ -75,7 +75,7 @@ \subsection*{Objective} %TODO Change to 'Objectives' and explain all of the obje
 This can be done for example by rendering the network that cannot have any viable configurations.
 
 \subsection{Thesis structure}
-The chapter \ref{sec:background} gives a succint theoretical background to the topic of this work.
+The section \ref{sec:background} gives a succint theoretical background to the topic of this work.
 First it explains ... %TODO Update these when background is done
 
-The chapter \ref{sec:implementation}
+The section \ref{sec:implementation}

thesis/sections/2_background.tex

@@ -6,7 +6,7 @@ \section{Background} \label{sec:background}
 In this section, we introduce relevant terminology and concepts to prepare the reader for the sections \ref{sec:research_question}-\ref{sec:implementation}.
 
 
-In the first section (\ref{sec:distributed_computing}) of this chapter, we discuss about the essential concepts in the theory of distributed computing.
+In the first section (\ref{sec:distributed_computing}) of this section, we discuss about the essential concepts in the theory of distributed computing.
 The section aims to explain the meaning of distributed computing and gives an introduction to the main model of distributed computing, \emph{message passing model}, from which many of the researched models inherit from.
 
 The second and third sections discuss about the Port number model and local model respectively.
@@ -337,7 +337,8 @@ \subsection{Port number model} \label{sec:port_number_model}
 Each node has communication ports numbered from $1$ to $d$ where $d$ is the degree of the node.
 The ports are numbered in an arbitrary order.
 
-All nodes are considered identical, however nodes know their degree and it might differ between different nodes depending on the underlying graph $G$.
+All nodes are considered identical.
+%TODO IS THIS NEEDED? However, nodes know their degree and there can be different degreed nodes, depending on the underlying graph $G$.
 Every node starts the execution simultaneously following the same PN-algorithm $A$.
 The execution of $A$ is done synchronously in parallel.
 A communication round consists of following synchronous steps
@@ -354,15 +355,14 @@ \subsection{Port number model} \label{sec:port_number_model}
 
 
 \subsection{Formalized port number model}
-As in the previous section, this section is based on the course material from \cite{HirvonenSuomelaDistAlg2020} unless otherwise mentioned.
-
 In the section \ref{sec:port_number_model} we briefly and informally introduced the PN model.
 Now in this section and in the following subsections we give a more formal definition to the PN model.
+As in the previous section, this section is based on the course material from \cite{HirvonenSuomelaDistAlg2020} unless otherwise mentioned.
 
 We call the network as a port number network or a PN network.
 PN network is a 3-element tuple $N = (V, P, p)$, where $V$ and $P$ are the sets of vertices and ports respectively, and $p: P \rightarrow P$ is a function that maps a port to another port, forming a communication channel.
 A port, an element of $P$, is a pair $(v, i)$ where $v \in V$ and $i \in \{1, 2, ...\}$.
-Additionally we assume that $p$ is an involution, that is, $\forall x \in P : p(p(x)) = x, $ i.e. each edge of the underlying graph is undirected.
+Additionally we assume that $p$ is an involution, that is, $\forall x \in P : p(p(x)) = x, $ i.e. each edge of the "underlying graph" is undirected.
 See the Figures \ref{fig:formal_pn1:a} and \ref{fig:formal_pn1:b} for examples of valid and invalid PN networks.
 
 \begin{figure}[H]
@@ -409,7 +409,7 @@ \subsection{Formalized port number model}
 There are multiple connections between two distinct nodes $v$ and $w$, if $p((v, i_1)) = (w, j_1)$, $p((v, i_2)) = (w, j_2)$, $i_1 \neq j_1$ and $i_2 \neq j_2$.
 For example the connections $p((b, 2)) = (d, 1)$ and $p((b, 3)) = (d, 2)$ in the Figure \ref{fig:formal_pn2:c}.
 
-If a PN network has neither loops or multiple connections, it is called a \emph{simple} network.
+If a PN network has neither loops or multiple connections, it is called a \emph{simple} PN network.
 For example the network is simple in the Figure \ref{fig:formal_pn2:a}.
 
 
@@ -450,7 +450,7 @@ \subsection{Formalized port number model}
 \subsubsection{Underlying graph}
 
 Each simple PN network $N=(V,P,p)$ has a concept called an \emph{underlying graph} $G=(V,E)$.
-An edge $(v, w)$ is part of the underlying network $G$ if and only if $v$ is connected to $w$, that is, $E = \{ \{v, w\} \, | \,  p((v, i)) = (w, j) \}$.% where ${v, w} \in E$.
+An edge $(v, w)$ is part of the underlying network $G$ if and only if $v$ is connected to $w$, that is, $E = \{ (v, w) \, | \,  p((v, i)) = (w, j) \}$.
 A network with multiple connections uses the same definition to determine an underlying network, but in that case $E$ has to be a multiset instead of a set, in order to allow multiple same edges.
 
 \begin{figure}[H]
@@ -520,7 +520,7 @@ \subsubsection{Distributed algorithms in the PN model}
 \newcommand{\algrecv}{\operatorname{receive}}
 
 A \emph{distributed algorithm} $A$ can be described as a state machine.
-The algorithm $A$ can possibly have infinitely many states or only finite many states.
+The algorithm $A$ can possibly have infinitely many states or only finitely many states.
 The components of $A$ are:
 \begin{enumerate}
   \item $\algin_A$ is the set of local inputs,
@@ -554,12 +554,7 @@ \subsubsection{Distributed algorithms in the PN model}
 Algorithm $A$ stops at time $T$ when each node is in an output state.
 %Algorithm $A$ stops in time $T$ if and only if each node is in an output state.
 
-
-
-
-
-The function
-
+\todo{Add an example execution of an example problem.} %TODO Add an example execution of an example problem.
 
 
 
@@ -571,6 +566,13 @@ \subsection{LOCAL model} \label{sec:local_model}
 \subsection{LCL problems} \label{sec:lcl_problems}
 
 \subsection{Boolean satisfiability problem}
+\todo{Explain
+\begin{itemize}
+  \item SAT problems, %TODO
+  \item DIMACS CNF, %TODO
+  \item SAT solvers, %TODO
+\end{itemize}}
+
 
 \clearpage
 

thesis/sections/4_prior_work.tex

@@ -5,6 +5,7 @@ \section{Prior work} \label{sec:prior_work}
 
 %TODO I'll draft some sections here that I probably should consider writing about.
 % Some might be really similiar or even identical.
+\subsection{\todo{these sections are WIP}}
 \subsection{Lower and upper bounds of LCL's}
 \subsection{Complexity classifications of LCL's}
 \subsection{Computation of lower and upper bounds}

thesis/sections/6_implementation.tex

@@ -2,65 +2,65 @@
 
 %\section{Automatically proving lower bounds for LCL problems} \label{sec:implementation}
 \section{Implementation} \label{sec:implementation}
-In this chapter we will cover all the important topics that are used in the actual implementation.
-The implementation itself is a computer program, that attempts to automatically find a proof which shows the nonsolvability of the given LCL problem in PN model (see section \ref{sec:port_number_model} for more information about PN model).
-
-%TODO should the discussion of the implementation be after explanation of the topics?
-For each pair of LCL problem and graph, we want to be able to check if labelling is impossible.
-To perform the checking, we first encode the problem and graph into a SAT problem.
-Then we leverage the power of SAT solvers to solve the SAT problem.
-We feed the SAT problem into the solver, which returns either SAT (satisfiable) or UNSAT (unsatisfiable) as a result.
-In case the result is UNSAT, we have found a counterexample and we are done.
-Otherwise we can continue searching using some other graph.
-The routine is illustrated on Figure \ref{fig:implementation:idea:1}.
+In this section we will cover all the important topics that are used in the actual implementation of the Algorithm \ref{alg:counterexample_finder} from the section \ref{sec:algorithm}.
+This includes the previously declared functions $\textsc{IsUnsolvable}(\Pi, g)$ and $\textsc{GenerateGraphs}(n, d_a, d_p)$, which were given without defining how their algorithms work.
+The implementation itself is a computer program, that attempts to automatically find a proof of unsolvability for a given LCL problem in PN model.
+We keep the explanations independent of any programming language, so that the reader can understand these upcoming topics without needing such knowledge.
+% (see section \ref{sec:port_number_model} for more information about PN model).
+
+The function $\textsc{IsUnsolvable}(\Pi, g)$ checks if an LCL problem $\Pi$ is unsolvable in some $(d_a, d_p)$-biregular multigraph $g$.
+To perform the checking, it is enough to show that there exists no valid labeling of $\Pi$ in $g$.
+In the implementation this is done with following steps:
+\begin{enumerate}
+    \item encode the problem $\Pi$ and multigraph $g$ into a SAT problem $S$,
+    \item solve the problem $S$ using some efficient SAT solver.
+\end{enumerate}
+When we feed the SAT problem $S$ into a SAT solver, we get either SAT (satisfiable) or UNSAT (unsatisfiable) as a result.
+In case the result is UNSAT, the SAT solver found no possible labeling for the problem.
+Thus we have found a counterexample and we are done.
+Otherwise we can continue searching using some other multigraph.
+The routine is illustrated on Figure \ref{fig:implementation:1}.
 
 \begin{figure}[H]
 \centering
 \includegraphics[]{diagrams/implementation_idea_diagram2.pdf}
-\caption{The SAT routine. When given a graph and an LCL problem, it checks if a valid labelling exists.}
-\label{fig:implementation:idea:1}
+\caption{The SAT routine. When given a multigraph and an LCL problem, it checks if a valid labelling exists.}
+\label{fig:implementation:1}
 \end{figure}
 
-We repeat the routine for each graph in the current search space and terminate early if the result is UNSAT.
-A solid and logical strategy is to first start with the smallest graphs and continue incrementally, increasing the size of graphs  after previous size has been searched entirely.
-This can be indeed trivially automated as long as the routine is implemented.
-User needs to only input the lower and upper bounds of graph sizes.
-Here the graph size is the number of vertices, that is, $n=|V|$.
-A search space can be for example every graph from $1$ to $15$.
-Then the set of graphs would be $\{(V, E) : |V| \in \{1, 2, ..., 15\} \}$.
+We repeat the routine for each multigraph, as shown in the Algorithm \ref{alg:counterexample_finder}, and terminate early if the result is UNSAT.
+\todo{WIP}
 
 \begin{figure}[H]
 \centering
 \includegraphics[]{diagrams/implementation_idea_diagram3.pdf}
-\caption{An example of an execution of multiple SAT routines. Execution terminates at graph $23077$ when first UNSAT is encountered.}
-\label{fig:implementation:idea:2}
+\caption{An example of an execution of multiple SAT routines. Execution terminates at graph $77$ when first UNSAT is encountered.}
+\label{fig:implementation:2}
 \end{figure}
 
 %TODO biregular multigraphs?
 %TODO LCL problems on biregular trees etc?
 
-When we assume that an LCL problem $\Pi$ is solvable in PN, we mean that there exists a deterministic distributed algorithm $A$ in PN model, that finds a solution for all multigraphs i.e. algorithm $A$ works in every multigraph.
-Every simple graph is also a multigraph, thus multigraphs are more relaxed in terms of definition.
-Allowing parallel edges potentially gives us counter examples with smaller graph sizes when we use the increasing strategy i.e. our algorithm might terminate succesfully much earlier with the desired result and graphs do not necessarily become as complex as they would be with only simple graphs.
-%TODO where to discuss about solutions that have been found only with multigraphs? Have we found any solutions with only simple graphs?
-Smaller graphs mean less complexity and less performance required but as there are also more graphs to iterate, it is not so simple to justify allowing parallel edges only with this argument.
-The main argument is that allowing parallel edges gives us more opportunities to find counterexamples.
-It might be that in some problems we cannot even find counterexamples without parallel.
+%When we assume that an LCL problem $\Pi$ is solvable in PN, we mean that there exists a deterministic distributed algorithm $A$ in PN model, that finds a solution for all multigraphs i.e. algorithm $A$ works in every multigraph.
+%Every simple graph is also a multigraph, thus multigraphs are more relaxed in terms of definition.
+%Allowing parallel edges potentially gives us counter examples with smaller graph sizes when we use the increasing strategy i.e. our algorithm might terminate succesfully much earlier with the desired result and graphs do not necessarily become as complex as they would be with only simple graphs.
+%%TODO where to discuss about solutions that have been found only with multigraphs? Have we found any solutions with only simple graphs?
+%Smaller graphs mean less complexity and less performance required but as there are also more graphs to iterate, it is not so simple to justify allowing parallel edges only with this argument.
+%The main argument is that allowing parallel edges gives us more opportunities to find counterexamples.
+%It might be that in some problems we cannot even find counterexamples without parallel.
 
 %This is indeed what we have used in this work.
 %Probably, we have to iterate a lot of graphs.
 %For this purpose we want to be able to generate the graphs.
 
 
 
+\subsection{Generating multigraphs}
 
 \subsection{Generating LCL-problems}
-%TODO parallelization
-\subsection{Generating multigraphs}
 
-%TODO parallelization
 \subsection{SAT encoding and solving}
-%TODO parallelization?
+
 %\subsection{Software optimizations
 \subsection{Caching}
 %TODO pre-computing multigraphs and lcl problems and saving them?