Utilizing Treewidth for Quantitative Reasoning on Epistemic Logic Programs (Extended Abstract)

1 Introduction

Answer Set Programming (ASP) [Brewka et al., 2011] is a well-studied problem modeling and solving framework that is particularly suited for solving problems related to knowledge representation and reasoning and artificial intelligence, see, e.g., the work [Brewka et al., 2011]. In ASP, questions are modeled in the form of logic programs (LPs), which can be seen as a rule-based language whose solutions are referred to by answer sets and which has been significantly extended over the time. The major driver in enabling logic programs for a broad use in both academia and industry was the development of efficient solvers. However, while the ASP framework is powerful, its limits in terms of expressiveness are visible when turning the attention to epistemic specifications.

The idea of these epistemic specifications, which dates back to the early 90s [Gelfond, 1991], allows to precisely describe the behavior of rational agents who are capable of reasoning over multiple worlds. There, depending on whether some objections are possible (true in some world) or known (i.e., true in all worlds) certain consequences have to be derived. This is often modeled by means of operators K or M, which represents that certain objections are known to be true or are possibly true, respectively. Internally these operators can be translated to epistemic negation not, which expresses that some objection is not known, i.e., not true in all worlds. Enhancing standard rules by such operators leads to the development of epistemic logic programs (ELPs). Indeed, depending on the different semantics for ELPs, which have been developed and refined over the years [Truszczynski, 2011; Kahl et al., 2015; Shen and Eiter, 2016; Cabalar et al., 2019], usual reasoning problems like world view existence and certain extensions reach the third and fourth level of the polynomial hierarchy, respectively, and are thus considered significantly harder than standard ASP [Eiter and Gottlob, 1995].

∗This is an extended abstract of [Besin et al., 2021].

In this work, we take a step further and initiate the study of quantitative reasoning for ELPs, where decisions concerning the acceptance of a given set of literals depend on the actual number (proportion) of world views compatible with the set. This allows us to reason about the acceptance of certain literals based on the likelyhood of being contained in an arbitrary world view. To the best of our knowledge, a few works on quantitiative reasoning in ASP exist [Fierens et al., 2015], but it has not yet been studied for ELPs. As a second contribution we present a new system tailored for quantitiative reasoning in ELPs. Although there has been progress in developing ELP solvers (e.g., EP-ASP [Son et al., 2017], selp [Bichler et al., 2020] and a very recent extension of clingo for epistemic logic programs, called eclingo [Cabalar et al., 2020]), these approaches basically rely on reducing ELP problems to standard ASP. Thus, these solvers typically materialize all world views, which is not necessary for quantitative reasoning. We take here a novel route by utilizing ideas from parameterized algorithmics which appear better suited for counting problems that underly the quantitative reasoning approach.

Our approach works on abstractions of the internal (graph) structure of ELPs; i.e., we take the primal graph 1 of an ELP and contract certain paths between nodes referring to epistemic literals. On this graph we implicitly utilize the measure treewidth, measuring the tree-likeness of a given graph. Treewidth gives rise to a so-called tree decomposition (TD), which allows to solve a problem by following a divide-andconquer approach, where world views of ELPs are computed by solving subprograms and combining world views accordingy. Our solver adheres to this approach, where we approximate suitable abstractions of the primal graph structure of an ELP in order to evaluate the program in a way that is guided along a TD of the abstraction. So, the idea of these abstractions compared to the full primal graph is to decrease treewidth such that still structural information can be utilized. In addition to the abstractions and in order to efficiently apply our approach also to (practical) ELPs of high treewidth, we present the following additions: (i) We nest the computation of abstractions and (ii) for hard combinatorial subprograms of (E)LPs, we employ existing standard solvers like (e)clingo.

1 The (E)LP's primal graph comprises the variables (atoms) with an edge between two atoms, whenever appearing together in a rule.

