uni/fmi/fmi23block1/practical-exercises.tex

\documentclass [10pt]{article}
  
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{fullpage}
\usepackage{enumerate}
\usepackage{amsmath}
\usepackage{hyperref}
\pagestyle{plain}

\newcommand{\todo}{\bf TODO}

\title{Formal Methods in Computer Science \\
 Exercise Sheet 1: Computability and Complexity }

\date{WS 2023/23}

\author{Norbert Tremurici, 11907086}


\begin{document}
\maketitle

\section*{Exercise 1}

%Provide a reduction that gets a graph as input and outputs a propositional formula 
%such that the valid colorings of the graph are in one-to-one correspondence to the models of the propositional formula and one can easily compute the corresponding coloring when given one of the models.

\subsection*{The Reduction}

For each vertex $v \in V$ and each color in $c \in C$ with $C = \{R, G, B\}$ we introduce the following variables:

\begin{itemize}
	\item a coloring function $\kappa(v, c) : V \times C \to L$, where $L$ is the set of literal indices $L = \{1, \dots, 3n + 2\}$, s.t. $\kappa(v, c) = 3v + c$
	\item an inverse coloring function $\kappa^{-1}(l) : \{1, \dots, 3n + 2\} \to (V, C)$, s.t. $\kappa^{-1}(l) = (\frac{l - l \mod 3}{3}, l \mod 3)$
	\item three functions $R(v) : V \to L$, $G(v) : V \to L$ and $B(v) : V \to L$, s.t. $R(v) = 3v + R = 3v + 0$, $G(v) = 3v + G = 3v + 1$ and $B(v) = 3v + B = 3v + 2$
	\item note: we are assuming $V$ to have size $|V| = n$ and to contain vertex indices in the range $\{1, \dots, n\}$ and we are assuming the set of colors $C$ to be equivalent to $\{0, 1, 2\}$
	\item note: we will use $R_v$, $G_v$ and $B_v$ as short-hand notation for $R(v)$, $G(v)$, $B(v)$ and these will be the literals for our formula $\varphi$
\end{itemize}

The basic idea is to expand the set of vertex indices s.t. every index has three corresponding literals, which are a combination of a vertex index and a color index.
If a vertex $v$ is colored (wlog) red, the corresponding literal $R_v$ will be true in an assignment that makes $\varphi$ satisfiable.
\\ [1ex]

We also introduce $E_v = \{ (v, w) \mid (v, w) \in E \} \subset E$ (the set of edges originating from $v$). The reduction:

%{\todo}: \emph{Add your reduction here. One possibility is to introduce for each constraint from the coloring problem a formula $\varphi_i$. The final formula $\varphi$ is then defined as the conjunction of all the formulas $\varphi_i$.\\
%You might want to use notation such as $\land, \lor, \to, \neg$, $\bigwedge_{v\in V}$, $\bigwedge_{(u,v)\in E}$, $\bigvee_{v\in V}$, and $\bigvee_{(u,v)\in E}$. Further, you can indicate as $V_{>2}$ the set of vertices that support more than two vertices. Feel free to define additional notation, if needed.}

\begin{itemize}
	\item Each vertex has exactly one color.
	\[ \varphi_1 = \bigwedge_{v \in V} (R_v \lor G_v \lor B_v) \land (\neg R_v \lor \neg G_v) \land (\neg R_v \lor \neg B_v) \land (\neg G_v \lor \neg B_v) \]	
	\item If vertex $b$ is colored blue, any vertex $a$ that supports $b$ must be either red or green. (Blue can only be supported by red or green.)
	\[ \varphi_2 = \bigwedge_{(a, b) \in E} \neg B_b \lor \neg B_a \]
	\item If vertex $a$ is colored green, then there has to be a vertex $b$ such that $a$ supports $b$ and $b$ is colored blue. (Green must support some blue vertex.)
	\[ \varphi_3 = \bigwedge_{a \in V} (\neg G_a \lor \bigvee_{(a, b) \in E_a} B_b) \]
	\item If a vertex $a$ supports more than $2$ vertices, then one of the vertices supported by $a$ must be green.
	\[ \varphi_4 = \bigwedge_{a \in V_{>2}} \bigvee_{(a, v) \in E_a} G_v \]
	\item At least one vertex must \emph{not} be colored red.
	\[ \varphi_5 = \bigvee_{v \in V} \neg R_v \]
\end{itemize}

We reduce a coloring instance $G=(V,E)$ to the CNF formula

\[ \varphi = \varphi_1 \land \varphi_2 \land \varphi_3 \land \varphi_4 \land \varphi_5 \]

$(V,E)$ has a valid coloring iff $\varphi$ has a model (is satisfiable).

\subsection*{Correctness Argument}

