## 3 A Single Traversal DP Algorithm
#### An Algorithm on the Semi-Incidence Graph
We define \(\dot{R}^{(t)}:R\to 2^{R^{(t)}}\) by \(\dot{R}^{(t)}(r):=\{r\}^{(t)}\) for \(r\in R\)._

After we explained how to obtain models, we describe how to compute counter-witnesses. Family \(\mathcal{C}\) consists of rows \((C,\rho)\) where \(C\subseteq\operatorname{at}(P)\cap\chi(t)\) is a _counter-witness set_ in \(t\) to \(M\). Similar to the sat-state \(\sigma\), the sat-state \(\rho\) for \(C\) under \(M\) represents whether rules of the GL reduct \(P_{t}^{M}\) are satisfied by a superset of \(C\). We can see counter-witness sets together with its sat-state as counter-witnesses. Thus, \(C\) witnesses the existence of \(C^{\prime}\subsetneq M^{\prime}\) satisfying \(C^{\prime}\models(P_{<t}\cup\rho)^{M^{\prime}}\) since \(M\) witnesses a model \(M^{\prime}\supseteq M\) where \(M^{\prime}\models P_{<t}\). In consequence, there exists an answer set of \(P\) if the root table contains \(\langle\emptyset,\emptyset,\emptyset\rangle\). We require local-reducts for deciding satisfiability of counter-witness sets. **Definition 2**. : _Let \(P\) be a program, \(\mathcal{T}=(\cdot,\chi)\) be a TD of \(S(P)\), \(t\) be a node of \(\mathcal{T}\), \(R\subseteq P_{t}\) and \(M\subseteq\operatorname{at}(P)\). We define local-reduct \(R^{(t,M)}\) by \(\left[R^{(t)}\right]^{M}\) and \(\dot{R}^{(t,M)}:R\to 2^{R^{(t,M)}}\) by \(\dot{R}^{(t,M)}(r):=\{r\}^{(t,M)},r\in R\)._

Definitions 1 and 2 together with Algorithm 2 provides the formal description of our algorithm to solve ASP instances by means of dynamic programming on tree decompositions of the semi-incidence graph of the input instance. In the following section, we argue for correctness of our algorithm. ### Correctness and Runtime of Algorithm 2 (\(\mathbb{SINC}\))

Next, we provide insights into the correctness and runtime of Algorithm 2 (\(\mathbb{SINC}\)). **Proposition 1**. : _Let \(P\) be a program and \(k:=tw(S(P))\). Then, the algorithm \(\mathtt{DP}_{\mathrm{SINC}}\) is correct and runs in time \(\mathcal{O}(2^{k+2}\cdot\|S(P)\|)\)._

Proof (Idea/Main Arguments). : Previous works [6; 11] established the correctness and runtime guarantees on the primal and incidence graph, respectively. Since the semi-incidence graph introduces a clique only for choice rule and the algorithm on the semi-incidence graph follows the algorithm on the incidence graph for non-choice rules and the one for the primal graph for choice rules, we immediately obtain correctness and runtime results as the cases never overlap. The remainder of this sections provides details on proving the statement above. The correctness proof investigates each node type separately. We have to show that a tuple at a node \(t\) guarantees existence of an answer set for the program \(P_{\leq t}\), proving soundness. Conversely, we have to show that each answer set is indeed evaluated while traversing the tree decomposition, which provides completeness. We employ this idea using the notions of (i) _partial solutions_ consisting of _partial models_ and the notion of (ii) _local partial solutions_. **Definition 3**. : _Let \(P\) be a program, \(\mathcal{T}=(T,\chi)\) be a tree decomposition of the semi-incidence graph \(S(P)\) of \(P\), where \(T=(N,\cdot,\cdot)\), and \(t\in N\) be a node. Further, let \(M,C\subseteq\mathrm{at}_{\leq t}\) be sets and \(\sigma\subseteq P_{\leq t}\) be a set of rules. The tuple \((C,\sigma)\) is a partial model for \(t\) under \(M\) if the following conditions hold:_

1. \(C\models(P_{<t})^{M}\)_,_
2. _for_ \(r\in P_{\leq t}\) _we require:_
3. _for disjunctive rule_ \(r\in P_{\leq t}\)_, we have_ \(B_{r}^{-}\cap M\
eq\emptyset\) _or_ \(B_{r}^{+}\cap\mathrm{at}_{\leq t}\
ot\subseteq C\) _or_ \(H_{r}\cap C\
eq\emptyset\) _if and only if_ \(r\in\sigma\)_;_ _(b)_ _for choice rule_ \(r\in P_{t}\)_, we have_ \(B_{r}^{-}\cap M\
eq\emptyset\) _or_ \(B_{r}^{+}\cap\mathrm{at}_{t}\
ot\subseteq C\) _or both_ \(H_{r}\subseteq\mathrm{at}_{t}\) _and_ \(H_{r}\cap(M\setminus C)=\emptyset\) _if and only if_ \(r\in\sigma\)_._

**Definition 4**.