diff --git a/sheets/03_card_sat/DBST/README.md b/sheets/03_card_sat/DBST/README.md new file mode 100644 index 0000000000000000000000000000000000000000..c1c557498be38b456368e7e6176a874bfcdd3d71 --- /dev/null +++ b/sheets/03_card_sat/DBST/README.md @@ -0,0 +1,85 @@ +# Solving the Degree-Constrained Bottleneck Spanning Tree Problem with a (cardinality) SAT solver + +## Problem Definition + +In the NP-hard *Degree-Constrained Bottleneck Spanning Tree (DBST)*, +we are given a complete graph $G=(V,E)$ with distance/weight function $dist: E \rightarrow \mathbb{N}^+_0$. +The set $V$ can be a set of point on the plane, and $dist(v,w)$ the euclidean distance between $v\in V$ and $w\in V$. +Additionally, we have a degree constraint $d\geq 2$. +The objective is to find a tree $T$ in $G$ in which no vertex has a degree greater the degree constraint, i.e., $\forall v\in V: deg_T(v)\leq d$, and the weight of the longest edge is minimized. + +## Modelling the DBST + +How can we optimize the DBST with only a SAT-solver? +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. +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?"*, +we ask it (Q) *"Is there a spanning tree with maximum degree $d$, whose longest edge has a weight of at most $b$?"*. + +A very useful observation is that the objective value (bottleneck) always equals the weight of a single edge, thus, +there are only $\mathcal{O}(n^2)$ different values to check. +Instead of randomly checking all, we first sort all these values and put them into a list on which we could apply a binary search. +This allows us to find the optimal solution by asking (i.e., running the SAT-solver) $\mathcal{O}(\log n)$ times the question (Q). + + +### Selection of variables + +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\}$. +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'$. + +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). + +### Degree constraint + +The degree constraint is the easiest to enforce, so we take care of that one first. +For a vertex $v\in V$, let $\delta_b(v) = \{vw \mid w \in V, vw\in E(b)\}$ be the edges in $E(b)$ that are incident to $v$. +We have to express that at most $b$ of them are allowed to be used. +Using a cardinality constraint, this is straight-forward: + +```math +\sum\limits_{e \in \delta_b(v)} x_e \leq d. +``` + +### Spanning tree + +Abschließend müssen wir noch erzwingen, dass der durch $E'$ aufgespannte Graph ein Baum ist. +Wir wollen also sicherstellen, dass der Graph zusammenhängend und kreisfrei ist. + +Dazu beobachten wir, dass alle Bäume auf $n$ Knoten genau $n-1$ Kanten haben. +Wir können also die Kardinalitätsbedingungen +\[\sum\limits_{e \in E(x)} x_e \leq n-1\text{ und } \sum\limits_{e \in E(x)}\bar{x}_e \leq |E(x)| - n + 1\] +einführen, um sicherzustellen, dass die gewählte Kantenmenge genau $n-1$ Kanten enthält. +Außerdem gilt, dass Graphen mit $n-1$ Kanten genau dann kreisfrei sind, wenn sie zusammenhängend sind. + +Daher brauchen wir nur eine dieser Eigenschaften zu modellieren. +Es gibt grundsätzlich verschiedene Möglichkeiten, Zusammenhang zu modellieren; siehe dazu auch den Abschnitt \nameref{sec:aufgaben}. + +Die einfachste Methode, die wir in unserem Beispiel verwenden, funktioniert wie folgt. +Für jede echte, nicht-leere Teilmenge $S \subsetneq V$ der Knoten fügen wir eine Klausel hinzu, +die sicherstellt, dass wenigstens eine Kante von einem Knoten in $S$ zu einem Knoten in $V \setminus S$ führt: +\[ \forall \emptyset \subsetneq S \subsetneq V: \bigvee\limits_{v \in S, w \notin S} x_{vw}. \] +Es gibt allerdings exponentiell viele solche Teilmengen $S$. +Daher ist es keine Option, diese einfach alle bei der Erzeugung der SAT-Formel hinzuzufügen. +In der Hoffnung, dass nur wenige dieser Teilmengen tatsächlich benötigt werden, +kann man allerdings wie folgt vorgehen. +Man löst zunächst ohne solche Bedingungen. +Falls dabei eine nicht zusammenhängende Lösung herauskommt, kann man die Zusammenhangskomponenten $V_1,\ldots,V_k$ dieser Lösung bestimmen. +Für jede Zusammenhangskomponente $S \in \{V_1,\ldots,V_k\}$ kann man dann eine Klausel der obigen Form hinzufügen, um sie in Zukunft zu verbieten, und daraufhin erneut lösen. +Dies wiederholt man so lange, bis eine zusammenhängende Lösung gefunden wird oder keine Lösung mehr existiert; +das geht in der Regel relativ schnell, weil der SAT-Solver einige Informationen zwischen den einzelnen Aufrufen zwischenspeichert. + diff --git a/sheets/03_card_sat/README.md b/sheets/03_card_sat/README.md index 4a27ed48b7b27b63397984c0645c4eeb62a581a7..0935623c1122ad96e35d3ff0821deea93963a0db 100644 --- a/sheets/03_card_sat/README.md +++ b/sheets/03_card_sat/README.md @@ -13,13 +13,16 @@ The boolean satisfiability problem (Satisfiability, SAT) is the first proved NP- In this problem, we are given propositional formula $\phi$ on a set of boolean variables $\{x_1, \ldots, x_n\}$ in [conjunctive normal form](https://en.wikipedia.org/wiki/Conjunctive_normal_form). Such a formula has the following form: -\[\phi = \underbrace{(\ell_{1,1} \vee \cdots \vee \ell_{1,k_1})}_{\text{Klausel 1}} \wedge \cdots \wedge \underbrace{(\ell_{m,1} \vee \cdots \vee \ell_{m,k_m})}_{\text{Klausel $m$}}.\] +```math +\phi = \underbrace{(\ell_{1,1} \vee \cdots \vee \ell_{1,k_1})}_{\text{Klausel 1}} \wedge \cdots \wedge \underbrace{(\ell_{m,1} \vee \cdots \vee \ell_{m,k_m})}_{\text{Klausel $m$}}. +``` The $\ell_{i,j}$ are so called *literals* and have either the form $x_u$ or $\bar{x}_u := \neg x_u$, i.e., they are either a variable or a negation of it. The formula $\phi$, thus, is a conjunction (AND-connections) of clauses, which are disjunction (OR-connections) of variables or negated variables. And example for such a formula would be -\[ \phi_1 = (x_1 \vee \bar{x}_2 \vee x_3) \wedge (x_2 \vee x_4). \] - +```math +\phi_1 = (x_1 \vee \bar{x}_2 \vee x_3) \wedge (x_2 \vee x_4). +``` The boolean satisfiability problem asks if a given formula $\phi$ is *satisfiable$. A formula is satisfiable if there is a *satifying assignment*, @@ -63,9 +66,17 @@ Thus, for every variable $i$ we will either have $i$ in the returned list if the When modelling some problem with boolean formulas, a frequent challenge is to model some cardinality constraints, i.e., from a set $L$ of literals, only at most $k$ are allowed to be satisfied. For example, a tree should have at most $n-1$ edges selected. If we interpret $\texttt{false}=0$ and $\texttt{true}=1$ (as commonly done in most programming languages), we can write these constraints as -\[\sum\limits_{\ell \in L} \ell \leq k\] +```math +\sum\limits_{\ell \in L} \ell \leq k +``` Such a constraint is called *cardinality constraint*. As this is a very common constraint, some SAT-solvers (e.g., the previously used *Gluecard4*) support them directly (on top of the classical conjunctive normal form). There are also automatic encodings that can convert cardinality constraints, but this is usually less efficient than telling the solver directly about the cardinality constraint, allowing it to use specialized algorithms. + + +## Beispielproblem: Gradbeschränkter Bottleneck Spanning Tree + +To illustrate this technique, without directly giving you the solution for the BTSP, we again look onto how to solve the Degree-Constrained Bottlneck Spanning Tree (DBST). +