# Practical Access to Dynamic Programming on Tree Decompositions +
## 3 An Interface for Dynamic Programming on Tree Decompositions
### Example: 3-Coloring
### Description of the Used MSO-Fragment

We only consider vocabularies \(\tau\) that contain the binary relation \(E^{2}\), and we only consider \(\tau\)-structures with a symmetric interpretation of \(E^{2}\), that is, we only consider structures that contain an undirected graph (but may also contain further relations). The fragment of MSO that we consider is constituted by formulas of the form \(\phi=\exists X_{1}\ldots\exists X_{k}\bigwedge_{i=1}^{n}\psi_{i}\), where the \(X_{j}\) are second-order variables and the \(\psi_{i}\) are first-order formulas of the form

\[\psi_{i}\in\{ \forall x\forall y\ E(x,y)\to\chi_{i},\ \forall x\exists y\ E(x,y)\wedge\chi_{i},\ \exists x \forall y\ E(x,y)\to\chi_{i},\] \[\exists x\exists y\ E(x,y)\wedge\chi_{i},\ \forall x\ \chi_{i},\ \exists x\ \chi_{i}\,\}.\]

Here, the \(\chi_{i}\) are quantifier-free first-order formulas in canonical normal form. It is easy to see that this fragment is already powerful enough to encode many classical problems as 3-coloring (\(\tilde{\phi}_{\text{\sc sol}}\) from the introduction is part of the fragment), or vertex-cover (note that, in this form, the formula is not very useful--every graph is a model of the formula if we choose \(S=V(G)\); we will discuss how to handle optimization in Section 4.4):

\[\tilde{\phi}_{\text{\sc vc}}=\exists S\forall x\forall y\ E(x,y)\to S(x) \lor S(y).\]

### A Syntactic Extension of the Fragment

Many interesting properties, such as connectivity, can easily be expressed in MSO, but not directly in the fragment that we study. Nevertheless, a lot of these properties can directly be checked by a model checker if it \"knows\" what kind of properties it actually checks. We present a _syntactic extension_ of our MSO-fragment which captures such properties. The extension consists of three new second order quantifiers that can be used instead of \(\exists X_{i}\). The first extension is a _\(k\)-partition quantifier_, which quantifies over partitions of the universe:

\[\exists^{\text{partition}}X_{1},\ldots,X_{k}\equiv\exists X_{1}\exists X_{2} \ldots\exists X_{k}\big{(}\forall x\ \bigvee_{i=1}^{k}X_{i}(x)\big{)}\wedge\big{(}\forall x\ \bigwedge_{i=1}^{k}\bigwedge_{j\
eq i}\
eg X_{i}(x)\wedge\
eg X_{j}(x)\big{)}.\]

This quantifier has two advantages. First, formulas like \(\tilde{\phi}_{\text{3 col}}\) can be simplified to

\[\phi_{\text{3 col}}=\exists^{\text{partition}}R,G,B\ \forall x\forall y\ E(x,y) \rightarrow\bigwedge\
eg C(x)\vee\
eg C(y),\]

and, second, the model checking problem for them can be solved more efficiently: the solver directly \"knows\" that a vertex must be added to exactly one of the sets. We further introduce two quantifiers that work with respect to the symmetric relation \(E^{2}\) (recall that we only consider structures that contain such a relation). The \(\exists^{\text{connected}}X\) quantifier guesses an \(X\subseteq U\) that is connected with respect to \(E\) (in graph theoretic terms), that is, it quantifies over connected subgraphs. The \(\exists^{\text{forest}}F\) quantifier guesses a \(F\subseteq U\) that is acyclic with respect to \(E\) (again in graph theoretic terms), that is, it quantifies over subgraphs that are forests. These quantifiers are quite powerful and allow, for instance, expressing that the graph induced by \(E^{2}\) contains a triangle as minor:

\[\phi_{\text{triangle-minor}}= \exists^{\text{connected}}R\ \exists^{\text{connected}}G\ \supseteq^{\text{connected}}B\.\] \[\big{(}\forall x\,(\
eg R(x)\vee\
eg G(x))\wedge(\
eg G(x) \vee\
eg B(x))\wedge(\
eg B(x)\vee\
eg R(x))\big{)}\] \[\wedge\big{(}\exists x\exists y\ E(x,y)\wedge R(x)\wedge G(y)\big{)} \wedge\big{(}\exists x\exists y\ E(x,y)\wedge G(x)\wedge B(y)\big{)}\] \[\wedge\big{(}\exists x\exists y\ E(x,y)\wedge B(x)\wedge R(y)\big{)}.\]

We can also express problems that usually require more involved formulas in a very natural way.