Epistemic logic programs (ELPs) [24], also referred to as the language of Epistemic Specifications [20], have received renewed attention in the research community as of late. ELPs are an extension of the language of Answer Set Programming (ASP) [6, 35] with epistemic operators. Gelfond (1991) introduced the operators K and M in order to represent the concepts of known to be true and may be true, and defined an initial semantics. Several improvements to the semantics have since been proposed in the literature [12, 21, 28, 38]. Shen and Eiter (2016) realized that these two operators can be represented via a single negation-type operator that they called epistemic negation, denoted not , and gave a new semantics based on this operator. Morak (2019) proposed a novel characterization of the central construct of the ELP semantics: the world view. While a recent analysis [7] has shown that this semantics still does not eliminate all existing flaws, we will make use of it in this paper, since no clear “winner” semantics has as of yet emerged, and our approach should be equally applicable to other existing semantics that have been proposed.

Evaluating ELPs is a computationally hard task. The central decision problem, checking whether an ELP has a world view, is -complete, and problems even higher on the polynomial hierarchy exist [32, 36]. In order to deal with this high complexity efficiently, we propose to use a method from the field of parameterized complexity, namely, investigate how the runtime behaves when looking at different structural parameters of the problem. For standard ASP, this topic has received considerable interest, [3, 13, 14, 18, 25, 31]. However, the parameterized complexity of epistemic ASP has remained largely unexplored so far. From the ASP case, we see strong evidence that this will be the case for ELPs as well. In this paper, we will investigate, in particular, whether ELPs can be solved efficiently if their treewidth (i.e., a measure for the tree-likeness of graphs) is bounded.

It turns out that this question can be answered in the affirmative: the main decision problems become tractable. In practice, a dynamic programming algorithm on tree decompositions can be used to exploit this directly, similarly to what was successfully proposed for ASP and QBF solvers [4, 8, 15, 17]. However, we also aim to investigate a more interesting angle. Many ELP solvers today work by making (up to exponentially many) calls to an underlying ASP solving system in order to check world view existence. Being able to find a bound on the number of these ASP solver calls would be very useful. Using so-called epistemic (primal) graphs of ELPs that focus on epistemically negated literals only, we can again employ treewidth to establish such bounds. This novel use of structural decomposition intuitively works well in some interesting cases including instances of the scholarship eligibility (SE)1 benchmark set, as provided with the system “EP-ASP” [37].

Using the epistemic primal graph representation, these instances naturally decompose into their individual subproblems, that is, one sub-instance of the SE problem for each student within the original instance.

Contributions. Our contributions are summarized below:

• We investigate the complexity of the ELP world view existence problem when parameterized by the treewidth of the ELP instance. We establish that this problem is fixed-parameter tractable in this setting, and, in fact, can be solved in linear time if the treewidth is bounded from above by a constant. The same holds for the even more complex problem of world view formula evaluation.

• Then, we propose a novel graph representation of ELPs, namely, the epistemic primal graph and show how this can be exploited to bound the number of calls to an underlying ASP solver in a classical ELP solver setting. It turns out that the number of calls is bounded in case the epistemic primal graph has bounded treewidth.

• Finally, we provide a full dynamic programming algorithm that could be used in practice to directly exploit the tractability result above. We also show that the worst-case runtime of this algoritm cannot be significantly improved under reasonable complexity-theoretic assumptions.

Answer Set Programming (ASP). A ground logic program with nested negation (also called answer set program, ASP program, or, simply, logic program) is a pair P = (A, R), where A is a set of propositional (i.e., ground) atoms and R is a set of rules of the form , where the comma symbol stands for conjunction, for all , and each is a literal, that is, either an atom a or its (default) negation for any atom .2 Note that, therefore, doubly negated atoms may occur. We will sometimes refer to such rules as standard rules. Each rule consists of a head and a body , and is alternatively denoted by . The positive body is given by . Sometimes, we add a set of rules to a logic program P = (A, R). By some abuse of notation, let denote the logic program , where is the set of atoms occurring in the rules of .

An interpretation I (over A) is a set of atoms, that is, . A literal is true in an interpretation , denoted , iff and , or and ; otherwise is false in I, denoted . Finally, for some literal , we define that if . This notation naturally extends to sets of literals. An interpretation M is called a model of r, denoted , if, whenever , it holds that . We denote the set of models of r by mods(r); the models of a logic program P = (A, R) are given by . We also write (resp. ) if (resp. ).