RelatedWork. Treewidth was utilized for the evaluation of standard LPs [Jakl et al., 2009; Hecher, 2022; Fandinno and Hecher, 2021] and competitions [Fichte et al., 2021a]. Abstractions were also stipulated before, but in a different context [Hecher et al., 2020b; Saribatur and Eiter, 2021] or for establishing theoretical results [Ganian et al., 2017]. However, we improve an existing algorithm [Hecher et al., 2020a] and while the solver selp [Bichler et al., 2020] uses TDs for breaking-up rules, our solver is the first implementation of TD-guided solving for ELPs. Studies of measures different from treewidth have been conducted for LPs [Lonc and Truszczynski, 2003; Bliem et al., 2016; Fichte et al., 2019].

2 Preliminaries

Answer Set Programming (ASP). We follow standard definitions of propositional ASP [Brewka et al., 2011] and refer by literal to an atom or its negation. A program (LP) P is a set of rules of the form a1 ∨ · · · ∨ ak ← ak+1, . . . , am,¬am+1, . . . ,¬an. The right side of "←" of a rule is called body; the left side is referred to by head. For a rule r, we let Hr := {a1, . . . ,aℓ}, B+r := {aℓ+1, . . . ,am}, and B-r := {am+1, . . . ,an}. We denote the atoms occurring in a rule r or program P by at(r) or at(P), respectively. An interpretation I ⊆ at(P) satisfies a rule r if (Hr ∪ B-r ) ∩ I ̸= /0, or B+r \ I ̸= /0, or both. I is a model of P if it satisfies all rules of P. The Gelfond-Lifschitz (GL) reduct of P under I is the program P I obtained from P by first removing all rules r with B-r ∩I ̸= /0 and then removing all ¬z where z ∈ B-r from the remaining rules r. Then, I is an answer set of a program P if I is a minimal model of P I ; AS(P) are the answer sets of P.

Example 1. Consider the logic program P = {a∨b←; c←¬d; d ←¬c}. The answer sets of P are {a,c}, {a,d}, {b,c}, and {b,d}.

Tree Decompositions (TDs). For preliminaries in graph theory, we refer to the literature, e.g., [Diestel, 2012]. 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) [Bodlaender and Kloks, 1996] 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). The width of a TD is the cardinality of its largest bag minus one. The treewidth of a graph G is the minimum width over all TDs of G.

3 Probabilistic Reasoning for Epistemic LPs

An epistemic logic program (ELP) Π is an extension of a LP, where each rule body can contain epistemic literals of the form notℓ using literal ℓ and epistemic negation not. Then, at(r) denotes the atoms ocurring in such a rule r, e-at(r) denotes the epistemic atoms, i.e., those used in epistemic literals of r, and a-at(r) refers to the atoms of r not under epistemic negation. We call r purely-epistemic if a-at(r) = /0. We write Kℓ ("ℓ is known") for a literal ℓ, referring to ¬notℓ.

Let I be a set of interpretations over a set A of atoms. Formally, a WVI I is compatible with I if: (1.) I ̸= /0; (2.) for each atom a ∈ I, it holds that for each J ∈I , a ∈ J; (3.) for each ¬a ∈ I, we have for each J ∈ I , a ̸∈ J; and (4.) for each atom a ∈ A with {a,¬a}∩I = /0, there are J, J ′ ∈ I , such that a ∈ J, but a ̸∈ J ′ . Then, a WVI I over at(Π) is a world view (WV) of Π iff I is compatible with the set AS(Π I ). Deciding for WV existence is Σ P 3 -complete [Truszczynski, 2011].

While there are many different semantics [Gelfond, 1991; Truszczynski, 2011; Kahl et al., 2015; Shen and Eiter, 2016], we follow the approach of [Gelfond, 1991], syntactically denoted according to [Morak, 2019]. A world view interpretation (WVI) I for Π is a consistent set I of literals over a set A⊆at(Π) of atoms. Intuitively, every ℓ ∈ I is considered "known" and every a ∈ A with {a,¬a}∩I = /0 is treated as "possible". The epistemic reduct Π I [Gelfond, 1991] of programΠ for a WVI I over A is defined by Π I := {r I | r ∈Π}, where r I denotes rule r where each epistemic literal notℓ over A is replaced by ⊥ if ℓ ∈ I, and by ⊤ otherwise.

