# structural_decompositions_of_epistemic_logic_programs__fea88cbd.pdf

The Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI-20)

Structural Decompositions of Epistemic Logic Programs

Markus Hecher,1,2 Michael Morak,3 Stefan Woltran1

1TU Wien, Vienna, Austria, 2University of Potsdam, Potsdam, Germany 3University of Klagenfurt, Klagenfurt, Austria {hecher, woltran}@dbai.tuwien.ac.at, michael.morak@aau.at

Epistemic logic programs (ELPs) are a popular generalization of standard Answer Set Programming (ASP) providing means for reasoning over answer sets within the language. This richer formalism comes at the price of higher computational complexity reaching up to the fourth level of the polynomial hierarchy. However, in contrast to standard ASP, dedicated investigations towards tractability have not been undertaken yet. In this paper, we give first results in this direction and show that central ELP problems can be solved in linear time for ELPs exhibiting structural properties in terms of bounded treewidth. We also provide a full dynamic programming algorithm that adheres to these bounds. Finally, we show that applying treewidth to a novel dependency structure given in terms of epistemic literals allows to bound the number of ASP solver calls in typical ELP solving procedures.

1 Introduction Epistemic logic programs (ELPs) (Gelfond and Przymusinska 1991), also referred to as the language of Epistemic Specifications (Gelfond 1991), have received renewed attention in the research community as of late. ELPs are an extension of the language of Answer Set Programming (ASP) (Brewka, Eiter, and Truszczynski 2011; Schaub and Woltran 2018) 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 (Gelfond 2011; Truszczynski 2011; Kahl et al. 2015; Fari nas del Cerro, Herzig, and Su 2015). Shen and Eiter (2016) realized that these two operators can be represented via a single negationtype 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 (Cabalar, Fandinno, and Fari nas del Cerro 2019) 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

Copyright c 2020, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

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 ΣP 3 -complete, and problems even higher on the polynomial hierarchy exist (Shen and Eiter 2016; Morak 2019). 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, (Lonc and Truszczynski 2003; Gottlob, Pichler, and Wei 2010; Fichte and Szeider 2015; Bliem, Ordyniak, and Woltran 2016; Fichte, Kronegger, and Woltran 2019; Fichte and Hecher 2019). 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 (Fichte et al. 2017; Bliem et al. 2017; Fichte, Hecher, and Zisser 2019; Charwat and Woltran 2019). 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 EPASP (Son et al. 2017). Using the epistemic primal graph representation, these

1Problem SE was a prime motivator for ELPs (Gelfond 1991).

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 fixedparameter 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.

2 Preliminaries 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 a1 al al+1, . . . , am, ℓ1, . . . , ℓn, where the comma symbol stands for conjunction, 0 l m, 0 n, ai A for all 1 i m, and each ℓi is a literal, that is, either an atom a or its (default) negation a for any atom a A.2 Note that, therefore, doubly negated atoms may occur. We will sometimes refer to such rules as standard rules. Each rule r R consists of a head H (r) = {a1, . . . , al} and a body B(r) = {al+1, . . . , am, ℓ1, . . . , ℓn}, and is alternatively denoted by H (r) B(r). The positive body is given by B+(r) = {al+1, . . . , am}. Sometimes, we add a set of rules R to a logic program P = (A, R). By some abuse of notation, let P R denote the logic program (A A , R R ), where A is the set of atoms occurring in the rules of R . An interpretation I (over A) is a set of atoms, that is, I A. A literal ℓis true in an interpretation I A, denoted I ℓ, iff a I and ℓ= a , or a I and ℓ= a; otherwise ℓis false in I, denoted I ℓ. Finally, for some literal ℓ, we define that I ℓif I ℓ. This notation naturally extends to sets of literals. An interpretation M is called a model of r, denoted M r, if, whenever M B(r), it holds that M H (r). We denote the set of models of r by mods(r); the models of a logic program P = (A, R) are given by mods(P) =

r R mods(r). We also write I r (resp. I P) if I mods(r) (resp. I mods(P)). The GL-reduct of a logic program P = (A, R) with respect to an interpretation I is given by PI = (A, RI) with RI = {H (r) B+(r) | r R, ( ℓ) B(r) : I ℓ}.

