## 3 A Single Traversal DP Algorithm
#### An Algorithm on the Semi-Incidence Graph
*/
1 if\(\text{type}(t)=\textit{leaf}\)then\(t:=\{\langle\emptyset,\emptyset,\emptyset\rangle\}\) elseif\(\text{type}(t)=\textit{int}\), \(a\in\chi_{t}\setminus P_{t}\) is introduced and \(\tau^{\prime}\in\textit{Child-Tabs}_{t}\)then \(\tau_{t}:=\{(\mathbb{A}_{t}^{+},\sigma\cup\text{SatPr}(\hat{p}_{t}^{(t)},M_{ t}^{+}),\)\(\{(C_{t}^{+},\rho\cup\text{SatPr}(\hat{p}_{t}^{(t,M_{t}^{+})},C_{t}^{+}))\mid(C,\rho)\in C\}\)\(\cup\) \(\{(C,\ \rho\cup\text{SatPr}(\hat{p}_{t}^{(t,M_{t}^{+})},C))\mid(C,\rho)\in C\}\cup\{(M,\sigma\cup \text{SatPr}(\hat{p}_{t}^{(t,M_{t}^{+})},M))\}\) \(\cup\) \(\{(M,\sigma\cup\text{SatPr}(\hat{p}_{t}^{(t,M_{t}^{+})},M),\)\(\{(C,\rho\cup\text{SatPr}(\hat{p}_{t}^{(t,M)},C))\mid(C,\rho)\in C\}\}\) \(\mid(M,\sigma,C)\in\tau^{\prime}\}\) elseif\(\text{type}(t)=\textit{int}\), \(r\in\chi_{t}\capOur table algorithm \(\mathbb{SINC}\) computes and stores (i) sets of atoms (witnesses) that are relevant for the Sat part (finding a model of the program) and (ii) sets of atoms (counter-witnesses) that are relevant for the Unsat part (checking for minimality). In addition, we need to store for each set of witnesses as well as its set of counter-witnesses satisfiability states (_sat-states_ for short). For the following reason: By Definition of TDs and the semi-incidence graph, it is true for every atom \(a\) and every rule \(r\) of a program that if atom \(a\) occurs in rule \(r\), then \(a\) and \(r\) occur together in at least one bag of the TD. In consequence, the table algorithm encounters every occurrence of an atom in any rule. In the end, on removal of \(r\), we have to ensure that \(r\) is among the rules that are already satisfied. However, we need to keep track whether a witness _satisfies_ a rule, because not all atoms that occur in a rule occur together in exactly one bag. Hence, when our algorithm traverses the TD and an atom is forgotten we still need to store this _sat-state_, as setting the forgotten atom to a certain truth value influences the satisfiability of the rule. Since the semi-incidence graph contains a clique on every set \(A\) of atoms that occur together in choice rule head, those atoms \(A\) occur together in a common bag of any TD of the semi-incidence graph. For that reason, we do _not_ need to incorporate choice rules into the satisfiability state, in contrast to the algorithm for the incidence graph [11]. We can see witness sets together with its sat-state as _witness_. Then, in Algorithm 2 (\(\mathbb{SINC}\)) a row in the table \(\tau_{t}\) is a triple \(\langle M,\sigma,\mathcal{C}\rangle\). The set \(M\subseteq\operatorname{at}(P)\cap\chi(t)\) represents a witness set. The family \(\mathcal{C}\) of sets concerns counter-witnesses, which we will discuss in more detail below. The _sat-state_\(\sigma\) for \(M\) represents rules of \(\chi(t)\) satisfied by a superset of \(M\). Hence, \(M\) witnesses a model \(M^{\prime}\supseteq M\) where \(M^{\prime}\models P_{<t}\cup\sigma\). We use binary operator \(\cup\) to combine sat-states, which ensures that rules satisfied in at least one operand remain satisfied. We compute a new sat-state \(\sigma\) from a sat-state and satisfied rules, formally, \(\operatorname{SatPr}(\dot{R},M):=\{r\mid(r,R)\in\dot{R},M\models R\}\) for \(M\subseteq\chi(t)\setminus P_{t}\) and program \(\dot{R}(r)\) constructed by \(\dot{R}\), mapping rules to local-programs as given in the following definition. **Definition 1**. : _Let \(P\) be a program, \(\mathcal{T}=(\cdot,\chi)\) be a TD of \(S(P)\), \(t\) be a node of \(\mathcal{T}\) and \(R\subseteq P_{t}\). The local-program \(R^{(t)}\) is obtained from \(R\cup\{\gets B_{r}\mid r\in R\) is a choice rule, \(H_{r}\subsetneq\operatorname{at}_{\leq t}\}\) (We require to add \(\{\gets B_{r}\mid r\in R\) is a choice rule, \(H_{r}\subsetneq\operatorname{at}_{\leq t}\}\) in order to decide satisfiability for corner cases of choice rules involving counter-witnesses of Line 3 in Algorithm 2.) by removing from every rule all literals \(a,\
eg a\) with \(a\
ot\in\chi(t)\).