Treewidth and Counting Projected Answer Sets

TL;DR

This paper presents new algorithms for counting projected answer sets in logic programming, exploiting small treewidth and establishing complexity bounds, advancing the efficiency and theoretical understanding of #PAs.

Contribution

The paper introduces novel dynamic programming algorithms for projected answer set counting that leverage small treewidth and extends existing methods to various classes of logic programs.

Findings

Algorithms run in polynomial time with double exponential dependence on treewidth for certain programs.

Extended algorithms for tight, normal, and disjunctive programs improve counting efficiency.

Lower bounds under ETH show no significant runtime improvements are possible.

Abstract

In this paper, we introduce novel algorithms to solve projected answer set counting (#PAs). #PAs asks to count the number of answer sets with respect to a given set of projected atoms, where multiple answer sets that are identical when restricted to the projected atoms count as only one projected answer set. Our algorithms exploit small treewidth of the primal graph of the input instance by dynamic programming (DP). We establish a new algorithm for head-cycle-free (HCF) programs and lift very recent results from projected model counting to #PAs when the input is restricted to HCF programs. Further, we show how established DP algorithms for tight, normal, and disjunctive answer set programs can be extended to solve #PAs. Our algorithms run in polynomial time while requiring double exponential time in the treewidth for tight, normal, and HCF programs, and triple exponential time for disjunctive programs. Finally, we take the exponential time hypothesis (ETH) into account and establish lower bounds of bounded treewidth algorithms for #PAs. Under ETH, one cannot significantly improve our obtained worst-case runtimes.

Tables

Table 1. Table 1: Overview of upper and lower bounds using treewidth  k 𝑘 k of the primal graph of instance  Π Π \Pi ; bold entries were established in the course of this paper.

Problem	Restriction	Upper Bound	Lower Bound (under ETH)
SAT, $\#$SAT	-	$2^{𝒪\left(k\right)}\cdot poly\left(\Vert \Pi \Vert \right)$ [44]	$2^{\Omega \left(k\right)}\cdot poly\left(\Vert \Pi \Vert \right)$ [29]
As, $\#$As	tight	${\mathrm{𝟐}}^{𝒪\left(𝐤\right)}\cdot \mathrm{𝐩𝐨𝐥𝐲}\left(\Vert 𝚷\Vert \right)$	$2^{\Omega \left(k\right)}\cdot poly\left(\Vert \Pi \Vert \right)$ [29]
As, $\#$As	normal, HCF	${\mathrm{𝟐}}^{𝒪\left(𝐤\cdot \mathrm{𝐥𝐨𝐠}\left(𝐤\right)\right)}\cdot \mathrm{𝐩𝐨𝐥𝐲}\left(\Vert 𝚷\Vert \right)$	$2^{\Omega \left(k\right)}\cdot poly\left(\Vert \Pi \Vert \right)$ [29]
As, $\#$As	disjunctive	$2^{2^{𝒪\left(k\right)}}\cdot poly\left(\Vert \Pi \Vert \right)$ [30]	$2^{2^{\Omega \left(k\right)}}\cdot poly\left(\Vert \Pi \Vert \right)$
Proj. $\#$SAT	-	$2^{2^{𝒪\left(k\right)}}\cdot poly\left(\Vert \Pi \Vert \right)$ [21]	$2^{2^{\Omega \left(k\right)}}\cdot poly\left(\Vert \Pi \Vert \right)$ [21]
$\#$PAs	tight	${\mathrm{𝟐}}^{{\mathrm{𝟐}}^{𝒪\left(𝐤\right)}}\cdot \mathrm{𝐩𝐨𝐥𝐲}\left(\Vert 𝚷\Vert \right)$	${\mathrm{𝟐}}^{{\mathrm{𝟐}}^{𝛀\left(𝐤\right)}}\cdot \mathrm{𝐩𝐨𝐥𝐲}\left(\Vert 𝚷\Vert \right)$
$\#$PAs	normal, HCF	${\mathrm{𝟐}}^{{\mathrm{𝟐}}^{𝒪\left(𝐤\cdot \mathrm{𝐥𝐨𝐠}\left(𝐤\right)\right)}}\cdot \mathrm{𝐩𝐨𝐥𝐲}\left(\Vert 𝚷\Vert \right)$	${\mathrm{𝟐}}^{{\mathrm{𝟐}}^{𝛀\left(𝐤\right)}}\cdot \mathrm{𝐩𝐨𝐥𝐲}\left(\Vert 𝚷\Vert \right)$
$\#$PAs	disjunctive	${\mathrm{𝟐}}^{{\mathrm{𝟐}}^{{\mathrm{𝟐}}^{𝒪\left(𝐤\right)}}}\cdot \mathrm{𝐩𝐨𝐥𝐲}\left(\Vert 𝚷\Vert \right)$	${\mathrm{𝟐}}^{{\mathrm{𝟐}}^{{\mathrm{𝟐}}^{𝛀\left(𝐤\right)}}}\cdot \mathrm{𝐩𝐨𝐥𝐲}\left(\Vert 𝚷\Vert \right)$

Equations

$$2^{(k+1{)}^{(c+1)/c}}\ge (k+1)\cdot k!$$

$$2^{(k+1{)}^{1/c}\cdot (k+1)}\ge (k+1)\cdot k!$$

$$2^{(k+1{)}^{1/c}+k\cdot (k+1{)}^{1/c}}\ge (k+1)\cdot k!$$

$$2^{(k+1{)}^{1/c}}\cdot 2^{k\cdot (k+1{)}^{1/c}}\ge (k+1)\cdot k!$$

$$2^{(k+1{)}^{1/c}}\cdot k!{\ge }^{IH}(k+1)\cdot k!$$

$$2^{(k+1{)}^{1/c}}\ge (k+1)$$

$$2^{(k+1{)}^{1/c}}\ge 2^{{\text{log}}_2(k+1)}\ge (k+1)$$

$$\text{ where }k\ge k_0\text{ for some fixed }{k}_0\text{ since }{\text{log}}_2\in O(\text{exp}(1/c))$$

$${\mathrm{SatExt}}_{\le t}(\rho ):=\bigcup _{\vec{u}\in \rho }\{X\mid X\in {\mathrm{Ext}}_{\le t}(\vec{u}),X\subseteq Y,Y\in \mathrm{Exts}\}.$$

$$\mathcal{I}({\mathrm{Ext}}_{\le n}[\tau (n)])=\{\hat{I}\mid ⟨\hat{I},\hat{\mathcal{P}},\hat{\sigma }⟩\text{ is a }\mathbb{PHC}\text{-solution up to }n\}$$

$$=\{I\mid I\in 2^{\text{at}(\Pi )},I\text{ is an answer set of }\Pi \}.$$

$$\mathcal{I}({\mathrm{SatExt}}_{\le t}[\tau (t)])$$

$$=\{\hat{I}\mid ⟨\hat{I},\hat{\mathcal{P}},\hat{\sigma }⟩\text{ is a }\mathbb{PHC}\text{-solution up to }t,\text{ there is answer set }$$

$$I^{\prime }\supseteq \hat{I}\text{ of }\Pi \text{ such that }{I}^{\prime }\subseteq I\cup (\text{at}(\Pi )\setminus {\text{at}}_{\le t})\}$$

$$=\{I\mid I\in 2^{{\text{at}}_{\le t}},I\models {\Pi }_{\le t},\text{ there is an answer set }$$

$$I^{\prime }\supseteq I\text{ of }\Pi \text{ such that }{I}^{\prime }\subseteq I\cup (\text{at}(\Pi )\setminus {\text{at}}_{\le t})\}.$$

$${\mathrm{pasc}}_{\le t}(\rho ):=\left|\bigcup _{\vec{u}\in \rho }{\mathcal{I}}_P({\mathrm{SatExt}}_{\le t}(\{\vec{u}\}))\right|$$

$${\mathrm{ipasc}}_{\le t}(\rho ):=\left|\bigcap _{\vec{u}\in \rho }{\mathcal{I}}_P({\mathrm{SatExt}}_{\le t}(\{\vec{u}\}))\right|$$

$${\mathrm{ipasc}}_{\le n}(\mathrm{local}(n,{\mathrm{SatExt}}_{\le n}[\tau (n)]))$$

$$=$$

$$J\text{ is an answer set of }\Pi \}|$$

$$\left|\bigcap_{i\in X}X_{i}\right|=\Bigg{|}\,\left|\bigcup^{n}_{j=1}X_{j}\right|+\sum_{\emptyset\subsetneq I\subsetneq X}(-1)^{\left|I\right|}\left|\bigcap_{i\in I}X_{i}\right|\,\Bigg{|}.$$

Full text

We establish a new algorithm for head-cycle-free (HCF) programs and lift very recent results from projected model counting to $\#$PAs when the input is restricted to HCF programs. Further, we show how established DP algorithms for tight, normal, and disjunctive answer set programs can be extended to solve $\#$PAs. Our algorithms run in polynomial time while requiring double exponential time in the treewidth for tight, normal, and HCF programs, and triple exponential time for disjunctive programs.

Finally, we take the exponential time hypothesis (ETH) into account and establish lower bounds of bounded treewidth algorithms for $\#$PAs. Under ETH, one cannot significantly improve our obtained worst-case runtimes.

Introduction

Answer Set Programming (ASP) [10] is an active research area of artificial intelligence. It provides a logic-based declarative modelling language and problem solving framework [24] for hard computational problems, which has been widely applied [2, 40, 41, 27]. In ASP, questions are encoded into rules and constraints that form a disjunctive (logic) program over atoms. Solutions to the program are so-called answer sets. Lately, two computational problems of ASP have received increasing attention, namely, $\#$As [19] and $\#$PAs [1]. The problem $\#$As asks to output the number of answer sets of a given disjunctive program. When considering computational complexity $\#$As can be classified as #$\cdot$coNP-complete [19], which is even harder than counting the models of a Boolean formula. A natural abstraction of $\#$As is to consider projected counting where we ask to count the answer sets of a disjunctive program with respect to a given set of projected atoms ($\#$PAs). Particularly, multiple answer sets that are identical when reduced to the projected atoms are considered as only one solution. Intuitively, $\#$PAs is needed to count answer sets without counting functionally independent auxiliary atoms. Under standard assumptions the problem $\#$PAs is complete for the class #$\cdot\Sigma_{2}P$. However, if we take all atoms as projected, then $\#$PAs is again #$\cdot$coNP-complete and if there are no projected atoms then it is simply $\Sigma^{p}_{2}$-complete. But some fragments of ASP have lower complexity. A prominent example is the class of head-cycle-free (HCF) programs [4], which requires the absence of cycles in a certain graph representation of the program. Deciding whether a HCF program has an answer set is NP-complete.

A way to solve computationally hard problems is to employ parameterized algorithmics [12], which exploits certain structural restrictions in a given input instance. Because structural properties of an input instance often allow for algorithms that solve problems in polynomial time in the size of the input and exponential time in a measure of the structure, whereas under standard assumptions an efficient algorithm is not possible if we consider only the size of the input. In this paper, we consider the treewidth of a graph representation associated with the given input program as structural restriction, namely the treewidth of the primal graph [30]. Generally speaking, treewidth111Google Scholar outputs 18,800 results employing treewidth (queried: March. 27, 2019). measures the closeness of a graph to a tree, based on the observation that problems on trees are often easier to solve than on arbitrary graphs.

Our results are as follows: We establish the classical complexity of $\#$PAs and a novel algorithm that solves ASP problems by exploiting treewidth when the input program is restricted to HCF programs in runtime single exponential in the treewidth. We introduce a framework for counting projected answer sets by exploiting treewidth. Therefore, we lift recent results from projected model counting in the domain of Boolean formulas to counting projected answer sets. We establish algorithms that are (i) double exponential in the treewidth if the input is restricted to tight, normal or HCF programs and (ii) triple exponential in the treewidth if we allow disjunctive programs. Using the exponential time hypothesis (ETH), we establish that $\#$PAs cannot be solved in time better than double exponential in the treewidth for tight, normal, and HCF programs, and not better than triple exponential for disjunctive programs, respectively.

Related Work. Gebser, Kaufmann and Schaub [23] considered projected enumeration for ASP. Aziz [1] introduced techniques to modify modern ASP-solvers in order to count projected answer sets. Jakl, Pichler and Woltran [30] presented DP algorithms that solve ASP counting in time double exponential in the treewidth. Pichler et al. [43] investigated the complexity of extended programs and also presented DP algorithms for it. We employ ideas from their algorithms to solve head-cycle-free programs. Fichte et al. [19, 20] presented algorithms to solve $\#$As for the full standard syntax of modern ASP solvers. Recently, Fichte et al. [21] gave DP algorithms for projected $\#$SAT including lower bounds, c.f., Table 1.

Preliminaries

Basics and Combinatorics. For a set $X$, let $2^{X}$ be the power set of $X$ consisting of all subsets $Y$ with $\emptyset\subseteq Y\subseteq X$. For given sequence $\vec{s}$ and integer $i>0$, $\vec{s}_{(i)}$ refers to the $i$-th element of $\vec{s}$ and $<_{\vec{s}}\,\mathrel{\mathop{:}}=\{(\vec{s}_{(i)},\vec{s}_{(j)})\mid 1\leq i<j\leq\left|\vec{s}\right|\}$ denotes its induced ordering. Given some integer $n$ and a family of finite sets $X_{1}$, $X_{2}$, $\ldots$, $X_{n}$, the generalized inclusion-exclusion principle [26] states that the number of elements in the union over all subsets is $\left|\cup^{n}_{j=1}X_{j}\right|=\Sigma_{I\subseteq\{1,\ldots,n\},I\neq\emptyset}(-1)^{\left|I\right|-1}\left|\cap_{i\in I}X_{i}\right|$.

Computational Complexity. We assume familiarity with standard notions in computational complexity [42] and parameterized complexity [12], and use counting complexity classes as defined by Durand, Hermann and Kolaitis [14].

Let $\Sigma$ and $\Sigma^{\prime}$ be finite alphabets, $I\in\Sigma^{*}$ be an instance and $\|I\|$ denote the size of $I$. A witness function $\mathcal{W}\colon\Sigma^{*}\rightarrow 2^{{\Sigma^{\prime}}^{*}}$ maps an instance $I\in\Sigma^{*}$ to its witnesses. A parameterized counting problem $L:\Sigma^{*}\times\mathbb{N}\rightarrow\mathbb{N}_{0}$ is a function that maps a given instance $I\in\Sigma^{*}$ and an integer $k\in\mathbb{N}$ to the cardinality of its witnesses $\left|\mathcal{W}(I)\right|$. Let $\mathcal{C}$ be a decision complexity class, e.g., P. Then, $\#\cdot\mathcal{C}$ denotes the class of all counting problems whose witness function $\mathcal{W}$ satisfies (i) there is a function $f:\mathbb{N}_{0}\rightarrow\mathbb{N}_{0}$ such that for every instance $I\in\Sigma^{*}$ and every $W\in\mathcal{W}(I)$ we have $\left|W\right|\leq f(\|I\|)$ and $f$ is computable in time ${\mathcal{O}}(\|I\|^{c})$ for some constant $c$ and (ii) for every instance $I\in\Sigma^{*}$ decision problem $\mathcal{W}(I)$ is inthe complexity class $\mathcal{C}$. Then, $\#\cdot\textsc{P}$ is the complexity class consisting of all counting problems associated with decision problems in NP.