The GL-reduct of a logic program P = (A, R) with respect to an interpretation I is given by with .

Definition 1 ([22, 23, 30]). is an answer set of a logic program P if (1) and (2) there is no subset such that .

The set of answer sets of a logic program P is denoted by AS(P). The consistency problem of ASP, that is, to decide whether for a given logic program P it holds that , is -complete [11], and remains so also in the case where doubly negated atoms are allowed in rule bodies [33].

Epistemic Logic Programs. An epistemic literal is a formula , where is a literal and not is the epistemic negation operator. A ground epistemic logic program (ELP) is a pair , where A is a set of atoms and R is a set of ELP rules, which are implications of the form , where each is an atom from A, each is a literal over A, and each is an epistemic literal of the form , where is a literal over A. Similarly to logic programs, let , and let B(r) = . Further, denotes the set of atoms ocurring in ELP rule r, and denotes the set of atoms used in epistemic literals of r. These notions naturally extend to sets of rules.

In order to define the semantics of an ELP, we will use the approach by Morak [32], which follows the semantics defined in [36], but uses a different formal representation. Note that, however, our results can be adapted to other “reduct-based” semantics, by changing the definition of the reduct appropriately. Given an ELP , a candidate world interpretation (CWI) I for is a consistent subset , where L is the set of all literals that can be built from atoms in A. Note that a CWI I naturally gives rise to a three-valued truth assignment to all the atoms in A; hence, we will sometimes treat a CWI I as a triple of disjoint sets , where , and , with the intended meaning that atoms in , , and are “always true,” “always false,” and “unknown,” respectively.

With the above definition in mind, we now define when a CWI is compatible with a given set of interpretations.

Definition 2. Let I be a set of interpretations over a set of atoms A. Then, a CWI I is compatible with I iff we have:

1. I ̸= ∅;

2. for each atom , it holds that for each ;

3. for each atom , we have for each ;

4. for each atom , it holds that there are , such that , but .

The epistemic reduct [32, 36] of program w.r.t. a CWI I, denoted , is defined as where denotes rule r where each epistemic literal is replaced by if , and by otherwise. Note that, hence, is a plain logic program with all occurrences of epistemic negation removed.3

Now, a CWI I is a candidate world view (CWV) of iff I is compatible with the set of answer sets. The set of CWVs of an ELP is denoted . Following the principle of knowledge minimization, furthermore I is a world view (WV) iff it is a CWV and there is no proper subset such that . The set of WVs of an ELP is denoted .

One of the main reasoning tasks regarding ELPs is the world view existence problem, that is, given an ELP , decide whether (or, equivalently, whether ). This problem is known to be -complete [32, 36]. Another interesting reasoning task is deciding, given an ELP and an arbitrary propositional formula over A, whether holds in some WV, that is, whether there exists such that . This formula evaluation problem is even harder, namely -complete [36].

Tree Decompositions and Treewidth. We assume that graphs are undirected, simple, and free of self-loops. Let G = (V, E) be a graph, T a rooted tree, and a labeling function that maps every node t of T to a subset called the bag of t. The pair is called a tree decomposition (TD) [34] of G iff (i) for each , there exists a t in T, such that ; (ii) for each , there exists t in T, such that ; and (iii) for each r, s, t of T, such that s lies on the unique path from r to t, we have . For a node t

In order to exploit the structural information, we need to define how logical structures can be represented as graphs, and how their treewidth is then defined: Given a structure A over some logical signature of arity at most two (sufficent for us), we say that the treewidth of A equals , where is a graph with V = dom(A) and edge iff , where r is some relation in .

MSO formulas over structures of bounded treewidth are important in the context of parameterized complexity in order to establish running time bounds, as the following landmark theorem by Courcelle shows:

Theorem 3 ([9]). Let be a fixed MSO formula over signature and let A be a -structure with , for some integer k. Then, evaluating over A can be done in time , for some function f not depending on |A|.

Problems with a parameter k that can be solved in time , where c is a constant and f only depends on k, are called fixed-parameter tractable (FPT) [10].