2In this case, we say that it is a literal over A.

Definition 1 ((Gelfond and Lifschitz 1988; 1991; Lifschitz, Tang, and Turner 1999)). M A is an answer set of a logic program P if (1) M mods(P) and (2) there is no subset M M such that M mods(PM). 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 AS(P) = , is Σ2 P-complete (Eiter and Gottlob 1995), and remains so also in the case where doubly negated atoms are allowed in rule bodies (Pearce, Tompits, and Woltran 2009).

Epistemic Logic Programs. An epistemic literal is a formula not ℓ, where ℓis a literal and not is the epistemic negation operator. A ground epistemic logic program (ELP) is a pair Π = (A, R), where A is a set of atoms and R is a set of ELP rules, which are implications of the form a1 ak ℓ1, . . . , ℓm, ξ1, . . . , ξj, ξj+1, . . . , ξn, where each ai is an atom from A, each ℓi is a literal over A, and each ξi is an epistemic literal of the form not ℓ, where ℓis a literal over A. Similarly to logic programs, let H (r) = {a1, . . . , ak}, and let B(r) = {ℓ1, . . . , ℓm, ξ1, . . . , ξj, ξj+1, . . . , ξn}. Further, at(r) A denotes the set of atoms ocurring in ELP rule r, and atel(r) at(r) 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 (2019), which follows the semantics defined in (Shen and Eiter 2016), 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, R), a candidate world interpretation (CWI) I for Π is a consistent subset I L, 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 IP , IN, IU , where IP = {a | a I A}, IN = {a | a I} and IU = (A \ IP ) \ IN, with the intended meaning that atoms in IP , IN, and IU 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 a IP , it holds that for each J I, a J; 3. for each atom a IN, we have for each J I, a J; 4. for each atom a IU, it holds that there are J, J I, such that a J, but a J . The epistemic reduct (Shen and Eiter 2016; Morak 2019) of program Π = (A, R) w.r.t. a CWI I, denoted ΠI, is defined as ΠI = (A, {r I | r R}) where r I denotes rule r where each epistemic literal not ℓis replaced by ℓif ℓ I, and by otherwise. Note that, hence, ΠI is a plain logic program with all occurrences of epistemic negation removed.3

3In fact, ΠI may contain triple-negated atoms a. Accord-

Now, a CWI I is a candidate world view (CWV) of Π iff I is compatible with the set AS(ΠI) of answer sets. The set of CWVs of an ELP Π is denoted cwv(Π). Following the principle of knowledge minimization, furthermore I is a world view (WV) iff it is a CWV and there is no proper subset J I such that J cwv(Π). The set of WVs of an ELP Π is denoted wv(Π). One of the main reasoning tasks regarding ELPs is the world view existence problem, that is, given an ELP Π, decide whether wv(Π) = (or, equivalently, whether cwv(Π) = ). This problem is known to be ΣP 3 -complete (Shen and Eiter 2016; Morak 2019). Another interesting reasoning task is deciding, given an ELP Π = (A, R) and an arbitrary propositional formula ϕ over A, whether ϕ holds in some WV, that is, whether there exists W wv(Π) such that W ϕ. This formula evaluation problem is even harder, namely ΣP 4 -complete (Shen and Eiter 2016).

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 χ(t) V called the bag of t. The pair T = (T, χ) is called a tree decomposition (TD) (Robertson and Seymour 1984) of G iff (i) for each v V , there exists a t in T, such that v χ(t); (ii) for each {v, w} E, there exists t in T, such that {v, w} χ(t); and (iii) for each r, s, t of T, such that s lies on the unique path from r to t, we have χ(r) χ(t) χ(s). For a node t of T, we say that type(t) is leaf if t has no children and χ(t) = ; join if t has children t and t with t = t and χ(t) = χ(t ) = χ(t ); intr ( introduce ) if t has a single child t , χ(t ) χ(t) and |χ(t)| = |χ(t )| + 1; rem ( removal ) if t has a single child t , χ(t ) χ(t) and |χ(t )| = |χ(t)| + 1. If for every node t T, type(t) {leaf, join, intr, rem}, then (T, χ) is called nice. The width of a TD is defined as the cardinality of its largest bag minus one. The treewidth of a graph G, denoted by tw(G), is the minimum width over all TDs of G. Note that if G is a tree, then tw(G) = 1.