We want to prove that $G = (V, E)$ has a valid coloring iff $\varphi$ has a model (is satisfiable).
Thus we will assume the either of these and derive the correspondence. \\[1ex]

First assume $G$ has a valid coloring (``$\rightarrow$'').
We will show the satisfiability of $\varphi$ by showing the satisfiability of all conjuncts as we constructed them earlier.
We can reiterate the conditions for a valid coloring and examine the rules we provided, under the condition that a literal $l_v$ will be set to true iff its corresponding vertex is colored with the color of the literal:
\\ [.1ex]

\textit{Each vertex has exactly one color.}
We encoded this statement in $\varphi_1$ such that any two of the three corresponding literals $R_v$, $G_v$ and $B_v$ of a vertex $v$ cannot be true at the same time (mutual exclusion).
We can see that $\varphi_1$ is satisfiable only iff exactly one of the three corresponding literals is true for every vertex.
This is satisfiable because a vertex can have only one color.
\\ [.1ex]

\textit{If vertex $b$ is colored blue, any vertex $a$ that supports $b$ must be either red or green. (Blue can only be supported by red or green.)}
Our $\varphi_2$ is equivalent to $\bigwedge_{(a, b) \in E} (B_b \to \neg B_a)$ which the statement that for all edges, the support and the supported cannot be blue at the same time. Because $G$ has a valid coloring, $\varphi_2$ must be satisfiable.
\\ [.1ex]

\textit{If vertex $a$ is colored green, then there has to be a vertex $b$ such that $a$ supports $b$ and $b$ is colored blue. (Green must support some blue vertex.)}
The big disjunction $\bigvee_{(a, b) \in E_a} B_b$ in our formula $\varphi_3$ is equivalent to an existential quantifier $\exists (a, b) \in E_a : B_b$, so our formula could be re-expressed as $\varphi_3 = \bigwedge_{a \in V} (G_a \to \exists (a, b) \in E_a : B_b)$.
Because $G$ has a valid coloring, we know that there must be a supported vertex colored blue for all vertices colored green.
For these support vertices $a$, $G_a$ will be true and for at least one supported vertex $b$ such that $B_b$ will be true.
Thus our formula is satisfiable.
\\ [.1ex]

\textit{If a vertex $a$ supports more than $2$ vertices, then one of the vertices supported by $a$ must be green.}
Our formula $\varphi_4$ restricted itself to the set of vertices supporting more than $2$ vertices, $V_{>2}$.
For every such vertex $a \in V_{>2}$, we consider the edges that originate from $a$, $(a, v) \in E_a$.
Every conjunctive clause contains a disjunction for all the green literals of vertices $v$ supported by $a$.
In a valid coloring, every vertex supported by $a$ must have at least one edge in which the supported vertex $v$ is colored green and thus $\varphi_4$ is satisfiable.
\\ [.1ex]

\textit{At least one vertex must \emph{not} be colored red.}
We know that there exists at least one vertex $v$ such that $v$ is not red.
Then $R_v$ if false and thus $\varphi_5 = \bigvee_{u \in V} \neg R_u$ must be true.
\\ [1ex]

Now assume $\varphi$ is satisfiable (``$\leftarrow$'').
We can construct a coloring of $G$ in which we color every vertex $v$ to a color iff the corresponding literal $l_v$ has been set to true, e.g. $R_v \to v$ set to red.
Now we have to prove that the properties of a valid coloring a preserved.
\\ [.1ex]

\textit{Each vertex has exactly one color.}
Our formula specifies mutual exclusion of literals $R_v$, $G_v$, $B_v$ for all vertices $v$.
Thus we can construct an unambiguous coloring of $v$.
\\ [.1ex]

\textit{If vertex $b$ is colored blue, any vertex $a$ that supports $b$ must be either red or green. (Blue can only be supported by red or green.)}
For all such vertices $b$ we know $B_b$ is true.
Our formula is a big conjunction of implications of the form $B_b \to \neg B_a$ for all supported vertices $a$, so we know no such $B_a$ can be true.
We color all such $b$ blue and avoid coloring any such $a$ blue.
\\ [.1ex]

\textit{If vertex $a$ is colored green, then there has to be a vertex $b$ such that $a$ supports $b$ and $b$ is colored blue. (Green must support some blue vertex.)}
We have argued before that the formula $\varphi_3$ encodes an implication with an existential quantifier.
We know that for all such $a$, $G_a$ is true and thus there must exist a $b$ such that $B_b$ is true.
We can simply color $a$ green and $b$ blue.
\\ [.1ex]