The main objective in this section is to investigate how the semantics of ELPs can be encoded in terms of an MSO formula and thereby investigate, from a theoretical perspective, the time complexity of evaluating ELPs, specifically looking at tree-like instances.

Now, our goal will be to offer a fixed MSO encoding to exploit Theorem 3, in the spirit of [25], which is able to solve the world view existence problem for an ELP by evaluating it over a suitable logical structure representing the ELP. In order to begin the construction of this, we first need to fix the signature over which our MSO encoding will be expressed. To this end, let signature

atom, rule

where atom(a) and rule(r) represent the fact that domain elements a and r are an atom and a rule, respectively; where h(a, r) represents that atom a appears in the head of rule r; and where , with and the empty word, represents that fact that the sub-formula , for atom a, appears in the body of rule r. Next we construct the encoding.

Lemma 4. Consider the signature above. WV existence can be expressed by means of a fixed MSO formula over .

Proof. Recall that, in order to check the existence of a WV, it suffices to check the existence of a CWV (since WVs are simply subset-minimal CWVs). We will construct an MSO formula cwv(P, N, U) with the intended meaning that it evaluates to true iff the input set variables P, N, and U represent a CWV W with , and . To this end, our formula will be of the following form:

where cwi ensures that P, N, and U indeed encode a valid CWI (i.e., a three-partition of the set of atoms stored in atom), and verifies that Condition i of Definition 2 holds. We will now give the construction of these checks. First, the check for a valid CWI is expressed as follows:

The four remaining checks have a similar structure:

The four checks encode precisely the conditions of Definition 2, where as(X, P, N, U) is a sub-formula, to be defined below, that expresses that X is an answer set of the epistemic reduct w.r.t. the CWI represented by the sets P, N, and U. For example, encodes that for each atom X that is set to “always false” in the CWI (i.e., ), it must hold that for every stable model X of the epistemic reduct, X must not be true in that stable model (i.e., ).

It now remains to define the sub-formula for checking answer sets. This construction is based on the one presented in [25, Theorem 3.5], but adapted to take the computation of the epistemic reduct into account. Firstly, a set of atoms M is an answer set if it is a model and no proper subset of M is a model of the GL-reduct w.r.t. M. This is expressed as follows (note that any model M is also a model of its GL-reduct):

The intuitive meaning of gl(X, Y, P, N, U) is that it should hold iff Y is a model of the GL-reduct w.r.t. X of the epistemic reduct w.r.t. the CWI represented by P, N, and U:

Note that the definition of the gl-relation is such that it precisely mirrors the definition of both the epistemic reduct and the GL-reduct. It amounts to checking that every rule in the GL-reduct is satisfied, and amounts to a large case distinction, dealing with all seven cases of how atoms can appear in a rule (that is, either in the head, or nested under six combinations of default and epistemic negation in the body). For example, in line three, the first disjunct says that rule R is satisfied if there is an atom Z in the positive body, but this atom is not present in the reduct model Y (satisfying rule R by not satisfying the body). Line four treats the case of an epistemically negated atom Z in the body. Such a rule is satisfied iff Z is set to “always true” in the CWI (since otherwise the epistemic literal is replaced by in the epistemic reduct, and the rule cannot be satisfied solely by this body element in this case), and

Z is false in the original model X (since in the epistemic reduct, the epistemic negation turns into default negation in this case, and default-negated atoms are evaluated over the original model X). This completes our MSO encoding. Correctness follows by construction, as explained above. In order to solve the WV existence problem via this encoding, we simply have to quantify the relevant set variables:

Evaluating this formula over a -structure P that represents an ELP , we get that has a CWV iff .

With the above reduction in mind, lets take a closer look at what worst-case solving time guarantees we can give for solving ELPs, in particular w.r.t. structural properties. Let be an ELP, and let P be the -structure that represents it. Recall that . In our case, coincides with the so-called incidence graph of the ELP , a graph representation that is well-known and studied in the literature for a wide range of logic-based formalisms, and, in particular, for ASP [15, 27]. The incidence graph of an ELP is the graph G = (V, E) with and iff atom occurs in rule in . It is not difficult to verify that the -structure P, when represented as a graph, mirrors the incidence graph of precisely. From this correspondence, Theorem 3, and Lemma 4, we thus obtain the following, fundamental parameterized complexity result:

