DynASP2.5: Dynamic Programming on Tree Decompositions in Action ^†

Abstract

Efficient exact parameterized algorithms are an active research area. Such algorithms exhibit a broad interest in the theoretical community. In the last few years, implementations for computing various parameters (parameter detection) have been established in parameterized challenges, such as treewidth, treedepth, hypertree width, feedback vertex set, or vertex cover. In theory, instances, for which the considered parameter is small, can be solved fast (problem evaluation), i.e., the runtime is bounded exponential in the parameter. While such favorable theoretical guarantees exists, it is often unclear whether one can successfully implement these algorithms under practical considerations. In other words, can we design and construct implementations of parameterized algorithms such that they perform similar or even better than well-established problem solvers on instances where the parameter is small. Indeed, we can build an implementation that performs well under the theoretical assumptions. However, it could also well be that an existing solver implicitly takes advantage of a structure, which is often claimed for solvers that build on Sat-solving. In this paper, we consider finding one solution to instances of answer set programming (ASP), which is a logic-based declarative modeling and solving framework. Solutions for ASP instances are so-called answer sets. Interestingly, the problem of deciding whether an instance has an answer set is already located on the second level of the polynomial hierarchy. An ASP solver that employs treewidth as parameter and runs dynamic programming on tree decompositions is DynASP2. Empirical experiments show that this solver is fast on instances of small treewidth and can outperform modern ASP when one counts answer sets. It remains open, whether one can improve the solver such that it also finds one answer set fast and shows competitive behavior to modern ASP solvers on instances of low treewidth. Unfortunately, theoretical models of modern ASP solvers already indicate that these solvers can solve instances of low treewidth fast, since they are based on Sat-solving algorithms. In this paper, we improve DynASP2 and construct the solver DynASP2.5, which uses a different approach. The new solver shows competitive behavior to state-of-the-art ASP solvers even for finding just one solution. We present empirical experiments where one can see that our new implementation solves ASP instances, which encode the Steiner tree problem on graphs with low treewidth, fast. Our implementation is based on a novel approach that we call multi-pass dynamic programming ($\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$). In the paper, we describe the underlying concepts of our implementation (DynASP2.5) and we argue why the techniques still yield correct algorithms.

1. Introduction

Answer set programming (ASP) is a logic-based declarative modeling language and problem solving framework [1], where a program consists of sets of rules over propositional atoms and is interpreted under extended stable model semantics [2]. In ASP, problems are usually modeled in such a way that the stable models answer sets of a program directly form a solution to the considered problem instance. Computational problems for disjunctive, propositional ASP such as deciding whether a program has an answer set are complete for the second level of the polynomial hierarchy [3] and we can solve ASP problems by encoding it into solving quantified Boolean formulas (QBF) [4,5]. A standard encoding usually involves an existential part (guessing a model of the program) and a universal part (minimality check).

Interestingly, when considering a more fine-grained complexity analysis one can take a structural parameter such as treewidth into account. On that account, one usually defines a graph representation of an input program such as the primal graph or the incidence graph and can show that solving ASP is double exponential (upper bound) in the treewidth of the graph representation and linear in the number of atoms of the input instance [6]. For a tighter conditional lower runtime bound, we can take a standard assumption in computational complexity, such as the Exponential Time Hypothesis (ETH), into account. Unsurprisingly, given its classical computational complexity, one can establish that the runtime of various computational ASP problems is double exponential in the treewidth (lower bound) in the worst case if we believe that ETH is true [7,8].

Despite the seemingly bad results in classical complexity, researchers implemented a variety of successful CDCL-based ASP solvers, among them Clasp [9] and WASP [10]. When viewing practical results from a parameterized perspective, one can find a solver (DynASP2) that build upon ideas from parameterized algorithmics and solves ASP problems by dynamic programming along tree decompositions [11]. The solver DynASP2 performs according to the expected theoretical worst case runtime guarantees and runs practically well if the input program has low treewidth. If we consider counting problems on instances of low treewidth, runtimes of DynASP2 are even faster than those of Clasp. However, conditional lower bounds seem to forbid significant improvement under theoretical aspects unless we design a multi-variate algorithm that takes additional structure into account. In the following of this paper, we outline how to construct a novel algorithm that additionally takes a “second parameter” into account.

The solver DynASP2 (i) takes a tree decomposition of a graph representation of the given input instance and (ii) solves the program via dynamic programming (DP) on the tree decomposition by traversing the tree exactly once. Both finding a model and checking minimality are considered at the same time. Once the root node has been reached, complete solutions (if exist) for the input program can be constructed. Due to the exhaustive nature of dynamic programming, all potential values are computed locally for each node of the tree decomposition. In consequence, space requirements can be quite extensive resulting in long running times. Moreover, in practice, dynamic programming algorithms on tree decompositions may yield extremely diverging run-times on tree decompositions of the exact same width [12].