Answer Set Programming (ASP). We follow standard definitions of propositional disjunctive ASP. For comprehensive foundations, we refer to introductory literature [10, 31]. Let $\ell$, $m$, $n$ be non-negative integers such that $\ell\leq m\leq n$, $a_{1}$, $\ldots$, $a_{n}$ be distinct atoms. Moreover, we refer by literal to an atom or the negation thereof. A program $\Pi$ is a finite set of rules of the form $a_{1}\vee\cdots\vee a_{\ell}\leftarrow\,a_{\ell+1},\ldots,a_{m},\neg a_{m+1},\ldots,\neg a_{n}.$ For a rule $r$, we let $H_{r}\,\mathrel{\mathop{:}}=\{a_{1},\ldots,a_{\ell}\}$, $B^{+}_{r}\,\mathrel{\mathop{:}}=\{a_{\ell+1},\ldots,a_{m}\}$, and $B^{-}_{r}\,\mathrel{\mathop{:}}=\{a_{m+1},\ldots,a_{n}\}$. We denote the sets of atoms occurring in a rule $r$ or in a program $\Pi$ by $\text{at}(r)\,\mathrel{\mathop{:}}=H_{r}\cup B^{+}_{r}\cup B^{-}_{r}$ and $\text{at}(\Pi)\,\mathrel{\mathop{:}}=\cup_{r\in\Pi}\text{at}(r)$. Let $\Pi$ be a program. A program $\Pi^{\prime}$ is a sub-program of $\Pi$ if $\Pi^{\prime}\subseteq\Pi$. Program $\Pi$ is normal if $\left|H_{r}\right|\leq 1$ for every $r\in\Pi$. The positive dependency digraph $D_{\Pi}$ of $\Pi$ is the directed graph defined on the set of atoms from $\bigcup_{r\in\Pi}H_{r}\cup B^{+}_{r}$, where for every rule $r\in\Pi$ two atoms $a\in B^{+}_{r}$ and $b\in H_{r}$ are joined by an edge $(a,b)$. A head-cycle of $D_{\Pi}$ is an $\{a,b\}$-cycle222Let $G=(V,E)$ be a digraph and $W\subseteq V$. Then, a cycle in $G$ is a $W$-cycle if it contains all vertices from $W$. for two distinct atoms $a$, $b\in H_{r}$ for some rule $r\in\Pi$. Program $\Pi$ is tight (head-cycle-free [4]) if $D_{\Pi}$ contains no cycle (head-cycle).

An interpretation $I$ is a set of atoms. $I$ satisfies a rule $r$ if $(H_{r}\,\cup\,B^{-}_{r})\,\cap\,I\neq\emptyset$ or $B^{+}_{r}\setminus I\neq\emptyset$. $I$ is a model of $\Pi$ if it satisfies all rules of $\Pi$, in symbols $I\models\Pi$. The Gelfond-Lifschitz (GL) reduct of $\Pi$ under $I$ is the program $\Pi^{I}$ obtained from $\Pi$ by first removing all rules $r$ with $B^{-}_{r}\cap I\neq\emptyset$ and then removing all $\neg z$ where $z\in B^{-}_{r}$ from the remaining rules $r$ [25]. $I$ is an answer set of a program $\Pi$ if $I$ is a minimal model of $\Pi^{I}$. Deciding whether a disjunctive program has an answer set is $\Sigma_{\textrm{2}}^{\textrm{P}}$-complete [15]. The problem is called consistency (As) of an ASP program. If the input is restricted to normal programs, the complexity drops to NP-complete [5, 38]. A head-cycle-free program $\Pi$ can be translated into a normal program in polynomial time [4]. The following well-known characterization of answer sets is often invoked when considering normal programs [36]. Given a model $I$ of a normal program $\Pi$ and an ordering $\sigma$ of atoms over $I$. An atom $a\in I$ is proven if there is a rule $r\in\Pi$ with $a\in H_{r}$ where (i) $B^{+}_{r}\subseteq I$, (ii) $b<_{\sigma}a$ for every $b\in B_{r}^{+}$, and (iii) $I\cap B^{-}_{r}=\emptyset$ and $I\cap(H_{r}\setminus\{a\})=\emptyset$. Then, $I$ is an answer set of $\Pi$ if (i) $I$ is a model of $\Pi$, and (ii) every atom $a\in I$ is proven. This characterization vacuously extends to head-cycle-free programs by applying the results of Ben-Eliyahu and Dechter [4]. Given a program $\Pi$, we assume in the following that every atom $a\in\text{at}(\Pi)$ occurs in some head of a rule of $\Pi$ [3].

Example 1**.**

Consider $\Pi\,\mathrel{\mathop{:}}=\{\overbrace{a\lor b\leftarrow\,}^{r_{1}};\,\overbrace{c\lor e\leftarrow\,}^{r_{2}};\,\overbrace{d\lor e\leftarrow\,b}^{r_{3}};\,\overbrace{b\leftarrow\,e,\neg d}^{r_{4}};\,\overbrace{d\leftarrow\,\neg b}^{r_{5}}\}.$ It is easy to see that $\Pi$ is a head-cycle-free program. The set $A=\{b,c,d\}$ is an answer set of $\Pi$. Consider the ordering $\sigma=\langle b,c,d\rangle$, from which we can prove atom $b$ by rule $r_{1}$, atom $c$ by rule $r_{2}$, and atom $d$ by rule $r_{3}$. Further answer sets are $B=\{a,c,d\}$, $C=\{b,e\}$, and $D=\{a,d,e\}$.

Counting Projected Answer Sets. An instance is a pair $(\Pi,P)$, where $\Pi$ is a program and $P\subseteq\text{at}(\Pi)$ is a set of projection atoms. The projected answer sets count of $\Pi$ with respect to $P$ is the number of subsets $I\subseteq P$ such that $I\cup J$ is an answer set of $\Pi$ for some set $J\subseteq\text{at}(\Pi)\setminus P$. The counting projected answer sets problem ($\#$PAs) asks to output the projected answer sets count of $\Pi$, i.e., $\left|\{I\cap P\mid I\in S\}\right|$ where $S$ is the set of all answer sets of $\Pi$. Note that $\#$As is $\#$PAs, where $P=\text{at}(\Pi)$, and that deciding As equals $\#$PAs, where $P=\emptyset$.

Example 2**.**

Consider program $\Pi$ from Example 1 and its four answer sets $\{a,c,d\}$, $\{b,c,d\}$, $\{b,e\}$, and $\{a,d,e\}$, as well as the set $P\,\mathrel{\mathop{:}}=\{d,e\}$ of projection atoms. When we project the answer sets to $P$, we only have the three answer sets $\{d\}$, $\{e\}$, and $\{d,e\}$, i.e., the projected answer sets count of $(\Pi,P)$ is 3.

Theorem 1** ($\star$333Proofs marked with “$\star$” are in the appendix.).**

The problem $\#\textsc{PAs}$ is #$\cdot\Sigma_{2}P$-complete for disjunctive programs and #$\cdot$NP-complete for head-cycle-free, normal or tight programs.

Tree Decompositions (TDs). We follow standard terminology on graphs and digraphs [13, 9]. For a tree $T=(N,A,n)$ with root $n$ and a node $t\in N$, we let $\operatorname{children}(t,T)$ be the sequence of all nodes $t^{\prime}$ in arbitrarily but fixed order, which have an edge $(t,t^{\prime})\in A$. Let $G=(V,E)$ be a graph. A tree decomposition (TD) of graph $G$ is a pair $\mathcal{T}=(T,\chi)$, where $T=(N,A,n)$ is a rooted tree, $n\in N$ the root, and $\chi$ a mapping that assigns to each node $t\in N$ a set $\chi(t)\subseteq V$, called a bag, such that the following conditions hold: (i) $V=\bigcup_{t\in N}\chi(t)$ and $E\subseteq\bigcup_{t\in N}\{\{u,v\}\mid u,v\in\chi(t)\}$; and (ii) for each $r,s,t$, such that $s$ lies on the path from $r$ to $t$, we have $\chi(r)\cap\chi(t)\subseteq\chi(s)$. Then, $\operatorname{width}(\mathcal{T})\,\mathrel{\mathop{:}}=\max_{t\in N}\left|\chi(t)\right|-1$. The treewidth $\mathit{tw}(G)$ of $G$ is the minimum $\operatorname{width}({\mathcal{T}})$ over all TDs $\mathcal{T}$ of $G$. For arbitrary but fixed $w\geq 1$, it is feasible in linear time to decide if a graph has treewidth at most $w$ and, if so, to compute a TD of width $w$ [7]. For simplifications we always use so-called nice TDs, which can be computed in linear time without increasing the width [33] and are defined as follows. For a node $t\in N$, we say that $\operatorname{type}(t)$ is leaf if $\operatorname{children}(t,T)=\langle\rangle$; join if $\operatorname{children}(t,T)=\langle t^{\prime},t^{\prime\prime}\rangle$ where $\chi(t)=\chi(t^{\prime})=\chi(t^{\prime\prime})\neq\emptyset$; int (“introduce”) if $\operatorname{children}(t,T)=\langle t^{\prime}\rangle$, $\chi(t^{\prime})\subseteq\chi(t)$ and $|\chi(t)|=|\chi(t^{\prime})|+1$; rem (“removal”) if $\operatorname{children}(t,T)=\langle t^{\prime}\rangle$, $\chi(t^{\prime})\supseteq\chi(t)$ and $|\chi(t^{\prime})|=|\chi(t)|+1$. If for every node $t\in N$, $\operatorname{type}(t)\in\{\textit{leaf},\textit{join},\textit{int},\textit{rem}\}$, and $\chi(t^{\prime})=\emptyset$ for root and leaf $t^{\prime}$, the TD is nice.

Example 3**.**

Figure 1 illustrates a graph $G_{1}$ and a tree decomposition of $G_{1}$ of width $2$. By a property444The vertices $e$,$b$,$d$ that are all neighbors to each other in $G_{1}$. of tree decompositions [33], the treewidth of $G_{1}$ is $2$.

Dynamic Programming on TDs

In order to use TDs for ASP solving, we need a dedicated graph representation of ASP programs [19].The primal graph $G_{\Pi}$ of program $\Pi$ has the atoms of $\Pi$ as vertices and an edge $\{a,b\}$ if there exists a rule $r\in\Pi$ and $a,b\in\text{at}(r)$.

Example 4**.**

Recall program $\Pi$ from Example 1 and observe that graph $G_{1}$ in Figure 1 is the primal graph $G_{\Pi}$ of $\Pi$.

Let ${\cal T}=(T,\chi)$ be a TD of primal graph $G_{\Pi}$ of a program $\Pi$. Further, let $T=(N,\cdot,n)$ and $t\in N$. The bag-program is defined as $\Pi_{t}\,\mathrel{\mathop{:}}=\{r\mid r\in\Pi,\text{at}(r)\subseteq\chi(t)\}$, the program below $t$ as $\Pi_{\leq t}\,\mathrel{\mathop{:}}=\{r\mid r\in\Pi_{t^{\prime}},t^{\prime}\in\operatorname{post-order}(T,t)\}$, and the program strictly below $t$ as $\Pi_{<t}\,\mathrel{\mathop{:}}=\Pi_{\leq t}\setminus\Pi_{t}$. It holds that $\Pi_{\leq n}=\Pi_{<n}=\Pi$ [19]. Analogously, we define the atoms below $t$ by $\text{at}_{\leq t}\,\mathrel{\mathop{:}}=\cup_{t^{\prime}\in\operatorname{post-order}(T,t)}\chi(t^{\prime})$, and the atoms strictly below $t$ by $\text{at}_{<t}\,\mathrel{\mathop{:}}=\text{at}_{\leq t}\setminus\chi(t)$. For an example we refer to Example 10⋆.

Algorithms that decide consistency or solve $\#$As  [19, 30] proceed by dynamic programming (DP) along the TD (in post-order) where at each node of the tree information is gathered [8] in a table by a (local) table algorithm $\mathbb{A}$. More generally, a table is a set of rows, where a row $\vec{}u$ is a sequence of fixed length. Similar as for sequences when addressing the $i$-th element, for a set $U$ of rows (table) we let $U_{(i)}\,\mathrel{\mathop{:}}=\{\vec{u}_{(i)}\mid\vec{u}\in U\}$. The actual length, content, and meaning of the rows depend on the algorithm $\mathbb{A}$. Since we later traverse the TD repeatedly running different algorithms, we explicitly state $\mathbb{A}$-row if rows of this type are syntactically used for algorithm $\mathbb{A}$ and similar $\mathbb{A}$-table for tables. In order to access tables computed at certain nodes after a traversal as well as to provide better readability, we attribute TDs with an additional mapping to store tables. Formally, a tabled tree decomposition (TTD) of graph $G$ is a triple $\mathcal{T}=(T,\chi,\tau)$, where $(T,\chi)$ is a TD of $G$ and $\tau$ maps nodes $t$ of $T$ to tables. If not specified otherwise, we assume that $\tau(t)=\{\}$ for every node $t$ of $T$. When a TTD has been computed using algorithm $\mathbb{A}$ after traversing the TD, we call the decomposition the $\mathbb{A}$-TTD of the given instance. DP for ASP performs the following steps:

1. Given program $\Pi$, compute a tree decomposition of the primal graph $P_{\Pi}$.

2. Run algorithm $\mathtt{DP}_{\mathbb{A}}$ (see Listing 1). It takes a TTD $\mathcal{T}=(T,\chi,\iota)$ with $T=(N,\cdot,n)$ and traverses $T$ in post-order555$\text{post-order}(T,n)$ provides the sequence of nodes for tree $T$ rooted at $n$.. At each node $t\in N$ it computes a new $\mathbb{A}$-table $o(t)$ by executing the algorithm $\mathbb{A}$. Algorithm $\mathbb{A}$ has a “local view” on the computation and can access only $t$, the atoms in the bag $\chi(t)$, the bag-program $\Pi_{t}$, and $\mathbb{A}$-table $o(t^{\prime})$ for any child $t^{\prime}$ of $t$.666Note that in Listing 1, $\mathbb{A}$ takes in addition as input set $P$ and table $\iota_{t}$, used later. Later, $P$ represents the projected atoms and $\iota_{t}$ is a table at $t$ from an earlier traversal. Finally, $\mathtt{DP}_{\mathbb{A}}$ returns an $\mathbb{A}$-TTD $(T,\chi,o)$.

3. Print the result by interpreting table $o(n)$ for root $n$ of $T$.

Then, the actual computation of algorithm $\mathbb{A}$ is a somewhat technical case distinction of the types $\operatorname{type}(t)$ we see when considering node $t$. Algorithms for counting answer sets of disjunctive programs [30] and its extensions [19] have already been established. Implementations of these algorithms can be useful also for solving [19, 20], but the running time is clearly double exponential time in the treewidth in the worst case. We, however, establish an algorithm (${\mathbb{PHC}}$) that is restricted to head-cycle-free programs. The runtime of our algorithm is factorial in the treewidth and therefore faster than previous algorithms. Our constructions are inspired by ideas used in previous DP algorithms  [43]. In the following, we first present the table algorithm for deciding whether a head-cycle-free program has an answer set (As). In the end, this algorithm outputs a new TTD, which we later reuse to solve the actual counting problem. Note that the TD itself remains the same, but for readability, we keep computed tables and nodes aligned.

Consistency of Head-Cycle-Free Programs. We can use algorithm $\mathtt{DP}_{\mathbb{PHC}}$ to decide the consistency problem As for head-cycle-free programs and simply specify our new table algorithm (${\mathbb{PHC}}$) that “transforms” tables from one node to another. As graph representation we use the primal graph. The idea is to implicitly apply along the TD the characterization of answer sets by Lin and Zhao [36] extended to head-cycle-free programs [4]. To this end, we store in table $o(t)$ at each node $t$ rows of the form $\langle I,\mathcal{P},\sigma\rangle$. The first position consists of an interpretation $I$ restricted to the bag $\chi(t)$. For a sequence $\vec{}u$, we write $\mathcal{I}(\vec{}u)\,\mathrel{\mathop{:}}=\vec{u}_{(1)}$ to address the interpretation part. The second position consists of a set $\mathcal{P}\subseteq I$ that represents atoms in $I$ for which we know that they have already been proven. The third position $\sigma$ is a sequence of the atoms in $I$ such that there is a super-sequence $\sigma^{\prime}$ of $\sigma$, which induces an ordering $<_{\sigma^{\prime}}$. Our table algorithm ${\mathbb{PHC}}$ stores interpretation parts always restricted to bag $\chi(t)$ and ensures that an interpretation can be extended to a model of sub-program $\Pi_{\leq t}$. More precisely, it guarantees that interpretation $I$ can be extended to a model $I^{\prime}\supseteq I$ of $\Pi_{\leq t}$ and that the atoms in $I^{\prime}\setminus I$ (and the atoms in $\mathcal{P}\subseteq I$) have already been proven, using some induced ordering $<_{\sigma^{\prime}}$ where $\sigma$ is a sub-sequence of $\sigma^{\prime}$. In the end, an interpretation $\mathcal{I}(\vec{u})$ of a row $\vec{u}$ of the table $o(n)$ at the root $n$ proves that there is a superset $I^{\prime}\supseteq\mathcal{I}(\vec{u})$ that is an answer set of $\Pi=\Pi_{\leq n}$.

Listing 2 presents the algorithm ${\mathbb{PHC}}$. Intuitively, whenever an atom $a$ is introduced (int), we decide whether we include $a$ in the interpretation, determine bag atoms that can be proven in consequence of this decision, and update the sequence $\sigma$ accordingly. To this end, we define for a given interpretation $I$ and a sequence $\sigma$ the set $\operatorname{proven}(I,\sigma,\Pi_{t})\,\mathrel{\mathop{:}}=\cup_{r\in\Pi_{t},a\in H_{r}}\{a\mid B_{r}^{+}\subseteq I,I\cap B^{-}_{r}=\emptyset,I\cap(H_{r}\setminus\{a\})=\emptyset,B^{+}_{r}<_{\sigma}a\}$ where $B^{+}_{r}<_{\sigma}a$ holds if $b<_{\sigma}a$ is true for every $b\in B^{+}_{r}$. Moreover, given a sequence $\sigma=\langle\sigma_{1},\ldots,\sigma_{k}\rangle$ and a set $A$ of atoms, we compute the potential sequences involving $A$. Therefore, we let $\operatorname{ords}(\sigma,A)\,\mathrel{\mathop{:}}=\{\sigma\mid A=\emptyset\}\cup\bigcup_{a\in A}\{\langle a,\sigma_{1},\ldots,\sigma_{k}\rangle,\ldots,\langle\sigma_{1},\ldots,\sigma_{k},a\rangle\}$. When removing (rem) an atom $a$, we only keep those rows where $a$ has been proven (contained in $\mathcal{P}$) and then restrict remaining rows to the bag (not containing $a$). In case the node is of type join, we combine two rows in two different child tables, intuitively, we are enforced to agree on interpretations $I$ and sequences $\sigma$. However, concerning individual proofs $\mathcal{P}$, it suffices that an atom is proven in one of the rows.

Example 5**.**

Recall program $\Pi$ from Example 1. Figure 2 depicts a TD $\mathcal{T}=(T,\chi)$ of the primal graph $G_{1}$ of $\Pi$. Further, the figure illustrates a snippet of tables of the TTD $(T,\chi,\tau)$, which we obtain when running $\mathtt{DP}_{{\mathbb{PHC}}}$ on program $\Pi$ and TD $\mathcal{T}$ according to Listing 2. In the following, we briefly discuss some selected rows of those tables. Note that for simplicity and space reasons, we write $\tau_{j}$ instead of $\tau(t_{j})$ and identify rows by their node and identifier $i$ in the figure. For example, the row $\vec{}u_{13.3}=\langle I_{13.3},\mathcal{P}_{13.3},\sigma_{13.3}\rangle\in\tau_{13}$ refers to the third row of table $\tau_{13}$ for node $t_{13}$. Node $t_{1}$ is of type leaf. Table $\tau_{1}$ has only one row, which consists of the empty interpretation, empty set of proven atoms, and the empty sequence (Line 2). Node $t_{2}$ is of type int and introduces atom $a$. Executing Line 2 results in $\tau_{2}=\{\langle\emptyset,\emptyset,\langle\rangle\rangle,\langle\{a\},\emptyset,\langle a\rangle\rangle\}$. Node $t_{3}$ is of type int and introduces $b$. Then, bag-program at node $t_{3}$ is $\Pi_{t_{3}}=\{a\vee b\leftarrow\,\}$. By construction (Line 2) we ensure that interpretation $I_{3.i}$ is a model of $\Pi_{t_{3}}$ for every row $\langle I_{3.i},\mathcal{P}_{3.i},\sigma_{3.i}\rangle$ in $\tau_{3}$. Node $t_{4}$ is of type rem. Here, we restrict the rows such that they contain only atoms occurring in bag $\chi(t_{4})=\{b\}$. To this end, Line 2 takes only rows $\vec{}u_{3.i}$ of table $\tau_{3}$ where atoms in $I_{3.i}$ are also proven, i.e., contained in $\mathcal{P}_{3.i}$. In particular, every row in table $\tau_{4}$ originates from at least one row in $\tau_{3}$ that either proves $a\in\mathcal{P}_{3.i}$ or where $a\not\in I_{3.i}$. Basic conditions of a TD ensure that once an atom is removed, it will not occur in any bag at an ancestor node. Hence, we also encountered all rules where atom $a$ occurs. Nodes $t_{5},t_{6},t_{7}$, and $t_{8}$ are symmetric to nodes $t_{1},t_{2},t_{3}$, and $t_{4}$. Nodes $t_{9}$ and $t_{10}$ again introduce atoms. Observe that $\mathcal{P}_{10.4}=\{e\}$ since $\sigma_{10.4}$ does not allow to prove $b$ using atom $e$. However, $\mathcal{P}_{10.5}=\{b,e\}$ as the sequence $\sigma_{10.5}$ allows to prove $b$. In particular, in row $\vec{}u_{10.5}$ atom $e$ is used to derive $b$. As a result, atom $b$ can be proven, whereas ordering $\sigma_{10.4}=\langle b,e\rangle$ does not serve in proving $b$. We proceed similar for nodes $t_{11}$ and $t_{12}$. At node $t_{13}$ we join tables $\tau_{4}$ and $\tau_{12}$ according to Line 2. Finally, $\tau_{14}\neq\emptyset$, i.e., $\Pi$ has an answer set; joining interpretations $I$ of yellow marked rows of Figure 2 leads to $\{b,e\}$.

Next, we provide a notion to reconstruct answer sets from a computed TTD, which allows for computing for a given row its predecessor rows in the corresponding child tables, c.f., [21]. Let $\Pi$ be a program, $\mathcal{T}=(T,\chi,\tau)$ be an $\mathbb{A}$-TTD of $G_{\Pi}$, and $t$ be a node of $T$ where $\operatorname{children}(t,T)=\langle t_{1},\ldots,t_{\ell}\rangle$. Given a sequence $\vec{s}=\langle s_{1},\ldots,s_{\ell}\rangle$, we let $\langle\{\vec{s}\}\rangle{\,\mathrel{\mathop{:}}=}\langle\{s_{1}\},\ldots,\{s_{\ell}\}\rangle$. For a given $\mathbb{A}$-row $\vec{u}$, we define the originating $\mathbb{A}$-rows of $\vec{u}$ in node $t$ by $\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\vec{}u){\,\mathrel{\mathop{:}}=}\{\vec{s}\mid\vec{s}\in\tau(t_{1})\times\cdots\times\tau({t_{\ell}}),\vec{u}\in{\mathbb{A}}(t,\chi(t),\cdot,(\Pi_{t},\cdot),\langle\{\vec{s}\}\rangle)\}.$ We extend this to an $\mathbb{A}$-table $\rho$ by $\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\rho){\,\mathrel{\mathop{:}}=}\bigcup_{\vec{u}\in\rho}\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\vec{u})$.