Theorem 5. Let be an ELP, let G be its incidence graph, and let , for some integer k. Then, checking whether can be done in time , for some function f that does not depend on .

Using a simple extension of the MSO construction in the proof of Lemma 4, we can state a similar result for the formula evaluation problem. The MSO formula

checks whether there is at least one WV that satisfies formula , where the atom encodes the check that the WV represented by P, N, and U cautiously entails formula , a straightforward model-checking construction left to the interested reader. We obtain the following by the same argument as the one for Theorem 5:

Theorem 6. Let , and k be as in Theorem 5, and let be a propositional formula. Then, checking whether has a WV that cautiously entails can be done in time , for some function f that does not depend on .

From the above theorems we immediately obtain the fact that ELPs of bounded treewidth can be solved in linear time in the size of the ELP. We will investigate how to exploit this result and pinpoint function f(k) in the next two sections.

Before providing a concrete algorithm for the FPT result in Theorem 5 we will investigate a more abstract approach. Many ELP solvers today make use of standard ASP solvers to check the compatibility of a CWI with the set of answer sets of its epistemic reduct. However, the number of calls to such an ASP solver can be at worst exponential. In this section, we will propose an algorithm that makes use of the structural relationships between the epistemic literals in an ELP in order to control the number of ASP solver calls needed and give finer-grained worst-case bounds on this number. In the next section, we will then extend these concepts to a full dynamic programming algorithm that exploits the result in Theorem 5.

We first need to define the structural relationship between atoms occurring in epistemic literals in an ELP. To this end, let be an ELP. Then, the primal graph of is a graph with V = A and iff atoms a and b with appear together in a rule in R, that is, iff . Two vertices a, b in the primal graph are non-epistemically connected iff there is a path with in , such that each vertex , belongs to the set . Now, the epistemic primal graph of is a graph with the vertex set being the set of atoms appearing in epistemic literals in , and an edge iff and vertices a, b are non-epistemically connected in . Intuitively, two atoms from form an edge in iff they are connected in via atoms that do not appear in epistemic literals. The concept of epistemic primal graph is inspired by the notion of the torso graph [19], which is used in parameterized complexity to decompose certain abstraction graphs.

Example 7. Consider the classic scholarship eligibility problem encoding, first investigated by Gelfond [20]: .

Now, assume the above abstract (non-ground) program is instantiated with two students (assume that it is copied twice and mike and mark are substituted for X ), and that we add the following rules, resulting in ELP :

Epistemic primal graph contains only four nodes: eligible(mike), ineligible(mike), and the same two for mark. Further, does not have any edges except an edge between the two mike-atoms, and the same for mark. Since forms a forest, the treewidth of is 1.

While the epistemic primal graph does not directly provide new complexity results, it will allow us to give firm guarantees on the number of ASP solver calls needed. As a side-effect, this algorithm is conceptually simpler than the one of the next section, but prepares ideas for later.

Algorithms that solve problems of bounded treewidth typically proceed by dynamic programming (DP), bottomup, along a TD where at each node t of the TD information is gathered [5] in a table . A table is a set of rows, where a row in is a fixed-length sequence of elements. Tables are derived by an algorithm executed in each bag, called bag algorithm, which determine the actual content and meaning of the rows. Then, the DP approach for an epistemic logic program and a given bag algorithm B performs the following steps:

1. Construct graph representation G of that is used by B.

2. Heuristically compute a (nice) TD of G.

3. Execute B for every node t in TD T in post-order. As input, B takes a node t, a bag , a solving program (depending on and B), which is the part of currently visible in t, and the tables computed at children of t. Bag algorithm B outputs a table .

4. Print the result by interpreting the table for root n of T.

Next, we define a bag algorithm EPRIM for the epistemic primal graph representation of . To this end, let (A, R) be the given input epistemic program, be a nice TD of be a node of T , and be any arbitrary total ordering among the nodes in T . To ease notation, for some set , let conn(X) be the set of vertices (i.e., atoms) from that lie on a path that non-epistemically connects any two vertices a and b in X.4 We now define the induced bag rules for node t of T , denoted by , as follows. For every rule is compatible with node t of T iff (a) , and (b) is subset-maximal among all nodes of T . Now, iff t is the -minimal node among all nodes in T with compatible with r. The induced bag program for node t is the ELP .