Example 2. Consider program Π := P∪{a ←¬Kb; b ← ¬Ka; c ← ¬Kd; d ← ¬Kc; ← ¬Ka,¬K¬a; ← ¬Kb,¬K¬b; ← ¬Ka,¬Kc; ← ¬Ka,¬Kb,Kc; ← Kc,Kd}, where P is given in Example 1. When constructing a WVI I over e-at(Π) one guesses for each atom a ∈ e-at(Π) either (1) a ∈ I, (2) ¬a ∈ I or (3) {a,¬a} ∩ I = /0 as described earlier, i.e., for the three atoms in e-at(Π) we obtain 3 4 possibilities. Consider I1 = {a,d,¬b,¬c} with its epistemic reduct Π I1 = P∪{a; d}. Note that the epistemic reduct is an LP, since by semantics of logic programs, rules r with ⊥ ∈ B+r or ⊤ ∈ B-r can obviously be dropped. Since AS(Π I1 ) = {{a, d}}, compatibility of I1 can be checked trivially which validates I1 as WV of Π. Similarly WVIs I2 = {a, c, ¬b, ¬d} and I3 = {b, c, ¬a, ¬d} can be constructed and correctly validated as WVs, i.e., WVS(Π) = {I1, I2, I3}.

Counting and Reasoning. In this work, we mainly cover the following counting problem, which can then be used as a basis to solve (quantitative) reasoning problems.

Definition 1 (WorldViewCounting). Let Πbe an ELP andQ be a WVI, called query, over atoms at(Π). Then, the problem #ELP(Π,Q) asks to count the number of world views W with Q∩at(Π) ⊆W and {a | ¬a ∈ Q}∩W = /0.

As a special case, where Q = /0, problem #ELP(Π, /0) amounts to counting world views. Interestingly, the problem can be used to reason about the likelihood of an atom or a set of atoms being contained in an arbitrary world view:

Definition 2 (Probability of World ViewAcceptance). Let Π be an ELP and Q be a WVI over at(Π). We define the probability of Q being compatible with a world view by prob(Π,Q) := #ELP(Π,Q) #ELP(Π, /0) .

Consequently, counting allows us to reason about the degree of believing in literals being part of world views. This degree of belief can then be used for accepting literals depending on its probability exceeding a certain value, referred to by probabilistic world view acceptance.

Example 3. Recall Π from Example 2. Given Q := {a,¬b}, the number #ELP(Π,Q) = 2 agrees with the number of WVs including a, but not b. The probability prob(Π,Q) = 2 3 can be used to argue about the chance of a WV of Π containing a but not b, which renders a and ¬b very likely.

4 Abstractions for Dynamic Programming

Algorithms utilizing treewidth for solving a problem in linear time typically proceed by dynamic programming (DP) along a TD. Thereby, the tree is traversed in post-order and at each node t of the tree, information is gathered [Bodlaender and Kloks, 1996] in a table τt , such that the root table yields the final result. A table τt is a set of rows, which are sequences or tuples of fixed length. The actual length, content, and meaning of the rows depend on the algorithm that derives tables.

Before we sketch our algorithm, we need a graph representation. Let therefore Π be an epistemic logic program. Then, the primal graph GΠ uses atoms and epistemic atoms as vertices and it is defined by GΠ := ({a◦ | a ∈ ◦-at(Π),◦ ∈ {a,e}},E), where E := {{a◦ ,b⋆ } | r ∈ Π,a ∈ ◦-at(r),b ∈ ⋆-at(r), {◦, ⋆} ⊆ {a, e}} ∪ {{a a , a e } | a ∈ e-at(Π)}.

Example 4. Figure 1 (left) shows primal graph GΠ for our running example Π, assuming simple edges (no self-loops).

For our purposes, we require suitable abstractions of GΠ. In the following, for S ⊆ at(Π) we denote S e := {s e | s ∈ S}.

