# Practical Access to Dynamic Programming on Tree Decompositions +
## 3 An Interface for Dynamic Programming on Tree Decompositions
### Example: 3-Coloring
For instance, the feedback-vertex-set problem can be described by the following formula (again, optimization will be handled in Section 4.4):

\[\tilde{\phi}_{\text{fvs}}=\exists S\,\exists^{\text{forest}}F\,\forall x\ S(x) \lor F(x).\]

### Description of the Model Checker

We describe our model checker in terms of a nondeterministic tree automaton that works on a tree decomposition of the graph induced by \(E^{2}\) (note that, in contrast to other approaches in the literature (see, for instance, [10]), we do not work on the Gaifman graph). We define any state of the automaton as a bit-vector, and we stipulate that the initial state at every leaf is the zero-vector. For any quantifier or subformula, there will be some area in the bit-vector reserved for that quantifier or subformula and we describe how state transitions effect these bits. The \"algorithmic idea\" behind the implementation of these transitions is not new, and a reader familiar with folklore dynamic programs on tree decompositions (for instance for vertex-cover or steiner-tree) will probably recognize them. An overview over common techniques can be found in the standard textbooks [1; 10]. #### 4.3.1 The Partition Quantifier

We start with a detailed description of the \(k\)-partition quantifier \(\exists^{\text{partition}}X_{1},\ldots,X_{q}\) (in fact, we do not implement an additional \(\exists X\) quantifier, as we can always state \(\exists X\equiv\exists^{\text{partition}}X,\bar{X}\)): Let \(k\) be the maximum bag-size of the tree decomposition. We reserve \(k\cdot\log_{2}q\) bit in the state description (Here, and in the following, \(\log(x)\) denotes the number of bits to store \(x\), i. e., \(\log(x)=\lfloor\log_{2}(x)\rfloor+1\)), where each block of length \(\log q\) indicates in which set \(X_{i}\) the corresponding element of the bag is. On an introduce-bag (e. g., for \(v\in U\)), the nondeterministic automaton guesses an index \(i\in\{1,\ldots,q\}\) and sets the \(\log q\) bits that are associated with the tree-index of \(v\) to \(i\). Equivalently, the corresponding bits are cleared when the automaton reaches a forget-bag. As the partition is independent of any edges,an edge-bag does not change any of the bits reserved for the \(k\)-partition quantifier. Finally, on join-bags, we may only join states that are identical on the bits describing the partition (as otherwise the vertices of the bag would be in different partitions)--meaning this transition is symmetric with respect to these bits (in terms of Section 3.1). #### 4.3.2 The Connected Quantifier

The next quantifier we describe is \(\exists^{\text{connected}}X\), which has to overcome the difficulty that an introduced vertex may not be connected to the rest of the bag in the moment it got introduced, but may be connected to it when further vertices \"arrive.\" The solution to this dilemma is to manage a partition of the bag into \(k^{\prime}\leq k\) connected components \(P_{1},\ldots,P_{k^{\prime}}\), for which we reserve \(k\cdot\log k\) bit in the state description. Whenever a vertex \(v\) is introduced, the automaton either guesses that it is not contained in \(X\) and clears the corresponding bits, or it guesses that \(v\in X\) and assigns some \(P_{i}\) to \(v\). Since \(v\) is isolated in the bag in the moment of its introduction (recall that we work on a very nice tree decomposition), it requires its own component and is therefore assigned to the smallest empty partition \(P_{i}\). When a vertex \(v\) is forgotten, there are four possible scenarios:

1. \(v\
ot\in X\), then the corresponding bits are already cleared and nothing happens;
2. \(v\in X\) and \(v\in P_{i}\) with \(|P_{i}|>1\), then \(v\) is just removed and the corresponding bits are cleared;
3. \(v\in X\) and \(v\in P_{i}\) with \(|P_{i}|=1\) and there are other vertices \(w\) in the bag with \(w\in X\), then the automaton rejects the configuration, as \(v\) is the last vertex of \(P_{i}\) and may not be connected to any other partition anymore;
4.