\textit{If a vertex $a$ supports more than $2$ vertices, then one of the vertices supported by $a$ must be green.}
For all such vertices $a$, there is a corresponding clause in which a big disjunction forces at least one of the supported vertices $b$ to have its blue literal $B_b$ evaluate to true.
We can simply color the corresponding vertices $b$ blue.
\\ [.1ex]

\textit{At least one vertex must \emph{not} be colored red.}
There will be at least one vertex $v$ such that $R_v$ is true for $\varphi_5$ to be satisfiable, we can simply color this vertex red.
\\ [.1ex]

Finally we will make clear, it cannot be the case that all formulas $\varphi_i$ are satisfiable but in the coloring we construct any two of the conditions conflict with each other.
In such a case, $\varphi_i$ would not have been satisfiable, which is a consequence the conjunction of all formulas $\varphi_i$.
It could be however, that not all vertices are \textit{forced} to a color by the more specific properties of a valid coloring, but in this case we are free to choose any color, provided we choose only one and already have a vertex not colored red.

\section*{Exercise 2}

%Now assume your are given a set of vertices $B \subseteq V$ which have to be colored blue. Extend your reduction from Exercise 1 such that it only returns valid colorings which color all vertices in $B$ blue.
%Again, this reduction should be such that the valid colorings of the graph which color all vertices in $B$ blue are in one-to-one correspondence to the models of the propositional formula and one can easily compute the corresponding coloring when given one of the models.

\subsection*{The Reduction}

We are given the additional set $B$ that further constrains a possible solution because all $b \in B$ must to be colored blue.
Thus we can extend our previous solution by adding an additional sub-formula to the CNF $\varphi$.

$\varphi$ from Exercise 1 is extended by the formula

\[ \varphi_6 = \bigwedge_{b \in B} B_b \]

We reduce a coloring instance $(G=(V,E), B)$ to the CNF formula