Example 5. Given epistemic atoms A= {b,c,d}, the nested primal graph G A Π for our running example Π can be constructed with edges {b e ,c e } and {c e ,d e } through any nonepistemic paths between the two correlating vertices in GΠ, shown in Figure 1 (middle). Observe that G e-at(Π) Π =GΠ.

Definition 3. Assume an abstraction A ⊆ e-at(Π). A non-epistemic path in GΠ is of the form a e ,v1, . . . ,vl ,b e with {v1, . . . ,vl}∩A e = /0. The nested primal graph G A Π is defined by G A Π := (A e ,E ′ ) with E ′ := {{a e ,b e } | {a,b} ⊆ A, there is a non-epistemic path from a e to b e in GΠ}.

Interestingly, these abstractions can be used to separate solving effort between DP and nested (standard) solving. If we used the primal graph, i.e., the trivial abstraction G e-at(Π) Π , then full effort goes into DP (no nested solving). If on the other hand we used the empty abstraction, i.e., G /0 Π = ( /0, /0), then no effort is left for DP (full effort into nested solving). Even further, the TD partitions the effort for nested solving.

Example 6. Figure 1 (right) shows a corresponding TD T = (T,χ) for the nested primal graph G A Π , using ELP Π and abstraction A = {b,c,d} from Example 5. The purelyepistemic rules (constraints) comprising only atoms, whose vertices are in the corresponding bags, are called bag programs, which are evaluated via DP. For node t1, this program is {←¬Kb,¬K¬b}, since χ(t1) = {b e ,c e }; for t2 this is {←Kc,Kd}, since χ(t2) = {c e ,d e }. Intuitively, the remaining rules of Π are subject to nesting. When removing vertices {b e ,c e ,d e } from GΠ one can identify two connected components; one over {a a ,b a ,a e } and the other component over {c a , d a }. Observe that vertices a a , b a , a e are only contained in non-epistemic paths involving epistemic atoms in χ(t1); vertices c a ,d a are only contained in non-epistemic paths using χ(t2). Consequently, our approach defines for every node a nested bag program, which for t1 comprises {a∨ b←;a←¬Kb; b←¬Ka; ←¬Ka,¬K¬a; ←¬Ka,¬Kc; ← ¬Ka,¬Kb,Kc;}, i.e., rules of Π using a,b,c; for t2 this program is {c←¬d; d←¬c; c←¬Kd; d←¬Kc}, comprising rules over atoms c, d. For precise definitions ensuring unique nested bag programs, we refer to [Besin et al., 2021]. This example extends [Besin et al., 2021, Ex. 7] and fixes a typo.

Nested Dynamic Programming for ELPs. The concept of our algorithm is called nested dynamic programming and relies on computing abstractions in order to keep the width of the obtained TD manageable and to separate solving effort between DP and nested solving. Example 6 above shows the smaller (nested) bag programs obtained by using abstractions and nested primal graphs, which basically shows one step of our algorithm. For the outlined nested bag programs, our algorithm recursively computes abstractions and the nested primal graph, thereby providing a way to maintain tables needed for probabilistic reasoning via two counting problems of Definition 2. So in contrast to enumeration-based methods, our approach efficiently counts by materializing and combining solution parts (and not whole solutions).

For hard combinatorial subproblems that turn up during nesting, where the counts are not needed or not many solutions are expected, we delegate the task to standard (CDCLbased) solvers. Similarly, if a certain nesting depth is reached, further nesting and decomposing might not be beneficial, so subproblems are also delegated to standard solvers, thereby efficiently combining DP and search-based solving. For details we refer to the long version [Besin et al., 2021].

5 Implementation &Experiments

We implemented our algorithm, resulting in the solver nestelp 2 , which is written in Python3. It is based on the system nesthdb that was presented for variants of model counting [Hecher et al., 2020b]. For manipulating tables during DP, nestelp uses the open source database Postgres 12, which supports instant parallelization and was run on a tmpfsramdisk as intended by nesthdb. In order to compute TDs we use htd [Abseher et al., 2017], which for every instance outputs TDs of decent widths in a runtime below some seconds. For solving decision problems of (epistemic) logic programs we utilize clingo 5.4 (eclingo 0.2). For finding good abstractions, we employ a logic program (available on github) using built-in optimization of clingo, where we take the best results after running at most 35 seconds. Our implementation supports both world view counting as given in Definition 1 as well as probabilistic world view acceptance of Definition 2.