Example 6**.**

Consider program $\Pi$ and ${\mathbb{PHC}}$-TTD $(T,\chi,\tau)$ from Example 5. We focus on $\vec{u_{1.1}}=\langle\emptyset,\emptyset,\langle\rangle\rangle$ of table $\tau_{1}$ of leaf $t_{1}$. The row $\vec{u_{1.1}}$ has no preceding row, since $\operatorname{type}(t_{1})=\textit{leaf}$. Hence, we have $\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}(t_{1},\vec{u_{1.1}})=\{\langle\rangle\}$. The origins of row $\vec{u_{11.1}}$ of table $\tau_{11}$ are given by $\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}(t_{11},\vec{u_{11.1}})$, which correspond to the preceding rows in table $\tau_{10}$ that lead to row $\vec{u_{11.1}}$ of table $\tau_{11}$ when running algorithm ${\mathbb{PHC}}$, i.e., $\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}(t_{11},\vec{u_{11.1}})=\{\langle\vec{u_{10.1}}\rangle,\langle\vec{u_{10.6}}\rangle,\langle\vec{u_{10.7}}\rangle\}$. Origins of row $\vec{{u}_{12.2}}$ are given by $\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}(t_{12},\vec{u_{12.2}})=\{\langle\vec{u_{11.2}}\rangle,\langle\vec{u_{11.6}}\rangle\}$. Note that $\vec{u_{11.4}}$ and $\vec{u_{11.5}}$ are not among those origins, since $d$ is not proven. Observe that $\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}(t_{j},\vec{}u)=\emptyset$ for any row $\vec{}u\not\in\tau_{j}$. For node $t_{13}$ of type join and row $\vec{u_{13.2}}$, $\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}(t_{13},\vec{u_{13.2}})$ $=\{\langle\vec{u_{4.2}},$ $\vec{u_{12.2}}\rangle,\langle\vec{u_{4.2}},$ $\vec{u_{12.3}}\rangle\}$.

Next, we provide statements on correctness and a runtime analysis.

Theorem 2** ($\star$).**

The algorithm $\mathtt{DP}_{\mathbb{PHC}}$ is correct. In other words, given a head-cycle-free program $\Pi$ and a TTD ${\cal T}=(T,\chi,\cdot)$ of $G_{\Pi}$ where $T=(N,\cdot,n)$ with root $n$. Then, $\mathtt{DP}_{\mathbb{PHC}}((\Pi,\cdot),\mathcal{T})$ returns the ${\mathbb{PHC}}$-TTD $(T,\chi,\tau)$ such that $\Pi$ has an answer set if and only if $\langle\emptyset,\emptyset,\langle\rangle\rangle\in\tau(n)$. Further, we can construct all the answer sets of $\Pi$ from transitively following the origins of $\tau(n)$.

Proof (Idea).

For soundness, we state and establish an invariant for every node $t\in N$. For each row $\vec{}u=\langle I,\mathcal{P},\sigma\rangle\in\tau(t)$, we have $I\subseteq\chi(t),\mathcal{P}\subseteq I$, and $\sigma$ is a sequence over atoms in $I$. Intuitively, we ensure existence of $I^{\prime}\supseteq I$ s.t. $I^{\prime}\models\Pi_{\leq t}$ and that exactly the atoms in $\text{at}_{<t}$ and $\mathcal{P}$ can be proven using a super-sequence $\sigma^{\prime}$ of $\sigma$. By construction, we guarantee that we can decide consistency if row $\langle\emptyset,\emptyset,\langle\rangle\rangle\in\tau(n)$. Further, we can even reconstruct answer sets, by following $\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}$ of this single row back to the leaves. For completeness, we show that we indeed obtain all required rows to output all the answer sets of $\Pi$. ∎

Theorem 3**.**

Given a head-cycle-free program $\Pi$ and a TD ${\cal T}=(T,\chi)$ of $G_{\Pi}$ of width $k$ with $g$ nodes. Algorithm $\mathtt{DP}_{{\mathbb{PHC}}}$ runs in time $\mathcal{O}(3^{k}\cdot k!\cdot g)=\mathcal{O}(2^{k\cdot\text{log}(k)}\cdot g)$.

Proof (Sketch).

Let $d=k+1$ be maximum bag size of the tree decomposition $\mathcal{T}$. The table $\tau(t)$ has at most $3^{d}\cdot d!$ rows, since for a row $\langle I,\mathcal{P},\sigma\rangle$ we have $d!$ many sequences $\sigma$, and by construction of algorithm ${\mathbb{PHC}}$, an atom can be either in $I$, both in $I$ and $\mathcal{P}$, or neither in $I$ nor in $\mathcal{P}$. In total, with the help of efficient data structures, e.g., for nodes $t$ with $\operatorname{type}(t)=\textit{join}$, one can establish a runtime bound of ${\mathcal{O}}({3^{d}\cdot d!})$. Then, we apply this to every node $t$ of the tree decomposition, which resulting in running time ${\mathcal{O}}({3^{d}\cdot d!}\cdot g)\subseteq{\mathcal{O}}(3^{k}\cdot k!\cdot g)$. ∎

In order to obtain an upper bound on width factorial $k!$, we can simply take $k!\leq 2^{k}$ for any fixed width $k\leq 3$. While in general $k!$ is obviously not bounded by $2^{k}$ for any fixed $k\geq 4$, asymptotically $k!$ is bounded by $2^{k^{(c+1)/c}}$ for any fixed positive integer $c\geq 1$ as stated in Lemma 1.

Lemma 1** ($\star$).**

Given any fixed positive integer $c\geq 1$ and functions $f(k){\,\mathrel{\mathop{:}}=}k!,g(k){\,\mathrel{\mathop{:}}=}2^{k^{(c+1)/c}}$, where $k$ is a non-negative integer. Then, $f\in{\mathcal{O}}(g)$.

In particular, $k!\leq 2^{k^{4/3}}$ for $k\geq 342$, $k!\leq 2^{k^{5/4}}$ for $k\geq 34556$, and $k!\leq 2^{k^{6/5}}$ for $k\geq 3413636$.

A natural question is whether we can significantly improve this algorithm for fixed $k$. To this end, we take the exponential time hypothesis (ETH) into account [29], which states that there is some real $s>0$ such that we cannot decide satisfiability of a given 3-CNF formula $F$ in time $2^{s\cdot\left|F\right|}\cdot\|F\|^{\mathcal{O}(1)}$.

Proposition 1**.**

Unless ETH fails, consistency of head-cycle-free, normal or tight program $\Pi$ cannot be decided in time $2^{o(k)}\cdot\|\Pi\|^{o(k)}$ where $k=\mathit{tw}(G_{\Pi})$.

Proof.

Reduction from SAT to As similar to the proof of Theorem 1. ∎

In the construction above, we store an arbitrary but fixed ordering $\sigma$ on the involved atoms. We believe that we cannot avoid these orderings in general, since we have to compensate arbitrarily “bad” orderings induced by the decomposition. Hence, we claim that As for head-cycle-free programs is slightly superexponential, rendering our algorithm asymptotically worst-case optimal. Lokshtanov, Marx and Saurabh confirm such an expectation [37] whenever orderings are required.

Conjecture 1**.**

Unless ETH fails, consistency of a head-cycle-free program $\Pi$ cannot be decided in time $2^{o(k\cdot\text{log}(k))}\cdot\|\Pi\|^{o(k)}$ where $k=\mathit{tw}(G_{\Pi})$.

Dynamic Programming for $\#\textsc{PAs}$

