diff --git a/sheets/03_card_sat/DBST/README.md b/sheets/03_card_sat/DBST/README.md index 64d636733a4563fb897367beb7433e15af991d15..458f52f05347f9e4d09db250ae8569d42dc7b0ee 100644 --- a/sheets/03_card_sat/DBST/README.md +++ b/sheets/03_card_sat/DBST/README.md @@ -16,7 +16,7 @@ There are multiple challenges, we are going to address one after the other. ### Optimization vs. Decision Problem While the DBST is an optimization problem, SAT is a pure decision problem. -A SAT-solver does not find the optimal solution but just returns as any feasible assignment. +A SAT-solver does not find the optimal solution but just returns any feasible assignment. To still obtain an optimal solution with a SAT-solver (instead of just any feasible), we use it repeatedly instead of just once. We transform the optimization problem into its corresponding decision problem. Instead of asking the SAT-solver *"What is the spanning tree with maximum degree $d$ and shortest possible longest edge?"*, @@ -32,17 +32,17 @@ This allows us to find the optimal solution by asking (i.e., running the SAT-sol We want a tree on a given set of vertices $V$. Thus, we are looking for a subset of edges. -The set of all edfges is given by $E = \{vw \mid v,w \in V\}$. +The set of all edges is given by $E = \{vw \mid v,w \in V\}$. Given a bound $b$ for question (Q) on the weight of the longest edge, only edges of $E(b) = \{vw \mid v,w \in V, d(v,w) \leq b\}$ are feasible. -To answer our question (Q) of specific $b$, we are looking for any subset $E'\subseteq E(b)$ that contains a tree with a maximum degree of at most $d$ that spans $V$. -Such a subset can be encoded by introducing for every $e\in E(b)$ a boolean variable that is $\texttt{true}$ if and only if $e$ is in $E'$. +To answer our question (Q) for specific $b$, we are looking for any subset $E'\subseteq E(b)$ that contains a tree with a maximum degree of at most $d$ that spans $V$. +Such a subset can be encoded by introducing a boolean variable for every $e\in E(b)$ that is $\texttt{true}$ if and only if $e$ is in $E'$. If we are able to express, via clauses and cardinality constraints, that $E'$ 1. has at most degree $b$, and 2. is a spanning tree on $V$ -we can answer our question (Q) with a SAT-solver (and solve the optimization problem by repeated applications of it). +we can answer our question (Q) with a SAT-solver (and solve the optimization problem by repeated applications of it). ### Degree constraint @@ -63,7 +63,7 @@ Thus, we want to ensure that the graph is connected and free of cycles. A fundamental observation is that every tree on $n$ vertices has exactly $n-1$ edges. Thus, we can define the cardinality constraint ```math -\sum\limits_{e \in E(b)} x_e \leq n-1\text{ und } \sum\limits_{e \in E(b)}\bar{x}_e \leq |E(b)| - n + 1 +\sum\limits_{e \in E(b)} x_e \leq n-1\text{ and } \sum\limits_{e \in E(b)}\bar{x}_e \leq |E(b)| - n + 1 ``` to deal with that. @@ -80,8 +80,8 @@ For every real and non-empty subset $S \subsetneq V$ of vertices, we introduce a Unfortunately, there are exponentially many such subsets $S$ and it is no option to just add all of them directly to the SAT-formula. However, only a small amount of these subsets will actually be relevant and we can instead do the following: Start without these constraints and look onto the assignment returned by the SAT-solver. -If is is connected, we are fine. -If it is not connected, we can easily add the clause for any connected component $S \in \{V_1,\ldots,V_k\}$ in the solution and run the SAT-solver again. +If it is connected, we are fine. +If it is not connected, we can easily add the clause for any connected component $S \in \{V_1,\ldots,V_k\}$ in the solution and run the SAT-solver again. We can repeat this until the returned solution is connected or the SAT-solver tells us that the formula has become infeasible. This may sound inefficient but many SAT-solvers allow incremental formula building and will save the insights the gained on the previous formula. No assignment that has already been discarded by the previous runs can become feasible ever again, making solving the slightly refined formula (often) very fast to solve.