\[ \varphi' = \varphi \land \varphi_6 \]

$(V,E)$ has a valid coloring such that all vertices in $B$ are colored blue iff $\varphi'$ has a model (is satisfiable).

\subsection*{Correctness Argument}

Again, we argue for both sides of the 1-to-1 correspondence by assuming only one of the premises to be true.

First assume $G$ has a valid coloring (``$\rightarrow$'').
We already know that in this case, $\varphi$ constructed from $G$ must be satisfiable.
Furthermore we know all vertices $b \in B \subset V'$ have been colored blue.
This is a direct correspondence to forcing literals $B_b$ to be true by adding them as unit clauses to the CNF $\varphi$.
Because the valid coloring of $G$ colored them blue, we know that each unit clause $B_b$ must evaluate to true.
Insofar as the restriction on vertices $b \in B$ has not made the other colorability conditions unfulfillable, the other clauses $\varphi_i$ must still be satisfiable.
Thus $\varphi'$ is still satisfiable.

Now assume $\varphi'$ is satisfiable (``$\leftarrow$'').
We know that $\varphi$, which is just part of the CNF $\varphi'$, must be satisfiable.
We also know that $\varphi_6$ must be satisfiable.
From these two facts we can infer that the original colorability conditions can be met as a valid coloring for $G$ resulting from $\varphi$, but also that all $b \in B$ can be colored blue resulting from $\varphi_6$.
Thus $G$ with the extended condition must still be colorable.

\section*{Exercise 3}
%In Exercise 2, we wanted to color all vertices in a given set blue. In this exercise,
%given a valid coloring $C$ which colors a set of vertices $S$ blue, we are interested in checking whether this set is maximal,
%i.e., whether we can color further vertices $v \in V, v \not\in S$ blue as well.
%If there is no such coloring, we call $C$ a blue-maximal coloring. More precisely:

%   Let $C$ be a valid coloring and let $S$ be the set of vertices that $C$ colors blue. We say that $C$ is \emph{blue-maximal}
%   if there is no other valid coloring $C^\prime$ that colors a set $S^\prime\supset S$ of vertices blue.

%Note that in the above definition, we do not require $C^\prime$ to color the vertices outside of $S^\prime$ in the same color as the original coloring $C$ does.

% Provide a reduction that takes an instance of the above problem (a graph $G$ and a valid coloring $C$ for $G$) as input and provides a propositional formula such that the formula is unsatisfiable if and only if $C$ is blue-maximal. 
%Again, this reduction should be such that one can easily obtain a coloring from a model of the formula, i.e., a counterexample $C^\prime$ for the blue-maximality of $C$.\\[1ex]

\subsection*{The Reduction}

$\varphi$ from Exercise 1 is extended by the formula

\[ \varphi_7 = \bigwedge_{s \in S} B_s \land \bigvee_{v \in V \setminus S} B_v \]

We reduce a max-coloring instance $(G=(V,E), C)$ to the CNF formula

\[ \varphi'' = \varphi \land \varphi_7 \]

$\varphi''$ is unsatisfiable iff $C$ is a blue-maximal coloring in $G$.

\subsection*{Correctness Argument}

Again, we argue for both sides of the 1-to-1 correspondence by assuming only one of the premises to be true.
\\ [.1ex]

First assume $C$ is a blue-maximal coloring in $G$ (``$\rightarrow$'').
We know from our previous proof that the resulting formula $\varphi$ must be satisfiable.
The introduction of $\varphi_7$ could make the formula unsatisfiable however, so we should examine whether this is the case.
Now apply an iteration of the blue-maximality algorithm by taking the vertices $s \in S \subset V$ for all vertices colored blue in $C$.
Each vertex will be added as a blue unit clause $B_s$ to $\varphi_7$, but they are already satisfied and will remain satisfied, which must be so because blue-maximality is defined with respect to set inclusion.
The remaining big disjunct of all vertices $\bigvee_{v \in V \setminus S} B_v$ is either satisfiable or not.
It it is not, then we know that for $\varphi$ no vertex that was not already colored blue can be colored blue (we know this by way of the previously showed correctness of the general reduction from $G$ to $\varphi$) (this case is fine).
If it is, then it means that there exists a blue literal that can be set to true and was not already set to true.
Because of our construction, this translates to a vertex that we could have colored blue but did not, but this contradicts our assumption that $C$ is already a blue-maximal coloring in $G$.
\\ [.1ex]

Next up, assume $\varphi''$ is unsatisfiable (``$\leftarrow$'').
We still require $\varphi$ to be satisfiable (if $\varphi$ is unsatisfiable, then there is no valid coloring for $G$).
Thus we know that $\varphi_7$ must be unsatisfiable, but also that there exists a valid coloring for $G$ (that is not necessarily blue-maximal).
Now we assume that the coloring $C$ resulting from $\varphi$ is not blue-maximal, that means that there must exist a vertex $v$, the color of which can be changed to blue.
We know that $v \not \in S$, if we take $S$ to be the set of vertices colored blue in $C$, but $v \in V \setminus S$.
Thus the blue literal of $v$ (any such vertex) cannot be a unit clause in $\varphi_7$.
But the blue literal of $v$ is contained in the big disjunction $\bigvee_{v \in V \setminus S} B_v$.
For $\varphi_7$ to be unsatisfiable, it would mean that no such literal can be set to true.
But we by assumption we know that $C$ is not blue-maximal and $v$ specifically can be colored blue.
The disjunction must be satisfiable due to $B_v$, the unit clauses must already be satisfiable (by construction) and $\varphi$ must also be satisfiable because a valid coloring exists.
Our original assumptions were wrong and this case is impossible, $\varphi''$ is unsatisfiable and the coloring $C$ of $G$ is blue-maximal.

\section*{Encoding the Variables}

To use the SAT-solver, we have to encode the variables (propositional atoms) used in our reduction to integers. In the following table, sketch how your encoding works.\\[1ex]

We can assume $V = \{1, \dots, n\}$:

  \begin{center}
    \begin{tabular}{c | c | c | c}
      Variable & Vertex & Color & Encoding\\
      \hline
      \emph{$R_1$} & 1 & R & \emph{1}\\
      \emph{$G_1$} & 1 & G & \emph{2}\\
      \emph{$B_1$} & 1 & B & \emph{3}\\
      \emph{$R_2$} & 2 & R & \emph{4}\\
      \ldots & \ldots 
    \end{tabular}
  \end{center}
  
\section*{Testing the Code}  

To test the code, the existing graphs were observed and the results manually verified to fulfill the necessary conditions.
Tests were performed for all parts of the exercise we had to implement.
Additional test graphs were added and the implementation tested against them.

The first additional test was a star graph, but with forwards and backwards edges.
The center vertex intentionally has all the connections, while the outer vertices have just one connection back.
This forces the center vertex to support a green vertex, which in turn forces the center vertex to be blue.
This test not only tests for correctness, but also whether the iterative blue-maximality algorithm works as intended.

The second test was an impossible graph.
For this, we chose the Petersen graph, which is quite interconnected.
There is not solution for this graph, as the algorithm correctly points out.

Finally, we wanted another positive result in which we could easily verify if blue-maximality is truly achieved.
For this we chose the friendship graph $F_i$, which consists of a center vertex that connects to $i$ 3-cycles.
We used $F_5$, so there are 5 3-cycles in which the center vertex is always contained.
In this structure, every cycle should be able to support exactly one blue vertex and running our algorithm we can see that this is the case.

Some manual debugging was of course also performed.

We are confident of the correctness of our code insofar the translation of the reduction described thus far has been implemented correctly.
  
\end{document}