Monadic Second Order Logic and Courcelle s Theorem. Monadic Second Order logic (MSO) extends First Order logic (FO) with set variables that range over sets of domain elements. Atomic MSO-formulas over a signature σ are either (1) atoms over some predicate in σ; (2) equality atoms; or (3) atoms of the form x S, where x is a FO variable, and S is a set variable. MSO-formulas are closed under FO operators. It is convenient to use symbols like , , , , or , with the obvious meanings as abbreviations for the corresponding MSO (sub-)formulas. A σ-structure A is a set of atoms over predicates in σ. Let dom(A) denote its domain. 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 tw(GA), where GA = (V, E) is a graph with V = dom(A) and edge

ing to (Lifschitz, Tang, and Turner 1999), such formulas are equivalent to simple negated atoms a, and we treat them as such.

{a, b} E iff r(a, b) A, 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 ((Courcelle 1990)). Let ϕ be a fixed MSO formula over signature σ and let A be a σ-structure with tw(A) k, for some integer k. Then, evaluating ϕ over A can be done in time O(f(k) |A|), for some function f not depending on |A|.

Problems with a parameter k that can be solved in time O(f(k) nc), where c is a constant and f only depends on k, are called fixed-parameter tractable (FPT) (Downey and Fellows 1999).

3 An MSO Encoding for ELPs

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 (Gottlob, Pichler, and Wei 2010), 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, h, b, b , bnot , bnot , b not , b not }, 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 b (a, r), with {ε, , not , not , not , not } and ε the empty word, represents that fact that the sub-formula a, 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 W P = P, W N = N, and W U = U. To this end, our formula will be of the following form: cwv(P, N, U) cwi(P, N, U) 4 i=1 chki(P, N, U) 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 chki 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: cwi(P, N, U) X (atom(X ) X P N U) X ((X P N) (X N U) (X P U))

The four remaining checks have a similar structure:

chk1(P, N, U) X as(X, P, N, U); chk2(P, N, U) X (X P X (as(X, P, N, U) X X)) ;

chk3(P, N, U) X (X N X (as(X, P, N, U) X X)) ; chk4(P, N, U) X (X U ( X (as(X, P, N, U) X X) X (as(X, P, N, U) X X))) .

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, chk3 encodes that for each atom X that is set to always false in the CWI (i.e., X N), it must hold that for every stable model X of the epistemic reduct, X must not be true in that stable model (i.e., X X). It now remains to define the sub-formula for checking answer sets. This construction is based on the one presented in (Gottlob, Pichler, and Wei 2010, 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): as(X, P, N, U) gl(X, X, P, N, U) Y (Y X gl(X, Y, P, N, U)) . 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:

