123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281 |
- \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}
|