# Practical Access to Dynamic Programming on Tree Decompositions +
## 3 An Interface for Dynamic Programming on Tree Decompositions
### Example: 3-Coloring  
Let us illustrate the usage of the interface with our running example of 3-coloring. A State of the automaton can be modeled as a simple integer array that stores a color (an integer) for every vertex in the bag. A StateVector stores a set of State objects, that is, essentially a set of integer arrays. Introducing a vertex \(v\) to a StateVector therefore means that three duplicates of each stored state have to be created, and, for every duplicate, a different color has to be assigned to \(v\). Listing 2 illustrates how this operation could be realized in Java. ``` Listing 2: Exemplary implementation of the introduce method for 3-coloring. In the listing, the variable states is stored by the StateVector object and represents all currently possible states. ```
StateVector<T>introduce(Bag<T>b,Tv,Map<T,Integer>idx){ Set<State>newStates=newHashSet<>(); for(Statestate:states){//'states'isthesetofstates'} for(intcolor=1;color<=3;color++){ StatenewState=newState(state);//copythestate newState.colors[idx.get(v)]=color; newStates.add(newState); } } states=newStates; returnthis; }
```

The three other methods can be implemented in a very similar fashion: in the forget-method, we set the color of \(v\) to 0; in the edge-method, we remove states in which both endpoints of the edge have the same color; and, in the join-method, we compute the intersection of the state sets of both StateVector objects. Note that, when we forget a vertex \(v\), multiple states may become identical, which is handled here by the implementation of the Java Set-class, which takes care of duplicates automatically. A reference implementation of this 3-coloring solver is publicly available [12], and a detailed description of it can be found in the manual of Jdrasil [13]. Note that this implementation is only meant to illustrate the interface and that we did not make any effort to optimize it. Nevertheless, this very simple implementation (the part of the program that is responsible for the dynamic program only contains about 120 lines of structured Java-code) performs surprisingly well. ## 4 A Lightweight Model Checker for an MSO-Fragment

Experiments with the coloring solver of the previous section have shown a huge difference in the performance of general solvers as D-Flat and Sequoia against a concrete implementation of a tree automaton for a specific problem (see Section 5). This is not necessarily surprising, as a general solver needs to keep track of way more information. In fact, an MSO model checker on formula \(\phi\) can probably (unless \(P=\NP\)) not run in time \(f(|\phi|+\tw)\cdot\poly(n)\) for any elementary function \(f\)[14]. On the other hand, it is not clear (in general) what the concrete running time of such a solver is for a concrete formula or problem (see e. g., [15] for a sophisticated analysis of some running times in Sequoia). We seek to close this gap between (slow) general solvers and (fast) concrete algorithms. Our approach is to concentrate only on a fragment of MSO, which is powerful enough to express many natural problems, but which is restricted enough to allow model checking in time that matches or is close to the running time of a concrete algorithm for the problem. As a bonus, we will be able to derive upper bounds on the running time of the model checker directly from the syntax of the input formula. Based on the interface of Jdrasil, we have implemented a publicly available prototype called Jatatosk [16]. In Section 5, we describe various experiments on different problems on multiple sets of graphs. It turns out that Jatatosk is competitive against the state-of-the-art solvers D-Flat and Sequoia. Arguably, these two programs solve a more general problem and a direct comparison is not entirely fair. However, the experiments do reveal that it seems very promising to focus on smaller fragments of MSO (or perhaps any other description language) in the design of treewidth based solvers.