gl(X, Y, P, N, U) R (rule(R) Z ( (h(Z, R) Z Y) (b(Z, R) Z Y) (b (Z, R) Z X)) (bnot (Z, R) Z P Z X) (bnot (Z, R) Z N Z X) (b not (Z, R) ((Z N U) (Z P Z X))) (b not (Z, R) ((Z P U) (Z N Z X)))

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: ϕ = P N U cwv(P, N, U). Evaluating this formula over a σ-structure P that represents an ELP Π, we get that Π has a CWV iff P ϕ.

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 Π = (A, R) be an ELP, and let P be the σ-structure that represents it. Recall that tw(P) = tw(GP). In our case, GP 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 (Jakl, Pichler, and Woltran 2009; Fichte et al. 2017). The incidence graph of an ELP Π is the graph G = (V, E) with V = A R and {a, r} E iff atom a A occurs in rule r R 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 tw(G) k, for some integer k. Then, checking whether cwv(Π) = can be done in time O(f(k) |Π|), 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 P N U cwv(P, N, U) entails(P, N, U, ϕ) ( P N U (P P N N) cwv(P , N , U )) checks whether there is at least one WV that satisfies formula ϕ, where the atom entails(P, N, U, ϕ) 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 Π, G, 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 O(f(k) |Π|), 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.

4 Bounding Calls to Standard ASP Solvers 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 Π = (A, R) be an ELP. Then, the primal graph PΠ = (V, E) of Π is a graph with V = A and {a, b} E iff atoms a and b with a = b appear together in a rule in R, that is, iff r R : {a, b} at(r). Two vertices a, b in the primal graph are non-epistemically connected iff there is a path a, v1, . . . , vn, b with n 0 in PΠ, such that each vertex vi, 1 i n, belongs to the set A \ atel(Π). Now, the epistemic primal graph EΠ = (V, E) of Π is a graph with the vertex set V = atel(Π) being the set of atoms appearing in epistemic literals in Π, and an edge {a, b} E iff a = b and vertices a, b are non-epistemically connected in PΠ. Intuitively, two atoms from atel(Π) form an edge in EΠ iff they are connected in PΠ via atoms that do not appear in epistemic literals. The concept of epistemic primal graph is inspired by the notion of the torso graph (Ganian, Ramanujan, and Szeider 2017), which is used in parameterized complexity to decompose certain abstraction graphs.

Example 7. Consider the classic scholarship eligibility problem encoding, first investigated by Gelfond (1991): eligible(X ) high GPA(X ) ineligible(X ) low GPA(X ) eligible(X ), ineligible(X ) interview(X ) not eligible(X ), not ineligible(X ). 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 Π: low GPA(mike) high GPA(mike) low GPA(mark) high GPA(mark) Epistemic primal graph EΠ contains only four nodes: eligible(mike), ineligible(mike), and the same two for mark. Further, EΠ does not have any edges except an edge between the two mike-atoms, and the same for mark. Since EΠ forms a forest, the treewidth of EΠ 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), bottom-up, along a TD where at each node t of the TD information is gathered (Bodlaender and Kloks 1996) in a table τ(t). A table τ(t) is a set of rows, where a row in τ(t) 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 DPB 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 T = (T, χ) of G.