Observe that any set of vertices that form a clique within will appear together in some node t of T . Note that for each node t of T that has not a non-subset-maximal bag, or has one, but is not -minimal for any compatible R, the induced bag program is empty. Therefore, we have that for each rule there is exactly one node t of T where , and, even more stringent, that each atom appears only in the induced bag program of t, but not in any other node. The bag algorithm EPRIM uses the induced bag program as its solving program, and, following the argument above, can check all rules containing atoms from in a single node. Hence, during its traversal of the tree decomposition, it does not need to store anything about these atoms. Instead, every row computed as part of a table by EPRIM for a node t, called an epistemic row, is of the form , where is a partial CWI (that is, a CWI restricted to and defined w.r.t. )5. For easy identification, the CWI part of the rows in our algorithms will always be printed using an orange color.

Listing 1 presents algorithm EPRIM. For the ease of presentation, it deals with nice TDs only, but can be generalized to arbitrary TDs, requiring a more involved case distinction. Intuitively, since for each leaf node t we have , bag algorithm EPRIM ensures in Line 1 that consists only of the empty epistemic row. Then, when an atom a appears in bag for a node t, but does not occur in child bags, CWI J, with either , , or , is computed in Line 3. Further, if the solving program with rules is not empty, i.e., t is the unique node responsible for evaluating all the rules in , the four conditions of Definition 2 are checked in Line 4. Note that these checks can be performed by calling a black-box ASP solvers a limited number of times for each row in t:

Proposition 8. To compute a row in a table of EPRIM, an ASP solver needs to be called at most times.

On an abstract level, bag algorithm EPRIM hence provides a method for solving epistimic logic programs by means of plain ASP solvers based on the structure of the epistemic literals of . Whenever an epistemic atom a is removed in node t, indicating that a does not occur in any ancestor bag of t, information about the “role” of a in any CWI is not needed anymore. Finally, for join nodes, Line 7 ensures that the CWIs in coincide with the ones that both child bags have in common. The last step is the evaluation of the root node. If in the root a non-empty table is computed by EPRIM, then the input ELP has a CWV.

Example 9. The epistemic primal graph from Example 7 is a “best case”-scenario for using our TD-based approach: the TD naturally separates the ELP into one part each for the two students, and algorithm EPRIM would evaluate the two completely separately, which is exactly what intuition would tell us to do. However, standard ELP solvers seem to struggle in this setting when the number of students increases; cf. e.g. [2].

From Proposition 8, and the facts that there are only linearly many TD nodes in the size of the input ELP , and that the number of rows per tree node is at most exponential in the treewidth of , we obtain the following statement:

Theorem 10. Given an input ELP of size n, algorithm described above makes at most calls to an underlying ASP solver, where .

Correctness of the algorithm presented above can be established along the same lines as for established TDbased dynamic programming algorithms for ASP [15, 27]. A more formal correctness argument will be given in the next section.

In this section, we will extend the EPRIM algorithm in such a way that it no longer relies on an underlying ASP solver, but solves an ELP completely on its own, using dynamic programming. This new algorithm, PRIM, will operate on the primal graph, instead of on the epistemic primal graph, and makes use of features of the entire ELP structure.

Recall that the primal graph is defined on all atoms of an ELP, instead of just on the ones appearing in epistemic literals. As a result, we need to define a different solving program for TD nodes. To this end, for the remainder of the section, assume we are a given ELP to solve. Further, let be a nice TD of the primal graph of , and t a node of T . Then, the bag rules for t, denoted are defined as the set , that is, all the rules of that are completely “covered” by . Further, the bag program of t is defined as .

