# Practical Access to Dynamic Programming on Tree Decompositions +
## 3 An Interface for Dynamic Programming on Tree Decompositions
### Example: 3-Coloring
\(v\in X\) is the last vertex of the bag that is contained in \(X\), then the connected component is \"done\", the corresponding bits are cleared and one additional bit is set to indicate that the connected component cannot be extended anymore. When an edge \(\{u,v\}\) is introduced, components might need to be merged. Assume \(u,v\in X\), \(u\in P_{i}\), and \(v\in P_{j}\) with \(i<j\) (otherwise, an edge-bag does not change the state), then we essentially perform a classical union-operation from the well-known union-find data structure. Hence, we assign all vertices that are assigned to \(P_{i}\) to \(P_{i}\). Finally, at a join-bag, we may join two states that agree locally on the vertices that are in \(X\) (that is, they have assigned the same vertices to some \(P_{i}\)); however, they do not have to agree in the way the different vertices are assigned to \(P_{i}\) (in fact, there does not have to be an isomorphism between these assignments). Therefore, the transition at a join-bag has to connect the corresponding components analogous to the edge-bags--in terms of Section 3.1, this transition is not symmetric. The description of the remaining quantifiers and subformulas is very similar and summarized in the following overview: \begin{tabular}{|l l|} \hline \(\exists^{\text{forest}}X\) & \\ \hline \#Bit: & \(k\cdot\log k\) \\ Introduce: & As for \(\exists^{\text{connected}}X\). \\  & Just clear the corresponding bits. \\  & As for \(\exists^{\text{connected}}X\), but reject \\ Edge: & if two vertices of the same \\  & component are connected. \\  & As for \(\exists^{\text{connected}}X\), but track \\  & if the join introduces a cycle. \\ \hline \end{tabular} \begin{tabular}{|l l|} \hline \(\forall x\forall y\ E(x,y)\rightarrow\chi_{i}\) \\ \hline \#Bit: & 0 \\ Introduce: & - \\ Forget: & - \\ Edge: & Reject if \(\chi_{i}\) is not satisfied for \\  & the vertices of the edge. \\ Join: & - \\ \hline \end{tabular} 

### Extending the Model Checker to Optimization Problems

As the example formulas from the previous section already indicate, performing model checking alone will not suffice to express many natural problems. In fact, every graph is a model of the formula \(\bar{\phi}_{\text{vc}}\) if \(S\) simply contains all vertices. It is therefore a natural extension to consider an optimization version of the model checking problem, which is usually formulated as follows [1; 10]: Given a logical structure \(\mathcal{S}\), a formula \(\phi(X_{1},\ldots,X_{p})\) of the MSO-fragment defined in the previous section with free unary second-order variables \(X_{1},\ldots,X_{p}\), and weight functions \(\omega_{1},\ldots,\omega_{p}\) with \(\omega_{i}\colon U\to\mathbb{Z}\); find \(S_{1},\ldots,S_{p}\) with \(S_{i}\subseteq U\) such that \(\sum_{i=1}^{p}\sum_{s\in S_{i}}\omega_{i}(s)\) is _minimized_ under \(\mathcal{S}\models\phi(S_{1},\ldots,S_{p})\), or conclude that \(\mathcal{S}\) is not a model for \(\phi\) for any assignment of the free variables. We can now correctly express the (actually _weighted_) optimization version of vertex-cover as follows:

\[\phi_{\text{vc}}(S)=\forall x\forall y\ E(x,y)\to\big{(}S(x)\lor S(y)\big{)}.\]

Similarly, we can describe the optimization version of dominating-set if we assume the input does not have isolated vertices (or is reflexive), and we can also fix the formula \(\bar{\phi}_{\text{fvs}}\):

\[\phi_{\text{ds}}(S) =\forall x\exists y\ E(x,y)\wedge\big{(}S(x)\lor S(y)\big{)},\] \[\phi_{\text{fvs}}(S) =\exists^{\text{forest}}F\ \forall x\ \big{(}S(x)\lor F(x)\big{)}.\]

We can also _maximize_ the term \(\sum_{i=1}^{p}\sum_{s\in S_{i}}\omega_{i}(s)\) by multiplying all weights with \(-1\) and, thus, express problems such as independent-set:

\[\phi_{\text{is}}(S)=\forall x\forall y\ E(x,y)\to\big{(}\
eg S(x)\lor\
eg S( y)\big{)}.\]

The implementation of such an optimization is straightforward: there is a 2-partition quantifier for every free variable \(X_{i}\) that partitions the universe into \(X_{i}\) and \(\bar{X}_{i}\).