3. Execute B for every node t in TD T in post-order. As input, B takes a node t, a bag χ(t), a solving program (depending on χ(t) 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 τ(t).

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, T = (T, χ) be a nice TD of EΠ, t be a node of T , and be any arbitrary total ordering among the nodes in T . To ease notation, for some set X atel(R), let conn(X) be the set of vertices (i.e., atoms) from PΠ that lie on a path that nonepistemically connects any two vertices a and b in X.4 We now define the induced bag rules for node t of T , denoted by RE t , as follows. For every rule r R, r is compatible with node t of T iff (a) at(r) conn(atel(R)) conn(χ(t)), and (b) χ(t) is subset-maximal among all nodes of T . Now, r RE t iff t is the -minimal node among all nodes t in T with type(t ) = intr compatible with r. The induced bag program for node t is the ELP ΠE t = (at(RE t ), RE t ). Observe that any set of vertices that form a clique within EΠ 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 R, the induced bag program is empty. Therefore, we have that for each rule r R there is exactly one node t of T where r RE t , and, even more stringent, that each atom a at(r)\atel(r) 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 A \ atel(Π) 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 I , where I 2{a, a|a χ(t)} is a partial CWI (that is, a CWI restricted to and defined w.r.t. χ(t))5. 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 χ(t) = , bag algorithm EPRIM ensures in Line 1 that τ(t) consists only of the empty epistemic row. Then, when an atom a appears in bag χ(t) for a node t, but does not occur in child bags, CWI J, with either a JP , a JN, or a JU, is computed in Line 3. Further, if the solving program with rules RE t is not empty, i.e., t is the unique node responsible for evaluating all the rules in RE t , 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:

4Note that we may have that a = b, and hence, conn({a}) contains all those vertices from A \ atel(Π) connected to atom a. 5This also means that JP , JN, and JU are defined w.r.t. χ(t).

Listing 1: Bag algorithm EPRIM(t, χt, ΠE t , τ1, . . . ) for nice TDs of the epistemic primal graph representation.

In: Node t, bag χt, induced bag program ΠE t , tables τ1, . . . for child nodes t1, . . . of t. Out: Table τ(t).

1 if type(t) = leaf then τ(t) = { }/* Abbrevs. below */

2 else if type(t) = intr, and a χt is introduced then

3 τ(t)={ J | I τ1, J {I+ a , I+ a, I}, P=(ΠE t )J, RE t = or

4 [ AS(P) = , AS(P { (JP JN)}) = , for every b JU: AS(P { b}) = , AS(P { b}) = ]}

5 else if type(t) = rem, and a χt is removed then

6 τ(t)={ I a | I τ1}

7 else if type(t) = join then τ(t) = τ1 τ2

S+ e := S {e}, S e := S \ {e, e}, S := { s | s S}.

Proposition 8. To compute a row in a table of EPRIM, an ASP solver needs to be called at most 2 + 2 |χ(t)| 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 χ(t) 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. (Bichler, Morak, and Woltran 2018). 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 EΠ, we obtain the following statement: Theorem 10. Given an input ELP Π of size n, algorithm DPEPRIM described above makes at most O(2k n) calls to an underlying ASP solver, where k = tw(EΠ). Correctness of the algorithm presented above can be established along the same lines as for established TD-based dynamic programming algorithms for ASP (Jakl, Pichler, and Woltran 2009; Fichte et al. 2017). A more formal correctness argument will be given in the next section.

5 A Full Dynamic Programming Algorithm 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 Π = (A, R) to solve. Further, let T = (T, χ) be a nice TD of the primal graph PΠ of Π, and t a node of T . Then, the bag rules for t, denoted Rt are defined as the set {r | r R, at(r) χ(t)}, that is, all the rules of Π that are completely covered by χ(t). Further, the bag program of t is defined as Πt = (A χ(t), Rt).

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 M χ(t) be an interpretation and C 2χ(t) a set of interpretations w.r.t. χ(t). Then, we refer to a tuple M, C as an answer set tuple. This construct, proposed in (Fichte et al. 2017), 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 GL-reduct 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 I, M, K, S , where I corresponds to a CWI restricted to χ(t) as in EPRIM, and sets M, K, S consist of answer set tuples, where M 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 u τ(n) is required in table τ(n) 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 u 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 ΠI of some extension I I of I. For ensuring Conditions (2) and (3), the set K in u 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 u 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 I, M, K, S is proving if (1) there is a M, C M with C = , (2) there is no M, C K with C = , and (3) there is no M, C S with C = .

Listing 2: Bag algorithm PRIM(t, χt, Πt, τ1, . . . ) for nice TDs of the primal graph representation.

In: Node t, bag χt, bag program Πt, τ1, . . . is the seq. of tables for child nodes t1, . . . of t. Out: Table τ(t).

1if type(t) = leaf then τ(t) = { , { , }, , }

2else if type(t) = intr, a χt introduced, a atel(Πt) then

3 τ(t)={ I, M , K , S | I, M, K, S τ1, P=(Πt)I, M = int Ts(a, M, P), K = int Ts(a, K, P),

4 S succ S(a, M , S, P)}

5else if type(t) = intr, a χt introduced, a atel(Πt) then

6 τ(t)={ J, M , K K , S S | I, M, K, S τ1, P= (Πt)J, M = int Ts(a, M, P), K = int Ts(a, K, P),

7 S succ S(a, M , S, P), J {I+ a , I+ a, I},

8 K = int Ts(a,

S M{S | a JP }, P { a}) int Ts(a,

S M{S | a JN}, P { a}),

9 {M , M } M , S ={M , M | a JU}={M , M | a JU, M P { a}, M P { a}}}

10else if type(t) = rem, and a χt is removed then

11 τ(t)={ I a , M a , K a , S a | I, M, K, S τ1}

12else if type(t) = join then

13 τ(t)={ I, M1 M2, [K1 (K2 M2)] [K2 (K1 M1)], [S1 (S2 M2)] [S2 (S1 M1)] | I, M1, K1, S1 τ1, I, M2, K2, S2 τ2,

14 |S1|=|S1 (S2 M2)|, |S2|=|S2 (S1 M1)|}

S+ e := S {e}, S e := S \ {e, e}, S e := { M e , {C e | C C} | M, C S}, M1 M2 := { M, (C+ M D) (C D+ M) | M, C M1, M, D M2}.

Algorithm PRIM is designed to ensure existence of such a proving primal row in τ(n) of root node n of the TD, iff a WV exists. PRIM uses the following constructs, assuming an answer set tuple M, C , an atom a A, and a program P. For updating an answer set tuple, we let upd T(M, C, P) = { M, C mods(PM) | M P}. 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 int T(a, M, C, P) = upd T(M + a ,

C C{M, C, C+ a }, P) upd T(M, C, P), which is generalized to sets M of answer set tuples as follows: int Ts(a, M, P) =

M,C M int T(a, M, C, P). 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 succ S(a, M, C, P) = {S | S M, |S | = |S|, for every M, C S : int T(a, M, C, P) S = }.

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 a atel(Π) 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 τ(t). If an atom a atel(Π) 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 a JP , and a JN, respectively) are added to K. For Condition (4), Line 9 ensures that if a JN, 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 S1 or S2 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 T = (T, χ) a TD of PΠ. Then there is a proving row in table τ(n) obtained by DPPRIM for root n of T iff there is a WV for Π. Then, correctness of DPEPRIM, cf., Sec. 4, is a special case. Corollary 13 (Correctness of DPEPRIM). Let Π be an ELP Π and T = (T, χ) a TD of EΠ. Then there is a row in table τ(n) for root n obtained by DPEPRIM iff there is a WV for Π.