In order to define PRIM, we need to define what a row of a table for a TD node t looks like. Since PRIM, in contrast to EPRIM, now also needs to compute the answer sets underlying a CWV, we start with the following, preliminary definition. Let be an interpretation and a set of interpretations w.r.t. . Then, we refer to a tuple as an answer set tuple. This construct, proposed in [15], directly follows the definition of answer sets as in Definition 1, namely, (1) set M, called a witness, is used for storing (parts of) an answer set candidate of some ASP program, and (2) set C, called counterwitnesses, holds a set of (partial) models of the GLreduct w.r.t. M that are potential subsets of M, and hence may be counter-examples to M being extendable to an answer set. An answer set tuple with an empty set of counterwitnesses is referred to as proving answer set tuple, which, vaguely speaking, proves that M can be indeed extended to an answer set of some ASP program, which the tuple was constructed for. Answer set tuples are used by algorithm PRIM in order to “transport” information—in the form of parts of models restricted to the respective bags—of already evaluated rules of the ASP program from the leaves towards the root during TD traversal.

With this definition in mind, we are now ready to define a row for node t used in algorithm PRIM. Such a row, called primal row, is of the form , where I (printed in orange) corresponds to a CWI restricted to as in EPRIM, and sets M, K, S consist of answer set tuples, where M (printed in blue) represents a set of possible witness answer sets for Condition 1 of Definition 2, K represents possible witnesses for disproving Conditions 2 and 3, and S represents possible witnesses for guaranteeing Condition 4. In the root node n of the TD, a specific primal row is required in table to answer the question of WV existence of positively, and PRIM is designed to maintain primal rows accordingly. The set M of answer set tuples in is used for ensuring Condition (1) of Definition 2, where a proving answer set tuple in M gives rise to an answer set of some ASP program of some extension of I. For ensuring Conditions (2) and (3), the set K in shall not contain any proving program tuples, i.e., proving program tuples of K are required to vanish (get “killed”) during the TD traversal, otherwise Conditions (2) or (3) would be violated. Finally, S in serves to establish Condition (4), where no non-proving answer set tuple is allowed, that is, each answer set tuple needs to “survive”.

Definition 11. A primal row is proving if (1) there is a with , (2) there is no with , and (3) there is no with .

Algorithm PRIM is designed to ensure existence of such a proving primal row in of root node n of the TD, iff a WV exists. PRIM uses the following constructs, assuming an answer set tuple , an atom , and a program P. For updating an answer set tuple, we let . When some atom a is introduced in an intr-type node, we need to distinguish between a already being in the interpretation, or not. We define , which is generalized to sets M of answer set tuples as follows: . Finally, to obtain good runtime bounds later and at the same time still ensure Condition (4) of Definition 2 using a set S of answer set tuples, we need to find, for each answer set tuple in S, exactly one “succeeding” answer set tuple among the set M of answer set tuples. We formalize this by defining for every .

Bag algorithm PRIM, as presented in Listing 2, again distinguishes between different types of tree nodes during the post-order traversal of T . For leafs, Line 1 returns the primal row consisting of the empty CWI, where the second component M contains only the proving answer set tuple (since is the smallest model of the empty program), and K, S are both empty as there is no need to remove or create answer set tuples, respectively. If an atom is introduced, Line 3 updates M and K. Line 4 ensures that each answer set tuple in S has at least one succeeding answer set tuple in every primal row of table . If an atom is introduced, the sets M, K, and S are similarly updated in Line 6, but the three cases (true, false, and unknown) need to be considered when adding a to I. Conditions (2) and (3) are handled in Line 8, where answer set tuples in M that violate these two conditions (for , and , respectively) are added to K. For Condition (4), Line 9 ensures that if , there is both a succeeding answer set tuple where a is set to true, and one where it is false. If an atom a is removed, a is removed from the primal rows in Line 11, since we have processed every part of where a occurs. Finally, for join nodes, we combine only “compatible” primal rows in Line 13. In particular, Line 14 ensures that no answer set tuple is lost in or of the child primal rows.

In the following, we briefly mention correctness and runtime bounds for bag algorithms PRIM and EPRIM.

Theorem 12 (Correctness). Let be an ELP , and a TD of . Then there is a proving row in table obtained by for root n of T iff there is a WV for .

Then, correctness of , cf., Sec. 4, is a special case.

Corollary 13 (Correctness of ). Let be an ELP and a TD of . Then there is a row in table for root n obtained by iff there is a WV for .

Proof (Idea). T can be turned into a TD of by adding to each the set A, where on T is, therefore, just a simplification of on .

Theorem 14 (Runtime). runs in time for epistemic program , and treewidth k of .

Indeed, under reasonable assumptions in computational complexity, that is, the exponential time hypothesis (ETH) [26], one cannot significantly improve since is ETH-tight.

