## 3 A Single Traversal DP Algorithm
#### An Algorithm on the Semi-Incidence Graph
Then, the table algorithm \(\texttt{DPL}_{\mathbb{W},\mathbb{C}}\) applies a post-order traversal and links witnesses to counter-witnesses in Line 10. \(\texttt{DPL}_{\mathbb{W},\mathbb{C}}\) searches for origins (orig) of a certain witness \(\vec{u}\), uses the counter-witnesses (\(f_{\textit{cw}}\)) linked to these origins, and then determines the evolution (evol) in order to derive counter-witnesses (using subs) of \(\vec{u}\). ### An Elaborated Example

**Example 5**. : _Let \(k\) be some integer and \(P_{k}\) be some program that contains the following rules \(r_{c}:=\{a_{1},\cdots,a_{k}\}\gets f\), \(r_{2}:=\leftarrow\
eg a_{2}\),..., \(r_{k}:=\leftarrow\
eg a_{k}\), and \(r_{f}:=\leftarrow\
eg f\) and \(r_{cf}:=\{f\}\leftarrow\
eg\). The rules \(r_{1}\),..., \(r_{k}\) simulate that only certain subsets of \(\{a_{1},\cdots,a_{k}\}\) are allowed. Rules \(r_{f}\) and \(r_{cf}\) enforce that \(f\) is set to true. Let \(\mathcal{T}=(T,\mathcal{X},t_{3})\) be a TD of the semi-incidence graph \(\hat{S}(P_{k})\) of program \(P_{k}\) where \(T=(V,E)\) with \(V=\{t_{1},t_{2},t_{3}\}\), \(E=\{(t_{1},t_{2}),(t_{2},t_{3})\}\), \(\mathcal{X}(t_{1})=\{a_{1},\cdots,a_{k},f,r_{cf},r_{cf}\}\), \(\mathcal{X}(t_{2})=\{a_{1},\cdots,a_{k},r_{2},\cdots,r_{k},r_{f}\}\), and \(\mathcal{X}(t_{3})=\emptyset\). Figure 5 (left) illustrates the tables for program \(P_{2}\) after \(\texttt{DP}_{\text{SINC}}\), whereas Figure 5 (right) presents tables using \(\texttt{M-DP}_{\text{SINC}}\), which are exponentially smaller in \(k\), mainly due to cleanup. Observe that Traversal 3.II M-DP\({}_{\text{SINC}}\), \"temporarily\" materializes counter-witnesses only for \(\tau_{1}\), presented in table \(\tau_{1}^{\text{CMOD}}\). Hence, using multi-traversal algorithm M-DP\({}_{\text{SINC}}\) results in an exponential speedup. Note that we can trivially extend the program such that we have the same effect for a TD of minimum width and even if we take the incidence graph. In practice, programs containing the rules above frequently occur when encoding by means of saturation [3]. The program \(P_{k}\) and the TD \(\mathcal{T}\) also reveal that a different TD of the same width, where \(f\) occurs already very early in the bottom-up traversal, would result in a smaller table \(\tau_{1}\) even when running \(\mathtt{DP}_{\mathsf{SINC}}\)._

### Correctness and Runtime of DynASP2.5

Theorem 1: _For a program \(P\) of semi-incidence treewidth \(k:=\mathit{tw}(S(P))\), the algorithm \(\mathtt{M\text{-}DP}_{\mathsf{SINC}}\) is correct and runs in time \(\mathcal{O}(2^{2k+2}\cdot\|P\|)\)._

Proof (Sketch): We sketch the proof idea for enumerating answer sets of disjunctive ASP programs by means of \(\mathtt{M\text{-}DP}_{\mathsf{SINC}}\). Below we present a more detailed approach to establish the correctness. Let \(P\) be a disjunctive program and \(k:=\mathit{tw}(S(P))\). We establish a reduction \(R(P,k)\) of EnumMap to EnumMinSAT1, such that there is a one-to-one correspondence between answer sets and models of the formula, more precisely, for every answer set \(M\) of \(P\) and for the resulting instance \((F,K^{\prime})=R(P,k)\) the set \(M\cup\{sol\}\) is a subset-minimal model of \(F\) and \(k^{\prime}=\mathit{tw}(I(F))\) with \(k^{\prime}\leq 7k+2\). We compute in time \(2^{\mathcal{O}(k^{3})}\cdot\|F\|\) a TD of width at most \(k^{\prime}\)[26] and add \(sol\) to every bag. Using a table algorithm designed for SAT [32] we compute witnesses and counter-witnesses. Observe that witnesses and counter-witnesses are essentially the same objects in a table algorithm for computing subset-minimal models of a propositional formula, since witnesses and counter-witnesses of traversals 3.I and 3.II, respectively, are essentially the same objects in a table algorithm for computing subset-minimal models of a propositional formula. Conceptually, one could also modify \(\mathbb{M\text{-}OD}\) for this task.