Proof (Idea). T can be turned into a TD T of PΠ by adding to each χ(t) the set A, where (ΠE t ) = (A, ). DPEPRIM on T is, therefore, just a simplification of DPPRIM on T .

Theorem 14 (Runtime). DPPRIM runs in time 222O(k) |A| for epistemic program Π = (A, R), and treewidth k of PΠ. Indeed, under reasonable assumptions in computational complexity, that is, the exponential time hypothesis (ETH) (Impagliazzo, Paturi, and Zane 2001), one cannot significantly improve DPPRIM since DPPRIM is ETH-tight. Proposition 15 (cf. (Fichte, Hecher, and Pfandler 2019), Theorem 19). Let Π = (A, ) be an epistemic logic program with PΠ of treewidth k. Then, unless ETH fails, WV

existence for Π cannot be decided in time 222o(k) 2o(|A|).

6 Conclusions 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 (Bichler, Morak, and Woltran 2018), 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 (Bichler, Morak, and Woltran 2016). 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 (Cabalar, Fandinno, and Fari nas del Cerro 2019; Lifschitz and Turner 1994). 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. (Gelfond 1991; 2011; Kahl et al. 2015). There, we do not anticipate large obstacles, since most semantics are reduct-based, and the reduct is an easily exchangeable part in our algorithms.

Acknowledgements M. Hecher and S. Woltran were supported by the Austrian Science Fund (FWF) under grants Y698 and P32830.

References Bichler, M.; Morak, M.; and Woltran, S. 2016. The power of non-ground rules in answer set programming. TPLP 16(56):552 569. Bichler, M.; Morak, M.; and Woltran, S. 2018. Single-shot epistemic logic program solving. In Proc. IJCAI, 1714 1720. Bliem, B.; Moldovan, M.; Morak, M.; and Woltran, S. 2017. The impact of treewidth on ASP grounding and solving. In Proc. IJCAI, 852 858. Bliem, B.; Ordyniak, S.; and Woltran, S. 2016. Clique-width and directed width measures for answer-set programming. In Proc. ECAI, 1105 1113. Bodlaender, H. L., and Kloks, T. 1996. Efficient and constructive algorithms for the pathwidth and treewidth of graphs. J. Algorithms 21(2):358 402. Brewka, G.; Eiter, T.; and Truszczynski, M. 2011. Answer set programming at a glance. Commun. ACM 54(12):92 103. Cabalar, P.; Fandinno, J.; and Fari nas del Cerro, L. 2019. Splitting epistemic logic programs. In Proc. LPNMR, 120 133. Charwat, G., and Woltran, S. 2019. Expansion-based QBF solving on tree decompositions. Fundam. Inform. 167(12):59 92. Courcelle, B. 1990. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85(1):12 75. Downey, R. G., and Fellows, M. R. 1999. Parameterized Complexity. Monographs in Computer Science. Springer. Eiter, T., and Gottlob, G. 1995. On the computational cost of disjunctive logic programming: Propositional case. Ann. Math. Artif. Intell. 15(3-4):289 323. Fari nas del Cerro, L.; Herzig, A.; and Su, E. I. 2015. Epistemic equilibrium logic. In Proc. IJCAI, 2964 2970. Fichte, J. K., and Hecher, M. 2019. Treewidth and counting projected answer sets. In Proc. LPNMR, 105 119. Fichte, J. K., and Szeider, S. 2015. Backdoors to tractable answer set programming. Artif. Intell. 220:64 103. Fichte, J. K.; Hecher, M.; Morak, M.; and Woltran, S. 2017. Answer set solving with bounded treewidth revisited. In Proc. LPNMR, 132 145. Fichte, J. K.; Hecher, M.; and Pfandler, A. 2019. TE-ETH: Lower Bounds for QBFs of Bounded Treewidth. Preliminary version available at https://tinyurl.com/y7wnvu6w. Fichte, J. K.; Hecher, M.; and Zisser, M. 2019. An improved GPU-based SAT model counter. In Proc. CP, 491 509. Fichte, J. K.; Kronegger, M.; and Woltran, S. 2019. A multiparametric view on answer set programming. Ann. Math. Artif. Intell. 86(1-3):121 147.

