Structural Decompositions of Epistemic Logic Programs? Markus Hecher1,2 , Michael Morak3 , and Stefan Woltran1 1 TU Wien, Austria, {hecher, woltran}@dbai.tuwien.ac.at 2 University of Potsdam, Germany 3 University of Klagenfurt, Austria, michael.morak@aau.at 1 Introduction 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. 2 Runtime Results for ELPs and Treewidth 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. Theorem 1 (Solving World View Existence for Treewidth in Linear Time). There is an algorithm for solving world view existence of a given epistemic program Π with n 2O(k) many atoms, running in time 22 · n, where k is the treewidth of the primal graph PΠ . Interestingly, under reasonable assumptions in computational complexity, that is, the exponential time hypothesis (ETH), one cannot significantly improve this runtime [3]. ? This is an extended abstract of a work that has been published [6] at AAAI’2020. Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 2 Hecher, Morak, and Woltran 3 Bounding Calls to Standard ASP Solvers 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 [4]. 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 [5]. We observed that this domain seems to be a “best case”-scenario for using our approach, where our algorithm naturally separates the ELPs into parts. However, standard ELP solvers seem to struggle in this setting when the program sizes increase; cf. e.g. [1]. 4 Conclusions 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 [2]. For future work, we aim to extend our algorithms to the formula evaluation problem, which 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. There, we do not anticipate large obstacles, since most semantics are reduct-based, and the reduct is an easily exchangeable part in our algorithms. References 1. Bichler, M., Morak, M., Woltran, S.: Single-shot epistemic logic program solving. In: Proc. IJCAI. pp. 1714–1720 (2018) 2. Cabalar, P., Fandinno, J., Fariñas del Cerro, L.: Splitting epistemic logic programs. In: Proc. LPNMR. pp. 120–133 (2019) 3. Fichte, J.K., Hecher, M., Pfandler, A.: Lower bounds for QBFs of bounded treewidth. In: LICS. pp. 410–424. ACM (2020) 4. Ganian, R., Ramanujan, M.S., Szeider, S.: Combining treewidth and backdoors for CSP. In: Proc. STACS. pp. 36:1–36:17 (2017) 5. Gelfond, M.: Strong introspection. In: Proc. AAAI. pp. 386–391. AAAI Press (1991) 6. Hecher, M., Morak, M., Woltran, S.: Structural decompositions of epistemic logic programs. In: AAAI. pp. 2830–2837. AAAI Press (2020) 7. Shen, Y., Eiter, T.: Evaluating epistemic negation in answer set programming. Artif. Intell. 237, 115–135 (2016)