In this section, we present our DP algorithm777Later we use (among others) $\mathtt{PCNT}_{{\mathbb{PHC}}}$ where $\mathbb{A}={\mathbb{PHC}}$. $\mathtt{PCNT}_{\mathbb{A}}$, which allows for solving the projected answer set counting problem ($\#$PAs). $\mathtt{PCNT}_{\mathbb{A}}$ is based on an approach of projected counting for Boolean formulas [21] where TDs are traversed multiple times. We show that ideas from that approach can be fruitfully extended to answer set programming. Figure 3 illustrates the steps of $\mathtt{PCNT}_{\mathbb{A}}$. First, we construct the primal graph $G_{\Pi}$ of the input program $\Pi$ and compute a TD of $\Pi$. Then, we traverse the TD a first time by running $\mathtt{DP}_{\mathbb{A}}$ (Step 2a), which outputs a TTD $\mathcal{T}_{\text{cons}}=(T,\chi,\tau)$, where $T=(N,\cdot,n)$. Afterwards, we traverse $\mathcal{T}_{\text{cons}}$ in pre-order and remove all rows from the tables that cannot be extended to an answer set (“Purge non-solutions”). In other words, we keep only rows $\vec{u}$ of table $\tau(t)$ at node $t$, if $\vec{u}$ is involved in those rows that are used to construct an answer set of $\Pi$, and let the resulting TTD888Table $\nu(t)$ contains rows obtained by recursively following origins of $\tau(n)$ for root $n$. Formal details are in Definition 1⋆. be $\mathcal{T}_{\text{purged}}=(T,\chi,\nu)$. We refer to $\nu$ as purged table mapping. In Step 2b ($\mathtt{DP}_{\mathbb{PROJ}}$), we traverse $\mathcal{T}_{\text{purged}}$ to count interpretations with respect to the projection atoms and obtain $\mathcal{T}_{\text{proj}}=(T,\chi,\pi)$. From the table $\pi(n)$ at the root $n$ of $T$, we can then read the projected answer sets count of the input instance. In the following, we only describe the table algorithm $\mathbb{PROJ}$, since the traversal in $\mathtt{DP}_{\mathbb{PROJ}}$ is the same as before. For $\mathbb{PROJ}$, a row at a node $t$ is a pair $\langle\rho,c\rangle\in\pi(t)$, where $\rho\subseteq\nu(t)$ is an $\mathbb{A}$-table and $c$ is a non-negative integer. In fact, integer $c$ stores the number of intersecting solutions ($\operatorname{ipasc}$). However, we aim for the projected answer sets count ($\operatorname{pasc}$), whose computation requires

a few additional definitions. Therefore, we can simply widen definitions from very recent work [21].

In the remainder, we assume $(\Pi,P)$ to be an instance of $\#$PAs, $(T,\chi,\tau)$ to be an $\mathbb{A}$-TTD of $G_{\Pi}$ and the mappings $\tau$, $\nu$, and $\pi$ as used above. Further, let $t$ be a node of $T$ with $\operatorname{children}(t,T)=\langle t_{1},\ldots,t_{\ell}\rangle$ and let $\rho\subseteq\nu(t)$. The relation $\operatorname{=_{P}}\subseteq\rho\times\rho$ considers equivalent rows with respect to the projection of its interpretations by $\operatorname{=_{P}}{\,\mathrel{\mathop{:}}=}\{(\vec{u},\vec{v})\mid\vec{u},\vec{v}\in\rho,\mathcal{I}(\vec{u})\cap P=\mathcal{I}(\vec{v})\cap P\}.$ Let $\operatorname{buckets}_{P}(\rho)$ be equivalence classes induced by $\operatorname{=_{P}}$ on $\rho$, i.e., $\operatorname{buckets}_{P}(\rho){\,\mathrel{\mathop{:}}=}\,(\rho/\operatorname{=_{P}})=\{[\vec{u}]_{P}\mid\vec{u}\in\rho\}$, where $[\vec{u}]_{P}=\{\vec{v}\mid\vec{v}\operatorname{=_{P}}\vec{u},\vec{v}\in\rho\}$ [45]. Further, $\operatorname{sub\hbox{-}\nobreak\hskip 0.0ptbuckets}_{P}(\rho){\,\mathrel{\mathop{:}}=}\cup_{S\mid\emptyset\neq S\subseteq\operatorname{buckets}_{P}(\rho)}\{S\}$.

Example 7**.**

Consider program $\Pi$, set $P$, TTD $(T,\chi,\tau)$, and table $\tau_{10}$ from Example 2 and Figure 2. Rows $\vec{u_{10.2}}$ and $\vec{u_{10.8}},\ldots,\vec{u_{10.13}}$ are removed (highlighted gray) during purging, since they are not involved in any answer set, resulting in $\nu_{10}$. Then, $\vec{u_{10.4}}=_{P}\vec{u_{10.5}}$ and $\vec{u_{10.6}}=_{P}\vec{u_{10.7}}$. The set $\nu_{10}/\operatorname{=_{P}}$ of equivalence classes of $\nu_{10}$ is $\operatorname{buckets}_{P}(\nu_{10})=\{\{\vec{u_{10.1}}\},\{\vec{u_{10.3}}\},\{\vec{u_{10.4}},\vec{u_{10.5}}\},\{\vec{u_{10.6}},\vec{u_{10.7}}\}\}$.

Later, we require to construct already computed projected counts for tables of children of a given node $t$. Therefore, we define the stored $\operatorname{ipasc}$ of a table $\rho\subseteq\nu(t)$ in table $\pi(t)$ by $\operatorname{s-ipasc}(\pi(t),\rho){\,\mathrel{\mathop{:}}=}\Sigma_{\langle\rho,c\rangle\in\pi(t)}c.$ We extend this to a sequence $s=\langle\pi(t_{1}),\ldots,\pi(t_{\ell})\rangle$ of tables of length $\ell$ and a set $O=\{\langle\rho_{1},\ldots,\rho_{\ell}\rangle,\langle\rho_{1}^{\prime},\ldots,\rho_{\ell}^{\prime}\rangle,\ldots\}$ of sequences of $\ell$ tables by $\operatorname{s-ipasc}(s,O)=\Pi_{i\in\{1,\ldots,\ell\}}\operatorname{s-ipasc}(s_{(i)},O_{(i)}).$ So we select the $i$-th position of the sequence together with sets of the $i$-th positions.

Intuitively, when we are at a node $t$ in algorithm $\mathtt{DP}_{\mathbb{PROJ}}$ we have already computed $\pi(t^{\prime})$ of $\mathcal{T}_{\text{proj}}$ for every node $t^{\prime}$ below $t$. Then, we compute the projected answer sets count of $\rho\subseteq\nu(t)$. Therefore, we apply the inclusion-exclusion principle to the stored projected answer sets count of origins. We define $\operatorname{pasc}(t,\rho,\langle\pi(t_{1}),\ldots\rangle){\,\mathrel{\mathop{:}}=}\Sigma_{\emptyset\subsetneq O\subseteq{\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\rho)}}$ $(-1)^{(\left|O\right|-1)}\cdot\operatorname{s-ipasc}(\langle\pi(t_{1}),\ldots\rangle,O)$. Intuitively, $\operatorname{pasc}$ determines the $\mathbb{A}$-origins of table $\rho$, goes over all subsets of these origins and looks up stored counts ($\operatorname{s-ipasc}$) in $\mathbb{PROJ}$-tables of children $t_{i}$ of $t$.

Example 8**.**

Consider again program $\Pi$ and TD $\mathcal{T}$ from Example 1 and Figure 2. First, we compute the projected count $\operatorname{pasc}(t_{4},\{\vec{u_{4.1}}\},\langle\pi(t_{3})\rangle)$ for row $\vec{u_{4.1}}$ of table $\nu(t_{4})$, where \pi(t_{3}){\,\mathrel{\mathop{:}}=}\allowdisplaybreaks[4]\big{\{}\langle\{\vec{u_{3.1}}\},1\rangle, \langle\{\vec{u_{3.2}}\},1\rangle,\langle\{\vec{u_{3.1}},\vec{u_{3.2}}\},1\rangle\big{\}} with $\vec{u_{3.1}}=\langle\emptyset,\emptyset,\langle\rangle\rangle$ and $\vec{u_{3.2}}=\langle\{a\},\emptyset,\langle a\rangle\rangle$. Note that $t_{5}$ has only the child $t_{4}$ and therefore the product in $\operatorname{s-ipasc}$ consists of only one factor. Since $\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}(t_{4},\vec{u_{4.1}})=\{\langle\vec{u_{3.1}}\rangle\}$, only the value of $\operatorname{s-ipasc}$ for set $\{\langle\vec{u_{3.1}}\rangle\}$ is non-zero. Hence, we obtain $\operatorname{pasc}(t_{4},\{\vec{u_{4.1}}\},\langle\pi(t_{3})\rangle)$ $=1$. Next, we compute $\operatorname{pasc}(t_{4},\{\vec{u_{4.1}},\vec{u_{4.2}}\},\langle\pi(t_{3})\rangle)$. Observe that $\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}(t_{4},\{\vec{u_{4.1}},\vec{u_{4.2}}\})=\{\langle\vec{u_{3.1}}\rangle,\langle\vec{u_{3.2}}\rangle\}$. We sum up the values of $\operatorname{s-ipasc}$ for sets $\{\vec{u_{4.1}}\}$ and $\{\vec{u_{4.2}}\}$ and subtract the one for set $\{\vec{u_{4.1}},\vec{u_{4.2}}\}$. Hence, we obtain $\operatorname{pasc}(t_{4},\{\vec{u_{4.1}},\vec{u_{4.2}}\},\langle\pi(t_{3})\rangle)=1+1-1=1$.

Next, we provide a definition to compute $\operatorname{ipasc}$ at a node $t$ for given table $\rho\subseteq\nu(t)$ by computing $\operatorname{pasc}$ for children $t_{i}$ of $t$ using stored $\operatorname{ipasc}$ values from tables $\pi(t_{i})$, and subtracting and adding $\operatorname{ipasc}$ values for subsets $\emptyset\subsetneq\varphi\subsetneq\rho$ accordingly. Formally, $\operatorname{ipasc}(t,\rho,s){\,\mathrel{\mathop{:}}=}1$ if $\operatorname{type}(t)=\textit{leaf}$ and otherwise \operatorname{ipasc}(t,\rho,s){\,\mathrel{\mathop{:}}=}\big{|}\operatorname{pasc}(t,\rho,s) +\Sigma_{\emptyset\subsetneq\varphi\subsetneq\rho}(-1)^{\left|\varphi\right|}\cdot\operatorname{ipasc}(t,\varphi,s)\big{|} where $s=\langle\pi(t_{1}),\ldots\rangle$. In other words, if a node is of type leaf the $\operatorname{ipasc}$ is one, since bags of leaf nodes are empty. Otherwise, we compute the “non-overlapping” count of given table $\rho\subseteq\nu(t)$ with respect to $P$, by exploiting inclusion-exclusion principle on $\mathbb{A}$-origins of $\rho$ such that we count every projected answer set only once. Then we have to subtract and add $\operatorname{ipasc}$ values (“all-overlapping” counts) for strict subsets $\varphi$ of $\rho$, accordingly. Finally, Listing 3 presents table algorithm $\mathbb{PROJ}$, which stores $\pi(t)$ consisting of every sub-bucket of given table $\nu(t)$ together with its $\operatorname{ipasc}$.

Example 9**.**

Recall instance $(\Pi,P)$, TD $\mathcal{T}$, and tables $\tau_{1}$, $\ldots$, $\tau_{14}$ from Examples 2, 5, and Figure 2. Figure 4 depicts selected tables of $\pi_{1},\ldots,\pi_{14}$ obtained after running $\mathtt{DP}_{\mathbb{PROJ}}$ for counting projected answer sets. We assume that row $i$ in table $\pi_{t}$ corresponds to $\vec{v_{t.i}}=\langle\rho_{t.i},c_{t.i}\rangle$ where $\rho_{t.i}\subseteq\nu(t)$. Recall that there are rows among different ${\mathbb{PHC}}$-tables that are removed (highlighted gray in Figure 2) during purging. By purging we avoid to correct stored counters (backtracking) whenever a row has no “succeeding” row in the parent table. Next, we discuss selected rows obtained by $\mathtt{DP}_{\mathbb{PROJ}}((\Pi,P),(T,\chi,\nu))$. Tables $\pi_{1}$, $\ldots$, $\pi_{14}$ are shown in Figure 4. Since $\operatorname{type}(t_{1})=\textit{leaf}$, we have $\pi_{1}=\langle\{\langle\emptyset,\emptyset,\langle\rangle\rangle\},1\rangle$. Intuitively, at $t_{1}$ the row $\langle\emptyset,\emptyset,\langle\rangle\rangle$ belongs to $1$ bucket. Node $t_{2}$ introduces atom $a$, which results in table \pi_{2}{\,\mathrel{\mathop{:}}=}\big{\{}\langle\{\vec{u_{2.1}}\},1\rangle,\langle\{\vec{u_{2.2}}\},1\rangle,\langle\{\vec{u_{2.1}},\vec{u_{2.2}}\},1\rangle\big{\}}, where $\vec{u_{2.1}}=\langle\emptyset,\emptyset,\langle\rangle\rangle$ and $\vec{u_{2.2}}=\langle\{a\},\emptyset,\langle a\rangle\rangle$ (derived similarly to table $\pi_{4}$ as in Example 8). Node $t_{10}$ introduces projected atom $e$, and node $t_{11}$ removes $e$. For row $\vec{v_{11.1}}$ we compute the count $\operatorname{ipasc}(t_{11},\{\vec{u_{11.1}}\},\langle\pi_{10}\rangle)$ by means of $\operatorname{pasc}$. Therefore, take for $\varphi$ the singleton set $\{\vec{u_{11.1}}\}$. We simply have $\operatorname{ipasc}(t_{11},\{\vec{u_{11.1}}\},\langle\pi_{10}\rangle)=\operatorname{pasc}(t_{11},\{\vec{u_{11.1}}\},\langle\pi_{10}\rangle)$. To compute $\operatorname{pasc}(t_{11},\{\vec{u_{11.1}}\},$ $\langle\pi_{10}\rangle)$, we take for $O$ the sets $\{\vec{u_{10.1}}\}$, $\{\vec{u_{10.6}}\}$, $\{\vec{u_{10.7}}\}$, and $\{\vec{u_{10.6}},\vec{u_{10.7}}\}$ into account, since all other non-empty subsets of origins of $\vec{u_{11.1}}$ in $\nu_{10}$ do not occur in $\pi_{10}$. Then, we take the sum over the values $\operatorname{s-ipasc}(\langle\pi_{10}\rangle,\{\vec{u_{10.1}}\})=1$, $\operatorname{s-ipasc}(\langle\pi_{10}\rangle,\{\vec{u_{10.6}}\})=1$, $\operatorname{s-ipasc}(\langle\pi_{10}\rangle,\{\vec{u_{10.7}}\})=1$ and subtract $\operatorname{s-ipasc}(\langle\pi_{10}\rangle,$ $\{\vec{u_{10.6}},\vec{u_{10.7}}\})=1$. This results in $\operatorname{pasc}(t_{11},\{\vec{u_{11.1}}\},\langle\pi_{10}\rangle)=c_{10.1}+c_{10.7}\;+$ $c_{10.8}-c_{10.9}=2$. We proceed similarly for row $v_{11.2}$, resulting in $c_{11.2}=1$. Then for row $v_{11.3}$, $\operatorname{ipasc}(t_{11},\{\vec{u_{11.1}},\vec{u_{11.6}}\},\langle\pi_{10}\rangle)=|\operatorname{pasc}(t_{11},\{\vec{u_{11.1}},\vec{u_{11.6}}\},\langle\pi_{10}\rangle)-\operatorname{ipasc}(t_{11},\{$ $\vec{u_{11.1}}\},\langle\pi_{10}\rangle)$ $-\operatorname{ipasc}(t_{11},\{\vec{u_{11.6}}\},\langle\pi_{10}\rangle)|=|2-c_{11.1}-$ $c_{11.2}|=|2-$ $2-1|=\left|-1\right|=1=c_{11.3}$. Hence, $c_{11.3}=1$ represents the number of projected answer sets, both rows $\vec{u_{11.1}}$ and $\vec{u_{11.6}}$ have in common. We then use it for table $t_{12}$. Node $t_{12}$ removes projection atom $d$. For node $t_{13}$ where $\operatorname{type}(t_{13})=\textit{join}$ one multiplies stored $\operatorname{s-ipasc}$ values for $\mathbb{A}$-rows in the two children of $t_{13}$ accordingly. In the end, the projected answer sets count of $\Pi$ is $\operatorname{s-ipasc}(\langle\pi_{14}\rangle,\vec{u_{14.1}})=3$.

Next, we present upper bounds on the runtime of $\mathtt{DP}_{\mathbb{PROJ}}$. Therefore, let $\gamma(n)\in\mathcal{O}(n\cdot log\,n\cdot log\,log\,n)$ [34, 28] be the runtime for multiplying two $n$-bit integers.

Theorem 4**.**

$\mathtt{DP}_{\mathbb{PROJ}}$* runs in time $\mathcal{O}(2^{4m}\cdot g\cdot\gamma(\|\Pi\|))$ for instance $(\Pi,P)$ and TTD $\mathcal{T}_{\text{purged}}=(T,\chi,\nu)$ of $G_{\Pi}$ of width $k$ with $g$ nodes, where $m{\,\mathrel{\mathop{:}}=}\max_{t\,\text{in}\,T}(|\nu(t)|)$.*

Proof.

Let $d=k+1$ be maximum bag size of the TD $\mathcal{T}$. For each node $t$ of $T$, we consider the table $\nu(t)$ of $\mathcal{T}_{\text{purged}}$. Let TDD $(T,\chi,\pi)$ be the output of $\mathtt{DP}_{\mathbb{PROJ}}$. In worst case, we store in $\pi(t)$ each subset $\rho\subseteq\nu(t)$ together with exactly one counter. Hence, we have at most $2^{m}$ many rows in $\rho$. In order to compute $\operatorname{ipasc}$ for $\rho$, we consider every subset $\varphi\subseteq\rho$ and compute $\operatorname{pasc}$. Since $\left|\rho\right|\leq m$, we have at most $2^{m}$ many subsets $\varphi$ of $\rho$. Finally, for computing $\operatorname{pasc}$, we consider in the worst case each subset of the origins of $\varphi$ for each child table, which are at most $2^{m}\cdot 2^{m}$ because of nodes $t$ with $\operatorname{type}(t)=\textit{join}$. In total, we obtain a runtime bound of ${\mathcal{O}}(2^{m}\cdot 2^{m}\cdot 2^{m}\cdot 2^{m}\cdot\gamma(\|\Pi\|))\subseteq{\mathcal{O}}(2^{4m}\cdot\gamma(\|\Pi\|))$ due to multiplication of two $n$-bit integers for nodes $t$ with $\operatorname{type}(t)=\textit{join}$ at costs $\gamma(n)$. Then, we apply this to every node of $T$ resulting in runtime ${\mathcal{O}}(2^{4m}\cdot g\cdot\gamma(\|\Pi\|))$. ∎