Ganian, R.; Ramanujan, M. S.; and Szeider, S. 2017. Combining treewidth and backdoors for CSP. In Proc. STACS, 36:1 36:17. Gelfond, M., and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proc. ICLP/SLP, 1070 1080. MIT Press. Gelfond, M., and Lifschitz, V. 1991. Classical negation in logic programs and disjunctive databases. New Generation Comput. 9(3/4):365 386. Gelfond, M., and Przymusinska, H. 1991. Definitions in epistemic specifications. In Proc. LPNMR, 245 259. Gelfond, M. 1991. Strong introspection. In Proc. AAAI, 386 391. AAAI Press / The MIT Press. Gelfond, M. 2011. New semantics for epistemic specifications. In Proc. LPNMR, 260 265. Gottlob, G.; Pichler, R.; and Wei, F. 2010. Bounded treewidth as a key to tractability of knowledge representation and reasoning. Artif. Intell. 174(1):105 132. Impagliazzo, R.; Paturi, R.; and Zane, F. 2001. Which problems have strongly exponential complexity? J. Comput. Syst. Sci. 63(4):512 530. Jakl, M.; Pichler, R.; and Woltran, S. 2009. Answer-set programming with bounded treewidth. In Proc. IJCAI, 816 822. Kahl, P. T.; Watson, R.; Balai, E.; Gelfond, M.; and Zhang, Y. 2015. The language of epistemic specifications (refined) including a prototype solver. J. Log. Comput. 25. Lifschitz, V., and Turner, H. 1994. Splitting a logic program. In Proc. ICLP, 23 37. Lifschitz, V.; Tang, L. R.; and Turner, H. 1999. Nested expressions in logic programs. Ann. Math. Artif. Intell. 25(34):369 389. Lonc, Z., and Truszczynski, M. 2003. Fixed-parameter complexity of semantics for logic programs. ACM Trans. Comput. Log. 4(1):91 119. Morak, M. 2019. Epistemic logic programs: A different world view. In Proc. ICLP, 52 64. Pearce, D.; Tompits, H.; and Woltran, S. 2009. Characterising equilibrium logic and nested logic programs: Reductions and complexity. TPLP 9(5):565 616. Robertson, N., and Seymour, P. D. 1984. Graph minors. III. planar tree-width. J. Comb. Theory, Ser. B 36(1):49 64. Schaub, T., and Woltran, S. 2018. Special issue on answer set programming. KI 32(2-3). Shen, Y., and Eiter, T. 2016. Evaluating epistemic negation in answer set programming. Artif. Intell. 237:115 135. Son, T. C.; Le, T.; Kahl, P. T.; and Leclerc, A. P. 2017. On computing world views of epistemic logic programs. In Proc. IJCAI, 1269 1275. Truszczynski, M. 2011. Revisiting epistemic specifications. In Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning - Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday.