# Practical Access to Dynamic Programming on Tree Decompositions +
## 3 An Interface for Dynamic Programming on Tree Decompositions
### Example: 3-Coloring
We assign a current value of \(\sum_{i=1}^{p}\sum_{s\in S_{i}}\omega_{i}(s)\) to every state of the automaton, which is adapted if elements are \"added\" to some of the free variables at introduce nodes. Note that, since we optimize an affine function, this does not increase the state space: even if multiple computational paths lead to the same state with different values at some node of the tree, it is well defined which of these values is the optimal one. Therefore, the cost of optimization only lies in the partition quantifier, that is, we pay with \(k\) bits in the statedescription of the automaton per free variable--independently of the weights (Of course, for each state, we still have to store the weight and we have to perform arithmetic operations on these weights). ### Handling Symmetric and Non-Symmetric Joins

In Section 4.3, we have defined the states of our automaton with respect to a formula, Table 1 gives an overview of the number of bits we require for the different parts of the formula. Let \(\mathrm{bit}(\phi,k)\) be the number of bits that we have to reserve for a formula \(\phi\) and a tree decomposition of maximum bag size \(k\) that is, the sum over the required bits of each part of the formula. By Observation 1, this implies that we can simulate the automaton (and hence solve the model checking problem) in time \(O^{*}\big{(}(2^{\mathrm{bit}(\phi,k)})^{2}\big{)}\), or by Observation 2 in time \(O^{*}\big{(}2^{\mathrm{bit}(\phi,k)}\big{)}\), if the automaton is symmetric (The notation \(O^{*}\) supresses polynomial factors). Unfortunately, this is not always the case, in fact, only the quantifier \(\exists^{\mathrm{partition}}X_{1},\ldots,X_{q}\), the bits needed to optimize over free variables, as well as the formulas that do not require any bits, yield a symmetric tree automaton. This means that the simulation is wasteful if we consider a mixed formula (for instance, one that contains a partition and a connected quantifier). To overcome this issue, we partition the bits of the state description into two parts: first, the \"symmetric\" bits of the quantifiers \(\exists^{\mathrm{partition}}X_{1},\ldots,X_{q}\) and the bits required for optimization, and in the \"asymmetric\" ones of all other elements of the formula. Let \(\mathrm{symmetric}(\phi,k)\) and \(\mathrm{asymmetric}(\phi,k)\) be defined analogously to \(\mathrm{bit}(\phi,k)\). We implement the join of states as in the following lemma, allowing us to deduce the running time of the model checker for concrete formulas. Table 2 provides an overview for formulas presented here. **Lemma 1**. : _Let \(x\) be a join node of \(T\) with children \(y\) and \(z\), and let \(Q_{y}\) and \(Q_{z}\) be sets of states in which the automaton may be at \(y\) and \(z\). Then, the set \(Q_{x}\) of states in which the automaton may be at node \(x\) can be computed in time \(O^{*}\big{(}2^{\mathrm{symmetric}(\phi,k)+2\cdot\mathrm{asymmetric}(\phi,k) }\big{)}\)._

Proof. : To compute \(Q_{x}\), we first split \(Q_{y}\) into \(B_{1},\ldots,B_{q}\) such that all elements in one \(B_{i}\) share the same \"symmetric bits.\" This can be done in time \(|Q_{y}|\) using bucket-sort. Note that we have \(q\leq 2^{\mathrm{symmetric}(\phi,k)}\) and \(|B_{i}|\leq 2^{\mathrm{asymmetric}(\phi,k)}\). With the same technique, we identify for every element \(v\) in \(Q_{z}\) its corresponding partition \(B_{i}\). Finally, we compare \(v\) with the elements in \(B_{i}\) to identify those for which there is a transition in the automaton. This yields an overall running time of the form \(|Q_{z}|\cdot\max_{i=1}^{q}|B_{i}|\leq 2^{\mathrm{bit}(\phi,k)}\cdot 2^{ \mathrm{asymmetric}(\phi,k)}=2^{\mathrm{symmetric}(\phi,k)+2\cdot\mathrm{asymmetric}( \phi,k)}\).