Corollary 1**.**

Given an instance $(\Pi,P)$ of $\#$PAs where $\Pi$ is head-cycle-free and $k=\mathit{tw}(G_{\Pi})$. Then, $\mathtt{PCNT}_{{\mathbb{PHC}}}$ runs in time $\mathcal{O}(2^{3^{k+1.27}\cdot k!}\cdot\|\Pi\|\cdot\gamma(\|\Pi\|))$.

Proof.

We can compute in time $2^{\mathcal{O}(k^{3})}\cdot\|G_{\Pi}\|$ a TD ${\cal T^{\prime}}$ with $g\leq\|\Pi\|$ nodes of width at most $k$ [7]. Then, we can simply run $\mathtt{DP}_{{\mathbb{PHC}}}$, which runs in time $\mathcal{O}({3^{k}\cdot k!}\cdot\|\Pi\|)$ by Theorem 3 and since the number of nodes of a tree decomposition is linear in the size of the input instance [7]. Then, we again traverse the TD for purging and output $\mathcal{T}_{\text{purged}}$, which runs in time single exponential in the treewidth and linear in the instance size. Finally, we run $\mathtt{DP}_{\mathbb{PROJ}}$ and obtain by Theorem 4 that the runtime bound $\mathcal{O}(2^{4\cdot 3^{k}\cdot k!}\cdot\|\Pi\|\cdot\gamma(\|\Pi\|))\subseteq$ $\mathcal{O}(2^{3^{k+1.27}\cdot k!}\cdot\|\Pi\|\cdot\gamma(\|\Pi\|))$. Hence, the corollary holds. ∎

Then, we present lower bounds, and show that $\mathtt{PCNT}_{{\mathbb{PHC}}}$ is indeed correct.

Theorem 5** (Lower Bound).**

Under ETH, $\#\textsc{PAs}$ cannot be solved in time $2^{2^{o(k)}}\cdot\|\Pi\|^{o(k)}$ for $(\Pi,P)$ s.t. $\Pi$ is head-cycle-free, normal or tight, $k=\mathit{tw}(G_{\Pi})$.

Proof.

Assume for proof by contradiction that there is such an algorithm. We show that this contradicts a very recent result [35, 21], which states that one cannot decide the validity of a QBF $\forall{V_{1}}.\exists V_{2}.E$ in time $2^{2^{o(k)}}\cdot\|E\|^{o(k)}$, where $E$ is in CNF. Let $(\forall{V_{1}}.\exists V_{2}.E,k)$ be an instance of $\forall\exists$-SAT parameterized by the treewidth $k$. Then, we reduce to an instance $((\Pi,P),2k)$ of the decision version $\#\textsc{PAs}$-exactly-$2^{\left|V_{1}\right|}$ when parameterized by treewidth of $G_{\Pi}$ such that $P=V_{1}$, the number of solutions is exactly $2^{\left|V_{1}\right|}$, and $\Pi$ is as follows. For each $v\in V_{1}\cup V_{2}$, program $\Pi$ contains rules $v\leftarrow\neg nv$ and $nv\leftarrow\neg v$. Each clause $x_{1}\vee\ldots\vee x_{i}\vee\neg x_{i+1}\vee\ldots\vee\neg x_{j}$ results in one additional rule $\leftarrow\,\neg x_{1},\ldots,\neg x_{i},x_{i+1},\ldots,x_{j}$. It is easy to see that the reduction is correct and therefore instance $((\Pi,P),2k)$ is a yes instance of $\#\textsc{PAs}$-exactly-$2^{\left|V_{1}\right|}$ if and only if $(\forall{V_{1}}.\exists V_{2}.E,k)$ is a yes instance of problem $\forall\exists$-SAT. In fact, $\Pi$ is head-cycle-free, normal and tight, and the reduction runs in polynomial time of $\Pi$ and at most doubles the treewidth due to duplication of atoms, which establishes the result. ∎

Finally, we state that indeed $\mathtt{PCNT}_{{\mathbb{PHC}}}$ gives the projected answer sets count of a given head-cycle-free program $\Pi$.

Proposition 2** ($\star$).**

Algorithm $\mathtt{PCNT}_{{\mathbb{PHC}}}$ is correct and outputs for any instance of $\#$PAs restricted to head-cycle-free programs its projected answer sets count.

Proof (Idea).

Soundness follows by establishing an invariant for any row of $\pi(t)$ guaranteeing that the values of $\operatorname{ipasc}$ indeed capture “all-overlapping” counts of $\Pi_{\leq t}$. One can show that the invariant is a consequence of the properties of ${\mathbb{PHC}}$ and the additional “purging” step, which neither destroys soundness nor completeness of $\mathtt{DP}_{\mathbb{PHC}}$. Further, completeness guarantees that all required rows are computed. ∎

Solving $\#$PAs for Disjunctive Programs. We extend our algorithm to projected answer set counting for disjunctive programs. Therefore, we simply use a table algorithm $\mathbb{A}$=$\mathbb{PRIM}$ for disjunctive ASP that was introduced in the literature [19, 30]. Recall algorithm $\mathtt{PCNT}_{\mathbb{A}}$ illustrated in Figure 3. First, we heuristically compute a TD of the primal graph. Then, we run $\mathtt{DP}_{\mathbb{PRIM}}$ as first traversal resulting in TTD $(T,\chi,\tau)$. Next, we purge rows of $\tau$, which cannot be extended to an answer set resulting in TTD $(T,\chi,\nu)$. Finally, we use $(T,\chi,\nu)$ to compute the projected answer sets count by $\mathtt{DP}_{\mathbb{PROJ}}$ and obtain TTD $(T,\chi,\pi)$.

Proposition 3** ($\star$).**

$\mathtt{PCNT}_{\mathbb{PRIM}}$* is correct, i.e., it outputs the projected answer sets count for any instance of $\#$PAs.*

The following lemma states the runtime results.

Lemma 2**.**

$\mathtt{PCNT}_{\mathbb{PRIM}}$* runs in time $\mathcal{O}(2^{2^{2^{k+3}}}\cdot\|\Pi\|\cdot\gamma(\|\Pi\|))$ for given instance $(\Pi,P)$ of $\#$PAs where $\Pi$ is a disjunctive program, and $k=\mathit{tw}(G_{\Pi})$.*

Proof.

The first two steps follow the proof of Corollary 1. However, $\mathtt{DP}_{\mathbb{PRIM}}$ runs in time $\mathcal{O}(2^{2^{k+2}}\cdot\|\Pi\|)$ [19]. Finally, we run $\mathtt{DP}_{\mathbb{PROJ}}$ and obtain by Theorem 4 that $\mathcal{O}(2^{4\cdot 2^{2^{k+2}}}\cdot\|\Pi\|\cdot\gamma(\|\Pi\|))\subseteq$ $\mathcal{O}(2^{2^{2^{k+3}}}\cdot\|\Pi\|\cdot\gamma(\|\Pi\|))$. ∎

Then, the runtime of algorithm $\mathtt{PCNT}_{\mathbb{PRIM}}$ cannot be significantly improved.

Theorem 6** (Lower Bound).**

$\#$PAs* cannot be solved in time $2^{2^{2^{o(k)}}}\cdot\|\Pi\|^{o(k)}$ for given instance $(\Pi,P)$, where $k=\mathit{tw}(G_{\Pi})$, unless ETH fails.*

Proof.

Assume for proof by contradiction that there is such an algorithm. We show that this contradicts a rather recent result [22] stating that one cannot decide validity of QBF $Q=\forall{V_{1}}.\exists V_{2}.\forall V_{3}.E$ in time $2^{2^{2^{o(k)}}}\cdot\|E\|^{o(k)}$ where $E$ is in DNF, which was anticipated by Marx and Mitsou [39]. Assume we have given such an instance when parameterized by the treewidth $k$. In the following, we employ a well-known reduction $R$ [15], which transforms $\exists V_{2}.\forall V_{3}.E$ into $\Pi=R(\exists V_{2}.\forall V_{3}.E)$ and gives a yes instance $\Pi$ of consistency if and only if $\exists V_{2}.\forall V_{3}.E$ is a yes instance of $\exists\forall$-SAT. Then, we reduce instance $(Q,k)$ via a reduction $S$ to an instance $((\Pi^{\prime},V_{1}),2k+2)$, where $\Pi^{\prime}=R(\exists V_{2}^{\prime}.\forall V_{3}.E)$, $V_{2}^{\prime}{\,\mathrel{\mathop{:}}=}V_{1}\cup V_{2}$, of the decision version $\#\textsc{PAs}$-exactly-$2^{\left|V_{1}\right|}$ of $\#\textsc{PAs}$ when parameterized by treewidth such that the number of projected answer sets is exactly $2^{\left|V_{1}\right|}$. It is easy to see that reduction $S$ gives a yes instance $(\Pi^{\prime},V_{1})$ of $\#\textsc{PAs}$-exactly-$2^{\left|V_{1}\right|}$ if and only if $\forall V_{1}.\exists V_{2}.\forall V_{3}.E$ is a yes instance of $\forall\exists\forall$-SAT. However, it remains to show that the reduction $S$ indeed increases the treewidth only linearly. Therefore, let $\mathcal{T}=(T,\chi)$ be TD of $E$. We transform $\mathcal{T}$ into a TD $\mathcal{T}^{\prime}=(T,\chi^{\prime})$ of $G_{\Pi^{\prime}}$ as follows. For each bag $\chi(t)$ of $\mathcal{T}$, we add vertices for the atoms $w$ and $w^{\prime}$ (two additional atoms introduced in reduction $R$) and in addition we duplicate each vertex $v$ in $\chi(t)$ (due to corresponding duplicate atoms introduced in reduction $R$). Observe that $\operatorname{width}(\mathcal{T}^{\prime})\leq 2\cdot\operatorname{width}(\mathcal{T})+2$. By construction of $R$, $\mathcal{T}^{\prime}$ is then a TD of $G_{\Pi^{\prime}}$. Hence, $S$ runs in polynomial time and linearly preserves the parameter. ∎

In total, we obtain results presented in Table 1. Indeed, there is an increase of complexity when going from As and $\#$As to $\#$PAs (c.f., Theorem 4). For solving As ($\#$As) on tight programs one can again reuse Algorithm $\mathbb{PHC}$ (Listing 2) without the orderings $\sigma$, or encode [16] to SAT and use established DP algorithms [44] for SAT ($\#$SAT). Then, $\#$PAs on tight programs can be solved after purging, followed by computing projected answer sets by means of $\mathtt{DP}_{\mathbb{PROJ}}$.

Conclusions

We introduced novel algorithms to count the projected answer sets ($\#$PAs) of tight, normal, head-cycle-free, and arbitrary disjunctive programs. Our algorithms employ dynamic programming and exploit small treewidth of the primal graph of the input program. More precisely, for disjunctive programs, the runtime is triple exponential in the treewidth and polynomial in the size of the instance, which can not be significantly improved under the exponential time hypothesis. When we restrict the input to tight, normal, and head-cycle-free programs, the runtime drops to double exponential, c.f., Table 1. Our results extend previous work to answer set programming and we believe it is applicable to further hard combinatorial problems, such as quantified Boolean formulas(QBF) [11] and circumscription [14].

Appendix A Additional Resources

Additional Examples

Example 10** (c.f.,[19]).**

Intuitively, the tree decomposition of Figure 1 enables us to evaluate program $\Pi$ by analyzing sub-programs $\{r_{2}\}$ and $\{r_{3},r_{4},r_{5}\}$, and combining results agreeing on $e$ followed by analyzing $\{r_{1}\}$. Indeed, for the given tree decomposition of Figure 1, $\Pi_{\leq t_{1}}=\{r_{2}\}$, $\Pi_{\leq t_{2}}=\{r_{3},r_{4},r_{5}\}$ and $\Pi=\Pi_{\leq t_{3}}=\{r_{1}\}\cup\Pi_{<t_{3}}$. Note that here $\Pi=\Pi_{\leq t_{3}}\neq\Pi_{<t_{3}}$ and the tree decomposition is not nice.

Parsimonious reductions

Let $L$ and $L^{\prime}$ be counting problems with witness functions $\mathcal{W}$ and $\mathcal{W}^{\prime}$. A parsimonious reduction from $L$ to $L^{\prime}$ is a polynomial-time reduction $r:\Sigma^{*}\rightarrow\Sigma^{\prime*}$ such that for all $I\in\Sigma^{*}$, we have $\left|\mathcal{W}(I)\right|=\left|\mathcal{W}^{\prime}(r(I))\right|$. It is easy to see that the counting complexity classes $\#\cdot\mathcal{C}$ defined above are closed under parsimonious reductions. It is clear for counting problems $L$ and $L^{\prime}$ that if $L\in\#\cdot\mathcal{C}$ and there is a parsimonious reduction from $L^{\prime}$ to $L$, then $L^{\prime}\in\#\cdot\mathcal{C}$.

Counting Complexity of $\#$PAs: Omitted proofs

Theorem 1.

The problem $\#\textsc{PAs}$ is #$\cdot\Sigma_{2}P$-complete when we allow disjunctive programs as input and #$\cdot$NP-complete when the input is restricted to head-cycle-free, normal or tight programs.

Proof.

Membership immediately holds as we can check for a given set $I\subseteq P$ whether there is an answer set $J\supseteq I$ of $\Pi$ with $J\cap(P\setminus I)=\emptyset$ by checking if there is an answer set of program $\Pi\cup\bigcup_{i\in I}\{\leftarrow\,\neg i\}\cup\bigcup_{i\in P\setminus I}\{\leftarrow\,i\}$. Note that if $\Pi$ is head-cycle-free, normal, or tight, this program is again head-cycle-free, normal, or tight, respectively. Hardness follows by establishing a parsimonious reduction from $\#\exists$-SAT or $\#\exists\forall$-SAT 999For quantified Boolean formulas (QBF) and its evaluation problem ($Q_{1}\ldots Q_{i}$-SAT for alternating $Q_{i}\in\{\exists,\forall\}$) we refer to standard texts [6, 32]., respectively. Assume that the input is restricted to head-cycle-free, normal or tight programs. Given an instance $(Q,Z)$ with $Q=\exists X.\phi(X,Z)$. We reduce to the instance $(R(Q),Z)$ of $\#\textsc{PAs}$, where $R(Q)$ is defined as follows. For each variable $v\in X\cup Z$, we add the rules $v\leftarrow\neg nv$ and $nv\leftarrow\neg v$. For each clause $\ell_{1}\vee\ldots\vee\ell_{k}$ in $\phi(X,Z)$, we add a rule $\leftarrow\,\bar{\ell_{1}},\ldots,\bar{\ell_{k}}$ where $\bar{\ell_{i}}$ corresponds to $x$ if $\ell_{i}=\neg x$ for a variable $x$, and $\neg x$ otherwise. Then, a counter $c$ solves $(Q,Z)$ if and only if $c$ solves $(R(Q),Z)$. Assume that we allow arbitrary disjunctive programs as input. Given an instance $(Q,Z)$, where $Q=\exists X.\forall Y.\phi(X,Y,Z)$. We reduce to the instance $(R(Q^{\prime}),Z)$ of $\#\textsc{PAs}$, where $Q^{\prime}=\exists X^{\prime}.\forall Y.\phi(X,Y,Z)$, $X^{\prime}=X\cup Z$, and $R(Q^{\prime})$ is defined exactly as by Eiter and Gottlob [15]. Then, since $R$ is a correct encoding of $\exists\forall$-SAT, the projected model count $c$ of $(Q,Z)$ is the projected answer sets count of $(R(Q^{\prime}),Z)$ and vice versa. Consequently, the proposition sustains. ∎

Worst-Case Analysis of $\mathtt{DP}_{{\mathbb{PHC}}}$: Omitted proofs

Lemma 1.

Given any fixed positive integer $c\geq 1$ and functions $f(k){\,\mathrel{\mathop{:}}=}k!,g(k){\,\mathrel{\mathop{:}}=}$ $2^{k^{(c+1)/c}}$, where $k$ is a non-negative integer. Then, $f\in{\mathcal{O}}(g)$.

Proof.

We proceed by simultaneous induction.

Base case ($k=c=1$): Obviously, $1^{2}\geq 1!$.

Induction hypothesis: $k!\in O(2^{k^{(c+1)/c}})$

Induction step ($k\rightarrow k+1$):

We have to show that for $k\geq k_{0}$ for some fixed $k_{0}$, the following equation holds.

[TABLE]

Induction step ($k\rightarrow k+1,c\rightarrow c+1$): Analogous, previous step works for any $c$.

Induction step ($c\rightarrow c+1$): Analogous. ∎

Characterizing Extensions

In the following, we assume $(\Pi,P)$ to be an instance of $\#\textsc{PAs}$. Further, let $\mathcal{T}=(T,\chi,\tau)$ be an $\mathbb{A}$-TTD of $G_{\Pi}$ where $T=(N,\cdot,n)$, node $t\in N$, and $\rho\subseteq\tau(t)$.

Definition 1**.**

Let $\vec{u}$ be a row of $\rho$.

An extension below $t$ is a set of pairs where a pair consist of a node $t^{\prime}$ of the induced sub-tree $T[t]$ rooted at $t$ and a row $\vec{v}$ of $\tau(t^{\prime})$ and the cardinality of the set equals the number of nodes in the sub-tree $T[t]$.

We define the family of extensions below $t$ recursively as follows. If $t$ is of type leaf, then $\operatorname{Ext}_{\leq t}(\vec{u}){\,\mathrel{\mathop{:}}=}\{\{\langle t,\vec{u}\rangle\}\}$; otherwise \operatorname{Ext}_{\leq t}(\vec{u}){\,\mathrel{\mathop{:}}=}\bigcup_{\vec{v}\in\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\vec{u})}\big{\{} \{\langle t,\vec{u}\rangle\}\cup X_{1}\cup\ldots\cup X_{\ell}\mid X_{i}\in\operatorname{Ext}_{\leq t_{i}}({\vec{v}}_{(i)})\big{\}} for the $\ell$ children $t_{1},\ldots,t_{\ell}$ of $t$. We extend this notation for an $\mathbb{A}$-table $\rho$ by $\operatorname{Ext}_{\leq t}(\rho){\,\mathrel{\mathop{:}}=}\bigcup_{\vec{u}\in\rho}\operatorname{Ext}_{\leq t}(\vec{u})$. Further, we let $\operatorname{Exts}{\,\mathrel{\mathop{:}}=}\operatorname{Ext}_{\leq n}(\tau(n))$ be the family of all extensions.