2 nestelp is readily available at github.com/viktorbesin/nestelp.

In our benchmarks we compare wall clock runtime of nestelp and eclingo [Cabalar et al., 2020], where a timeout is considered to occur after 1200 seconds and each solver was granted 16GB of main memory (RAM) per run. We restricted our solver to 12 physical cores. In single core mode (sc) of nestelp, only one physical core was used, allowing us to compare the performance with other single-core solvers.

We consider the following existing and generated instances.

Classic-Scholarship. As in previous works [Cabalar et al., 2020], this is a set of 25 non-ground ELP programs encoding the Scholarship Eligibility problem [Gelfond, 1991] for 1-25 students, where all entities are independent from each other. If a students eligibility is not determined by the plain logic rules, an epistemic rule implies the interview of the student.

Yale-Shooting. This is a set of 12 non-ground ELP programs [Cabalar et al., 2020] for the Yale Shooting problem [Hanks and Mcdermott, 1986]. For each instance the initial state, i.e., if a gun is initially loaded or not, is unknown. Large-Scholarship (L-S). While classic-scholarship is limited to 25 instances, large-scholarship can be configured for an arbitrary number of students. We implement a generator and use existing instances to initialize more students. This set consists of 500 instances ranging from 5 to 2500 students. Many-Scholarship (M-S). In contrast to classicscholarship, where all students are in one unique WV, here a students eligibility is ranked (low or high chances), yielding many WVs per student. This set has 500 instances.

5.1 Experimental Results

For the classic-scholarship and yale-shooting problems, we observed nestelp keeping up with a traditional solver like eclingo, but, as expected, nestelp introduces additional overhead by the creation of tables and the general build-up for dynamic programming. Small instances do not benefit from that process, that is why we expected such results. However, the number of solved instances is the same for both systems.

The line plot in Figure 2 (left) shows an outstanding performance of nestelp for instances L-S and even M-S. Both instance sets allow their instances to be arranged into decompositions with low treewidth, representing instances where nestelp can exploit all its features. Further it can be seen that parallelism of nestelp has better performance than the single-core experiments (nestelp (sc)), indicating that there are enough independent nodes such that parallelism is beneficial. Even with the fair comparison to eclingo, the solver nestelp proves to handle large-scale instances well.

As it can be seen in the cactus plot in Figure 2 (right), the effort for probabilistic reasoning is very small in comparison to world view counting. Since nestelp intuitively only processes sub-calls where they are justified, i.e., only when there are any world views, there is little to no difference in the plot. We are certain that the visible differences are due to scattering factors like query optimization and CPU clocking. To summarize, the systems performance can be described quite competitively with a higher number of solved instances in similar or even shorter runtimes. Furthermore, consider that nestelp uses eclingo for sub-calls, so every revision of eclingo will improve our system as well.

6 Conclusion

In this work, we count world views of epistemic logic programs (ELPs), which is extended to probabilistic reasoning. We took up ideas of a theoretical algorithm that utilizes treewidth and turned this into an efficient solver. Our solver nestelp works on iteratively computing and refining (graph) abstractions of the ELP and counting world views over epistemic atoms of the abstract program. For counting and probabilistic reasoning, nestelp seems to scale well. We plan on further optimizing nestelp, which automatically improves with the availability of faster (E)LP solvers. We expect "tightness" notions, e.g., [Fandinno and Hecher, 2021; Hecher, 2022], to aid in improving performance. Recent complexity insights for treewidth [Fichte et al., 2020; Fichte et al., 2021b] renders our approach useful for other formalisms.

Acknowledgments

This research has been supported by the Vienna Science and Technology Fund (WWTF) grant ICT19-065, and by the Austrian Science Fund (FWF) grants P32830 and Y698.