Epistemic logic programs (ELPs) [5] are a popular generalization of standard Answer Set Programming (ASP) providing means for reasoning over answer sets within the language. This is accomplished by the use of modal operators such as K and M in rule bodies. Shen and Eiter [7] have shown that these operators can be conveniently expressed via a single negation-type operator (epistemic negation not), and have provided a new semantics for ELPs based on this operator. The richer formalism of ELPs comes at the price of higher computational complexity, namely checking whether an ELP has a world view, is 3P -complete, but problems higher on the polynomial hierarchy exist. 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 based on the semantics by Eiter and Shen [7] can be solved in linear time for ELPs exhibiting structural properties in terms of bounded treewidth. Then, we provide an algorithm that adheres to bounded treewidth. 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 ELP solving procedures. Before we briefly discuss our results, we need to define some graph representation of ELPs. Let therefore be an ELP. We define the primal graph P as the graph, whose vertices comprises of all atoms of and we put an edge between two vertices whenever the two corresponding atoms appear together in at least one rule of . Then, we show that the world view existence for ELPs, whose primal graph has treewidth k can be solved in linear time. Further, we establish an algorithm and show the following theorem.
Hecher, Morak, and Woltran
Next, we present consequences of an algorithm for solving world view existence by
means of calls to ASP solvers. Notably, our algorithm allows to bound the number of ASP
solver calls such that for small treewidth only linearly many of these calls are required.
To this end, we say for a given ELP that two vertices a; b of primal graph P are
non-epistemically connected iff there is a path ha; v1; : : : ; vn; bi with n 0 in P , such
no vertex vi (1 i n) appears under epistemic negation in . Now, the epistemic
primal graph E of is a graph, whose vertices are only atoms of that appear under
epistemic negation and there is an edge between two vertices of E iff the corresponding
atoms are non-epistemically connected in P . Intuitively, two vertices form an edge in
E iff there is a direct edge in P or they are connected in P via atoms that do not
appear in epistemic literals. The concept of E is inspired by related work [
We establish an algorithm that allows to show the following theorem.
Theorem 2. Given an ELP using n many atoms, world view existence can be solved with at most O(2k n) calls to an underlying ASP solver, where k is the treewidth of E .
Indeed, our algorithm can be used for the classic scholarship eligibility problem [
This work provides the first parameterized complexity analysis of ELP solving w.r.t.
treewidth. Our approach partitions an ELP according to a tree decomposition, and then
solves the entire ELP by evaluating these parts in turn. Note that this is different from
(ELP) splitting [