Further, we define the local table for node $t$ and family $E$ of extensions (below some node) as $\operatorname{local}(t,E){\,\mathrel{\mathop{:}}=}\bigcup_{\hat{\rho}\in E}\{\langle\vec{u}\rangle\mid\langle t,\vec{u}\rangle\in\hat{\rho}\}$.

If we would construct all extensions below the root $n$, it allows us to also obtain all models of program $\Pi$. To this end, we state the following definition.

Definition 2**.**

We define the satisfiable extensions below $t$ for $\rho$ by

[TABLE]

Observation 1**.**

$\operatorname{SatExt}_{\leq n}(\tau(n))=\operatorname{Exts}$.

Definition 3**.**

We define the purged table mapping $\nu$ of $\tau$ by $\nu(t){\,\mathrel{\mathop{:}}=}\operatorname{local}(t,$ $\operatorname{SatExt}_{\leq t}[\tau(t)])$ for every $t\in N$.

Next, we define an auxiliary notation that gives us a way to reconstruct interpretations from families of extensions.

Definition 4**.**

Let $E$ be a family of extensions below $t$. We define the set $\mathcal{I}(E)$ of interpretations of $E$ by \mathcal{I}(E){\,\mathrel{\mathop{:}}=}\big{\{} \bigcup_{\langle\cdot,\vec{u}\rangle\in X}\mathcal{I}(\vec{u})\mid X\in E\big{\}} and the set $\mathcal{I}_{P}(E)$ of projected interpretations by \mathcal{I}_{P}(E){\,\mathrel{\mathop{:}}=}\big{\{}\bigcup_{\langle\cdot,\vec{u}\rangle\in X}\mathcal{I}(\vec{u})\cap P\mid X\in E\big{\}}.

Example 11**.**

Consider again program $\Pi$ and TTD $(T,\chi,\tau)$ of $G_{\Pi}$, where $t_{14}$ is the root of $T$, from Example 5. Let $X=\{\langle t_{13},\langle\{b\},\{b\},\langle b\rangle\rangle\rangle,\langle t_{12},\langle\{b\},\emptyset,\langle b\rangle\rangle\rangle,\langle t_{11},$ $\langle\{b\},\emptyset,\langle b\rangle\rangle\rangle,$ $\langle t_{10},\langle\{b,e\},\{e\},\langle b,e\rangle\rangle\rangle,$ $\langle t_{9},\langle\{e\},\{e\},\langle e\rangle\rangle\rangle,$ $\langle t_{4},\langle\{b\},\{b\},$ $\langle b\rangle\rangle\rangle,\langle t_{3},$ $\langle\{b\},\{b\},\langle b\rangle\rangle\rangle,\langle t_{1},\langle\emptyset,\emptyset,\langle\rangle\rangle\rangle\}$ be an extension below $t_{14}$. Observe that $X\in\operatorname{Exts}$ and that Figure 2 highlights those rows of tables for nodes $t_{13},t_{12},t_{11},t_{10},t_{9},t_{4},t_{3}$ and $t_{1}$ that also occur in $X$ (in yellow). Further, $\mathcal{I}(\{X\})=\{b,e\}$ computes the corresponding answer set of $X$, and $\mathcal{I}_{P}(\{X\})=\{e\}$ derives the projected answer sets of $X$. $\mathcal{I}(\operatorname{Exts})$ refers to the set of answer sets of $\Pi$, whereas $\mathcal{I}_{P}(\operatorname{Exts})$ is the set of projected answer sets of $\Pi$.

Correctness of $\mathtt{DP}_{{\mathbb{PHC}}}$: Omitted proofs

In the following, we assume $\Pi$ to be a head-cycle-free program. Further, let $\mathcal{T}=(T,\chi,\tau)$ be an $\mathbb{A}$-TTD of $G_{\Pi}$ where $T=(N,\cdot,n)$ and $t\in N$ is a node.

We state definitions required for the correctness proofs of our algorithm ${\mathbb{PHC}}$. In the end, we only store rows that are restricted to the bag content to maintain runtime bounds. Similar to related work [19], we define the content of our tables in two steps. First, we define the properties of so-called ${\mathbb{PHC}}$-solutions up to $t$. Second, we restrict these solutions to ${\mathbb{PHC}}$-row solutions at $t$.

Definition 5**.**

Let $\hat{I}\subseteq\text{at}_{\leq t}$ be an interpretation, $\hat{\mathcal{P}}\subseteq\hat{I}$ be a set of atoms and $\hat{\sigma}$ be an ordering over atoms $\hat{I}$. Then, $\langle\hat{I},\hat{\mathcal{P}},\hat{\sigma}\rangle$ is referred to as ${\mathbb{PHC}}$-solution up to $t$ if the following holds.

$\hat{I}\models\Pi_{\leq t}$, 2. 2.

for each $a\in\hat{I}\cap\text{at}_{<t}$, we have $a\in\hat{\mathcal{P}}$, and 3. 3.

$a\in\hat{\mathcal{P}}$* if and only if $a$ is proven using program $\Pi_{\leq t}$ and ordering $\hat{\sigma}$.*

Next, we observe that the ${\mathbb{PHC}}$-solutions up to $n$ suffice to capture all the answer sets.

Proposition 4**.**

The set of ${\mathbb{PHC}}$-solutions up to $n$ characterizes the set of answer sets of $\Pi$. In particular: $\{\hat{I}\mid\langle\hat{I},\hat{\mathcal{P}},\hat{\sigma}\rangle\text{ is a }{\mathbb{PHC}}\text{-solution up to }n\}=\{I\mid I\text{ is an answer set of }\Pi\}$.

Proof.

Observe that Definition 5 for root node $t=n$ indeed suffices for $\hat{I}$ to be a model of $\Pi_{\leq n}=\Pi$, and, moreover, every atom in $\hat{I}=\hat{P}$ is proven in $\Pi$ by ordering $\hat{\sigma}$. ∎

Definition 6**.**

Let $\langle\hat{I},\hat{\mathcal{P}},\hat{\sigma}\rangle$ be a ${\mathbb{PHC}}$-solution up to $t$. Then, $\langle\hat{I}\cap\chi(t),\hat{\mathcal{P}}\cap\chi(t),\sigma\rangle$, where $\sigma$ is the partial ordering of $\hat{\sigma}$ only containing $\chi(t)$, is referred to as ${\mathbb{PHC}}$-row solution at node $t$.

Given a ${\mathbb{PHC}}$-solution $\vec{\hat{}u}$ up to $t$ and a ${\mathbb{PHC}}$-row solution $\vec{}u$ at $t$. We say $\vec{\hat{}u}$ is a corresponding ${\mathbb{PHC}}$-solution up to $t$ of ${\mathbb{PHC}}$-row solution at $t$ if $\vec{\hat{}u}$ can be used to construct $\vec{}u$ according to Definition 6.

In fact, ${\mathbb{PHC}}$-row solutions at $t$ suffice to capture all the answer sets of $\Pi$. Before we show that, we need the following definition.

Definition 7**.**

Let $t\in N$ be a node of $\mathcal{T}$ with $\operatorname{children}(t,T)=\langle t_{1},\ldots,t_{\ell}\rangle$. Further, let $\vec{\hat{}u}=\langle\hat{I},\hat{\mathcal{P}},\hat{\sigma}\rangle$ be a ${\mathbb{PHC}}$-solution up to $t$ and $\vec{\hat{v}}=\langle\hat{I^{\prime}},\hat{\mathcal{P}^{\prime}},\hat{\sigma^{\prime}}\rangle$ be a ${\mathbb{PHC}}$-solution up to $t_{i}$. Then, $\vec{}u$ is compatible with $\vec{v}$ (and vice-versa) if

$\hat{I^{\prime}}=\hat{I}\cap\text{at}_{\leq t_{i}}$** 2. 2.

$\hat{\mathcal{P}^{\prime}}=\hat{\mathcal{P}}\cap\text{at}_{\leq t_{i}}$** 3. 3.

$\hat{\sigma^{\prime}}$* is a sub-sequence of $\hat{\sigma}$ such that $\hat{\sigma}$ may additionally contain atoms in $\text{at}_{\leq t}\setminus\text{at}_{\leq t_{i}}$*

Lemma 3** (Soundness).**

Let $t\in N$ be a node of $\mathcal{T}$ with $\operatorname{children}(t,T)=\langle t_{1},\ldots,t_{\ell}\rangle$. Further, let $\vec{v}_{i}$ be a ${\mathbb{PHC}}$-row solution at $t_{i}$ for $1\leq i\leq\ell$. Then, each row $\vec{}u=\langle I,\mathcal{P},\sigma\rangle$ in $\tau(t)$ with $\langle\vec{v}_{1},\ldots,\vec{v}_{\ell}\rangle\in\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\vec{}u)$ is also a ${\mathbb{PHC}}$-row solution at node $t$. Moreover, for any corresponding ${\mathbb{PHC}}$-solution ${\vec{\hat{}u}}$ up to $t$ (of $\vec{}u$) there are corresponding compatible ${\mathbb{PHC}}$-solutions $\vec{\hat{v_{i}}}$ up to $t_{i}$ (for $\vec{v}_{i}$).

Proof (Sketch).

We proceed by case distinctions. Assume case(i): $\operatorname{type}(t)=\textit{leaf}$. Then, $\langle\emptyset,\emptyset,\langle\rangle\rangle$ is a ${\mathbb{PHC}}$-row solution at $t$. This concludes case(i).

Assume case(ii): $\operatorname{type}(t)=\textit{int}$ and $\chi(t)\setminus\chi(t^{\prime})=\{a\}$. Let $\vec{v}_{1}=\langle I,\mathcal{P},\sigma\rangle$ be any ${\mathbb{PHC}}$-row solution at child node $t_{1}$, and $\vec{\hat{v_{1}}}=\langle\hat{I},\hat{\mathcal{P}},\hat{\sigma}\rangle$ be any corresponding ${\mathbb{PHC}}$-solution up to $t_{1}$, which exists by Definition 6. In the following, we show that the way ${\mathbb{PHC}}$ transforms ${\mathbb{PHC}}$-row solution $\vec{v}_{1}$ at $t_{1}$ to a ${\mathbb{PHC}}$-row solution $\vec{}u=\langle I^{\prime},\mathcal{P}^{\prime},\sigma^{\prime}\rangle$ at $t$ is sound. We identify several sub-cases.

