## 3 A Single Traversal DP Algorithm
#### An Algorithm on the Semi-Incidence Graph
: _Let \(P\) be a program, \(\mathcal{T}=(T,\chi)\) where \(T=(N,\cdot,n)\) be a tree decomposition of \(I(P)\), and \(t\in N\) be a node. A partial solution for \(t\) is a tuple \((M,\sigma,\mathcal{C})\) where \((M,\sigma)\) is a partial model under \(M\) and \(\mathcal{C}\) is a set of partial models \((C,\rho)\) under \(M\) with \(C\subsetneq M\)._

The following lemma establishes correspondence between answer sets and partial solutions. **Observation 1**. : _Let \(P\) be a program, \(\mathcal{T}=(T,\chi)\) be a tree decomposition of the semi-incidence graph \(S(P)\) of program \(P\), where \(T=(\cdot,\cdot,n)\), and \(\chi(n)=\emptyset\). Then, there exists an answer set \(M\) for \(P\) if and only if there exists a partial solution \(u=(M,\sigma,\emptyset)\) with \(\sigma P\) for root \(n\)._

Proof. : Given an answer set \(M\) of \(P\) we construct \(u=(M,\sigma,\emptyset)\) with \(\sigma:=P\) such that \(u\) is a partial solution for \(n\) according to Definition 4. For the other direction, Definition 3 and Definition 4 guarantee that \(M\) is an answer set if there exists some tuple \(u\). In consequence, the observation holds. Next, we define local partial solutions to establish a notion that corresponds to the tuples obtained in Algorithm 2 but on in relation to solutions that we are interested in. **Definition 5**. : _Let \(P\) be a program, \(\mathcal{T}=(T,\chi)\) a tree decomposition of the semi-incidence graph \(S(P)\), where \(T=(N,\cdot,n)\), and \(t\in N\) be a node. A tuple \(u=\langle M,\sigma,\mathcal{C}\rangle\) is a local partial solution for \(t\) if there exists a partial solution \(\hat{u}=(\hat{M},\hat{\sigma},\hat{\mathcal{C}})\) for \(t\) such that the following conditions hold:_

1. \(M=\hat{M}\cap\chi(t)\)_,_
2. \(\sigma=\hat{\sigma}\)_, and_
3. \(\mathcal{C}=\{\langle\hat{C}\cap\chi(t),\hat{\rho}^{t,\hat{M},\hat{\mathcal{C }}}\rangle\mid(\hat{C},\hat{\rho})\in\hat{\mathcal{C}}\}\)_._

_We denote by \(\hat{u}^{t}\) the local partial solution \(u\) for \(t\) given partial solution \(\hat{u}\)._The following observation provides justification that it suffices to store local partial solutions instead of partial solutions for a node \(t\in N\). **Observation 2**. : _Let \(P\) be a program, \(\mathcal{T}=(T,\chi)\) a tree decomposition of \(S(P)\), where \(T=(N,\cdot,n)\), and \(\chi(n)=\emptyset\). Then, there exists an answer set for \(P\) if and only if there exists a local partial solution of the form \(\langle\emptyset,\emptyset,\emptyset\rangle\) for the root \(n\in N\)._

Proof. : Since \(\chi(n)=\emptyset\), every partial solution for the root \(n\) is an extension of the local partial solution \(u\) for the root \(n\in N\) according to Definition 5. By Observation 1, we obtain that the observation is true. In the following, we abbreviate atoms occurring in bag \(\chi(t)\) by \(\mathrm{at}_{t}\), i.e., \(\mathrm{at}_{t}\ :=\chi(t)\setminus P_{t}\). **Lemma 1** (Soundness). : _Let \(P\) be a program, \(\mathcal{T}=(T,\chi)\) a tree decomposition of semi-incidence graph \(S(P)\), where \(T=(N,\cdot,\cdot)\), and \(t\in N\) a node. Given a local partial solution \(u^{\prime}\) of child table \(\tau^{\prime}\) (or local partial solution \(u^{\prime}\) of table \(\tau^{\prime}\) and local partial solution \(u^{\prime\prime}\) of table \(\tau^{\prime\prime}\)), each tuple \(u\) of table \(\tau_{t}\) constructed using table algorithm \(\mathbb{SINC}\) is also a local partial solution._

Proof. : Let \(u^{\prime}\) be a local partial solution for \(t^{\prime}\in N\) and \(u\) a tuple for node \(t\in N\) such that \(u\) was derived from \(u^{\prime}\) using table algorithm \(\mathbb{SINC}\). Hence, node \(t^{\prime}\) is the only child of \(t\) and \(t\) is either removal or introduce node. Assume that \(t\) is a removal node and \(r\in P_{t^{\prime}}\setminus P_{t}\) for some rule \(r\). Observe that \(u=\langle M,\sigma,\mathcal{C}\rangle\) and \(u^{\prime}=\langle M,\sigma^{\prime},\mathcal{C}^{\prime}\rangle\) are the same in witness \(M\).