Proposition 15 (cf. [16], Theorem 19). Let be an epistemic logic program with of treewidth k. Then, unless ETH fails, WV existence for cannot be decided in time .

This work provides the first parameterized complexity analysis of ELP solving w.r.t. treewidth. Tree decompositions (TDs) have been successfully used in the selp ELP solver [2], but for a different purpose, namely that ELPs are rewritten into non-ground ASP programs with long rules, which are then split up using rule decomposition [1]. Our approach partitions an ELP according to a TD, and then solves the entire ELP by evaluating these parts in turn. Note that this is different from (ELP) splitting [7, 29].

For future work, we aim to extend our DP algorithm to the formula evaluation problem, which, viz. Theorem 6, should work in a similar fashion to our existing algorithms, given a suitable graph representation. Furthermore, we would like to apply our approach to other ELP semantics; cf. [20, 21, 28]. There, we do not anticipate large obstacles, since most semantics are reduct-based, and the reduct is an easily exchangeable part in our algorithms.

M. Hecher and S. Woltran were supported by the Austrian Science Fund (FWF) under grants Y698 and P32830. Final version of this document will be available under AAAI proceedings.

[1] M. Bichler, M. Morak, and S. Woltran. The power of non-ground rules in answer set programming. TPLP, 16 (5-6):552–569, 2016.

[2] M. Bichler, M. Morak, and S. Woltran. Single-shot epistemic logic program solving. In Proc. IJCAI, pages 1714–1720, 2018.

[3] B. Bliem, S. Ordyniak, and S. Woltran. Clique-width and directed width measures for answer-set programming. In Proc. ECAI, pages 1105–1113, 2016. doi: 10.3233/978-1-61499-672-9-1105.

[4] B. Bliem, M. Moldovan, M. Morak, and S. Woltran. The impact of treewidth on ASP grounding and solving. In Proc. IJCAI, pages 852–858, 2017. doi: 10.24963/ijcai.2017/118.

[5] H. L. Bodlaender and T. Kloks. Efficient and constructive algorithms for the pathwidth and treewidth of graphs. J. Algorithms, 21(2):358–402, 1996. doi: 10.1006/jagm.1996.0049.

[6] G. Brewka, T. Eiter, and M. Truszczynski. Answer set programming at a glance. Commun. ACM, 54(12): 92–103, 2011. doi: 10.1145/2043174.2043195. URL http://doi.acm.org/10.1145/2043174.2043195.

[7] P. Cabalar, J. Fandinno, and L. Fari˜nas del Cerro. Splitting epistemic logic programs. In Proc. LPNMR, pages 120–133, 2019. doi: 10.1007/978-3-030-20528-7\ 10.

[8] G. Charwat and S. Woltran. Expansion-based QBF solving on tree decompositions. Fundam. Inform., 167 (1-2):59–92, 2019. doi: 10.3233/FI-2019-1810.

[9] B. Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput., 85(1):12–75, 1990.

[10] R. G. Downey and M. R. Fellows. Parameterized Complexity. Monographs in Computer Science. Springer, 1999. ISBN 978-1-4612-6798-0. doi: 10.1007/978-1-4612-0515-9.

[11] T. Eiter and G. Gottlob. On the computational cost of disjunctive logic programming: Propositional case. Ann. Math. Artif. Intell., 15(3-4):289–323, 1995. doi: 10.1007/BF01536399. URL http://dx.doi.org/10.1007/ BF01536399.

[12] L. Fari˜nas del Cerro, A. Herzig, and E. I. Su. Epistemic equilibrium logic. In Proc. IJCAI, pages 2964–2970, 2015.

[13] J. K. Fichte and M. Hecher. Treewidth and counting projected answer sets. In Proc. LPNMR, pages 105–119, 2019. doi: 10.1007/978-3-030-20528-7\ 9.

[14] J. K. Fichte and S. Szeider. Backdoors to tractable answer set programming. Artif. Intell., 220:64–103, 2015. doi: 10.1016/j.artint.2014.12.001.

[15] J. K. Fichte, M. Hecher, M. Morak, and S. Woltran. Answer set solving with bounded treewidth revisited. In Proc. LPNMR, pages 132–145, 2017. doi: 10.1007/978-3-319-61660-5\ 13.

