@@ -57,29 +57,31 @@ Using a cardinality constraint, this is straight-forward:
### 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.
Finally, we have to enforce that the graph induced by $E'$ is a spanning tree on $V$.
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
```
to deal with that.
Additionally, it is well known that a graph with $n$ vertices and $n-1$ edges is free of cycles if and only if it is connected.
Instead of prohibiting cycles we can alternatively enforce the graph to be connected.
In general, there are multiple options to model connectivity.
The simplest method, we are going to use in this example, is as follows.
For every real and non-empty subset $S \subsetneq V$ of vertices, we introduce a clause that enforces to have at least on edge connecting $S$ with $V\setminus S$.
```math
\forall \emptyset \subsetneq S \subsetneq V: \bigvee\limits_{v \in S, w \notin S} x_{vw}.
```
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.
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.