In this paper, we propose a multi-traversal approach ($\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$) for dynamic programming on tree decompositions as well as a new implementation (DynASP2.5). (The source code of our solver is available at https://github.com/daajoe/dynasp/releases/tag/v2.5.0.) In contrast to the approach described above, $\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$ traverses the given tree decomposition multiple times. Starting from the leaves, we compute and store (i) sets of atoms that are relevant for the existential part (finding a model of the program) up to the root. Then we go back again to the leaves and compute and store (ii) sets of atoms that are relevant for the universal part (checking for minimality). Finally, we go once again back to the leaves and (iii) link sets from past Traversals (i) and (ii) that might lead to an answer set in the future. As a result, we allow for early cleanup of candidates that do not lead to answer sets. Theoretically, such an algorithm resembles a multi-variate view on instances, even though we have a dynamic parameter, which we cannot simply compute before running the solvers.

Furthermore, we present technical improvements (including working on tree decompositions that do not have to be nice) and employ dedicated customization techniques for selecting tree decompositions. Our improvements are main ingredients to speedup the solving process for dynamic programming algorithms. Experiments indicate that DynASP2.5 is competitive even for finding one answer set using the Steiner tree problem on graphs with low treewidth. In particular, we are able to solve instances that have an upper bound on the incidence treewidth of 14 (whereas DynASP2 solved instances of treewidth at most 9).

1.1. Contributions

Our main contributions can be summarized as follows:

• We present a new dynamic programming algorithm on a graph representation that is somewhat in-between the incidence and primal graph and show its correctness.
• We establish a novel fixed-parameter linear algorithm ($\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$), which works in multiple traversals and computes existential and universal parts separately.
• We present an implementation (DynASP2.5) and an experimental evaluation.

1.2. Related Work

Jakl, Pichler, and Woltran [6] have considered ASP solving when parameterized by the treewidth of a graph representation and suggested fixed-parameter linear algorithms. Fichte et al. [11] have established additional algorithms and presented empirical results on an implementation that is dedicated to counting answer sets for the full ground ASP language. The present paper extends their work by a multi-traversal dynamic programming algorithm. Algorithms for particular fragments of ASP [13] and for further language extensions of ASP [14] were proposed, including lower bounds [15]. Compared to general systems [16], our approach directly treats ASP. Bliem et al. [17] have introduced a general multi-traversal approach and an implementation (D-FLAT^2) for dynamic programming on tree decompositions solving subset minimization tasks. Their approach allows to specify dynamic programming algorithms by means of ASP. In a way, one can see ASP in their approach as a meta-language to describe table algorithms (See Algorithm 1 for the concept of table algorithms.), whereas our work presents a dedicated algorithm to find an answer set of a program. In fact, our implementation extends their general ideas for subset minimization (disjunctive rules) to also support weight rules. However, due to space constraints we do not report on weight rules in this paper. Beyond that, we require specialized adaptions to the ASP problem semantics, including three valued evaluation of atoms, handling of tree decompositions that can be not nice, and optimizations in join nodes to be competitive. Abseher, Musliu, and Woltran [18] have presented a framework that computes tree decompositions via heuristics, which is also used in our solver. Other tree decomposition systems can be found on the PACE challenge track A website [19]. Note that improved heuristics for finding a tree decomposition of smaller width (if possible) directly yields faster results for our solver. Other parameters than treewidth have been considered in the literature, however, mostly in a theoretical context [20,21], some also consider just improving on solving the universal part [22], or take multiple parameters into account [23].

1.3. Journal Version

This paper is an extended and updated version of a paper that appeared in the proceedings of the 12th International Symposium on Parameterized and Exact Computation (IPEC’17). The present paper provides a higher level of detail, in particular regarding proofs and examples. We extend its previous versions in the following way. Additionally, we provide comprehensive details on the entire setting of our empirical work, present full listings of encodings, and include results for several runs with varying tree decompositions.

2. Preliminaries

2.1. Tree Decompositions

We assume that the reader is familiar with basic notions in graph theory [24,25], but we will fix some basic terminology below. An undirected graph or simply a graph is a pair $G=(V,E)$ where $V\ne \varnothing$ is a set of vertices and $E\subseteq \left\{\right\{u,v\}\subseteq V\mid u\ne vs.\}$ is a set of edges. We denote an edge $\{v,w\}$ by $uv$ or $vu$. A path of length k is a graph with $k+1$ pairwise distinct vertices $v_1,\cdots ,v_{k+1}$, and k distinct edges $v_i{v}_{i+1}$ where $1\le i\le k$. A path is called simple if all its vertices are distinct. A graph G is called a tree if any two vertices in G can be connected by a unique simple path.

Let $G=(V,E)$ be a graph; $T=(N,F,n)$ a rooted tree with a set N of nodes, a set F of edges, and a root $n\in N$; and $\chi :N\to 2^V$ a function that maps each node $t\in N$ to a set of vertices. We call the sets $\chi (·)$ bags. Then, the pair $\mathcal{T}=(T,\chi )$ is a tree decomposition (TD) of G if the following conditions hold:

1.

for every vertex $v\in V$ there is a node $t\in N$ with $v\in \chi \left(t\right)$;

2.

for every edge $e\in E$ there is a node $t\in N$ with $e\subseteq \chi \left(t\right)$; and

3.

for any three nodes $t_1,t_2,t_3\in N$ whenever $t_2$ lies on the unique path from $t_1$ to $t_3$, then we have $\chi \left(t_1\right)\cap \chi \left(t_3\right)\subseteq \chi \left(t_2\right)$.

We call $max\left\{\right|\chi \left(t\right)|-1\mid t\in N\}$ the width of the TD. The treewidth $\mathit{tw}\left(G\right)$ of a graph G is the minimum width over all possible TDs of G. Note that each graph has a trivial TD $(T,\chi )$ consisting of the tree $\left(\right\{n\},\varnothing ,n)$ and the mapping $\chi \left(n\right)=V$. It is well known that the treewidth of a tree is 1, and a graph containing a clique of size k has at least treewidth $k-1$. For some arbitrary but fixed integer k and a graph of treewidth at most k, we can compute a TD of width $⩽k$ in time $2^{\mathcal{O}\left(k^3\right)}·\left|V\right|$ [26]. Given a TD $(T,\chi )$ with $T=(N,·,·)$, for a node $t\in N$ we say that $type\left(t\right)$ is $\mathit{leaf}$ if t has no children; $\mathit{join}$ if t has children $t^{\prime }$ and $t^{″}$ with $t^{\prime }\ne t^{″}$ and $\chi \left(t\right)=\chi \left(t^{\prime }\right)=\chi \left(t^{″}\right)$; $\mathit{int}$ (“introduce”) if t has a single child $t^{\prime }$, $\chi \left(t^{\prime }\right)\subseteq \chi \left(t\right)$ and $\left|\chi \left(t\right)\right|=|\chi \left(t^{\prime }\right)|+1$; $\mathit{forget}$ (“removal”) if t has a single child $t^{\prime }$, $\chi \left(t^{\prime }\right)\supseteq \chi \left(t\right)$ and $|\chi \left(t^{\prime }\right)|=|\chi \left(t\right)|+1$. If every node $t\in N$ has at most two children, $type\left(t\right)\in \{\mathit{leaf},\mathit{join},\mathit{int},\mathit{forget}\}$, and bags of leaf nodes and the root are empty, then the TD is called nice. For every TD, we can compute a nice TD in linear time without increasing the width [26]. Later, we traverse a TD bottom up, therefore, let $post-order(T,t)$ be the sequence of nodes in post-order of the induced sub-tree $T^{\prime }=(N^{\prime },·,t)$ of T rooted at t.

2.2. Answer Set Programming (ASP)

Answer Set Programming, or ASP for short, is a declarative modeling and problem solving framework that combines techniques of knowledge representation and database theory. In this paper, we restrict ourselves to so-called ground ASP programs. For a comprehensive introduction, we refer the reader to standard texts [1,27,28,29].

2.2.1. Syntax

We consider a universe U of propositional atoms. A literal is an atom $a\in U$ or its negation $\neg a$. Let ℓ, m, n be non-negative integers such that $\ell \le m\le n$, $a_1$, …, $a_n$ distinct propositional atoms, and l a literal. A choice rule is an expression of the form $\{a_1;\dots ;a_{\ell }\}\leftarrow a_{\ell +1},\dots ,a_m,\neg a_{m+1},\dots ,\neg a_n$. A disjunctive rule is of the form $a_1\vee \cdots \vee a_{\ell }\leftarrow a_{\ell +1},\dots ,a_m,\neg$ $a_{m+1}$, …, $\neg a_n$. An optimization rule is an expression of the form $l$. A rule is either a disjunctive, a choice, or an optimization rule. For a choice or disjunctive rule r, let $H_r:=\{a_1,\dots ,a_{\ell }\}$, $B_r^{+}:=\{a_{\ell +1},\dots ,a_m\}$, and $B_r^{-}:=\{a_{m+1},\dots ,a_n\}$. Usually, if $B_r^{-}\cup B_r^{+}=\varnothing$ we write for a rule r simply $H_r$ instead of $H_r\leftarrow$. For an optimization rule r, if $l=a_1$, let $B_r^{+}:=\left\{a_1\right\}$ and $B_r^{-}:=\varnothing$; and if $l=\neg a_1$, let $B_r^{-}:=\left\{a_1\right\}$ and $B_r^{+}:=\varnothing$. For a rule r, let $\mathrm{at}\left(r\right):=H_r\cup B_r^{+}\cup B_r^{-}$ denote its atoms and $B_r:=B_r^{+}\cup \{\neg b\mid b\in B_r^{-}\}$ its body. Let a program P be a set of rules, and $\mathrm{at}\left(P\right):={\bigcup }_{r\in P}\mathrm{at}\left(r\right)$ denote its atoms. Furthermore, let $CH\left(P\right)$, $DISJ\left(P\right)$, and $OPT\left(P\right)$ denote the set of all choice, disjunctive, and optimization rules in P, respectively.

2.2.2. Semantics

A set $M\subseteq \mathrm{at}\left(P\right)$ satisfies a rule r if (i) $(H_r\cup B_r^{-})\cap M\ne \varnothing$ or $B_r^{+}⊈M$ for $r\in DISJ\left(P\right)$ or (ii) $r\in CH\left(P\right)\cup OPT\left(P\right)$. Hence, choice and optimization rules are always satisfied. M is a model of P, denoted by $M\vDash P$, if M satisfies every rule $r\in P$. The reduct $r^M$ (i) of a choice rule r is the set $\{a\leftarrow B_r^{+}\mid a\in H_r\cap M,B_r^{-}\cap M=\varnothing \}$ of rules, and (ii) of a disjunctive rule r is the singleton $\{H_r\leftarrow B_r^{+}\mid B_r^{-}\cap M=\varnothing \}$. $P^M:={\bigcup }_{r\in P}{r}^M$ is called GL reduct of P with respect to M. A set $M\subseteq \mathrm{at}\left(P\right)$ is an answer set of P if (i) $M\vDash P$ and (ii) there is no $M^{\prime }⊊M$ such that $M^{\prime }\vDash P^M$, that is, M is subset minimal with respect to $P^M$. We call $\mathrm{cst}(P,M):=\left|\right\{r\mid r\in P,r\mathrm{is}\mathrm{an}\mathrm{optimization}\mathrm{rule},(B_r^{+}\cap M)\cup (B_r^{-}\setminus M)\ne \varnothing \left\}\right|$ the cost of answer set M for P. An answer set M of P is optimal if its cost is minimal over all answer sets.

Intuitively, a choice rule of the form $\{a_1;\dots ;a_{\ell }\}\leftarrow a_{\ell +1},\dots ,a_m,\neg a_{m+1},\dots ,\neg a_n$ allows us to conclude that if all atoms $a_{\ell +1},\dots ,a_m$ are in an answer set M and there is no evidence that any atom of $a_{m+1},\dots ,a_n$ is in M (so subset-minimality with respect to the reduct forces that $a_{m+1},\dots ,a_n\notin M$), we can conclude that any subset of the atoms $a_1,\dots ,a_{\ell }$ can be in M. In other words, the atoms $a_1,\dots ,a_{\ell }$ are “excluded” from subset minimization. A disjunctive rule of the form $a_1\vee \cdots \vee a_{\ell }\leftarrow a_{\ell +1},\dots ,a_m,\neg$$a_{m+1}$, …, $\neg a_n$ allows us to conclude that if all atoms $a_{\ell +1},\dots ,a_m$ are in M and there is no evidence that any atom of $a_{m+1},\dots ,a_n$ is in M, we can conclude that a subset of the atoms $a_1,\dots ,a_{\ell }$ can be in M, however, remains subject to subset minimization with respect to the reduct. The meaning of optimization rules is simply that we minimize the cardinality of a set M of atoms with respect to the literals in M that occur in any minimization rule positively and not in M for those that occur in any minimization rules negatively.

Example 1.

Consider program

$$\begin{array}{c}\hfill P=\{\stackrel{r_{ab}}{\overbrace{\left\{e_{ab}\right\}}};\stackrel{r_{bc}}{\overbrace{\left\{e_{bc}\right\}}};\stackrel{r_{cd}}{\overbrace{\left\{e_{cd}\right\}}};\stackrel{r_{ad}}{\overbrace{\left\{e_{ad}\right\}}};\stackrel{r_b}{\overbrace{a_b\leftarrow e_{ab}}};\stackrel{r_d}{\overbrace{a_d\leftarrow e_{ad}}};\stackrel{r_{c1}}{\overbrace{a_c\leftarrow a_b,e_{bc}}};\stackrel{r_{c2}}{\overbrace{a_c\leftarrow a_d,e_{cd}}};\stackrel{r_{\neg c}}{\overbrace{\leftarrow \neg a_c}}\}.\end{array}$$

The set $A=\{e_{ab},e_{bc},a_b,a_c\}$ is an answer set of P, since $\{e_{ab},e_{bc},a_b,a_c\}$ is the only minimal model of $P^A=\{e_{ab}\leftarrow ;e_{bc}\leftarrow ;a_b\leftarrow e_{ab};a_d\leftarrow e_{ad};a_c\leftarrow a_b,e_{bc};a_c\leftarrow a_d,e_{cd}\}.$ Then, consider program $R=\{a\vee c\leftarrow b;b\leftarrow c,\neg g;c\leftarrow a;b\vee c\leftarrow e;h\vee i\leftarrow g,\neg c;a\vee b;g\leftarrow \neg i;c;\{d\}\leftarrow g\}$. The set $B=\{b,c,d,g\}$ is an answer set of R since $\{b,c,d,g\}$ and $\{a,c,d,g\}$ are the minimal models of $R^B=\{a\vee c\leftarrow b;c\leftarrow a;b\vee c\leftarrow e;a\vee b;g;c;d\leftarrow g\}$.

In this paper, we mainly consider the output answer set problem, that is, output an answer set for an ASP program. The decision version of this problem is ${\Sigma }_2^p$-complete. When sketching correctness, we also consider the following two problems: listing all optimal answer sets of P, EnumAsp for short; and we the entailment problem of listing every subset-minimal model M of F with $sol\in M$, or EnumMinSAT1, for a given propositional formula F and an atom $sol$.

2.3. Graph Representations of Programs

In order to use TDs for ASP solving, we need dedicated graph representations of programs. The incidence graph $I\left(P\right)$ of P is the bipartite graph that has the atoms and rules of P as vertices and an edge $ar$ if $a\in \mathrm{at}\left(r\right)$ for some rule $r\in P$ [11]. The semi-incidence graph $S\left(P\right)$ of P is a graph that has the atoms and rules of P as vertices and (i) an edge $ar$ if $a\in \mathrm{at}\left(r\right)$ for some rule $r\in P$ as well as (ii) an edge $ab$ for disjoint atoms $a,b\in H_r$ where $r\in P$ is a choice rule. Since for every program P the incidence graph $I\left(P\right)$ is a subgraph of the semi-incidence graph, we have that $\mathit{tw}\left(I\right(P\left)\right)\le \mathit{tw}\left(S\right(P\left)\right)$. Furthermore, by definition of a TD and the construction of a semi-incidence graph that head atoms of choice rules, respectively, occur in at least one common bag of the TD.

2.4. Sub-Programs

Let $\mathcal{T}=(T,\chi )$ be a nice TD of graph representation $S\left(P\right)$ of a program P. Furthermore, let $T=(N,·,n)$ and $t\in N$. The bag-program is defined as $P_t:=P\cap \chi \left(t\right)$. Further, the set ${\mathrm{at}}_{\le t}:=\{a\mid a\in \mathrm{at}\left(P\right)\cap \chi \left(t^{\prime }\right),t^{\prime }\in post-order(T,t)\}$ is called atoms below t, the program below t is defined as $P_{\le t}:=\{r\mid r\in P_{t^{\prime }},t^{\prime }\in post-order(T,t)\}$, and the program strictly below t is $P_{<t}:=P_{\le t}\setminus P_t$. It holds that $P_{\le n}=P_{<n}=P$ and ${\mathrm{at}}_{\le n}=\mathrm{at}\left(P\right)$.

Example 2.

Figure 1 (upper) illustrates the semi-incidence graph of program P from Example 1. Figure 1 (lower) shows a tree decomposition of this graph. Intuitively, the tree decomposition enables us to evaluate P by analyzing sub-programs and combining results agreeing on $a_c$. Indeed, for the given TD of Figure 1 (left), $P_{\le t_6}=\{r_{ab},r_b\}$ and ${\mathrm{at}}_{\le t_6}=\{e_{ab},a_b\}$, $P_{\le t_{23}}=\{r_{ad},r_d\}$ and ${\mathrm{at}}_{\le t_{23}}=\{e_{ad},a_d\}$, as well as $P_{<t_{29}}=\{r_{ad},r_{cd},r_d\}$.

3. A Single Traversal DP Algorithm

A dynamic programming based ASP solver, such as DynASP2 [11], splits the input program P into “bag-programs” based on the structure of a given nice tree decomposition for P and evaluates P in parts, thereby storing the results in tables for each TD node. More precisely, the algorithm works in the following steps:

1.

Construct a graph representation $G\left(P\right)$ of the given input program P.

2.

Compute a TD $\mathcal{T}$ of the graph $G\left(P\right)$ by means of some heuristic, thereby decomposing $G\left(P\right)$ into several smaller parts and fixing an ordering in which P will be evaluated.

3.

For every node $t\in T$ in the tree decomposition $\mathcal{T}=\left(\right(T,E,n),\chi )$ (in a bottom-up traversal), run an algorithm $\mathbb{A}$, which we call table algorithm, and compute a “table” $\mathbb{A}-\mathrm{Tabs}[t]$, which is a set of tuples (or rows for short). Intuitively, algorithm $\mathbb{A}$ transforms tables of child nodes of t to the current node, and solves a “local problem” using bag-program $P_t$. The algorithm thereby computes (i) sets of atoms called (local) witness sets and (ii) for each local witness set M subsets of M called counter-witness sets [11], and directly follows the definition of answer sets being (i) models of P and (ii) subset minimal with respect to $P^M$.

4.

For root n interpret the table $\mathbb{A}-\mathrm{Tabs}[n]$ (and tables of children, if necessary) and print the solution to the considered ASP problem.

Algorithm 1: Algorithm ${\mathtt{DP}}_{\mathbb{A}}\left(\mathcal{T}\right)$ for Dynamic Programming on TD $\mathcal{T}$ for ASP [11].

An Algorithm on the Semi-Incidence Graph

Next, we propose a new table algorithm ($\mathbb{SINC}$) for programs without optimization rules. Since our algorithm trivially extends to counting and optimization rules by earlier work [11], we omit such rules. The table algorithm $\mathbb{SINC}$ employs the semi-incidence graph and is depicted in Algorithm 2. ${\mathtt{DP}}_{\mathbb{SINC}}$ merges two earlier algorithms for the primal and incidence graph [11] resulting in slightly different worst case runtime bounds (c.f., Proposition 1).

Algorithm 2: Table algorithm $\mathbb{SINC}(t,{\chi }_t,P_t,{\mathrm{at}}_{\le t},{\mathrm{Child}-\mathrm{Tabs}}_t)$.

Our table algorithm $\mathbb{SINC}$ computes and stores (i) sets of atoms (witnesses) that are relevant for the Sat part (finding a model of the program) and (ii) sets of atoms (counter-witnesses) that are relevant for the Unsat part (checking for minimality). In addition, we need to store for each set of witnesses as well as its set of counter-witnesses satisfiability states (sat-states for short). For the following reason: By Definition of TDs and the semi-incidence graph, it is true for every atom a and every rule r of a program that if atom a occurs in rule r, then a and r occur together in at least one bag of the TD. In consequence, the table algorithm encounters every occurrence of an atom in any rule. In the end, on removal of r, we have to ensure that r is among the rules that are already satisfied. However, we need to keep track whether a witness satisfies a rule, because not all atoms that occur in a rule occur together in exactly one bag. Hence, when our algorithm traverses the TD and an atom is forgotten we still need to store this sat-state, as setting the forgotten atom to a certain truth value influences the satisfiability of the rule. Since the semi-incidence graph contains a clique on every set A of atoms that occur together in choice rule head, those atoms A occur together in a common bag of any TD of the semi-incidence graph. For that reason, we do not need to incorporate choice rules into the satisfiability state, in contrast to the algorithm for the incidence graph [11]. We can see witness sets together with its sat-state as witness. Then, in Algorithm 2 ($\mathbb{SINC}$) a row in the table ${\tau }_t$ is a triple $\langle M,\sigma ,\mathcal{C}\rangle$. The set $M\subseteq \mathrm{at}\left(P\right)\cap \chi \left(t\right)$ represents a witness set. The family $\mathcal{C}$ of sets concerns counter-witnesses, which we will discuss in more detail below. The sat-state σ for M represents rules of $\chi \left(t\right)$ satisfied by a superset of M. Hence, M witnesses a model $M^{\prime }\supseteq M$ where $M^{\prime }\vDash P_{<t}\cup \sigma$. We use binary operator ∪ to combine sat-states, which ensures that rules satisfied in at least one operand remain satisfied. We compute a new sat-state $\sigma$ from a sat-state and satisfied rules, formally, $SatPr(\dot{R},M):=\{r\mid (r,R)\in \dot{R},M\vDash R\}$ for $M\subseteq \chi \left(t\right)\setminus P_t$ and program $\dot{R}\left(r\right)$ constructed by $\dot{R}$, mapping rules to local-programs as given in the following definition.

Definition 1.

Let P be a program, $\mathcal{T}=(·,\chi )$ be a TD of $S\left(P\right)$, t be a node of $\mathcal{T}$ and $R\subseteq P_t$. The local-program $R^{\left(t\right)}$ is obtained from $R\cup \{\leftarrow B_r\mid r\in Risachoicerule,H_r⊊{\mathrm{at}}_{\le t}\}$ (We require to add $\{\leftarrow B_r\mid r\in Risachoicerule,H_r⊊{\mathrm{at}}_{\le t}\}$ in order to decide satisfiability for corner cases of choice rules involving counter-witnesses of Line 3 in Algorithm 2.) by removing from every rule all literals $a,\neg a$ with $a\notin \chi \left(t\right)$. We define ${\dot{R}}^{\left(t\right)}:R\to 2^{R^{\left(t\right)}}$ by ${\dot{R}}^{\left(t\right)}\left(r\right):={\left\{r\right\}}^{\left(t\right)}$ for $r\in R$.

After we explained how to obtain models, we describe how to compute counter-witnesses. Family $\mathcal{C}$ consists of rows $(C,\rho )$ where $C\subseteq \mathrm{at}\left(P\right)\cap \chi \left(t\right)$ is a counter-witness set in t to M. Similar to the sat-state $\sigma$, the sat-state $\rho$ for C under M represents whether rules of the GL reduct $P_t^M$ are satisfied by a superset of C. We can see counter-witness sets together with its sat-state as counter-witnesses. Thus, C witnesses the existence of $C^{\prime }⊊M^{\prime }$ satisfying $C^{\prime }\vDash {(P_{<t}\cup \rho )}^{M^{\prime }}$ since M witnesses a model $M^{\prime }\supseteq M$ where $M^{\prime }\vDash P_{<t}$. In consequence, there exists an answer set of P if the root table contains $\langle \varnothing ,\varnothing ,\varnothing \rangle$. We require local-reducts for deciding satisfiability of counter-witness sets.

Definition 2.

Let P be a program, $\mathcal{T}=(·,\chi )$ be a TD of $S\left(P\right)$, t be a node of $\mathcal{T}$, $R\subseteq P_t$ and $M\subseteq \mathrm{at}\left(P\right)$. We define local-reduct $R^{(t,M)}$by ${\left[R^{\left(t\right)}\right]}^M$ and ${\dot{R}}^{(t,M)}:R\to 2^{R^{(t,M)}}$ by ${\dot{R}}^{(t,M)}\left(r\right):={\left\{r\right\}}^{(t,M)},r\in R$.

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

3.1. Correctness and Runtime of Algorithm 2 ($\mathbb{SINC}$)

Next, we provide insights into the correctness and runtime of Algorithm 2 ($\mathbb{SINC}$).

Proposition 1.

Let P be a program and $k:=\mathit{tw}\left(S\right(P\left)\right)$. Then, the algorithm ${\mathtt{DP}}_{\mathbb{SINC}}$ is correct and runs in time $\mathcal{O}(2^{2^{k+2}}·\parallel S\left(P\right)\parallel )$.

Proof (Idea/Main Arguments)

Previous works [6,11] established the correctness and runtime guarantees on the primal and incidence graph, respectively. Since the semi-incidence graph introduces a clique only for choice rule and the algorithm on the semi-incidence graph follows the algorithm on the incidence graph for non-choice rules and the one for the primal graph for choice rules, we immediately obtain correctness and runtime results as the cases never overlap.  □

The remainder of this sections provides details on proving the statement above. The correctness proof investigates each node type separately. We have to show that a tuple at a node t guarantees existence of an answer set for the program $P_{\le t}$, proving soundness. Conversely, we have to show that each answer set is indeed evaluated while traversing the tree decomposition, which provides completeness. We employ this idea using the notions of (i) partial solutions consisting of partial models and the notion of (ii) local partial solutions.

Definition 3.

Let P be a program, $\mathcal{T}=(T,\chi )$ be a tree decomposition of the semi-incidence graph $S\left(P\right)$ of P, where $T=(N,·,·)$, and $t\in N$ be a node. Further, let $M,C\subseteq {\mathrm{at}}_{\le t}$ be sets and $\sigma \subseteq P_{\le t}$ be a set of rules. The tuple $(C,\sigma )$ is a partial model for t under Mif the following conditions hold:

1. 

$C\vDash {\left(P_{<t}\right)}^M$,

2. 

for $r\in P_{\le t}$ we require:

3. 

 

(a) 

for disjunctive rule $r\in P_{\le t}$, we have $B_r^{-}\cap M\ne \varnothing$ or $B_r^{+}\cap {\mathrm{at}}_{\le t}\neg \subseteq C$ or $H_r\cap C\ne \varnothing$ if and only if $r\in \sigma$;

(b) 

for choice rule $r\in P_t$, we have $B_r^{-}\cap M\ne \varnothing$ or $B_r^{+}\cap {\mathrm{at}}_t\neg \subseteq C$ or both $H_r\subseteq {\mathrm{at}}_t$ and $H_r\cap (M\setminus C)=\varnothing$ if and only if $r\in \sigma$.

Definition 4.

Let P be a program, $\mathcal{T}=(T,\chi )$ where $T=(N,·,n)$ be a tree decomposition of $I\left(P\right)$, and $t\in N$ be a node. A partial solution for t is a tuple $(M,\sigma ,\mathcal{C})$ where $(M,\sigma )$ is a partial model under M and $\mathcal{C}$ is a set of partial models $(C,\rho )$ under M with $C⊊M$.

The following lemma establishes correspondence between answer sets and partial solutions.

Observation 1.

Let P be a program, $\mathcal{T}=(T,\chi )$ be a tree decomposition of the semi-incidence graph $S\left(P\right)$ of program P, where $T=(·,·,n)$, and $\chi \left(n\right)=\varnothing$. Then, there exists an answer set M for P if and only if there exists a partial solution $u=(M,\sigma ,\varnothing )$ with $\sigma P$ for root n.

Proof. 

Given an answer set M of P we construct $u=(M,\sigma ,\varnothing )$ with $\sigma :=P$ such that u is a partial solution for n according to Definition 4. For the other direction, Definition 3 and Definition 4 guarantee that M is an answer set if there exists some tuple u. In consequence, the observation holds.  □

Next, we define local partial solutions to establish a notion that corresponds to the tuples obtained in Algorithm 2 but on in relation to solutions that we are interested in.

Definition 5.

Let P be a program, $\mathcal{T}=(T,\chi )$ a tree decomposition of the semi-incidence graph $S\left(P\right)$, where $T=(N,·,n)$, and $t\in N$ be a node. A tuple $u=\langle M,\sigma ,\mathcal{C}\rangle$ is a local partial solution for t if there exists a partial solution $\widehat{u}=(\widehat{M},\widehat{\sigma },\widehat{\mathcal{C}})$ for t such that the following conditions hold:

1.

$M=\widehat{M}\cap \chi \left(t\right)$,

2.

$\sigma =\widehat{\sigma }$, and

3.

$\mathcal{C}=\{\langle \widehat{C}\cap \chi \left(t\right),{\widehat{\rho }}^{t,\widehat{M},\widehat{C}}\rangle \mid (\widehat{C},\widehat{\rho })\in \widehat{\mathcal{C}}\}$.

We denote by ${\widehat{u}}^t$ the local partial solution u for t given partial solution $\widehat{u}$.

The following observation provides justification that it suffices to store local partial solutions instead of partial solutions for a node $t\in N$.

Observation 2.

Let P be a program, $\mathcal{T}=(T,\chi )$ a tree decomposition of $S\left(P\right)$, where $T=(N,·,n)$, and $\chi \left(n\right)=\varnothing$. Then, there exists an answer set for P if and only if there exists a local partial solution of the form $\langle \varnothing ,\varnothing ,\varnothing \rangle$ for the root $n\in N$.

Proof. 

Since $\chi \left(n\right)=\varnothing$, every partial solution for the root n is an extension of the local partial solution u for the root $n\in N$ according to Definition 5. By Observation 1, we obtain that the observation is true.  □

In the following, we abbreviate atoms occurring in bag $\chi \left(t\right)$ by ${\mathrm{at}}_t$, i.e., ${\mathrm{at}}_t:=\chi \left(t\right)\setminus P_t$.

Lemma 1

(Soundness). Let P be a program, $\mathcal{T}=(T,\chi )$ a tree decomposition of semi-incidence graph $S\left(P\right)$, where $T=(N,·,·)$, and $t\in N$ a node. Given a local partial solution $u^{\prime }$ of child table ${\tau }_{}^{\prime }$ (or local partial solution $u^{\prime }$ of table ${\tau }^{\prime }$ and local partial solution $u^{″}$ of table ${\tau }^{″}$), each tuple u of table ${\tau }_t$ constructed using table algorithm $\mathbb{SINC}$ is also a local partial solution.

Proof. 

Let $u^{\prime }$ be a local partial solution for $t^{\prime }\in N$ and u a tuple for node $t\in N$ such that u was derived from $u^{\prime }$ using table algorithm $\mathbb{SINC}$. Hence, node $t^{\prime }$ is the only child of t and t is either removal or introduce node.

Assume that t is a removal node and $r\in P_{t^{\prime }}\setminus P_t$ for some rule r. Observe that $u=\langle M,\sigma ,\mathcal{C}\rangle$ and $u^{\prime }=\langle M,{\sigma }^{\prime },{\mathcal{C}}^{\prime }\rangle$ are the same in witness M. According to Algorithm 2 and since u is derived from $u^{\prime }$, we have $r\in {\sigma }^{\prime }$ Similarly, for any $\langle C^{\prime },{\rho }^{\prime }\rangle \in {\mathcal{C}}^{\prime }$, $r\in {\rho }^{\prime }$. Since $u^{\prime }$ is a local partial solution, there exists a partial solution ${\widehat{u}}^{\prime }$ of $t^{\prime }$, satisfying the conditions of Definition 5. Then, ${\widehat{u}}^{\prime }$ is also a partial solution for node t, since it satisfies all conditions of Definitions 3 and 4. Finally, note that $u={\left({\widehat{u}}^{\prime }\right)}^t$ since the projection of ${\widehat{u}}^{\prime }$ to the bag $\chi \left(t\right)$ is u itself. In consequence, the tuple u is a local partial solution.

For $a\in {\mathrm{at}}_{t^{\prime }}\setminus {\mathrm{at}}_t$ as well as for introduce nodes, we can analogously check the lemma.

Next, assume that t is a join node. Therefore, let $u^{\prime }$ and $u^{″}$ be local partial solutions for $t^{\prime },t^{″}\in N$, , respectively, and u be a tuple for node $t\in N$ such that u can be derived using both $u^{\prime }$ and $u^{″}$ in accordance with the $\mathbb{SINC}$ algorithm. Since $u^{\prime }$ and $u^{″}$ are local partial solutions, there exists partial solution ${\widehat{u}}^{\prime }=({\widehat{M}}^{\prime },{\widehat{\sigma }}^{\prime },{\widehat{\mathcal{C}}}^{\prime })$ for node $t^{\prime }$ and partial solution ${\widehat{u}}^{″}=({\widehat{M}}^{″},{\widehat{\sigma }}^{″},{\widehat{\mathcal{C}}}^{″})$ for node $t^{″}$. Using these two partial solutions, we can construct where $\bowtie (·,·)$ is defined in accordance with Algorithm 2 as follows:

Then, we check all conditions of Definitions 3 and 4 in order to verify that $\widehat{u}$ is a partial solution for t. Moreover, the projection ${\widehat{u}}^t$ of $\widehat{u}$ to the bag $\chi \left(t\right)$ is exactly u by construction and hence, $u={\widehat{u}}^t$ is a local partial solution.

Since we have provided arguments for each node type, we established soundness in terms of the statement of the lemma.  □

Lemma 2

(Completeness). Let P be a program, $\mathcal{T}=(T,\chi )$ where $T=(N,·,·)$ be a tree decomposition of the semi-incidence graph $S\left(P\right)$ and $t\in N$ be a node. Given a local partial solution u of table t, either t is a leaf node, or there exists a local partial solution $u^{\prime }$ of child table ${\tau }_{}^{\prime }$ (or local partial solution $u^{\prime }$ of table ${\tau }_{}^{\prime }$ and local partial solution $u^{″}$ of table ${\tau }^{″}$) such that u can be constructed by $u^{\prime }$ (or $u^{\prime }$ and $u^{″}$, respectively) and using table algorithm $\mathbb{SINC}$.

Proof. 

Let $t\in N$ be a removal node and $r\in P_{t^{\prime }}\setminus P_t$ with child node $t^{\prime }\in N$. We show that there exists a tuple $u^{\prime }$ in table ${\tau }_{t^{\prime }}$ for node $t^{\prime }$ such that u can be constructed using $u^{\prime }$ by $\mathbb{SINC}$ (Algorithm 2). Since u is a local partial solution, there exists a partial solution $\widehat{u}=(\widehat{M},\widehat{\sigma },\widehat{\mathcal{C}})$ for node t, satisfying the conditions of Definition 5. Since r is the removed rule, we have $r\in \widehat{\sigma }$. By similar arguments, we have $r\in \widehat{\rho }$ for any tuple $(\widehat{C},\widehat{\rho })\in \widehat{\mathcal{C}}$. Hence, $\widehat{u}$ is also a partial solution for $t^{\prime }$ and we define $u^{\prime }:={\widehat{u}}^{t^{\prime }}$, which is the projection of $\widehat{u}$ onto the bag of $t^{\prime }$. Apparently, the tuple $u^{\prime }$ is a local partial solution for node $t^{\prime }$ according to Definition 5. Then, u can be derived using $\mathbb{SINC}$ algorithm and $u^{\prime }$. By similar arguments, we establish the lemma for $a\in {\mathrm{at}}_{t^{\prime }}\setminus {\mathrm{at}}_t$ and the remaining (three) node types. Hence, the lemma sustains.    □

Now, we are in situation to prove the correctness statement in Proposition 1.

Proof of Proposition 1 (Correctness).

We first show soundness. Let $\mathcal{T}=(T,\chi )$ be the given tree decomposition, where $T=(N,·,n)$. By Observation 2 we know that there is an answer set for P if and only if there exists a local partial solution for the root n. Note that the tuple is of the form $\langle \varnothing ,\varnothing ,\varnothing \rangle$ by construction. Hence, we proceed by induction starting from the leaf nodes. In fact, the tuple $\langle \varnothing ,\varnothing ,\varnothing \rangle$ is trivially a partial solution by Definitions 3 and 4 and also a local partial solution of $\langle \varnothing ,\varnothing ,\varnothing \rangle$ by Definition 5. We already established the induction step in Lemma 1. Hence, when we reach the root n, when traversing the tree decomposition in post-order by algorithm ${\mathtt{DP}}_{\mathbb{SINC}}$, we obtain only valid tuples in between and a tuple of the form $\langle \varnothing ,\varnothing ,\varnothing \rangle$ in the table of the root n witnesses an answer set. Next, we establish completeness by induction starting from the root n. Let therefore, M be an arbitrary answer set of P. By Observation 1, we know that for the root n there exists a local partial solution of the form $\langle \varnothing ,\varnothing ,\varnothing \rangle$ for partial solution $\langle M,\sigma ,\varnothing \rangle$ with $r\in \sigma$ for $r\in P$. We already established the induction step in Lemma 2. Hence, we obtain some (corresponding) tuples for every node t. Finally, stopping at the leaves n. In consequence, we have shown both soundness and completeness resulting in the fact that the correctness statement made in Proposition 1 is true.  □

Next, we turn our attention to the worst-case runtime bounds claimed in Proposition 1. First, we give a lemma on worst-case space requirements in tables for the nodes of our algorithm.

Lemma 3.

Given a program P, a tree decomposition $\mathcal{T}=(T,\chi )$ with $T=(N,·,·)$ of the semi-incidence graph $S\left(P\right)$, and a node $t\in N$. Then, there are at most $2^{k+1}·2^{k+1}·2^{2^{k+1}·2^{k+1}}$ tuples in ${\tau }_t$ using algorithm ${\mathtt{DP}}_{\mathbb{SINC}}$ for width k of $\mathcal{T}$.

Proof (Sketch).

Let P be the given program, $\mathcal{T}=(T,\chi )$ a tree decomposition of the semi-incidence graph $S\left(P\right)$, where $T=(N,·,·)$, and $t\in N$ a node of the tree decomposition. Then, by definition of a decomposition of the primal graph for each node $t\in N$, we have $\left|\chi \right(t\left)\right|-1\le k$. In consequence, we can have at most $2^{k+1}$ many witnesses, and for each witness a subset of the set of witnesses consisting of at most $2^{2^{k+1}}$ many counter-witnesses. In total, we need to distinguish $2^{k+1}$ two states for the sat-states $\sigma$ and for each witness of a tuple in the table ${\tau }_t$ for node t. Since for each witness in the table ${\tau }_t$ for node $t\in N$ we remember rule-states for at most $k+1$ rules, we store up to $2^{k+1}$ many combinations per witness. In total we end up with at most $2^{2^{k+1}·2^{k+1}}$ many counter-witnesses for each witness and rule-state in the worst case. Thus, there are at most $2^{k+1}·2^{k+1}·2^{2^{k+1}·2^{k+1}}$ tuples in table ${\tau }_t$ for node t. In consequence, we established the lemma.  □

Proof of Proposition 1 (Runtime).

Let P be a program, $S\left(P\right)=(V,·)$ its semi-incidence graph, and k be the treewidth of $P\left(P\right)$. Then, we can compute in time $2^{\mathcal{O}\left(k^3\right)}·\left|V\right|$ a tree decomposition of width at most k [30]. We take such a tree decomposition and compute in linear time a nice tree decomposition [31]. Let $\mathcal{T}=(T,\chi )$ be such a nice tree decomposition with $T=(N,·,·)$. Since the number of nodes in N is linear in the graph size and since for every node $t\in N$ the table ${\tau }_t$ is bounded by $2^{k+1}·2^{k+1}·2^{2^{k+1}·2^{k+1}}$ according to Lemma 3, we obtain a running time of $\mathcal{O}(2^{2^{k+2}}·\parallel S\left(P\right)\parallel )$.Consequently, the claimed runtime bounds in the proposition hold.  □

3.2. An Extended Example

In Example 3 we give an idea how we compute models of a given program using the semi-incidence graph. The resulting algorithm $\mathbb{MOD}$ is obtained from $\mathbb{SINC}$, by taking only the first two row positions (red and green parts). The remaining position (blue part), can be seen as an algorithm ($\mathbb{CMOD}$) that computes counter-witnesses. We assume that the ith-row in each table ${\tau }_t$ corresponds to $u_{t.i}=\langle M_{t.i},{\sigma }_{t.i}\rangle$.

Example 3.

Consider program P from Example 1, which was given by

$$\begin{array}{c}\hfill P=\{\stackrel{r_{ab}}{\overbrace{\left\{e_{ab}\right\}}};\stackrel{r_{bc}}{\overbrace{\left\{e_{bc}\right\}}};\stackrel{r_{cd}}{\overbrace{\left\{e_{cd}\right\}}};\stackrel{r_{ad}}{\overbrace{\left\{e_{ad}\right\}}};\stackrel{r_b}{\overbrace{a_b\leftarrow e_{ab}}};\stackrel{r_d}{\overbrace{a_d\leftarrow e_{ad}}};\stackrel{r_{c1}}{\overbrace{a_c\leftarrow a_b,e_{bc}}};\stackrel{r_{c2}}{\overbrace{a_c\leftarrow a_d,e_{cd}}};\stackrel{r_{\neg c}}{\overbrace{\leftarrow \neg a_c}}\},\end{array}$$

TD $\mathcal{T}=(·,\chi )$ in Figure 2, and the tables ${\tau }_1$,…, ${\tau }_{34}$, which illustrate computation results obtained during post-order traversal of $\mathcal{T}$ by ${\mathtt{DP}}_{\mathbb{MOD}}$. Note that Figure 2 does not show every intermediate node of TD $\mathcal{T}$. Table ${\tau }_1=\left\{\langle \varnothing ,\varnothing \rangle \right\}$ as $type\left(t_1\right)=\mathit{leaf}$ (see Algorithm 2 L1). Table ${\tau }_3$ is obtained via introducing rule $r_{ab}$, after introducing atom $e_{ab}$ ($type\left(t_2\right)=type\left(t_3\right)=\mathit{int}$). It contains two rows due to two possible truth assignments using atom $e_{ab}$ (L3–5). Observe that rule $r_{ab}$ is satisfied in both rows $M_{3.1}$ and $M_{3.2}$, since the head of choice rule $r_{ab}$ is in ${\mathrm{at}}_{\le t_3}$ (see L7 and Definition 1). Intuitively, whenever a rule r is proven to be satisfiable, sat-state ${\sigma }_{t.i}$ marks r satisfiable since an atom of a rule of $S\left(P\right)$ might only occur in one TD bag. Consider table ${\tau }_4$ with $type\left(t_4\right)=\mathit{forget}$ and $r_{ab}\in \chi \left(t_3\right)\setminus \chi \left(t_4\right)$. By definition (TDs and semi-incidence graph), we have encountered every occurrence of any atom in $r_{ab}$. In consequence, $\mathbb{MOD}$ enforces that only rows where $r_{ab}$ is marked satisfiable in ${\tau }_3$, are considered for table ${\tau }_4$. The resulting table ${\tau }_4$ consists of rows of ${\tau }_3$ with ${\sigma }_{4.i}=\varnothing$, where rule $r_{ab}$ is proven satisfied ($r_{ab}\in {\sigma }_{3.1},{\sigma }_{3.2}$, see L 11). Note that between nodes $t_6$ and $t_{10}$, an atom and rule remove as well as an atom and rule introduce node is placed. Observe that the second row $u_{6.2}=\langle M_{6.2},{\sigma }_{6.2}\rangle \in {\tau }_6$ does not have a “successor row” in ${\tau }_{10}$, since $r_b\notin {\sigma }_{6.2}$. Intuitively, join node $t_{34}$ joins only common witness sets in ${\tau }_{17}$ and ${\tau }_{33}$ with $\chi \left(t_{17}\right)=\chi \left(t_{33}\right)=\chi \left(t_{34}\right)$. In general, a join node marks rules satisfied, which are marked satisfied in at least one child (see L13–14).

We assume again row numbers per table ${\tau }_t$, i.e., $u_{t.i}=\langle M_{t.i},{\sigma }_{t.i},{\mathcal{C}}_{t.i}\rangle$ is the $i^{th}$-row. Further, for each counter-witness  $\langle C_{t.i.j},{\rho }_{t.i.j}\rangle \in {\mathcal{C}}_{t.i}$, j marks its “order” (as depicted in Figure 3 (right)) in set ${\mathcal{C}}_{t.i}$.

Example 4.

Again, we consider program P from Example 1, and $\mathcal{T}=(·,\chi )$ of Figure 3 as well as tables ${\tau }_1$, …, ${\tau }_{34}$ of Figure 3 (right) using ${\mathtt{DP}}_{\mathbb{SINC}}$. We only discuss certain tables. Table ${\tau }_1=\left\{\langle \varnothing ,\varnothing ,\varnothing \rangle \right\}$ as $type\left(t_1\right)=\mathit{leaf}$. Node $t_2$ introduces atom $e_{ab}$, resulting in table $\{\langle \left\{e_{ab}\right\},\varnothing ,\left\{(\varnothing ,\varnothing )\right\}\rangle ,\langle \varnothing ,\varnothing ,\varnothing \rangle \}$ (compare to Algorithm 2 L3–5). Then, node $t_3$ introduces rule $r_{ab}$, which is forgotten in node $t_4$. Note that $C_{3.1.1}=\langle \varnothing ,\varnothing \rangle \in {\mathcal{C}}_{3.1.1}$ does not have a “successor row” in table ${\tau }_4$ since $r_{ab}$ is not satisfied (see L11 and Definition 2). Table ${\tau }_6$ is then the result of a chain of introduce nodes, and contains for each witness set $M_{6.i}$ every possible counter-witness set $C_{6.i.j}$ with $C_{6.i.j}⊊M_{6.i}$. We now discuss table ${\tau }_{12}$, intuitively containing (a projection of) (counter-)witnesses of ${\tau }_{10}$, which satisfy rule $r_{bc}$ after introducing rule $r_{c1}$. Observe that there is no succeeding witness set for $M_{6.2}=\left\{e_{ab}\right\}$ in ${\tau }_{10}$ (nor ${\tau }_{12}$), since $e_{ab}\in M_{6.2}$, but $a_b\notin M_{6.2}$ (required to satisfy $r_b$). Rows $u_{12.1},u_{12.4}$ form successors of $u_{6.3}$, while rows $u_{12.2},u_{12.5}$ succeed $u_{6.1}$, since counter-witness set $C_{6.1.1}$ has no succeeding row in ${\tau }_{10}$ because it does not satisfy $r_b$. Remaining rows $u_{12.3}$, $u_{12.6}$ have “origin” $u_{6.4}$ in ${\tau }_6$.

4. DynASP2.5: Towards a III Traversal DP Algorithm

The classical DP algorithm ${\mathtt{DP}}_{\mathbb{SINC}}$ (Step 3 of Figure 4) follows a single traversal approach. It computes both witnesses and counter-witnesses by traversing the given TD exactly once. In particular, it stores exhaustively all potential counter-witnesses, even those counter-witnesses where the witnesses in the table of a node cannot be extended in the parent node. In addition, there can be a high number of duplicates among the counter-witnesses, which are stored repeatedly.

In this section, we propose a multi-traversal approach ($\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$) for DP on TDs and a new implementation (DynASP2.5), which fruitfully adapts and extends ideas from a different domain [17]. From a theoretical perspective, our novel algorithm $\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$ is multi-variate practically, considering treewidth together with the maximum number of witnesses in a table that lead to a solution at the root. Intuitively, this subtle difference can yield practical advantages, especially if the number of relevant witnesses in a table that lead to a solution is subexponential in the treewidth. Therefore, our novel algorithm is designed to allow for an early cleanup (purging) of witnesses that do not lead to answer sets, which in consequence (i) avoids to construct expendable counter-witnesses. Moreover, multiple traversals enable us to store witnesses and counter-witnesses separately, which in turn (ii) avoids storing counter-witnesses duplicately and (iii) allows for highly space efficient data structures (pointers) in practice when linking witnesses and counter-witnesses together. Figure 4 (right, middle) presents the control flow of the new multi-traversal approach DynASP2.5, where $\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$ introduces a much more elaborate computation in Step 3.

4.1. The Algorithm

Our algorithm ($\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$) executed as Step 3 runs ${\mathtt{DP}}_{\mathbb{MOD}}$, ${\mathtt{DP}}_{\mathbb{CMOD}}$ and ${\mathtt{DPL}}_{\mathbb{MOD},\mathbb{CMOD}}$ in three traversals (3.I, 3.II, and 3.III) as follows:

3.I.

First, we run the algorithm ${\mathtt{DP}}_{\mathbb{MOD}}$, which computes in a bottom-up traversal for every node t in the tree decomposition a table $\mathbb{MOD}-\mathrm{Tabs}[t]$ of witnesses for t. Then, in a top-down traversal for every node t in the TD remove from tables $\mathbb{MOD}-\mathrm{Tabs}[t]$ witnesses, which do not extend to a witness in the table for the parent node (“Purge non-witnesses”); these witnesses can never be used to construct a model (nor answer set) of the program.

3.II.

For this step, let $\mathbb{CMOD}$ be a table algorithm computing only counter-witnesses of $\mathbb{SINC}$ (blue parts of Algorithm 2). We execute ${\mathtt{DP}}_{\mathbb{CMOD}}$, for all witnesses, compute counter-witnesses at once and store the resulting tables in $\mathbb{CMOD}-\mathrm{Tabs}[·]$. For every node t, table $\mathbb{CMOD}-\mathrm{Tabs}[t]$ contains counter-witnesses to witness being ⊂-minimal. Again, irrelevant rows are removed (“Purge non-counter-witnesses”).

3.III.

Finally, in a bottom-up traversal for every node t in the TD, witnesses and counter-witnesses are linked using algorithm ${\mathtt{DPL}}_{\mathbb{MOD},\mathbb{CMOD}}$ (see Algorithm 3). ${\mathtt{DPL}}_{\mathbb{MOD},\mathbb{CMOD}}$ takes previous results and maps rows in $\mathbb{MOD}-\mathrm{Tabs}[t]$ to a table (set) of rows in $\mathbb{CMOD}-\mathrm{Tabs}[t]$.

Algorithm 3: Algorithm ${\mathtt{DPL}}_{\mathbb{W},\mathbb{C}}(\mathcal{T},\mathbb{W}-\mathrm{Tabs},\mathbb{C}-\mathrm{Tabs})$ for linking counter-witnesses to witnesses.

We already explained the table algorithms ${\mathtt{DP}}_{\mathbb{MOD}}$ and ${\mathtt{DP}}_{\mathbb{CMOD}}$ in the previous section. The main part of our multi-traversal algorithm is the algorithm ${\mathtt{DPL}}_{\mathbb{MOD},\mathbb{CMOD}}$ based on the general algorithm ${\mathtt{DPL}}_{\mathbb{W},\mathbb{C}}$ (Algorithm 3) with $\mathbb{W}=\mathbb{MOD}$, $\mathbb{C}=\mathbb{CMOD}$, which links those separate tables together. Before we quickly discuss the core of ${\mathtt{DPL}}_{\mathbb{W},\mathbb{C}}$ in Lines 6–10, note that Lines 3–5 introduce auxiliary definitions. Line 3 combines rows of the child nodes of given node t, which is achieved by a product over sets, where we drop the order and keep sets only. Line 4 concerns determining for a row $\overrightarrow{u}$ its origins (finding preceding combined rows that lead to $\overrightarrow{u}$ using table algorithm $\mathbb{W}$). Line 5 covers deriving succeeding rows for a certain child row combination its evolution rows via algorithm $\mathbb{C}$. In an implementation, origin as well as evolution are not computed, but represented via pointer data structures directly linking to $\mathbb{W}-\mathrm{Tabs}[·]$ or $\mathbb{C}-\mathrm{Tabs}[·]$, respectively. Then, the table algorithm ${\mathtt{DPL}}_{\mathbb{W},\mathbb{C}}$ applies a post-order traversal and links witnesses to counter-witnesses in Line 10. ${\mathtt{DPL}}_{\mathbb{W},\mathbb{C}}$ searches for origins (orig) of a certain witness $\overrightarrow{u}$, uses the counter-witnesses ($f_{cw}$) linked to these origins, and then determines the evolution (evol) in order to derive counter-witnesses (using subs) of $\overrightarrow{u}$.

4.2. An Elaborated Example

Example 5.

Let k be some integer and $P_k$ be some program that contains the following rules $r_c:=\{a_1,\cdots ,a_k\}\leftarrow f$, $r_2:=\leftarrow \neg a_2$, …, $r_k:=\leftarrow \neg a_k$, and $r_f:=\leftarrow \neg f$ and $r_{cf}:=\left\{f\right\}\leftarrow$. The rules $r_1$, …, $r_k$ simulate that only certain subsets of $\{a_1,\cdots ,a_k\}$ are allowed. Rules $r_f$ and $r_{cf}$ enforce that f is set to true. Let $\mathcal{T}=(T,\chi ,t_3)$ be a TD of the semi-incidence graph $S\left(P_k\right)$ of program $P_k$ where $T=(V,E)$ with $V=\{t_1,t_2,t_3\}$, $E=\{(t_1,t_2),(t_2,t_3)\}$, $\chi \left(t_1\right)=\{a_1,\cdots ,a_k,f,r_c,r_{cf}\}$, $\chi \left(t_2\right)=\{a_1,\cdots ,a_k,r_2,\cdots ,r_k,r_f\}$, and $\chi \left(t_3\right)=\varnothing$. Figure 5 (left) illustrates the tables for program $P_2$ after ${\mathtt{DP}}_{\mathbb{SINC}}$, whereas Figure 5 (right) presents tables using $\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$, which are exponentially smaller in k, mainly due to cleanup. Observe that Traversal 3.II $\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$, “temporarily” materializes counter-witnesses only for ${\tau }_1$, presented in table ${\tau }_1^{\mathbb{CMOD}}$. Hence, using multi-traversal algorithm $\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$ results in an exponential speedup. Note that we can trivially extend the program such that we have the same effect for a TD of minimum width and even if we take the incidence graph. In practice, programs containing the rules above frequently occur when encoding by means of saturation [3]. The program $P_k$ and the TD $\mathcal{T}$ also reveal that a different TD of the same width, where f occurs already very early in the bottom-up traversal, would result in a smaller table ${\tau }_1$ even when running ${\mathtt{DP}}_{\mathbb{SINC}}$.

4.3. Correctness and Runtime of DynASP2.5

Theorem 1.

For a program P of semi-incidence treewidth $k:=\mathit{tw}\left(S\right(P\left)\right)$, the algorithm $\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$ is correct and runs in time $\mathcal{O}(2^{2^{k+2}}·\parallel P\parallel )$.

We first sketch the outline of the proof.

Proof (Sketch).

We sketch the proof idea for enumerating answer sets of disjunctive ASP programs by means of $\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$. Below we present a more detailed approach to establish the correctness. Let P be a disjunctive program and $k:=\mathit{tw}\left(S\right(P\left)\right)$. We establish a reduction $R(P,k)$ of EnumAsp to EnumMinSAT1, such that there is a one-to-one correspondence between answer sets and models of the formula, more precisely, for every answer set M of P and for the resulting instance $(F,k^{\prime })=R(P,k)$ the set $M\cup \left\{sol\right\}$ is a subset-minimal model of F and $k^{\prime }=tw\left(I\left(F\right)\right)$ with $k^{\prime }\le 7k+2$. We compute in time $2^{\mathcal{O}\left(k^{\prime 3}\right)}·\parallel F\parallel$ a TD of width at most $k^{\prime }$ [26] and add $sol$ to every bag. Using a table algorithm designed for SAT [32] we compute witnesses and counter-witnesses. Observe that witnesses and counter-witnesses are essentially the same objects in a table algorithm for computing subset-minimal models of a propositional formula, since witnesses and counter-witnesses of traversals 3.I and 3.II, respectively, are essentially the same objects in a table algorithm for computing subset-minimal models of a propositional formula. Conceptually, one could also modify $\mathbb{MOD}$ for this task. In order to finally show correctness of linking counter-witnesses to witnesses as presented in ${\mathtt{DPL}}_{\mathbb{MOD},\mathbb{MOD}}$, we have to extend earlier work [17], (Theorem 3.25 and 3.26). Therefore, we enumerate subset-minimal models of F by following each witness set containing $sol$ at the root having counter-witnesses ∅ back to the leaves. This runs in time $\mathcal{O}(2^{2^{(7k+2)+2}}·\parallel P\parallel )$, c.f., [11,17]. A more involved (direct) proof, allows to decrease the runtime to $\mathcal{O}(2^{2^{k+2}}·\parallel P\parallel )$ (even for choice rules). □

In the following of this section, we go into more details to provide more depth arguments to support our statement above. Bliem et al. [17] have shown that augmentable $\mathbb{W}-\mathrm{Tabs}$ can be transformed into $\mathbb{W},\mathbb{W}-\mathrm{Tabs}$, which easily allows reading off subset-minimal solutions starting at the table $\mathbb{W},\mathbb{W}-\mathrm{Tabs}[n]$ for TD root n. We follow their concepts and define a slightly extended variant of augmentable tables. Therefore, we reduce the problem of enumerating disjunctive programs to $EnumMinSAT1$ and show that the resulting tables of algorithm $\mathbb{MOD}$ (see Algorithm 2) are augmentable. In the end, we apply an earlier theorem [17] transforming $\mathbb{MOD}-\mathrm{Tabs}$ obtained by ${\mathtt{DP}}_{\mathbb{MOD}}$ into $\mathbb{MOD},\mathbb{MOD}-\mathrm{Tabs}$ via the augmenting function $aug(·)$ proposed in their work. To this extent, we use auxiliary definitions ${\mathrm{Child}-\mathrm{Tabs}}_t$, ${orig}_t(·)$ and ${evol}_t(·)$ specified in Algorithm 3.

Definition 6.

Let $\mathcal{T}=(T,\chi )$ be a TD where $T=(N,·,·)$, $\mathbb{W}$ be a table algorithm, $t\in N$, and ${\tau }_{}\in \mathbb{W}-\mathrm{Tabs}\left[t\right]$ be the table for node t. For tuple $\overrightarrow{u}=\langle M,\sigma ,\cdots \rangle \in {\tau }_{}$, we define $\alpha \left(\overrightarrow{u}\right):=M$, $\beta \left(\overrightarrow{u}\right):=\sigma$. We inductively define

$${\alpha }^{*}\left({\tau }_{}\right):=\bigcup _{\overrightarrow{u}\in {\tau }_{}}\alpha \left(\overrightarrow{u}\right)\cup \bigcup _{{\tau }_{}^{\prime }\in {Child-Tabs}_t}{\alpha }^{*}\left({\tau }_{}^{\prime }\right),and$$

$${\beta }^{*}\left({\tau }_{}\right):=\bigcup _{\overrightarrow{u}\in {\tau }_{}}\beta \left(\overrightarrow{u}\right)\cup \bigcup _{{\tau }_{}^{\prime }\in {Child-Tabs}_t}{\beta }^{*}\left({\tau }_{}^{\prime }\right).$$

Moreover, we inductively define the extensions of a row $\overrightarrow{u}\in {\tau }_{}$ as

$$E\left(\overrightarrow{u}\right):=\left\{\left\{\overrightarrow{u}\right\}\cup U\mid U\in \bigcup _{\{\left\{{\overrightarrow{u}}_1^{\prime }\right\},\cdots ,\left\{{\overrightarrow{u}}_k^{\prime }\right\}\}\in {orig}_t\left(\overrightarrow{u}\right)}\{{\tau }_1\cup \cdots \cup {\tau }_k\mid {\tau }_i\in E\left({\overrightarrow{u}}_i^{\prime }\right)forall1\le i\le k\}\right\}.$$

Remark 1.

Any extension $U\in E\left(\overrightarrow{u}\right)$ contains $\overrightarrow{u}$ and exactly one row from each table that is a descendant of ${\tau }_{}$. If $\overrightarrow{u}$ is a row of a leaf table, $E\left(\overrightarrow{u}\right)=\left\{\left\{\overrightarrow{u}\right\}\right\}$ since ${orig}_t\left(\overrightarrow{u}\right)=\{\varnothing \}$ assuming ${\prod }_{i\in \varnothing }{S}_i=\left\{\left(\right)\right\}$.

Definition 7.

Let ${\tau }_n$ be the table in $\mathbb{W}-\mathrm{Tabs}$ for TD root n. We define the set $sol($$\mathbb{W}-\mathrm{Tabs}$) of solutions of $\mathbb{W}-\mathrm{Tabs}$ as $sol($$\mathbb{W}-\mathrm{Tabs}$$):=\{{\alpha }^{*}\left(U\right)\mid \overrightarrow{u}\in {\tau }_n,U\in E\left(\overrightarrow{u}\right)\}$

Definition 8.

Let ${\tau }_{}$ be a table in $\mathbb{W}-\mathrm{Tabs}$ such that ${\tau }_1^{\prime },\cdots ,{\tau }_k^{\prime }$ are the child tables ${\mathrm{Child}-\mathrm{Tabs}}_t$ and let $\overrightarrow{u},\overrightarrow{v}s.\in {\tau }_{}$. We say that $x\in X\left(\overrightarrow{u}\right)$ has been $X-$illegally introduced at $\overrightarrow{u}$ if there are $\{\left\{{\overrightarrow{u}}_1^{\prime }\right\},\cdots ,\left\{{\overrightarrow{u}}_k^{\prime }\right\}\}\in {orig}_t\left(\overrightarrow{u}\right)$ such that for some $1\le i\le k$ it holds that $x\notin X\left({\overrightarrow{u}}_i^{\prime }\right)$ while $x\in X^{*}\left({\tau }_i^{\prime }\right)$. Moreover, we say that $x\in X\left(\overrightarrow{v}\right)\setminus X\left(\overrightarrow{u}\right)$ has been $X-$illegally removed at $\overrightarrow{u}$ if there is some $U\in E\left(\overrightarrow{u}\right)$ such that $x\in X\left(U\right)$.

Definition 9.

We call a table ${\tau }_{}$ augmentable if the following conditions hold:

1. 

For all rows of the form $\langle M,\cdots ,\mathcal{C}\rangle$, we have $\mathcal{C}=\varnothing$.

2. 

For all $\overrightarrow{u},\overrightarrow{v}s.\in {\tau }_{}$ with $\overrightarrow{u}\ne \overrightarrow{v}$ it holds that $\alpha \left(\overrightarrow{u}\right)\cup \beta \left(\overrightarrow{u}\right)\ne \alpha \left(\overrightarrow{v}\right)\cup \beta \left(v\right)$.

3. 

For all $\overrightarrow{u}=\langle M,\sigma ,\cdots \rangle \in {\tau }_{}$, $\{\left\{{\overrightarrow{u}}_1^{\prime }\right\},\cdots ,\left\{{\overrightarrow{u}}_k^{\prime }\right\}\}\in {orig}_t\left(\overrightarrow{u}\right)$, $1\le i<j\le k$, $I\in E\left({\overrightarrow{u}}_i^{\prime }\right)$ and $J\in E\left({\overrightarrow{u}}_j^{\prime }\right)$ it holds that ${\alpha }^{*}\left(I\right)\cap {\alpha }^{*}\left(J\right)\subseteq M$ and ${\beta }^{*}\left(I\right)\cap {\beta }^{*}\left(J\right)\subseteq \sigma$.

4. 

No element of ${\alpha }^{*}\left({\tau }_{}\right)$ has been α-illegally introduced and no element of ${\beta }^{*}\left({\tau }_{}\right)$ has been β-illegally introduced.

5. 

No element of ${\alpha }^{*}\left({\tau }_{}\right)$ has been α-illegally removed and no element of ${\beta }^{*}\left({\tau }_{}\right)$ has been β-illegally removed.

call $\mathbb{W}-\mathrm{Tabs}$ augmentable if all its tables are augmentable.

It is easy to see that $\mathbb{MOD}-\mathrm{Tabs}$ are augmentable, that is, Algorithm 2 (${\mathtt{DP}}_{\mathbb{MOD}}(·)$) computes only augmentable tables.

Observation 3.

$\mathbb{MOD}-\mathrm{Tabs}$ are augmentable, since ${\mathtt{DP}}_{\mathbb{MOD}}(·)$ computes augmentable tables. $\mathbb{CMOD}-\mathrm{Tabs}$ are augmentable, since ${\mathtt{DP}}_{\mathbb{CMOD}}(·)$ computes augmentable tables.

The following theorem establishes that we can reduce an instance of EnumAsp (restricted to disjunctive input programs) when parameterized by semi-incidence treewidth to an instance of EnumMinSAT1 when parameterized by the treewidth of its incidence graph.

Lemma 4.

Given a disjunctive program P of semi-incidence treewidth $k=\mathit{tw}\left(S\right(P\left)\right)$. We can produce in time $\mathcal{O}(\parallel P\parallel )$ a propositional formula F such that the treewidth $k^{\prime }$ of the incidence graph $I\left(F\right)$ (he incidence graph $I\left(F\right)$ of a propositional formula F in CNF is the bipartite graph that has the variables and clauses of F as vertices and an edge $vc$ if v is a variable that occurs in c for some clause $c\in F$ [32].)T is $k^{\prime }\le 7k+2$ and the answer sets of P and subset-minimal models of $F^{*}$ are in a particular one-to-one correspondence. More precisely, M is an answer set of P if and only if $M\cup M_{\mathrm{aux}}\cup \left\{sol\right\}$ is a subset-minimal model of F where $M_{\mathrm{aux}}$ is a set of additional variables occurring in F, but not in P and variables introduced by Tseitin normalization.

Proof. 

Let P be a disjunctive program of semi-incidence treewidth $k=\mathit{tw}\left(S\right(P\left)\right)$. First, we construct a formula F consisting of a conjunction over formulas $F^{\mathrm{r}}$, $F^{\mathrm{impl}}$, $F^{\mathrm{sol}}$, $F^{\min }$ followed by Tseitin normalization of F to obtain $F^{*}$. Among the atoms (Note that we do not distinguish between atoms and propositional variables in terminology here.) of our formulas will the atoms $\mathrm{at}\left(P\right)$ of the program. Further, for each atom a such that $a\in B^{-}\left(r\right)$ for some rule $r\in P$, we introduce a fresh atom $a^{\prime }$. In the following, we denote by $Z^{\prime }$ the set $\{z^{\prime }:z\in Z\}$ for any set Z and by $B_P^{-}:={\bigcup }_{r\in P}{B}_r^{-}$. Hence, ${\left(B_P^{-}\right)}^{\prime }$ denotes a set of fresh atoms for atoms occurring in any negative body. Then, we construct the following formulas:

$$\begin{array}{cccc}\hfill F^{\mathrm{r}}\left(r\right):=& H_r\vee \neg B_r^{+}\vee {\left(B_r^{-}\right)}^{\prime }\hfill & \hfill & \mathrm{for}r\in P\hfill \end{array}$$

(1)

$$\begin{array}{cccc}\hfill F^{\mathrm{impl}}\left(a\right):=& a\to a^{\prime }\hfill & \hfill & \mathrm{for}a\in B_P^{-}\hfill \end{array}$$

(2)

$$\begin{array}{cccc}\hfill F^{\mathrm{sol}}\left(a\right):=& sol\to (a^{\prime }\to a)\hfill & \hfill & \mathrm{for}a\in B_P^{-}\hfill \end{array}$$

(3)

$$\begin{array}{ccc}\hfill F^{\min }:=& \neg sol\to \underset{a^{\prime }\in {\left(B_P^{-}\right)}^{\prime }}{\bigvee }(a^{\prime }\wedge \neg a)\hfill & \hfill \end{array}$$

(4)

$$\begin{array}{cc}\hfill F^{}:=& \underset{r\in P}{\bigwedge }{F}^{\mathrm{r}}\left(r\right)\wedge \underset{a\in B_P^{-}}{\bigwedge }{F}^{\mathrm{impl}}\left(a\right)\wedge \underset{a\in B_P^{-}}{\bigwedge }{F}^{\mathrm{sol}}\left(a\right)\wedge F^{\min }\hfill \end{array}$$

(5)

Next, we show that M is an answer set of P if and only if $M\cup {\left([M\cap B_P^{-}]\right)}^{\prime }\cup \left\{sol\right\}$ is a subset-minimal model of F.

(⇒): Let M be an answer set of P. We transform M into $Y:=M\cup {\left([M\cap B_P^{-}]\right)}^{\prime }\cup \left\{sol\right\}$. Observe that Y satisfies all subformulas of F and therefore $Y\vDash F$. It remains to show that Y is a minimal model of F. Assume towards a contradiction that Y is not a minimal model. Hence, there exists X with $X⊊Y$. We distinguish the following cases:

1.

$sol\in X$: By construction of F we have $X\vDash a^{\prime }\leftrightarrow a$ for any $a^{\prime }\in {\left(B_P^{-}\right)}^{\prime }$, which implies that $X\cap \mathrm{at}\left(P\right)\vDash P^M$. However, this contradicts our assumption that M is an answer set of P.

2.

$sol\notin X$: By construction of F there is at least one atom $a\in B_P^{-}$ with $a^{\prime }\in X$, but $a\notin X$. Consequently, $X\cap \mathrm{at}\left(P\right)\vDash P^M$. This contradicts again that M is an answer set of P.

(⇐): Given a formula F that has been constructed from a program P as given above. Then, let Y be a subset-minimal model of F such that $sol\in Y$. By construction we have for every $a^{\prime }\in Y\cap {\left(B_P^{-}\right)}^{\prime }$ that $a\in Y$. Hence, we let $M=\mathrm{at}\left(P\right)\cap Y$. Observe that M satisfies every rule $r\in P$ according to (A1) and is in consequence a model of P. It remains to show that M is indeed an answer set. Assume towards a contradiction that M is not an answer set. Then there exists a model $N⊊M$ of the reduct $P^M$. We distinguish the following cases:

1.

N is not a model of P: We construct $X:=N\cup [Y\cap {\left(B_P^{-}\right)}^{\prime }]$ and show that X is indeed a model of F. For this, for every $r\in P$ where $B^{-}\left(r\right)\cap M\ne \varnothing$ we have $X\vDash F^{\mathrm{r}}\left(r\right)$, since $(Y\cap {\left(B_P^{-}\right)}^{\prime })\subseteq X$ by definition of X. For formulas $\left(A1\right)$ constructed by $F^{\mathrm{r}}\left(r\right)$ using remaining rules r, we also have $X\vDash F^{\mathrm{r}}\left(r\right)$, since $N\vDash {\left\{r\right\}}^M$. In conclusion, $X\vDash F$ and $X⊊Y$, and therefore X contradicts Y is a subset-minimal model of F.

2.

N is also a model of P: Observe that then $X:=N\cup {[N\cap B_P^{-}]}^{\prime }\cup \left\{sol\right\}$ is also a model of F, which contradicts optimality of Y since $X⊊Y$.

By Tseitin normalization, we obtain $F^{*}$, thereby introducing fresh atoms $l_{a^{\prime }}$ for each $a^{\prime }\in {\left(B_P^{-}\right)}^{\prime }$:

$$\begin{array}{cccc}\hfill F^{\mathrm{r}*}\left(r\right):=& H_r\vee \neg B_r^{+}\vee {\left(B_r^{-}\right)}^{\prime }\hfill & \hfill & \mathrm{for}r\in P\hfill \end{array}$$

(A1)

$$\begin{array}{cccc}\hfill F^{\mathrm{impl}*}\left(a\right):=& \neg a\vee a^{\prime }\hfill & \hfill & \mathrm{for}a\in B_P^{-}\hfill \end{array}$$

(A2)

$$\begin{array}{cccc}\hfill F^{\mathrm{sol}*}\left(a\right):=& \neg sol\vee (\neg a^{\prime }\vee a)\hfill & \hfill & \mathrm{for}a\in B_P^{-}\hfill \end{array}$$

(A3)

$$\begin{array}{cc}\hfill F_1^{\min }:=& sol\vee \underset{a^{\prime }\in B_{P^{\prime }}^{-}}{\bigvee }\left(l_{a^{\prime }}\right)\hfill \end{array}$$

(A4a)

$$\begin{array}{cccc}\hfill F_2^{\min }\left(a\right):=& \neg a^{\prime }\vee a\vee l_{a^{\prime }}\hfill & \hfill & \mathrm{for}a\in B_P^{-}\hfill \end{array}$$

(A4b)

$$\begin{array}{cccc}\hfill F_3^{\min }\left(a\right):=& \neg l_{a^{\prime }}\vee a^{\prime }\hfill & \hfill & \mathrm{for}a\in B_P^{-}\hfill \end{array}$$

(A4c)

$$\begin{array}{cccc}\hfill F_4^{\min }\left(a\right):=& \neg l_{a^{\prime }}\vee \neg a\hfill & \hfill & \mathrm{for}a\in B_P^{-}\hfill \end{array}$$

(A4d)

Observe that the Tseitin normalization is correct and that there is a bijection between models of formula $F^{*}$ and formula F.

Observe that our transformations runs in linear time and that the size of $F^{*}$ is linear in $\parallel P\parallel$. It remains to argue that $tw\left(I\left(F^{*}\right)\right)\le 7k+2$. For this, assume that $\mathcal{T}=(T,\chi ,n)$ is an arbitrary but fixed TD of $S\left(P\right)$ of width w. We construct a new TD ${\mathcal{T}}^{\prime }:=(T,{\chi }^{\prime },n)$ where ${\chi }^{\prime }$ is defined as follows. For each TD node t,

$${\chi }^{\prime }\left(t\right):=\bigcup _{a\in B_P^{-}\cap \chi \left(t\right)}\{a^{\prime },l_{a^{\prime }}\}\cup [\chi \left(t\right)\cap \mathrm{at}\left(P\right)]\cup \left\{sol\right\}\cup cl\left(t\right)$$

where

$$cl\left(t\right):=\bigcup _{a\in B_P^{-}\cap \chi \left(t\right)}[F^{\mathrm{impl}*}\left(a\right),F^{\mathrm{sol}*}\left(a\right),F_2^{\min }\left(a\right),F_3^{\min }\left(a\right),F_4^{\min }\left(a\right)]\cup \left\{F_1^{\min }\right\}\cup \bigcup _{r\in P\cap \chi \left(t\right)}\left\{F^{\mathrm{r}*}\left(r\right)\right\}.$$

We can easily see that ${\mathcal{T}}^{\prime }$ is indeed a tree decomposition for $I\left(F^{*}\right)$ and that the width of ${\mathcal{T}}^{\prime }$ is at most $7w+2$. □

Definition 10.

We inductively define an augmenting function $aug(\mathbb{W}-Tabs)$ that maps each table ${\tau }_{}\in \mathbb{W}-Tabs\left[t\right]$ for node t from an augmentable table to a table in $\mathbb{W},\mathbb{W}-Tabs\left[t\right]$. Let the child tables of ${\tau }_{}$ be called ${\tau }_1^{\prime },\cdots ,{\tau }_k^{\prime }$. For any $1\le i\le k$ and $\overrightarrow{u}\in {\tau }_i$, we write $res\left(\overrightarrow{u}\right)$ to denote $\{\overrightarrow{v}s.\in aug\left({\tau }_i^{\prime }\right)\mid \alpha \left(\overrightarrow{u}\right)=\alpha \left(\overrightarrow{v}\right)\}$. We define $aug\left({\tau }_{}\right)$ as the smallest table that satisfies the following conditions:

1. 

For any $\overrightarrow{u}\in {\tau }_{}$, $\{\left\{{\overrightarrow{u}}_1^{\prime }\right\},\cdots ,\left\{{\overrightarrow{u}}_k^{\prime }\right\}\}\in {orig}_t\left(\overrightarrow{u}\right)$ and $\{\left\{{\overrightarrow{v}}_1^{\prime }\right\},\cdots ,\left\{{\overrightarrow{v}}_k^{\prime }\right\}\}\in {\widehat{\prod }}_{1\le i\le k}res\left({\overrightarrow{u}}_i^{\prime }\right)$, there is a row $\overrightarrow{v}s.\in aug\left({\tau }_{}\right)$ with $\alpha \left(\overrightarrow{u}\right)=\alpha \left(\overrightarrow{v}\right)$ and $\{\left\{{\overrightarrow{v}}_1^{\prime }\right\},\cdots ,\left\{{\overrightarrow{v}}_k^{\prime }\right\}\}\in {orig}_t\left(\overrightarrow{v}\right)$.

2. 

For any $\overrightarrow{u},\overrightarrow{v}s.\in aug\left({\tau }_{}\right)$ with $\overrightarrow{u}=\langle \cdots ,\mathcal{C}\rangle$ such that $\alpha \left(\overrightarrow{v}\right)\subseteq \alpha \left(\overrightarrow{u}\right)$, $\{\left\{{\overrightarrow{u}}_1^{\prime }\right\},\cdots ,\left\{{\overrightarrow{u}}_k^{\prime }\right\}\}\in {orig}_t\left(\overrightarrow{u}\right)$ and $\{\left\{{\overrightarrow{v}}_1^{\prime }\right\},\cdots ,\left\{{\overrightarrow{v}}_k^{\prime }\right\}\}\in {orig}_t\left(\overrightarrow{v}\right)$ the following holds: Let $1\le i\le k$ with ${\overrightarrow{u}}_i^{\prime }=\langle \cdots ,{\mathcal{C}}_i\rangle$, ${\overrightarrow{c}}_i=\langle C_i,\cdots \rangle \in ({\mathcal{C}}_i\cup \left\{{\overrightarrow{u}}_i^{\prime }\right\})$ with $C_i\subseteq \alpha \left({\overrightarrow{v}}_i^{\prime }\right)$, and $1\le j\le k$ with ${\overrightarrow{c}}_j\ne {\overrightarrow{u}}_j^{\prime }$ or $\alpha \left(\overrightarrow{v}\right)⊊\alpha \left(\overrightarrow{u}\right)$. Then, there is a row $\overrightarrow{c}\in \mathcal{C}$ with $\alpha \left(\overrightarrow{c}\right)\subseteq \alpha \left(\overrightarrow{v}\right)$ if and only if $\overrightarrow{c}\in {\tau }_{}$ and $\{\left\{{\overrightarrow{c}}_1\right\},\cdots ,\left\{{\overrightarrow{c}}_k\right\}\}\in {orig}_t\left(\overrightarrow{c}\right)$.

For $\mathbb{W}-Tabs$, we write $aug(\mathbb{W}-Tabs)$ to denote the result isomorphic to $\mathbb{W},\mathbb{W}-Tabs$ where each table ${\tau }_{}$ in $\mathbb{W}-Tabs$ corresponds to $aug\left({\tau }_{}\right)$.

Proposition 2.

Let $\mathbb{W}-Tabs$ be augmentable. Then,

$$sol(aug(\mathbb{W}-Tabs))=\{M\in sol(\mathbb{W}-Tabs)\mid \nexists M^{\prime }\in sol(\mathbb{W}-Tabs):M^{\prime }⊊M\}.$$

Proof (Sketch).

The proof follows previous work [17]. We sketch only differences from their work. Any row $\overrightarrow{u}\in {\tau }_{}$ of any table ${\tau }_{}$ not only consists of set $\alpha \left(\overrightarrow{u}\right)$ being subject to subset-minimization and relevant to solving EnumAsp. In addition, our definitions presented above also allow “auxiliary” sets $\beta \left(\overrightarrow{u}\right)$ per row $\overrightarrow{u}$, which are not subject to the minimization. Moreover, by the correctness of the table algorithm $\mathbb{SINC}$ above, we only require to store a set $\mathcal{C}$ of counter-witnesses $\langle C,\cdots \rangle \in \mathcal{C}$ per witness set M, where each C forms a strictly ⊂-smaller model of M. As a consequence, there is no need to differ between sets of counter-witnesses, which are strictly included or not, see [17]. Finally, we do not need to care about duplicate rows (solved via compression function $compr(·)$ in [17]) in ${\tau }_{}$, since ${\tau }_{}$ is a set. □

Theorem 2.

EnumAspwhen the input is restricted to disjunctive programs can be solved in time $2^{2^{(7k+4)}}·\parallel P\parallel$ computing $aug\left({\mathtt{DP}}_{\mathbb{MOD}}(·)\right)$, where k refers to the treewidth of $S\left(P\right)$.

Proof. 

First, we use reduction $R(P,k)=(F^{*},k^{\prime })$ defined in Lemma 4 to construct an instance of SAT given our disjunctive ASP program P. Note that $k^{\prime }=tw\left(I\left(F^{*}\right)\right)\le 7k+2$. Then, we can compute in time $2^{\mathcal{O}\left(k^{\prime 3}\right)}·\left|I\left(F^{*}\right)\right|$ a tree decomposition of width at most $k^{\prime }$ [26]. Note that since we require to look for solutions containing $sol$ at the root, we modify each bag of $\mathcal{T}$ such that it contains $sol$. We call the resulting tree decomposition ${\mathcal{T}}^{\prime }$. We compute $aug\left({\mathtt{DP}}_{\mathbb{MOD}}\left({\mathcal{T}}^{\prime }\right)\right)$ using formula $F^{*}$ as in Algorithm 2. Finally, by Proposition 2 and Lemma 4, we conclude that answer sets of P correspond to $\{M\in sol(aug\left({\mathtt{DP}}_{\mathbb{MOD}}\left({\mathcal{T}}^{\prime }\right)\right))\mid sol\in M,\nexists M^{\prime }\in sol\left({\mathtt{DP}}_{\mathbb{MOD}}\left({\mathcal{T}}^{\prime }\right)\right):M^{\prime }⊊M\}$.

The complexity proof sketched in work by Bliem et al. [17] only cares about the runtime being polynomial. In fact, the algorithm can be carried out in linear time, following arguments from above, which leads to a worst-case runtime of $2^{2^{(7k+4)}}·\parallel P\parallel$. □

We can now even provide a “constructive definition” of the augmenting function $aug(·)$.

Proposition 3.

The resulting table $aug(\mathbb{W}-\mathrm{Tabs})$ obtained via ${\mathtt{DP}}_{\mathbb{W}}\left(\mathcal{T}\right)$ for any TD $\mathcal{T}$ is equivalent to the table ${\mathtt{DPL}}_{\mathbb{W},\mathbb{W}}\left(\mathcal{T}\right)$ as given in Algorithm 3.

Proof (Idea).

Intuitively, Condition 1 of Definition 10 concerns completeness, i.e., ensures that no row is left out during the augmentation, and is ensured by Line 7 of Algorithm 3 since each $\overrightarrow{u}\in \mathbb{W}-\mathrm{Tabs}$ is preserved. Condition 2 enforces that there is no missing counter-witness for any witness, and the idea is that whenever two witnesses $\overrightarrow{u},\overrightarrow{v}s.\in {\tau }_{}$ are in a subset relation ($\alpha \left(\overrightarrow{v}\right)\subseteq \alpha \left(\overrightarrow{u}\right)$) and their corresponding linked counter-witnesses ($f_{cw}$) of the corresponding origins (orig) are in a strict subset relation, then there is some counter-witness c for u if and only if $\overrightarrow{c}\in {\tau }_{}$ is the successor (evol) of these corresponding linked counter-witnesses. Intuitively, we cannot miss any counter-witnesses in ${\mathtt{DPL}}_{\mathbb{W},\mathbb{W}}\left(\mathcal{T}\right)$ required by Condition 2, since this required that there are two rows ${\overrightarrow{u}}^{\prime },{\overrightarrow{v}}^{\prime }\in {\tau }_{}^{\prime }$ with $\alpha \left(\overrightarrow{v}\right)=\alpha \left(\overrightarrow{u}\right)$ for one table ${\tau }_{}^{\prime }$. Now, let the corresponding succeeding rows $\overrightarrow{u},\overrightarrow{v}\in {\tau }_{}$ (i.e., $\overrightarrow{u}\in {evol}_t\left(\left\{\left\{{\overrightarrow{u}}^{\prime }\right\}\right\}\right),\overrightarrow{v}\in {evol}_t\left(\left\{\left\{{\overrightarrow{v}}^{\prime }\right\}\right\}\right)$, respectively) with $\alpha \left(\overrightarrow{v}\right)⊊\alpha \left(\overrightarrow{u}\right)$, $\beta \left(\overrightarrow{v}\right)⊈\beta \left(\overrightarrow{u}\right)$ and $\beta \left(\overrightarrow{v}\right)⊉\beta \left(\overrightarrow{u}\right)$, mark the first encounter of a missing counter-witness. Since $\beta \left(\overrightarrow{v}\right)$ is incomparable to $\beta \left(\overrightarrow{u}\right)$, we conclude that the first encounter has to be in a table preceding ${\tau }_{}$. To conclude, one can show that ${\mathtt{DPL}}_{\mathbb{W},\mathbb{W}}\left(\mathcal{T}\right)$ does not contain “too many” rows, which do not fall under Conditions 1 and 2. □

Theorem 2 works not only for disjunctive ASP via reduction to EnumMinSAT1, where witnesses and counter-witnesses are derived with the same table algorithm $\mathbb{MOD}$. In fact, one can also link counter-witnesses to witnesses by means of ${\mathtt{DPL}}_{\mathbb{W},\mathbb{C}}(·)$, thereby using table algorithms $\mathbb{W},\mathbb{C}$ for computing witnesses and counter-witnesses, respectively. In order to show correctness of algorithm ${\mathtt{DPL}}_{\mathbb{MOD},\mathbb{CMOD}}(·)$ (Theorem 1) working for any ASP program, it is required to extend the definition of the augmenting function $aug(·)$ such that it is capable of using two different tables.

Corollary 1.

ProblemEnumAspcan be solved in time $f\left(k\right)·\parallel P\parallel$ computing ${\mathtt{DPL}}_{\mathbb{MOD},\mathbb{CMOD}}(·)$, where k refers to the treewidth of $S\left(P\right)$ and f is a computable function.

5. Experimental Evaluation

5.1. Implementation Details

Efficient implementations of dynamic programming algorithms on TDs are not a by-product of computational complexity theory and involve tuning and sophisticated algorithm engineering. Therefore, we present additional implementation details of algorithm $\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$ into our prototypical multi-traversal solver DynASP2.5, including two variations (depgraph, joinsize TDs).

Even though one can construct a nice TD from a TD without increasing its width, one may artificially introduce additional atoms in a nice TD. This results in several additional intermediate join nodes among such artificially introduced atoms requiring a significant amount of total unnecessary computation in practice. On that account, we use tree decompositions that do not have to be nice. In order to still obtain a fixed-parameter linear algorithm, we limit the number of children per node to a constant. Moreover, linking counter-witnesses to witnesses efficiently is crucial. The main challenge is to deal with situations where a row (witness) might be linked to different set of counter-witnesses depending on different predecessors of the row (hidden in set notation of the last line in Algorithm 3). In these cases, DynASP2.5 eagerly creates a “clone” in form of a very light-weighted proxy to the original row and ensures that only the original row (if at all required) serves as counter-witness during traversal three. Together with efficient caches of counter-witnesses, DynASP2.5 reduces overhead due to clones in practice.

Dedicated data structures are vital. Sets of witnesses and satisfied rules are represented in the DynASP2.5 system via constant-size bit vectors. 32-bit integers are used to represent by value 1 whether an atom is set to true or a rule is satisfied in the respective bit positions according to the bag. A restriction to 32-bit integers seems reasonable as we assume for now (practical memory limitations) that our approach works well on TDs of width $\le 20$. Since state-of-the-art computers handle such constant-sized integers extremely efficient, DynASP2.5 allows for efficient projections and joins of rows, and subset checks in general. In order to not recompute counter-witnesses (in Traversal 3.II) for different witnesses, we use a three-valued notation of counter-witness sets consisting of atoms set to true (T) or false (F) or false but true in the witness set (TW) used to build the reduct. Note that the algorithm enforces that only (TW)-atoms are relevant, i.e., an atom has to occur in a default negation or choice rule.

Minimum width is not the only optimization goal when computing TDs by means of heuristics. Instead, using TDs where a certain feature value has been maximized in addition (customized TDs) works seemingly well in practice [12,33]. While DynASP2.5 ($\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$) does not take additional TD features into account, we also implemented a variant (DynASP2.5 depgraph), which prefers one out of ten TDs that intuitively speaking avoids to introduce head atoms of some rule r in node t, without having encountered every body atom of r below t, similar to atom dependencies in the program [34]. The variant DynASP2.5 joinsize minimizes bag sizes of child nodes of join nodes, c.f. [18].

5.2. Benchmark Set

In the following empirical evaluation, we consider the uniform Steiner tree problem (St), which is a variant of a decision problem among the first well-known $\mathrm{NP}$-hard problems [35]. We take public transport networks as input graphs. The instance graphs have been extracted from publicly available mass transit data feeds and split by transportation type, e.g., train, metro, tram, combinations [36]. We heuristically computed tree decompositions [18] and obtained decompositions of small width relatively fast unless detailed bus networks were present. Among the graphs considered were public transit networks of the cities London, Bangladesh, Timisoara, and Paris. Benchmarks, encodings, and results are available online at https://github.com/daajoe/dynasp_experiments/tree/ipec2017. We assumed for simplicity, that edges have unit costs, and randomly generated a set of terminals.

5.2.1. Steiner Tree Problem

The considered version of the uniform Steiner tree problem can be formalized as follows:

Definition 11

(Uniform Steiner Tree Problem (St)). Let $G=(V,E)$ be a graph and $V_T\subseteq V$ be a set of vertices, called terminal vertices. Then, a uniform Steiner tree on G is a tree $S_G=(V_S,E_S)$ with $V_S\subseteq V$ and $E_S\subseteq E$ such that

1. 

all terminal vertices are covered : $V_T\subseteq V_S$, and

2. 

the number of edges in $E_S$ forms a minimum : there is no tree, where all terminal vertices are covered that consists of no more than $|E_S|-1$ many edges.

The uniform Steiner tree problem (St) asks to compute the uniform Steiner trees for G and $V_T$.

Example 6

(Encoding St into an ASP program). Let $G=(V,E)$ be a graph and $V_T\subseteq V$ be a set of terminal vertices. We encode the problem St into an ASP program as follows: Among the atoms of our program will be an atom $a_v$ for each vertex $v\in V_T$, and an atom $e_{vw}$ for each edge $vw\in E$ assuming $v<w$ for an arbitrary, but fixed total ordering < among V. Let s be an arbitrary vertex $s\in V_T$. We generate program $P(G,V_T):=\{\left\{e_{vw}\right\}\leftarrow ;$ $e_{vw}\mid vw\in E\}\cup \{a_v\leftarrow a_w,e_{vw};a_w\leftarrow a_v,e_{vw}\mid vw\in E,vs.<w\}\cup \{\leftarrow \neg a_v\mid vs.\in V_T\}\cup \{a_s\leftarrow \}$. It is easy to see that the answer sets of the program and the uniform Steiner trees are in a one-to-one correspondence.

5.2.2. Considered Encodings

We provide the encoding as non-ground ASP program, which allows to state first-order variables that are instantiated by present constants. This allows us to provide a readable encoding and avoid stating an encoder as an imperative program. Note that for certain non-ground programs, treewidth guarantees are known [37]. In the experiment, we used gringo [38] as grounder. An encoding for the problem St is depicted in Listing 1 and assumes a specification of the graph (via edge) and the terminal vertices (terminalVertex) as well as the number (numVertices) of vertices. Note that this encoding is quite compact and non-ground and therefore it contains first-order variables. Prior to solving, these first-order variables are instantiated by a grounder, which results in a ground program. Interestingly, the encoding in Listing 1 is based on the saturation technique [3] and in fact outperformed a different encoding presented in Listing 2 on all our instances using both solvers, Clasp and DynASP2.5. At first sight, this observation seems quite surprising, however, we benchmarked on more than 60 graphs with 10 varying decompositions for each solver variant and additional configurations and different encodings for Clasp.

Listing 1. Encoding for St.

vertex(X) ← edge(X,_).
vertex(Y) ← edge(_,Y).
edge(X,Y) ← edge(Y,X).
  
0 { selectedEdge(X,Y) } 1 ← edge(X,Y), X < Y.
  
s1(X) ∨ s2(X) ← vertex(X).
  
saturate ← selectedEdge(X,Y), s1(X), s2(Y), X < Y.
saturate ← selectedEdge(X,Y), s2(X), s1(Y), X < Y.
  
saturate ← N #count{ X : s1(X), terminalVertex(X) }, numVertices(N).
saturate ← N #count{ X : s2(X), terminalVertex(X) }, numVertices(N).
  
s1(X) ← saturate, vertex(X).
s2(X) ← saturate, vertex(X).
← not saturate.
   
#minimize{ 1,X,Y : selectedEdge(X,Y) }.
            

Listing 2. Alternative encoding for St.

edge(X,Y) ← edge(Y,X).
  
{ selectedEdge(X,Y) : edge(X,Y), X < Y }.
  
reached(Y) ← Y = #min{ X : terminalVertex(X) }.
reached(Y) ← reached(X), selectedEdge(X,Y).
reached(Y) ← reached(X), selectedEdge(Y,X).
  
← terminalVertex(X), not reached(X).
  
#minimize{ 1,X,Y : selectedEdge(X,Y) }.
            

5.3. Experimental Evaluation

We performed experiments to investigate the runtime behavior of DynASP2.5 and its variants, in order to evaluate whether our multi-traversal approach can be beneficial and has practical advantages over the classical single traversal approach (DynASP2). Further, we considered the dedicated ASP solver Clasp 3.3.0 (Clasp is available at https://github.com/potassco/clasp/releases/tag/v3.3.0.). Clearly, we cannot hope to solve programs with graph representations of high treewidth. However, programs involving real-world graphs such as graph problems on transit graphs admit TDs of acceptable width to perform DP on TDs. To get a first intuition, we focused on the Steiner tree problem (St) for our benchmarks. Note that we support the most frequently used SModels input format [39] for our implementation. For our experiments, we used gringo [38] for both Clasp and DynASP2.5 and therefore do not compare the time needed for grounding, since it is exactly the same for both solvers.

5.3.1. Benchmark Environment

The experiments presented ran on an Ubuntu 16.04.1 LTS Linux cluster of 3 nodes with two Intel Xeon E5-2650 CPUs of 12 physical cores each at 2.2 GHz clock speed and 256 GB RAM. All solvers have been compiled with GCC version 4.9.3 and executed in single core mode.

5.3.2. Runtime Limits

We mainly inspected the CPU time using the average over five runs per instance (five fixed seeds allow certain variance for heuristic TD computation). For each run, we limited the environment to 16 GB RAM and 1200 s CPU time. We used Clasp with options “--stats=2 --opt-strategy=usc,pmres,disjoint,stratify --opt-usc-shrink=min -q”, which enable improvements for unsatisfiable cores [40], and disabled solution printing/recording. We also benchmarked Clasp with branch-and-bound, which was, however, outperformed by the unsatisfiable core options on all our instances. In fact, without using unsatisfiable core advances, Clasp timed out on almost every instance.

5.3.3. Summary of the Results

The upper plot in Figure 6 shows the result of always selecting the best among five TDs, whereas the lower plot concerns about the median runtime among those runs.

The upper table of

Table 1. The table illustrates detailed benchmark results, where data for the best possible among all five runs is depicted (top) and results for the median run are shown (bottom). All columns illustrate values in seconds, except the first two columns. Column “Solver” indicates a solving system or configuration and “Solved” refers to the number of solved instances. Then, columns “TD”, “3.I”, “3.II”, and “3.III” list the total runtime in seconds over all solved instances for computation involving obtaining TDs, Pass 3.I, Pass 3.II, and Pass 3.III, respectively. Column “$\Sigma$” refers to the total runtime in seconds over all solved instances. The last column depicts the PAR2 score over all instances, where timeouts are treated as two times the timeout (“PAR2 score”). Bold-face text indicates the best result in the corresponding column.

Solver	Solved	Runtimes (Best) among Solved Instances					PAR2 Score
		TD	3.I	3.II	3.III	$\mathsf{\Sigma }$
Clasp 3.3.0	35	-	-	-	-	11,493.98	93,093.98
DynASP2	13	7.96 (0.2%)	-	-	-	3978.29	138,378.29
DynASP2.5	41	21.68 (0.2%)	130.10 (1.4%)	585.47 (6.2%)	8656.48 (92.2%)	9393.73	76,496.74
“depgraph”	45	408.72 (4.0%)	138.21 (1.4%)	595.58 (5.8%)	9033.70 (88.8%)	10,176.21	67,667.71
“joinsize”	37	22.82 (0.3%)	120.19 (1.3%)	544.18 (6.1%)	8250.16 (92.3%)	8937.35	85,654.00
Solver	Solved	Runtimes (median) among solved instances					PAR2 Score
		TD	3.I	3.II	3.III	$\Sigma$
Clasp 3.3.0	34	-	-	-	-	11,688.58	94,523.53
DynASP2	8	8.74 (0.2%)	-	-	-	4370.83	149,289.20
DynASP2.5	32	21.91 (0.2%)	140.08 (1.3%)	685.15 (6.4%)	9878.67 (92.1%)	10,725.81	96,405.37
“depgraph”	38	473.12 (4.1%)	146.33 (1.3%)	661.00 (5.8%)	10,118.22 (88.8%)	11,398.67	81,425.39
“joinsize”	32	25.47 (0.2%)	129.41 (1.3%)	596.62 (5.8%)	9538.77 (92.7%)	10,290.27	97,260.77

reports on the minimum running times (TD computation and Traversals 3.I, 3.II, 3.III) among the solved instances and the total PAR2 scores. We consider an instance as solved, if the minimum and median PAR2 score is below the timeout of 1200 s. The lower table of Table 1 depicts the median running times over solved instances and the total median PAR2 scores. For the variants depgraph and joinsize, runtimes for computing and selecting among ten TDs are included. Our empirical benchmark results confirm that DynASP2.5 exhibits competitive runtime behavior even for TDs of treewidth around 14. Compared to state-of-the-art ASP solver Clasp, DynASP2.5 is capable of additionally delivering the number of optimal solutions. In particular, variant “depgraph” shows promising runtimes.

5.4. A Brief Remark on Instances without Optimization

Our algorithm ($\mathtt{M}-{\mathtt{DP}}_{\mathbb{SINC}}$) is a multi-variate algorithm. The idea of avoiding to construct counter-witnesses focuses on situations were many models will be removed in the first traversal. This happens when (i) we have instances with only few models or (ii) we have optimization statements in our instances (minimizing cardinality of answer sets with respect to certain literals). The section above confirmed this expectation on Steiner tree instances. Technically, one might ask whether DynASP2.5 also improves over its predecessor when solving common graph problems that do not include optimization on the solution size such as variants of graph coloring, dominating set, and vertex cover. Clearly, the theoretical expectation would be that a multiple traversal algorithm (DynASP2.5) would not benefit much over a single traversal algorithm (DynASP2). This is indeed the case on graph problems. However, we omit details as it is not the focus of this paper and refer to a technical report [41] for benchmarks into this direction. There, DynASP2.5 was not able to significantly improve the running time required for problem solving, i.e., the additional overhead due to multiple traversals of DynASP2.5 did not pay off. One might ask a similar question for a comparison between Clasp and DynASP2.5. When taking Cases (i) and (ii) from above into account, we would expect the following. If we have few instances, Clasp does not have to run many steps with standard optimization strategies, which use branch-and-bound or unsatisfiable-based optimization running in multiple rounds of CDCL-search. If we have no optimization, Clasp will run only one round of CDCL-search and hence runs much faster than with optimization.

6. Conclusions

In this paper, we presented a novel approach for ASP solving based on ideas from parameterized complexity. Our algorithms runs in linear time assuming bounded treewidth of the input program. Our solver applies DP in three traversals, thereby avoiding redundancies. Experimental results indicate that our ASP solver is competitive for certain classes of instances with small treewidth, where the latest version of the well-known solver Clasp hardly keeps up.

An interesting question for future research is whether a linear amount of traversals (incremental dynamic programming) can improve the runtime behavior. It might also be worth investigating if more general parameters than treewidth can be used [42]. Furthermore, it might be interesting to apply high level approaches on dynamic programming that include the use of existing technology to answer set programming [43,44] or whether such an approach pays off for other domains such as default logic [45], argumentation [46], or description logics [47].