Case (a): Atom $a\not\in I^{\prime}$ is set to false. Then, ${\mathbb{PHC}}$ constructs $\vec{}u$ where $I^{\prime}=I,\sigma^{\prime}=\sigma$ and $\mathcal{P}^{\prime}=\mathcal{P}\cup\operatorname{proven}(I^{\prime},\sigma^{\prime},\Pi_{t})$. Note that by construction $I^{\prime}\models\Pi_{t}$. Towards showing soundness, we define how to transform $\vec{\hat{v_{1}}}$ into $\vec{\hat{}u}$ such that $\vec{\hat{}u}$ is indeed the corresponding ${\mathbb{PHC}}$-solution up to $t$ of row $\vec{u}$ constructed by ${\mathbb{PHC}}$. To this end, we define $\vec{\hat{}u}$ as follows: $\vec{\hat{}u}=\langle\hat{I},\hat{\mathcal{P}}\cup\operatorname{proven}(I^{\prime},\sigma^{\prime},\Pi_{t}),\hat{\sigma}\rangle$. Observe that $\vec{\hat{}u}$ is a ${\mathbb{PHC}}$-solution up to $t$ according to Definition 5. Moreover, by construction and Definition 6, $\vec{\hat{}u}$ is a corresponding ${\mathbb{PHC}}$-solution up to $t$ of $\hat{}u$. It remains to show, that indeed for any corresponding ${\mathbb{PHC}}$-solution ${\vec{\hat{}u}}=\langle\hat{I^{\prime}},\hat{\mathcal{P}^{\prime}},\hat{\sigma^{\prime}}\rangle$ up to $t$ (of $\vec{}u$, there is a corresponding ${\mathbb{PHC}}$-solution $\vec{\hat{\zeta_{1}}}$ up to $t_{1}$ (of $\vec{{v_{1}}}$). To this end, we define $\vec{\hat{\zeta_{1}}}=\langle\hat{I^{\prime}},\hat{\mathcal{P}^{\prime}}\setminus(\mathcal{P}^{\prime}\setminus\mathcal{P}),\hat{\sigma^{\prime}}\rangle$ that is by construction according to Definition 5 indeed a corresponding ${\mathbb{PHC}}$-solution up to $t_{1}$ of $\vec{\hat{v_{1}}}$. This concludes case (a).

Case (b): Atom $a\in I^{\prime}$ is set to true. Conceptually, the case works analogously. This concludes cases (b) and (ii).

The remaining cases for nodes $t$ with $\operatorname{type}(t)=\textit{rem}$ (slightly easier) and nodes $t$ with $\operatorname{type}(t)=\textit{join}$, where we need to consider ${\mathbb{PHC}}$-row solutions at two different child nodes of $t$, go through similarly. ∎

Lemma 4** (Completeness).**

Let $t\in N$ be node of $\mathcal{T}$ where $\operatorname{type}(t)\neq\textit{leaf}$ and $\operatorname{children}(t,T)=\langle t_{1},\ldots,t_{\ell}\rangle$. Given a ${\mathbb{PHC}}$-row solution $\vec{}u=\langle I,\mathcal{P},\sigma\rangle$ at node $t$, and any corresponding ${\mathbb{PHC}}$-solution $\vec{\hat{}u}$ up to $t$ (of $\vec{}u$). Then, there exists $\vec{s}=\langle{v_{1}},\ldots,{v_{\ell}}\rangle$ where ${v_{i}}$ is a ${\mathbb{PHC}}$-row solution at $t_{i}$ such that $\vec{s}\in\operatorname{{\mathbb{PHC}}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\vec{}u)$, and corresponding ${\mathbb{PHC}}$-solution $\vec{\hat{v_{i}}}$ up to $t_{i}$ (of $v_{i}$) that is compatible with $\vec{\hat{}u}$.

Proof (Idea).

Since $\vec{}u$ is a ${\mathbb{PHC}}$-row solution at $t$, there is by Definition 6 a corresponding ${\mathbb{PHC}}$-solution $\vec{\hat{}u}=\langle\hat{I},\hat{\mathcal{P}},\hat{\sigma}\rangle$ up to $t$.

We proceed again by case distinction. Assume that $\operatorname{type}(t)=\textit{int}$. Then we define $\vec{\hat{v_{1}}}{\,\mathrel{\mathop{:}}=}\langle\hat{I}\setminus\{a\},\hat{\mathcal{P}^{\prime}},\hat{\sigma^{\prime}}\rangle$, where $\hat{\sigma^{\prime}}$ is a sub-sequence of $\hat{\sigma}$ that does not contain $a$ and $\hat{\mathcal{P}}^{\prime}=\operatorname{proven}(\hat{I}\setminus\{a\},t_{1},\Pi_{\leq t_{1}})$. Observe that all the conditions of Definition 5 are met and that $\hat{\mathcal{P}}^{\prime}\subseteq\hat{\mathcal{P}^{\prime}}$. Then, we can easily define ${\mathbb{PHC}}$-row solution $\vec{v_{1}}$ at $t_{1}$ according to Definition 6 by using $\vec{\hat{v_{1}}}$. By construction of $\vec{\hat{v_{1}}}$ and by the definition of $\operatorname{proven}$, we conclude that $\vec{}u$ can be constructed with ${\mathbb{PHC}}$ using $\vec{v_{1}}$. Moreover, ${\mathbb{PHC}}$-solution $\vec{\hat{v_{1}}}$ up to $t_{1}$ is indeed compatible with $\vec{\hat{}u}$.

Assume that $\operatorname{type}(t)=\textit{rem}$. The case is slightly easier as the one above, and the remainder works similar.

Similarly, one can show the result for the remaining node with $\operatorname{type}(t)=\textit{join}$, but define ${\mathbb{PHC}}$-row solutions for two preceding child nodes of $t$. ∎

We are now in the position to proof our theorem.

Theorem 2.

The algorithm $\mathtt{DP}_{\mathbb{PHC}}$ is correct. More precisely, the algorithm $\mathtt{DP}_{\mathbb{PHC}}((\Pi,\cdot),\mathcal{T})$ returns ${\mathbb{PHC}}$-TTD $(T,\chi,\tau)$ such that we can decide consistency of $\Pi$ and even reconstruct the answer sets of $\Pi$:

[TABLE]

Proof (Idea).

By Lemma 3 we have soundness for every node $t\in N$ and hence only valid rows as output of table algorithm ${\mathbb{PHC}}$ when traversing the tree decomposition in post-order up to the root $n$. By Proposition 4 we then know that we can reconstruct answer sets given ${\mathbb{PHC}}$-solutions up to $n$. In more detail, we proceed by means of induction. For the induction base we only store ${\mathbb{PHC}}$-row solutions $\vec{}u\in\tau(t)$ at a certain node $t$ starting at the leaves. For nodes $t$ with $\operatorname{type}(t)=\textit{leaf}$, obviously there is only the following (one) ${\mathbb{PHC}}$-row solution at $t$: $\vec{}u=\langle\emptyset,\emptyset,\langle\rangle\rangle$.

Then, by Lemma 3 we establish the induction step, since algorithm ${\mathbb{PHC}}$ only creates ${\mathbb{PHC}}$-row solutions at every node $t$, assuming that it gets ${\mathbb{PHC}}$-row solutions at $t_{i}$ for every child node $t_{i}$ of $t$. As a result, if there is no answer set of $\Pi$, the table $\tau(n)$ is empty. On the other hand, if there is an answer set of $\Pi$, we obtain a ${\mathbb{PHC}}$-row solution $\vec{}u$ at root node $n$, for which by Definition 6 a corresponding ${\mathbb{PHC}}$-solution $\vec{\hat{}u}$ up to $n$ exists. Further, in the induction step we ensured that ${\mathbb{PHC}}$-solutions up to $t$ for every ${\mathbb{PHC}}$-row solution at $t$ for every node $t\in N$ can be found that are compatible to $\vec{\hat{}u}$. In other words, by keeping track of corresponding origin ${\mathbb{PHC}}$-row solutions of $\vec{}u$ we can combine interpretation positions $\mathcal{I}(\cdot)$ of rows by following origin rows top-down in order to reconstruct only valid answer set.

Next, we establish completeness by induction starting from the root $n$. Let therefore, $\hat{\rho}=\langle\hat{I},\hat{\mathcal{P}},\hat{\sigma}\rangle$ be the ${\mathbb{PHC}}$-solution up to node $n$. If $\hat{\rho}$ does not exist for node $n$, there is by definition no answer set of $\Pi$. Otherwise, by Definition 6, we know that for the root $n$ we can construct $\mathbb{PROJ}$-row solutions at $n$ of the form $\rho=\langle\emptyset,\emptyset,\langle\rangle\rangle$ for $\hat{\rho}$. We already established the induction step in Lemma 4 using $\rho$ and $\hat{\rho}$. As a consequence, we can reconstruct exactly all the answer sets of $\Pi$ by following origin rows (see Definition of $\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}$) back to the leaves and combining interpretation parts $\mathcal{I}(\cdot)$, accordingly. Hence, we obtain some (corresponding) rows for every node $t$. Finally, we stop at the leaves.

In consequence, we have shown both soundness and completeness. As a result, Theorem 2 is sustains. ∎

Corollary 2**.**

Algorithm $\mathtt{DP}_{\mathbb{PHC}}((\Pi,\cdot),\mathcal{T})$ returns ${\mathbb{PHC}}$-TTD $(T,\chi,\tau)$ such that:

[TABLE]

Proof.

The corollary follows from the proof of Theorem 2 applied up to node $t$ and by considering only rows that are involved in reconstructing answer sets (see Definition 2). ∎

Correctness of $\mathtt{PCNT}_{\mathbb{A}}$: Omitted proofs

In the following, we assume $(\Pi,P)$ to be an instance of $\#\textsc{PAs}$. Further, let $\mathcal{T}=(T,\chi,\tau)$ be an $\mathbb{A}$-TTD of $G_{\Pi}$ where $T=(N,\cdot,n)$, node $t\in N$, and $\rho\subseteq\tau(t)$.

Definition 8**.**

Table algorithm $\mathbb{A}$ is referred to as admissible, if for each row $\vec{u_{t.i}}\in\tau(t)$ of any node $t\in T$ the following holds:

$\mathcal{I}(\vec{u_{t.i}})\subseteq\chi(t)$** 2. 2.

For any $\langle\vec{v}_{1},\ldots,\vec{v}_{\ell}\rangle\in\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\vec{u_{t.i}})$ where $1\leq j\leq\ell$ and $\operatorname{children}(t,T)=\langle t_{1},\ldots,t_{\ell}\rangle$, we have $\mathcal{I}(\vec{v}_{j})\cap\chi(t_{j})\cap\chi(t)=\mathcal{I}(\vec{u}_{t.i})\cap\chi(t_{j})\cap\chi(t)$ 3. 3.

$\mathcal{I}(\operatorname{SatExt}_{\leq t}[\tau(t)])=\{I\mid I\in 2^{\text{at}_{\leq t}},I\models\Pi_{\leq t},\text{ there is an answer set }I\cup(\text{at}(\Pi)\setminus\text{at}_{\leq t})\supseteq I^{\prime}\supseteq I\text{ of }\Pi\}$** 4. 4.

If $t=n$ or $\operatorname{type}(t)=\textit{leaf}$: $\left|\operatorname{local}(t,\operatorname{SatExt}_{\leq t}[\tau(t)])\right|\leq 1$

Note that the last condition is not a hard restriction, since the bags of the leaf and root nodes of a tree decomposition are defined to be empty anyway. However, it rather serves as technical trick simplifying proofs.

Observation 2**.**

Table algorithms ${\mathbb{PHC}}$ and $\mathbb{PRIM}$ are admissible.

Proof.

Obviously, Conditions 1, 2, and 4 hold by construction of the table algorithms and by properties auf tree decompositions. For condition 3, we have to check for correctness and completeness, which has been shown [19] for algorithm $\mathbb{PRIM}$. For ${\mathbb{PHC}}$, see Theorem 2 and Corollary 2. ∎

In the following, we assume that whenever $\mathbb{A}$ occurs, $\mathbb{A}$ is an admissible table algorithm.

Proposition 5**.**

$\mathcal{I}(\operatorname{SatExt}_{\leq n}[\tau(n)])=\mathcal{I}(\operatorname{Exts})=\{I\mid I\in 2^{\text{at}(\Pi)},I\text{ is an answer }$* $\text{ set of }\Pi\}.$*

Proof.

Fill in Definition 8 with root $n$ of $\mathbb{A}$-TTD ${\cal T}$. ∎

The following definition is key for the correctness proof, since later we show that these are equivalent with the result of $\mathtt{DP}_{\mathbb{PROJ}}$ using purged table mapping $\nu$.

Definition 9**.**

The projected answer sets count $\operatorname{pasc}_{\leq t}(\rho)$ of $\rho$ below $t$ is the size of the union over projected interpretations of the satisfiable extensions of $\rho$ below $t$, formally,

[TABLE]

.

The intersection projected answer sets count $\operatorname{ipasc}_{\leq t}(\rho)$ of $\rho$ below $t$ is the size of the intersection over projected interpretations of the satisfiable extensions of $\rho$ below $t$, i.e.,

[TABLE]

.

In the following, we state definitions required for the correctness proofs of our algorithm $\mathbb{PROJ}$. In the end, we only store rows that are restricted to the bag content to maintain runtime bounds. We define the content of our tables in two steps. First, we define the properties of so-called $\mathbb{PROJ}$-solutions up to $t$. Second, we restrict these solutions to $\mathbb{PROJ}$-row solutions at $t$.

Definition 10**.**

Let $\emptyset\subsetneq\rho\subseteq\tau(t)$ be a table with $\rho\in\operatorname{sub\hbox{-}\nobreak\hskip 0.0ptbuckets}_{P}(\tau(t))$. We define a ${\mathbb{PROJ}}$-solution up to $t$ to be the sequence $\langle\hat{\rho}\rangle=\langle\operatorname{SatExt}_{\leq t}(\rho)\rangle$.

Before we present equivalence results between $\operatorname{ipasc}_{\leq t}(\ldots)$ and the recursive version $\operatorname{ipasc}(t,\ldots)$ used during the computation of $\mathtt{DP}_{\mathbb{PROJ}}$, recall that $\operatorname{ipasc}_{\leq t}$ and $\operatorname{pasc}_{\leq t}$ (Definition 9) are key to compute the projected answer sets count. The following corollary states that computing $\operatorname{ipasc}_{\leq n}$ at the root $n$ actually suffices to compute $\operatorname{pasc}_{\leq n}$, which is in fact the projected answer sets count of the input program.

Corollary 3**.**

[TABLE]

Proof.

The corollary immediately follows from Proposition 5 and since the cardinality of $\operatorname{local}(n,$ $\operatorname{SatExt}_{\leq n}[\tau(n)])$ is at most one at root $n$, by Definition 8. ∎

The following lemma establishes that the $\mathbb{PROJ}$-solutions up to root $n$ of a given tree decomposition solve the $\#$PAs problem.

Lemma 5**.**

The value c=\sum_{\langle\hat{\rho}\rangle\text{ is a \mathbb{PROJ}-solution up to }n}\left|\mathcal{I}_{P}(\hat{\rho})\right| corresponds to the projected answer sets count of $\Pi$ with respect to the set $P$ of projection atoms.

Proof.

(“$\Longrightarrow$”): Assume that c=\sum_{\langle\hat{\rho}\rangle\text{ is a \mathbb{PROJ}-solution up to }n}\left|\mathcal{I}_{P}(\hat{\rho})\right|. Observe that there can be at most one projected solution up to $n$ by Definition 8. If $c=0$, then $\tau(n)$ contains no rows. Hence, $\Pi$ has no answer sets, c.f., Proposition 5, and obviously also no answer sets projected to $P$. Consequently, $c$ is the projected answer sets count of $\Pi$. If $c>0$ we have by Corollary 3 that $c$ is equivalent to the projected answer sets count of $\Pi$ with respect to $P$.

(“$\Longleftarrow$”): The proof proceeds similar to the only-if direction. ∎

In the following, we provide for a given node $t$ and a given $\mathbb{PROJ}$-solution up to $t$, the definition of a $\mathbb{PROJ}$-row solution at $t$.

Definition 11**.**

Let $\langle\hat{\rho}\rangle$ be a $\mathbb{PROJ}$-solution up to $t$. Then, we define the $\mathbb{PROJ}$-row solution at $t$ by $\langle\operatorname{local}(t,\hat{\rho}),\left|\mathcal{I}_{P}(\hat{\rho})\right|\rangle$.

Observation 3**.**

Let $\langle\hat{\rho}\rangle$ be a $\mathbb{PROJ}$-solution up to a node $t\in N$. There is exactly one corresponding $\mathbb{PROJ}$-row solution $\langle\operatorname{local}(t,\hat{\rho}),\left|\mathcal{I}_{P}(\hat{\rho})\right|\rangle$ at $t$.

Vice versa, let $\langle\rho,c\rangle$ at $t$ be a $\mathbb{PROJ}$-row solution at $t$ for some integer $c$. Then, there is exactly one corresponding $\mathbb{PROJ}$-solution $\langle\operatorname{SatExt}_{\leq t}(\rho)\rangle$ up to $t$.

We need to ensure that storing $\mathbb{PROJ}$-row solutions at a node $t\in N$ suffices to solve the $\#$PAs problem, which is necessary to obtain the runtime bounds as presented in Corollary 1. For the root node $n$, this is sufficient, shown in the following.

Lemma 6**.**

There is a $\mathbb{PROJ}$-row solution at the root $n$ if and only if the projected answer sets count of $\Pi$ is larger than zero. Further, if there is a $\mathbb{PROJ}$-row solution $\langle\rho,c\rangle$ at root $n$, then $c$ is the projected answer sets count of $\Pi$.

Proof.

(“$\Longrightarrow$”): Let $\langle\rho,c\rangle$ be a $\mathbb{PROJ}$-row solution at root $n$ where $\rho$ is an $\mathbb{A}$-table and $c$ is a positive integer. Then, by Definition 11 there also exists a corresponding $\mathbb{PROJ}$-solution $\langle\hat{\rho}\rangle$ up to $n$ such that $\rho=\operatorname{local}(n,\hat{\rho})$ and $c=\left|\mathcal{I}_{P}(\hat{\rho})\right|$. Moreover, by Definition 8, we have $\left|\operatorname{local}(n,\operatorname{SatExt}_{\leq n}[\tau(n)])\right|=1$. Then, by Definition 10, $\hat{\rho}=\operatorname{SatExt}_{\leq n}[\tau(n)]$. By Corollary 3, we have $c=\left|\mathcal{I}_{P}(\operatorname{SatExt}_{\leq n}[\tau(n)])\right|$ equals the projected answer sets count of $\Pi$. Finally, the claim follows.

(“$\Longleftarrow$”): The proof proceeds similar to the only-if direction. ∎

Before we show that $\mathbb{PROJ}$-row solutions suffice, we require the following lemma.

Observation 4**.**

Let $n$ be a positive integer, $X=\{1,\ldots,n\}$, and $X_{1}$, $X_{2}$, $\ldots$, $X_{n}$ subsets of $X$. The number of elements in the intersection over all sets $A_{i}$ is

[TABLE]

Proof.

We take the well-known inclusion-exclusion principle [26] and rearrange the equation. ∎

Lemma 7**.**

