## 3 A Single Traversal DP Algorithm
#### An Algorithm on the Semi-Incidence Graph
Since for each witness in the table \(\tau_{t}\) for node \(t\in N\) we remember rule-states for at most \(k+1\) rules, we store up to \(2^{k+1}\) many combinations per witness. In total we end up with at most \(2^{2^{k+1}\cdot 2^{k+1}}\) many counter-witnesses for each witness and rule-state in the worst case. Thus, there are at most \(2^{k+1}\cdot 2^{k+1}\cdot 2^{2^{k+1}\cdot 2^{k+1}}\) tuples in table \(\tau_{t}\) for node \(t\). In consequence, we established the lemma. Proof of Proposition 1 (Runtime). : Let \(P\) be a program, \(S(P)=(V,\cdot)\) its semi-incidence graph, and \(k\) be the treewidth of \(P(P)\). Then, we can compute in time \(2^{\mathcal{O}(k^{3})}\cdot|V|\) a tree decomposition of width at most \(k\)[30]. We take such a tree decomposition and compute in linear time a nice tree decomposition [31]. Let \(\mathcal{T}=(T,\chi)\) be such a nice tree decomposition with \(T=(N,\cdot,\cdot)\). Since the number of nodes in \(N\) is linear in the graph size and since for every node \(t\in N\) the table \(\tau_{t}\) is bounded by \(2^{k+1}\cdot 2^{k+1}\cdot 2^{2^{k+1}\cdot 2^{k+1}}\) according to Lemma 3,we obtain a running time of \(\mathcal{O}(2^{2^{k+2}}\cdot\|S(P)\|)\).Consequently, the claimed runtime bounds in the proposition hold. ### An Extended Example

In Example 3 we give an idea how we compute models of a given program using the semi-incidence graph. The resulting algorithm \(\mathbb{MOD}\) is obtained from \(\mathbb{SINC}\), by taking only the first two row positions (red and green parts). The remaining position (blue part), can be seen as an algorithm (\(\mathbb{CMOD}\)) that computes counter-witnesses. We assume that the \(i\)th-row in each table \(\tau_{i}\) corresponds to \(u_{t.i}=\langle M_{t.i},\sigma_{t.i}\rangle\). **Example 3**. : _Consider program \(P\) from Example 1, which was given by_

\[P=\{\overbrace{\{e_{ab}\}}^{r_{ab}};\overbrace{\{e_{bc}\}}^{r_{bc}};\overbrace {\{e_{cd}\}}^{r_{cd}};\overbrace{\{e_{ad}\}}^{r_{ad}};\overbrace{a_{b} \leftarrow{e_{ab}\}}^{r_{b}};\overbrace{a_{d}\leftarrow{e_{ad}}}^{r_{d}}; \overbrace{a_{c}\leftarrow{a_{b},e_{bc}}}^{r_{c1}};\overbrace{a_{c} \leftarrow{a_{d},e_{cd}}}^{r_{c2}};\overbrace{\leftarrow{-a_{c}}}^{r_{c-c}} \},\]

_TD \(\mathcal{T}=(\cdot,\chi)\) in Figure 2, and the tables \(\tau_{1},\ldots,\tau_{34}\), which illustrate computation results obtained during post-order traversal of \(\mathcal{T}\) by \(\mathtt{DP_{MOD}}\). Note that Figure 2 does not show every intermediate node of TD \(\mathcal{T}\). Table \(\tau_{1}=\{\langle\emptyset,\emptyset\rangle\}\) as \(\mathtt{type}(t_{1})=\) leaf (see Algorithm 2.1). Table \(\tau_{3}\) is obtained via introducing rule \(r_{ab}\), after introducing atom \(e_{ab}\) (\(\mathtt{type}(t_{2})=\mathtt{type}(t_{3})=\) int). It contains two rows due to two possible truth assignments using atom \(e_{ab}\) (L3-5). Observe that rule \(r_{ab}\) is satisfied in both rows \(M_{3,1}\) and \(M_{3,2}\), since the head of choice rule \(r_{ab}\) is in \(\mathtt{at}_{\leq\tau_{3}}\) (see \(L7\) and Definition 1). Intuitively, whenever a rule \(r\) is proven to be satisfiable, sat-state \(\sigma_{t.i}\) marks \(r\) satisfiable since an atom of a rule of \(S(P)\) might only occur in one TD bag. Consider table \(\tau_{4}\) with \(\mathtt{type}(t_{4})=\) forget and \(r_{ab}\in\chi(t_{3})\setminus\chi(t_{4})\). By definition (TDs and semi-incidence graph), we have encountered every occurrence of any atom in \(r_{ab}\). In consequence, \(\mathbb{MOD}\) enforces that only rows where \(r_{ab}\) is marked satisfiable in \(\tau_{3}\), are considered for table \(\tau_{4}\). The resulting table \(\tau_{4}\) consists of rows of \(\tau_{3}\) with \(\sigma_{4.i}=\emptyset\), where rule \(r_{ab}\) is proven satisfied (\(r_{ab}\in\sigma_{3.1},\sigma_{3.2}\), see \(L1\)). Note that between nodes \(t_{6}\) and \(t_{10}\), an atom and rule remove as well as an atom and rule introduce node is placed.