[16] J. K. Fichte, M. Hecher, and A. Pfandler. TE-ETH: Lower Bounds for QBFs of Bounded Treewidth. Prelimi- nary version available at https://tinyurl.com/y7wnvu6w, 2019.

[17] J. K. Fichte, M. Hecher, and M. Zisser. An improved GPU-based SAT model counter. In Proc. CP, pages 491–509, 2019. doi: 10.1007/978-3-030-30048-7\ 29.

[18] J. K. Fichte, M. Kronegger, and S. Woltran. A multiparametric view on answer set programming. Ann. Math. Artif. Intell., 86(1-3):121–147, 2019. doi: 10.1007/s10472-019-09633-x.

[19] R. Ganian, M. S. Ramanujan, and S. Szeider. Combining treewidth and backdoors for CSP. In Proc. STACS, pages 36:1–36:17, 2017. doi: 10.4230/LIPIcs.STACS.2017.36.

[20] M. Gelfond. Strong introspection. In Proc. AAAI, pages 386–391. AAAI Press / The MIT Press, 1991.

[21] M. Gelfond. New semantics for epistemic specifications. In Proc. LPNMR, pages 260–265, 2011.

[22] M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In Proc. ICLP/SLP, pages 1070–1080. MIT Press, 1988.

[23] M. Gelfond and V. Lifschitz. Classical negation in logic programs and disjunctive databases. New Generation Comput., 9(3/4):365–386, 1991.

[24] M. Gelfond and H. Przymusinska. Definitions in epistemic specifications. In Proc. LPNMR, pages 245–259, 1991.

[25] G. Gottlob, R. Pichler, and F. Wei. Bounded treewidth as a key to tractability of knowledge representation and reasoning. Artif. Intell., 174(1):105–132, 2010. doi: 10.1016/j.artint.2009.10.003.

[26] R. Impagliazzo, R. Paturi, and F. Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4):512–530, 2001. doi: 10.1006/jcss.2001.1774.

[27] M. Jakl, R. Pichler, and S. Woltran. Answer-set programming with bounded treewidth. In Proc. IJCAI, pages 816–822, 2009. URL http://ijcai.org/Proceedings/09/Papers/140.pdf.

[28] P. T. Kahl, R. Watson, E. Balai, M. Gelfond, and Y. Zhang. The language of epistemic specifications (refined) including a prototype solver. J. Log. Comput., 25, 2015.

[29] V. Lifschitz and H. Turner. Splitting a logic program. In Proc. ICLP, pages 23–37, 1994.

[30] V. Lifschitz, L. R. Tang, and H. Turner. Nested expressions in logic programs. Ann. Math. Artif. Intell., 25 (3-4):369–389, 1999.

[31] Z. Lonc and M. Truszczynski. Fixed-parameter complexity of semantics for logic programs. ACM Trans. Comput. Log., 4(1):91–119, 2003. doi: 10.1145/601775.601779.

[32] M. Morak. Epistemic logic programs: A different world view. In Proc. ICLP, pages 52–64, 2019.

[33] D. Pearce, H. Tompits, and S. Woltran. Characterising equilibrium logic and nested logic programs: Reductions and complexity. TPLP, 9(5):565–616, 2009. doi: 10.1017/S147106840999010X. URL https://doi.org/10.1017/ S147106840999010X.

[34] N. Robertson and P. D. Seymour. Graph minors. III. planar tree-width. J. Comb. Theory, Ser. B, 36(1):49–64, 1984. doi: 10.1016/0095-8956(84)90013-3.

[35] T. Schaub and S. Woltran. Special issue on answer set programming. KI, 32(2-3), 2018. doi: 10.1007/s13218-018-0554-8. URL https://doi.org/10.1007/s13218-018-0554-8.

[36] Y. Shen and T. Eiter. Evaluating epistemic negation in answer set programming. Artif. Intell., 237:115–135, 2016.

[37] T. C. Son, T. Le, P. T. Kahl, and A. P. Leclerc. On computing world views of epistemic logic programs. In Proc. IJCAI, pages 1269–1275, 2017.

[38] M. Truszczynski. Revisiting epistemic specifications. In Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning - Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday, 2011.