# Practical Access to Dynamic Programming on Tree Decompositions +
## 3 An Interface for Dynamic Programming on Tree Decompositions
### Example: 3-Coloring
\begin{table}
\begin{tabular}{c c} \hline \hline
**Quantifier/Formula** & **Number of Bits** \\ \hline free variables \(X_{1},\ldots,X_{q}\) & \(q\cdot k\) \\ \(\exists^{\mathrm{partition}}X_{1},\ldots,X_{q}\) & \(k\cdot\log q\) \\ \(\exists^{\mathrm{connected}}X\) & \(k\cdot\log k+1\) \\ \(\exists^{\mathrm{forest}}X\) & \(k\cdot\log k\) \\ \(\forall x\forall y\ E(x,y)\to\chi_{i}\) & \(0\) \\ \(\forall x\exists y\ E(x,y)\wedge\chi_{i}\) & \(k\) \\ \(\exists x\forall y\ E(x,y)\to\chi_{i}\) & \(k+1\) \\ \(\exists x\exists y\ E(x,y)\wedge\chi_{i}\) & \(1\) \\ \(\forall x\ \chi_{i}\) & \(0\) \\ \

## 5 Applications and Experiments

To show the feasibility of our approach, we have performed experiments for widely investigated graph problems: 3-coloring (Figure 2), vertex-cover (Figure 3), dominating-set (Figure 4), independent-set (Figure 5), and feedback-vertex-set (Figure 6). All experiments were performed on an Intel Core processor containing four cores of 3.2 GHz each and 8 Gigabyte RAM. Jdrasil was used with Java 8.1 and both Sequoia and D-Flat were compiled with gcc 7.2. All compilations were performed with the default optimization settings. The implementation of Jdatatosk uses hashing to realize Lemma 1, which works well in practice. We use a data set assembled from different sources containing graphs with 18 to 956 vertices and treewidth 3 to 13. The first source is a collection of transit graphs from GTFS-transit feeds [17] that was also used for experiments in [18], the second source is real-world instances collected in [19], and the last one is that of the PACE challenge [2] with treewidth at most 11. In each of the experiments, the left picture always shows the difference of Jdatatosk against D-Flat and Sequoia. A positive bar means that Jdatatosk is faster by this amount in seconds, and a negative bar means that either D-Flat or Sequoia is faster by that amount. The bars are capped at 100 seconds. On every instance, Jdatatosk was compared against the solver that was faster on this particular instance. The image also shows for every instance the treewidth of the input. The right image always shows a cactus plot that visualizes the number of instances that can be solved by each of the solvers in \(x\) seconds, that is, faster growing functions are better. For each experiment, there is a table showing the average, standard deviation, and median of the time (in seconds) each solver needed to solve the problem. The best values are highlighted. The experiments reveal that Jdatatosk is faster than its competitors on many instances. However, there are also formulas such as the one for the vertex cover problem on which one of the other solvers performs better on some of the instances. For an overall picture, the cactus plot in Figure 7 is the \(sum\) of all cactus plots from the experiments. It reveals that overall Jdatatosk in fact outperforms its competitors. However, we stress once more that the comparison is not completely fair, as both Sequoia and D-Flat are powerful enough to model check the whole of MSO (and actually also MSO\({}_{2}\)), while Jdatatosk can only handle a fragment of MSO\({}_{1}\). \begin{table}
\begin{tabular}{c c c c} \hline \hline \(\boldsymbol{\phi}\) & \(\mathbf{symmetric}(\boldsymbol{\phi},\boldsymbol{k})\) & \(\mathbf{asymmetric}(\boldsymbol{\phi},\boldsymbol{k})\) & **Time** \\ \hline \(\phi_{\text{3 col}}\) & \(k\cdot\log(3)\) & 0 & \(O^{*}(3^{k})\) \\ \(\phi_{\text{vc}}(S)\) & \(k\) & 0 & \(O^{*}(2^{k})\) \\ \(\phi_{\text{ds}}(S)\) & \(k\) & \(k\) & \(O^{*}(8^{k})\) \\ \(\phi_{\text{triangle-minor}}\) & 0 & \(3k\cdot\log(k)+3\) & \(O^{*}(k^{6k})\) \\ \(\phi_{\text{fvs}}(S)\) & \(k\) & \(k\cdot\log(k)\) & \(O^{*}(2^{k}k^{2k})\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: The table gives an overview of formulas \(\phi\) used within this paper, together with the values \(\text{symmetric}(\phi,k)\) and \(\text{asymmetric}(\phi,k)\), as well as the precise time our algorithm will require to model check an instance for that particular formula.