Let $t\in N$ be a node of $\mathcal{T}$ with $\operatorname{children}(t,T)=\langle t_{1},\ldots,t_{\ell}\rangle$ and let $\langle\rho,\cdot\rangle$ be a $\mathbb{PROJ}$-row solution at $t$. Further, let $\pi$ be a partial mapping of $\pi^{\prime}$ (finally returned by $\mathtt{DP}_{\mathbb{PROJ}}((\Pi,P),\mathcal{T})=(T,\chi,\pi^{\prime})$), which maps nodes of the sub-tree $T[t]$ rooted at $t$ (excluding $t$) to $\mathbb{PROJ}$-tables. Then,

$\operatorname{ipasc}(t,\rho,\langle\pi(t_{1}),\ldots,\pi(t_{\ell})\rangle)=\operatorname{ipasc}_{\leq t}(\rho)$** 2. 2.

for $\operatorname{type}(t)\neq\textit{leaf}$:

$\operatorname{pasc}(t,\rho,\langle\pi(t_{1}),\ldots,\pi(t_{\ell})\rangle)=\operatorname{pasc}_{\leq t}(\rho)$.

Proof (Sketch).

We prove the statement by simultaneous induction.

(“Induction Hypothesis”): Lemma 7 holds for the nodes in $\operatorname{children}(t,T)$ and also for node $t$, but on strict subsets $\varphi\subsetneq\rho$. (“Base Cases”): Let $\operatorname{type}(t)=\textit{leaf}$. Then by definition, $\operatorname{ipasc}(t,\{\langle\emptyset,\ldots\rangle\},\langle\rangle)=\operatorname{ipasc}_{\leq t}(\{\langle\emptyset,\ldots\rangle\})=1$. Recall that for $\operatorname{pasc}$ the equivalence does not hold for leaves, but we use a node that has a node $t^{\prime}\in N$ with $\operatorname{type}(t^{\prime})=\textit{leaf}$ as child for the base case. Observe that by definition of a tree decomposition such a node $t$ can have exactly one child. Then, we have that $\operatorname{pasc}(t,\rho,\langle\pi(t^{\prime})\rangle)=\sum_{\emptyset\subsetneq O\subseteq{\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\rho)}}(-1)^{(\left|O\right|-1)}\cdot\operatorname{s-ipasc}(\langle\tau(t^{\prime})\rangle,O)=\left|\bigcup_{\vec{u}\in\rho}\mathcal{I}_{P}(\operatorname{SatExt}_{\leq t}(\{\vec{u}\}))\right|=\operatorname{pasc}_{\leq t}(\rho)=1$ where $\langle\rho,\cdot\rangle$ is a $\mathbb{PROJ}$-row solution at $t$.

(“Induction Step”): We proceed by case distinction.

Assume that $\operatorname{type}(t)=\textit{int}$. Let $a\in(\chi(t)\setminus\chi(t^{\prime}))$ be an introduced atom. We have two cases. Case (i) $a$ also belongs to $(\text{at}(\Pi)\setminus P)$, i.e., $a$ is not a projection atom; and Case (ii) $a$ also belongs to $P$, i.e., $a$ is a projection atom. Assume that we have Case (i). Let $\langle\rho,c\rangle$ be a $\mathbb{PROJ}$-row solution at $t$ for some integer $c$. As a consequence of admissible algorithm $\mathbb{A}$ (see Definition 8) there can be many rows in the table $\tau(t)$ for one row in the table $\tau(t^{\prime})$, more precisely, $\left|\operatorname{buckets}_{P}(\rho)\right|=1$. As a result, $\operatorname{pasc}_{\leq t}(\rho)=\operatorname{pasc}_{\leq t^{\prime}}(\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\rho))$ by applying Observation 3. We apply the inclusion-exclusion principle on every subset $\varphi$ of the origins of $\rho$ in the definition of $\operatorname{pasc}$ and by induction hypothesis we know that $\operatorname{ipasc}(t^{\prime},\varphi,\langle\pi(t^{\prime})\rangle)=\operatorname{ipasc}_{\leq t^{\prime}}(\varphi)$, therefore, $\operatorname{s-ipasc}(\pi(t^{\prime}),\varphi)=\operatorname{ipasc}_{\leq t^{\prime}}(\varphi)$. This concludes Case (i) for $\operatorname{pasc}$. The induction step for $\operatorname{ipasc}$ works similar by applying Observation 4 and comparing the corresponding $\mathbb{PROJ}$-solutions up to $t$ or $t^{\prime}$, respectively. Further, for showing the lemma for $\operatorname{ipasc}$, one has to additionally apply the hypothesis for node $t$, but on strict subsets $\emptyset\subsetneq\varphi\subsetneq\rho$ of $\rho$. Assume that we have Case (ii). We proceed similar as in Case (i), since Case (ii) is just a special case here, more precisely, we also have $\left|\operatorname{buckets}_{P}(\rho)\right|=1$ here.

Assume that $\operatorname{type}(t)=\textit{rem}$. Let $a\in(\chi(t^{\prime})\setminus\chi(t))$ be a removed atom. We have two cases. Case (i) $a$ also belongs to $(\text{at}(\Pi)\setminus P)$, i.e., $a$ is not a projection atom; and Case (ii) $a$ also belongs to $P$, i.e., $a$ is a projection atom. Assume that we have Case (i). Let $\langle\rho,c\rangle$ be a $\mathbb{PROJ}$-row solution at $t$ for some integer $c$. As a consequence of admissible table algorithms $\mathbb{A}$ (see Definition 8) there can be many rows in the table $\tau(t)$ for one row in the table $\tau(t^{\prime})$ (and vice-versa). Nonetheless we still have $\operatorname{pasc}_{\leq t}(\rho)=\operatorname{pasc}_{\leq t^{\prime}}(\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\rho))$, because $a\notin P$ by applying Observation 3. We apply the inclusion-exclusion principle on every subset $\varphi$ of the origins of $\rho$ in the definition of $\operatorname{pasc}$ and by induction hypothesis we know that $\operatorname{ipasc}(t^{\prime},\varphi,\langle\pi(t^{\prime})\rangle)=\operatorname{ipasc}_{\leq t^{\prime}}(\varphi)$, therefore, $\operatorname{s-ipasc}(\pi(t^{\prime}),\varphi)=\operatorname{ipasc}_{\leq t^{\prime}}(\varphi)$. This concludes Case (i) for $\operatorname{pasc}$. Again, the induction step for $\operatorname{ipasc}$ works similar, but swapped. Assume that we have Case (ii). Let $\langle\rho,c\rangle$ be a $\mathbb{PROJ}$-row solution at $t$ for some integer $c$. Here we cannot ensure $\operatorname{pasc}_{\leq t}(\rho)=\operatorname{pasc}_{\leq t^{\prime}}(\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\rho))$, since buckets fall together. However, by applying Observation 3 we have $\operatorname{pasc}_{\leq t}(\rho)=\sum_{\varphi\in\operatorname{buckets}_{P}(\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\rho)_{(1)})}\operatorname{pasc}(t^{\prime},\varphi,C)$ where the sequence $C$ consists of the tables $\pi(t^{\prime}_{i})$ of the children $t^{\prime}_{i}$ of $t^{\prime}$. For every $\varphi\in\operatorname{sub\hbox{-}\nobreak\hskip 0.0ptbuckets}_{P}(\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\rho)_{(1)})$ by induction hypothesis we know that $\operatorname{ipasc}(t^{\prime},\varphi,\langle\pi(t^{\prime})\rangle)=\operatorname{ipasc}_{\leq t^{\prime}}(\varphi)$. Hence, we apply the inclusion-exclusion principle over all subsets $\zeta$ of $\varphi$ for all $\varphi$ independently. By construction $\operatorname{s-ipasc}(\pi(t^{\prime}),\zeta)=\operatorname{ipasc}_{\leq t^{\prime}}(\zeta)$. Then, by construction $\operatorname{pasc}(t,\rho,C^{\prime})=\sum_{\emptyset\subsetneq O\subseteq{\operatorname{\mathbb{A}\hbox{-}\nobreak\hskip 0.0ptorigins}(t,\rho)}}(-1)^{(\left|O\right|-1)}\cdot\operatorname{s-ipasc}(C^{\prime},O)=\operatorname{pasc}_{\leq t}(\rho)$, where $C^{\prime}=\langle\pi(t^{\prime})\rangle$, since for the remaining terms $\operatorname{s-ipasc}(C^{\prime},O)$ is simply zero, including cases where different buckets are involved. This concludes Case (ii) for $\operatorname{pasc}$. Again, the induction step for $\operatorname{ipasc}$ works similar, but swapped by again applying Observation 4.

Assume that $\operatorname{type}(t)=\textit{join}$. We proceed similar to the introduce case. However, we have two $\mathbb{PROJ}$-tables for the children of $t$. Hence, we have to consider both sides when computing $\operatorname{s-ipasc}$ (see Definition of $\operatorname{s-ipasc}$). There we consider the cross-product of two $\mathbb{A}$-tables and we can also correctly apply the inclusion-exclusion principle on subsets of this cross-product, which we can do by simply multiplying $\operatorname{s-ipasc}$-values accordingly. The multiplication is closely related to the join case in table algorithm $\mathbb{A}$. For $\operatorname{ipasc}$ this does not apply, since the inclusion-exclusion principle is carried out at the node $t$ and not for its children.

Since we outlined all cases that can occur for node $t$, this concludes the proof sketch. ∎

Lemma 8** (Soundness).**

Let $t\in N$ be a node of $\mathcal{T}$ with $\operatorname{children}(t,T)=\langle t_{1},\ldots,t_{\ell}\rangle$. Then, each row $\langle\rho,c\rangle$ at node $t$ constructed by table algorithm $\mathbb{PROJ}$ is also a $\mathbb{PROJ}$-row solution for node $t$.

Proof (Idea).

Observe that Listing 3 computes a row for each sub-bucket $\rho\in\operatorname{sub\hbox{-}\nobreak\hskip 0.0ptbuckets}_{P}(\operatorname{local}(t,$ $\operatorname{SatExt}_{\leq t}[\tau(t)]))$. The resulting row $\langle\rho,c\rangle$ obtained by $\operatorname{ipasc}$ is indeed a $\mathbb{PROJ}$-row solution for $t$ according to Lemma 7. ∎

Lemma 9** (Completeness).**

Let $t\in N$ be node of $\mathcal{T}$ where $\operatorname{type}(t)\neq\textit{leaf}$ and $\operatorname{children}(t,T)=\langle t_{1},\ldots,t_{\ell}\rangle$. Given a $\mathbb{PROJ}$-row solution $\langle\rho,c\rangle$ at node $t$. There exists $\langle C_{1},\ldots,C_{\ell}\rangle$ where $C_{i}$ is set of $\mathbb{PROJ}$-row solutions at $t_{i}$ such that $\rho\in\mathbb{PROJ}(t,\cdot,\tau(t),\cdot,P,\langle C_{1},\ldots,C_{\ell}\rangle)$.

Proof (Idea).

Since $\langle\rho,c\rangle$ is a $\mathbb{PROJ}$-row solution for $t$, there is by Definition 11 a corresponding  $\mathbb{PROJ}$-solution $\langle\hat{\rho}\rangle$ up to $t$ such that $\operatorname{local}(t,\hat{\rho})=\rho$.

We proceed again by case distinction. Assume that $\operatorname{type}(t)=\textit{int}$. Then we define $\hat{\rho^{\prime}}{\,\mathrel{\mathop{:}}=}\{(t^{\prime},\hat{\varphi})\mid(t^{\prime},\hat{\varphi})\in\rho,t\neq t^{\prime}\}$. Then, for each subset $\emptyset\subsetneq\varphi\subseteq\operatorname{local}(t^{\prime},\hat{\rho^{\prime}})$, we define $\langle\varphi,\left|\mathcal{I}_{P}(\operatorname{SatExt}_{\leq t}(\varphi))\right|\rangle$ in accordance with Definition 11. By Observation 3, we have that $\langle\varphi,\left|\mathcal{I}_{P}(\operatorname{SatExt}_{\leq t}(\varphi))\right|\rangle$ is an $\mathbb{A}$-row solution at node $t^{\prime}$. Since we defined the $\mathbb{PROJ}$-row solutions for $t^{\prime}$ for all the respective $\mathbb{PROJ}$-solutions up to $t^{\prime}$, we encountered every $\mathbb{PROJ}$-row solution for $t^{\prime}$ that is required for deriving $\langle\rho,c\rangle$ via $\mathbb{PROJ}$ (c.f., Definitions of $\operatorname{ipasc}$ and of $\operatorname{pasc}$).

Assume that $\operatorname{type}(t)=\textit{rem}$. The case is slightly easier as the one above. We do not need to define a $\mathbb{PROJ}$-row solution for $t^{\prime}$ for all subsets $\varphi$, since we only have to consider subsets $\varphi$ here, with $\left|\operatorname{buckets}_{P}(\varphi)\right|=1$. The remainder works similar.

Similarly, one can show the result for the remaining node with $\operatorname{type}(t)=\textit{join}$, but define $\mathbb{PROJ}$-row solutions for two preceding child nodes of $t$. ∎

We are now in the position to proof our theorem.

Theorem 7**.**

The algorithm $\mathtt{DP}_{\mathbb{PROJ}}$ is correct. More precisely, the algorithm $\mathtt{DP}_{\mathbb{PROJ}}((\Pi,P),\mathcal{T})$ returns $\mathbb{PROJ}$-TTD $(T,\chi,\pi$) such that $c=\operatorname{s-ipasc}(\pi(n),\cdot)$ is the projected answer sets count of $\Pi$ with respect to the set $P$ of projection atoms.

Proof.

By Lemma 8 we have soundness for every node $t\in N$ and hence only valid rows as output of table algorithm $\mathbb{PROJ}$ when traversing the tree decomposition in post-order up to the root $n$. By Lemma 6 we know that the projected answer sets count $c$ of $\Pi$ is larger than zero if and only if there exists a certain $\mathbb{PROJ}$-row solution for $n$. This $\mathbb{PROJ}$-row solution at node $n$ is of the form $\langle\{\langle\emptyset,\ldots\rangle\},c\rangle$. If there is no $\mathbb{PROJ}$-row solution at node $n$, then $\tau(n)=\emptyset$ since the table algorithm $\mathbb{A}$ is admissible (c.f., Proposition 5). Consequently, we have $c=0$. Therefore, $c=\operatorname{s-ipasc}(\pi(n),\cdot)$ is the projected answer sets count of $\Pi$ with respect to $P$ in both cases.

Next, we establish completeness by induction starting from the root $n$. Let therefore, $\langle\hat{\rho}\rangle$ be the $\mathbb{PROJ}$-solution up to node $n$, where for each row in $\vec{u}\in\hat{\rho}$, $\mathcal{I}(\vec{u})$ corresponds to an answer set of $\Pi$. By Definition 11, we know that for the root $n$ we can construct a $\mathbb{PROJ}$-row solution at $n$ of the form $\langle\{\langle\emptyset,\ldots\rangle\},c\rangle$ for $\hat{\rho}$. We already established the induction step in Lemma 9. Hence, we obtain some (corresponding) rows for every node $t$. Finally, we stop at the leaves.

In consequence, we have shown both soundness and completeness. As a result, Theorem 7 is sustains. ∎

Corollary 4**.**

The algorithm $\mathtt{PCNT}_{\mathbb{A}}$ is correct and outputs for any instance of $\#$PAs its projected answer sets count.

Proof.

The result follows immediately, since $\mathtt{PCNT}_{\mathbb{A}}$ consists of two dynamic programming passes $\mathtt{DP}_{\mathbb{A}}$, a purging step, and $\mathtt{DP}_{\mathbb{PROJ}}$. For the soundness and completeness of $\mathtt{DP}_{\mathbb{PRIM}}$ we refer to other sources [19]. By Proposition 5, the “purging” step does neither destroy soundness nor completeness of $\mathtt{DP}_{\mathbb{A}}$. ∎

Proposition 2.

The algorithm $\mathtt{PCNT}_{{\mathbb{PHC}}}$ is correct and outputs for any instance of $\#$PAs its projected answer sets count.

Proof.

This is a direct consequence of Corollary 4. ∎

Proposition 3.

The algorithm $\mathtt{PCNT}_{\mathbb{PRIM}}$ is correct and outputs for any instance of $\#$PAs its projected answer sets count.

Proof.

This is a direct consequence of Corollary 4. ∎