Treewidth-Aware Complexity for Evaluating Epistemic Logic Programs

1 Introduction

The language of epistemic specifications [Gelfond, 1991; Gelfond and Przymusinska, 1993; Gelfond, 1994] (a.k.a. epistemic logic programs), proposed by Gelfond in 1991, extends disjunctive logic programs (under the stable model semantics; [Gelfond and Lifschitz, 1988; Gelfond and Lifschitz, 1991]) with modal constructs called subjective literals. The introduction of this extension was originally motivated by the need to correctly represent incomplete information in programs that have several stable models. Using subjective literals, it is possible to check whether a regular literal is true in every or some stable model of the program, those models are being collected in a set called world view. This allows for representing, within the language, whether some proposition should be understood accordingly to the open or the closed world assumption. See the work by [Fandinno et al., 2021] for a recent survey about epistemic logic programs (ELPs).

In general, deciding whether an epistemic logic program has a world view is ΣP3 -complete [Truszczy´nski, 2011]. However, for the head-cycle-free fragment, it complexity is reduced to ΣP2 -complete. Though the complexity of this fragment is the same as disjunctive logic programs under the stable models semantics, the language of epistemic logic programs allows us to write more natural representations of several problems in the polynomial hierarchy than previous logic programming techniques such as saturation [Eiter and Gottlob, 1995]. Examples of this are (length-bounded) conformant planning [Kahl et al., 2020; Cabalar et al., 2021] and action reversibility [Faber et al., 2021].

In this paper, we conduct a more fine-grained complexity analysis of epistemic logic programs in terms of parameters of a problem [Cygan et al., 2015]. In particular, we focus on the influence of the parameter treewidth for solving objectively tight and head-cycle-free epistemic programs. An epistemic logic programs is objectively tight if its dependency graph does not have positive cycles that involve exclusively objective atoms. For these classes, we show that deciding the existence of a world view is 22O(k) · poly(|A(Π)|) and 22O(k·log(k)) · poly(|A(Π)|), respectively, where k is the treewidth. That is, we can solve the consistency problem in polynomial time in the program size while being superpolynomial only in its treewidth. We also show that, under the Exponential Time Hypothesis (ETH) [Impagliazzo et al., 2001], our characterizations are tight, that is, consistency for these classes cannot be decided in time 22o(k) · poly(|A(Π)|) and 22o(k·log(k)) · poly(|A(Π)|), respectively.

Table 1 shows our results. So far, only the classical complexity [Shen and Eiter, 2016] as well as the parameterized complexity for treewidth on full ELPs are known [Hecher et al., 2020]. Our fine-grained complexity results on the presented ELP fragments are not only exponentially better, they utilize novel reductions via quantified Boolean formulas that ensure treewidth-guarantees. This allows us to demonstrate treewidthawareness of the completion used by modern solvers.

2 Preliminaries

We assume familiarity with complexity [Papadimitriou, 1994], graph theory [Bondy and Murty, 2008], and logic [Biere et al., 2009]. We also assume familiarity with logic programs under the stable model semantics [Gelfond and Lifschitz, 1988].

Epistemic Logic Programs. Let A be a set of atoms. An objective literal is either an atom a ∈ A (positive literal), an atom preceded by negation ¬a (negative literal) or a truth constant. 1 A subjective literal is an expression Ka s.t. a ∈ A. A rule r is an implication of the form a1 ∨ · · · ∨ an ← L1 ∧ · · · ∧ Lm (1) with n ≥ 1 and m ≥ 0, where each ai is an atom in A (or constant ⊥) and each Lj a literal. If n = 1, then rule r is called normal. The left-hand disjunction of (1) is called the rule head and its set of atoms is abbreviated by Hr. The right hand side of (1) is called the rule body and the set of its literals is abbreviated as Br. We denote by B+ r the set of all positive objective literals in Br, by Br the set of all negative objective literals in Br, and Bs r the set of all subjective literals in Br. By abuse of notation, we also write Br, B+ r , Br , and Bs r to denote the conjunction of all literals in those sets. Furthermore Bc r is ⊥ if ⊥ occurs in Br and ⊤ otherwise. Atoms in A appearing in a rule r are given by A(r). Further, A(Π) :=A. Rule r is called objective if its literals are objective; r is non-negative if it is normal and either all objective literals are atoms or Hr={⊥}.

A program Π is a set of rules and it is said to be objective, normal, or non-negative if all its rules are objective, normal, or non-negative, respectively. The (positive) dependency digraph DΠ of a program Π is the directed graph defined on the set of atoms from ⋃r∈Π Hr ∪B+ r , where there is a directed edge from vertex a to vertex b iff there is a rule r ∈ Π with a ∈ B+ r and b ∈ Hr. Recall that an objective program is called tight [Lifschitz, 1996] if its positive dependency graph contains no cycle. We generalize this notion to programs with subjective literals as follows. A program Π is (objectively) tight if DΠ contains no cycle. Further, program Π is called head-cycle-free (HCF) if DΠ contains no cycle consisting of at least two atoms of the head Hr of a rule r.

Note that according to our definition, the expression a ← K¬b (2) is not a valid rule. This restriction simplifies the narrative of the paper and does not limit the expressiveness of the language, because we can simulate these more general rules using auxiliary atoms. In our particular example, we can replace (2) with the set {a ← Knot b, not b ← ¬b}, where not b is a fresh auxiliary atom. Similarly, a ← ¬Kb is not a rule according to our narrow definition, but it can be encoded by rules a ← ¬k b and k b ←Kb, where k b is an auxiliary atom not occurring anywhere else in the program.

For a non-empty set of propositional interpretations W, we write W |= Ka if a ∈ I for all I ∈ W. We write W ̸|= Ka otherwise. Given a program Π, by ΠW we denote the objective program obtained from Π by replacing each subjective literal L by ⊤ if W |= L and by ⊥ otherwise. W is called a world view (WV) of Π if and only if the set of stable models of ΠW is W.

1 For brevity, we use constants with their usual meaning.

Tree Decompositions and Treewidth. For a rooted (directed) tree T = (N, A) with root root(T) and a node t ∈ N, we let chldr(t) be the set of all nodes t′ , which have an edge (t, t′ ) ∈ A. Let G = (V,E) be a graph. A tree decomposition (TD) of a graph G is a pair T = (T, χ), where T is a rooted tree, and χ is a mapping that assigns to each node t of T a set χ(t) ⊆ V , called a bag, such that:

Then, define width(T ) :=maxt of T |χ(t)|-1. The treewidth tw(G) of G is the minimum width(T ) over all tree decompositions T of G. Observe that for every vertex v ∈ V , there is a unique node t∗ with v ∈ χ(t∗ ) such that either t∗ = root(T) or there is a node t of T with chldr(t)={t∗ } and v /∈ χ(t). We refer to the node t∗ by last(v). For arbitrary but fixed w ≥ 1, it is feasible in linear time to decide if a graph has treewidth at most w and, if so, to compute a TD of width w [Cygan et al., 2015]. In this work, we assume only TDs (T, χ), where for every node t of T , |chldr(t)| ≤ 2. Such a TD can be obtained from any TD in linear time without increasing the width.

Treewidth-Dependent Tightness. The primal graph GΠ of a program Π has as vertices the atoms A(Π) with an edge between two vertices, whenever these vertices appear together in A(r) of a rule r ∈ Π. For an atom a ∈ A(Π) we denote the strongly-connected component (SCC) of a by scc(a), which is the ⊆-largest set C ⊆ A(Π) with a ∈ C such that for every two distinct atoms u, v in C there is a directed path from u to v in DΠ. Then, the tightness width of a TD T =(T, χ) of GΠ, is maxt of T maxx∈χ(t) |χ(t) ∩ scc(x)|. The tightness treewidth ι of Π is the smallest tightness width among every TD of width O(tw(GΠ)). If Π has tightness treewidth ι, we call Π "ι-tight" [Fandinno and Hecher, 2021].

Quantified Boolean Formulas. Let ℓ be a positive integer, which we call (quantifier) rank later, and ⊤ and ⊥ be the constant evaluating to 1 and 0, respectively. For a Boolean formula F, we abbreviate by var(F) the variables occurring in F and F(X1, . . . ,Xl) to indicate that X1, . . . ,Xl ⊆ var(F). A quantified Boolean formula ϕ (in prenex normal form), QBF for short, is an expression of the form ϕ = Q1X1.Q2X2. · · · QℓXℓ.F(X1, . . . , Xℓ), where for 1 ≤ i ≤ ℓ, we have Qi ∈ {∀, ∃} and Qi ̸= Qi+1, the Xi are disjoint, non-empty sets of Boolean variables, and F is a Boolean formula. We let matrix(ϕ) := F and we say that ϕ is closed if var(matrix(F)) = ⋃i∈ℓ Xi. We evaluate ϕ by ∃x.ϕ ≡ ϕ[x ↦→ 1] ∨ ϕ[x ↦→ 0] and ∀x.ϕ ≡ ϕ[x ↦→ 1] ∧ ϕ[x ↦→ 0] for a variable x. We assume that matrix(ϕ) = ψCNF ∧ψDNF, where ψCNF is in CNF (disjunction of conjunctions of literals) and ψDNF is in DNF (conjunction of disjunctions of literals). Then, depending on Qℓ, either ψCNF or ψCNF is optional, more precisely, ψCNF might be ⊤, if Qℓ = ∀, and ψDNF is allowed to be ⊤, otherwise. The problem ℓ-QSAT asks, given a closed QBF ϕ of rank ℓ, whether ϕ ≡ 1.

Treewidth for QBFs. For a given QBF ϕ with matrix(ϕ) = ψCNF ∧ ψDNF, we define the primal graph Gϕ = Gmatrix(ϕ), whose vertices are var(matrix(ϕ)). Two vertices of Gϕ are adjoined by an edge, whenever the corresponding variables share a clause of ψCNF or a term of ψDNF, respectively.

Let tower(i, p) be tower(i-1, 2p ) if i > 0 and p otherwise. Further, we assume that poly(n) is any polynomial for a given positive integer n. The following result is known for QSAT.

Proposition 1 ([Chen, 2004]). For any arbitrary QBF ϕ of quantifier rank ℓ > 0, the problem ℓ-QSAT can be solved in time tower(ℓ,O(tw(Gφ))) · poly(|var(ϕ)|).

Assuming the exponential time hypothesis (ETH) [Impagliazzo et al., 2001], one cannot significantly improve this runtime in the worst case. Intuitively, ETH implies that SAT=1-QSAT can not be decided in time better than 2o(|var(φ)|) for an arbitrary formula φ.

Proposition 2 ([Fichte et al., 2020]). Under ETH, for any arbitrary QBF φ of quantifier rank ℓ > 0, problem ℓ-QSAT cannot be solved in time tower(ℓ, o(tw(Gφ))) · poly(|var(φ)|).

The result still holds for QBFs whose treewidth comprises variables Vℓ of the inner-most quantifier, i.e., we may assume every TD bag contains constantly many variables not in Vℓ.

3 Epistemic Logic Programs as QBFs

In this section, we show how we can encode ELPs as QBFs.

Programs as formulas. We present a way to compute the stable models of a program by translating it into a propositional formula. These translations are straightforward generalizations of the completion [Clark, 1977] and level mappings [Niemel¨a, 2008] to programs with subjective literals.

Let us denote by K := {ka | a ∈ A(Π)} a set of fresh new atoms that do not occur in programΠ, that is K∩A = ∅, where we refer to A(Π) by A. Given any expression E (program, set, formula, etc.), by k(E) we denote the result of replacing each occurrence of a subjective literal of the formKa by atom ka.

Given a program Π, by COMP[Π] we refer to the completion, denoting the conjunction of the following formulas:

where Hr(a) := ∧h∈Hr\{a} ¬h. Note that COMP[Π] is analogous to the completion used by ASP solvers [Gebser et al., 2012; Alviano et al., 2019; Lin and Zhao, 2004; Lierler and Maratea, 2004], but with the extra atoms in k(Bs r ) to represent the subjective literals. These atoms behave as "externals" that can be fixed in order to compute the world views of the program. We formalize now this intuition.

Recall that for objective programs that are tight [Lifschitz, 1996], its stable models coincide with the classical models of its completion. We extend this to our notion of objectively tight programs below. Note that objective tightness only considers positive objective literals and is different from the notion of epistemically tight programs defined by [Cabalar et al., 2020], so positive dependencies among subjective literals are allowed.

Proposition 3. Let W be a non-empty set of propositional interpretations and Π be a program such that Π is objectively tight. Then, W is a world view of Π iff W is the set of all classical models of COMP[ΠW ].

Proof. If Π is objectively tight, then ΠW is tight. The result follows immediately from Fages' theorem [Fages, 1994].

Definition of SM[Π]. We extend this to normal (HCF) programs as follows. If Π is tight, we define SM[Π] to be COMP[Π]. Otherwise, SM[Π] is the conjunction of COMP[Π], where Formulas (3) are replaced as follows, using a strict partial ordering ≺2 among atoms [Lin and Zhao, 2003; Janhunen, 2006].

Proposition 4. Let W be a non-empty set of propositional interpretations and Π be a program. Then, W is a world view of Π iff W is the set of classical models of SM[ΠW ].

Proof. If Π is objectively tight, the result follows from Proposition 3. Otherwise, it holds by [Niemel¨a, 2008, Thm. 1].

We can also rewrite the right hand side of the equivalence of this proposition in terms of the auxiliary atoms in K as follows. If W is a non-empty set of propositional interpretations, then by k(W) we denote k(W) := {ka | a ∈ I for all I ∈W}.

Furthermore, if L is a subset of K, by F L, we denote the formula obtained from F by replacing each occurrences of atom ka by ⊤ if ka is in L and by ⊥ otherwise. Intuitively, F L formalizes the epistemic reduct applied to the formula corresponding to a program.

Corollary 5. Let W be a non-empty set of propositional interpretations and Π be a program. Then, W is a world view of Π iff W is the set of classical models of SM[Π]k(W) .

World views as QBFs. We now show howwe can characterize the world views of a program Π as a QBF formula. Our characterization is similar to the characterization of Autoepistemic Logic given by [Egly et al., 2000], but makes use of three modules that use the SM[Π] formula.

Proposition 6. Let L be a subset of K. The following holds:

1. L satisfies Fc[Π] iff SM[Π]L has a stable model;
2. L satisfies Fk [Π] iff, for all ka ∈ L, every stable model of SM[Π]L satisfies a;

2 Ordering ≺ has to be irreflexive, asymmetric, and transitive.

1. L satisfies Fp[Π] iff, for all ka ∈ K \ L, some stable model of SM[Π]L does not satisfy a.

The following formula characterizes world views:

Proposition 7. If W is a world view of Π, then k(W) satisfies F[Π]. Conversely, if L satisfies F[Π], then the set of classical models of SM[Π]L is a world view of Π.

Proof. Assume that W is a world view of Π. Then, from Corollary 5, W is the set of classical models of SM[Π]k(W) and it is non-empty. From Proposition 6, this implies that k(W) satisfies the three conjuncts of F[Π] and, thus, F[Π]. Conversely, assume that L satisfies F[Π] and let W be the set of classical models of SM[Π]L. Then, from Corollary 5, W is non-empty and k(W) = L. That is, W is the set of classical models of SM[Π]k(W) . From Corollary 5, this implies that W is a world view of Π.

Formula F[Π] can be transformed to a closed QBF in prenex normal form as follows, where K and A, as used in Fc[Π], are existentially quantified. Since the existentially quantified variables A in Fp[Π] depend on the variable a ∈ A of the outer-most conjunction, each conjunct has to be over fresh variables. Thereby every b ∈ A with b ̸= a appearing in the conjunct is replaced by a fresh variable ba, resulting in fresh sets Aa of existentially quantified variables. Finally, every universally quantified variable a ∈ A appearing in Fk[Π] has to be replaced by a fresh copy a′ , resulting in a formula F ′k [Π] over variables K and A′ (universally quantified).

4 Decomposition-Guided Reductions for ELPs

Inspired by related work [Hecher, 2022], a decompositionguided (DG) reduction R is a function that takes both a program Π and a TD T = (T, χ) of GΠ, and returns a QBF φ.

The way a DG reduction is constructed for Π, it yields a TD T ′ = (T, χ′ ) of Gφ of the resulting QBF φ. So, the idea of such a DG reduction is to construct φ from a TD node's point of view. Thereby, for each node t of T, the constructed bag χ′ (t) depends on the original bag χ(t), but also on the constructed bags of its child nodes. This gives rise to a function fR that takes a TD node t, its bag χ(t) and a set χ′ (chldr(t)) := {χ′ (ti) | ti ∈ chldr(t)} of constructed bags for the child nodes of t. Figure 1 illustrates such a function fR taking node t, its original bag χ(t), as well as χ′ (chldr(t)), to construct each bag χ′ (t), which then corresponds to f(t, χ(t), χ′ (chldr(t))).

Then, since width(T ) is bounded by O(maxt of T (|χ(t)|)), also the treewidth of the resulting QBF is at most O(maxt of T (|f(t, χ(t), χ′ (chldr(t))|)). So, these DG reductions are TD-guided; their construction adheres to dynamic programming, thereby giving treewidth guarantees.

Decomposition-Guided ProgramCompletion. As an example of DG reductions, we establish that Clark's completion [Clark, 1977], as created by ASP solvers, e.g., [Gebser et al., 2012; Alviano et al., 2019; Lin and Zhao, 2004; Lierler and Maratea, 2004] can be turned treewidth-aware. The completion ensures that rules are not only satisfied, but we have justifications for every atom in a stable model. For tight programs this suffices to characterize stable models. So, let Π be a tight program and recall the completion COMP[Π].

In terms of treewidth overhead, Formulas (3) are not an issue and can be easily converted into CNF without auxiliary variables. However, in case there are many rules containing a, Formulas (4) might be problematic. We resolve this issue by means of auxiliary variables introduced in the decompositionguided reduction. To this end, let T = (T, χ) be a TD of GΠ. We use auxiliary variables of the form a≤t for every atom a ∈ A(Π) and node t of T with a ∈ χ(t), and we guide evaluations along TD T . By definition of TDs, for every rule r ∈ Π there is a node t of T with A(r) ⊆ χ(t). For every node t, we refer by Πt to a subset of those rules at t, i.e., Πt ⊆{r ∈Π | A(r) ⊆ χ(t)}. Then, instead of Formulas (4), we create the following.

Intuitively, Formulas (6) ensure that whenever a holds, a≤t′ holds as well for a node t′ of T whose bag contains a such that the parent bags do not contain a. Then, Formulas (7) take care that whenever a≤t holds for a node t, either some ar holds with r ∈ Πt or a≤t′ holds for t′ ∈ chldr(t) below t. We refer to this version of the completion, comprising Formulas (3), (6), and (7), by COMP[Π, T ], which can be converted to CNF without additional auxiliary variables.

This slightly adapted construction of Clark's completion as used by ASP solvers indeed linearly preserves the treewidth.

Proposition 8 (TW-Aware Completion). Let Π be a program and T = (T, χ) be a TD of GΠ. Then, the completion Π′ = C(Π, T ) linearly preserves the (tree)width, i.e., there is a TD T of GΠ′ with |width(T ′ )| ≤ |width(T )|.

Proof. Without loss of generality, we assume that |Πt| ≤ 1 for every node t of T and that for every rule r there is a unique node t with r ∈ Πt, which can be established by adding intermediate auxiliary TD nodes. Further, we assume for every node t of T that |chldr(t)| ≤ 2, which can be also obtained via constructing auxiliary TD nodes. Since Π′ was constructed by means of a DG reduction, it easily gives rise to a TD T ′ := (T, χ′ ) of GΠ′ . Precisely, we define χ′ (t) := χ(t)∪{ar | r ∈ Πt, a ∈ Hr} ∪ {a≤t | a ∈ χ(t)} ∪ {a≤t′ | t′ ∈ chldr(t), a ∈ χ(t′ ) ∩ χ(t)} for every node t of T. Indeed T ′ is a welldefined TD of GΠ′ . Further, since |Πt| ≤ 1 and |chldr(t)| ≤

2, we have |χ(t′ )| ≤ 4 |χ(t)| + 1. Consequently, also for width(T ) = tw(GΠ), we have tw(GΠ′ ) ∈ O(tw(GΠ)).

Note that while treewidth-aware variants of the completion has been presented before [Fandinno and Hecher, 2021; Eiter et al., 2021], here we provide a different viewpoint, showing that the existing built-in reduction used by ASP solvers is almost treewidth-aware, i.e., only additional auxiliary variables are required to break-up long clauses. As above, one could extend our technique to HCF programs using a strict partial ordering ≺t among bag atoms [Fandinno and Hecher, 2021] for a TD node t. Below we pursue a different approach.

Definition of SM[Π, T ]. If Π is a tight program, we define SM[Π, T ] to be COMP[Π, T ]. Otherwise, i.e., for HCF programs Π, we first create a tight programΠ′ in a treewidthaware way, which will be discussed afterwards in Section 5.4.

5 Treewidth-Aware QBF Encodings for ELPs

In order to design treewidth-aware encodings, we follow the basic modules from Section 3, thereby utilizing decomposition-guided reductions of the previous section. Let Π be a tight program over atoms A = A(Π) and K be the set of fresh atoms for Π as defined in the previous section. Then, we solve the world view existence problem by ∃K.F[Π] using the QBF defined above. However, there is no guarantee on the treewidth of the primal graph of this formula.

In the following, we provide for each of the formulas Fc[Π], Fk [Π], Fp[Π] a decomposition-guided variant. To this end, let T = (T, χ) be a TD of GΠ in order to define three DG reductions constructing QBFs for solving WV existence on Π with the help of T . This will allow us then to evaluate problem parts locally for each node of T, thereby ensuring that the (tree)width is not increased arbitrarily. Precisely, we let F[Π, T ] := ∃K.Fc[Π, T ] ∧ Fk [Π, T ] ∧ Fp[Π, T ] and we define the three conjuncts in the following.

For the consistency part, i.e., in order to encode Fc[Π] in a way that is decomposition-guided, we define Fc[Π, T ] := ∃A. SM[Π, T ]. Indeed, Fc[Π, T ] linearly preserves treewidth.

Lemma 9. Given a tight program Π and a TD T = (T, χ) of GΠ. Then, the treewidth of GFc[Π,T ] is in O(width(T )).

Proof. We define a TD T ′ = (T, χ′ ) of GFc[Π,T ], where for every t in T we let χ′ (t) := χ(t) ∪ {ar | r ∈ Πt, a ∈ Hr} ∪ {a≤t | a ∈ χ(t)} ∪ {a≤t′ | t′ ∈ chldr(t), a ∈ χ(t) ∩ χ(t′ )} ∪ {ka | ka ∈ k(Bs r ), r ∈ Πt}. Observe that T ′ is well-defined; indeed all rules of SM[Π, T ] are covered, i.e., the variables of every clause of COMP[k(Π), T ] appear in at least one common bag of T ′ .

The definition of the remaining formulas Fk [Π, T ] and Fp[Π, T ] is more involved. Intuitively, in order to locally evaluate both formulas for each node of T , we require additional information that is guided along T , which we develop next.

5.1 Encoding Knowledge

Observe that in Fk [Π], the formula uses the result of SM[Π], which, when solving parts locally along the tree decomposition T (bottom-up), is not available until the root of T has been processed. Consequently, we require auxiliary variables that store and maintain this information.

To this end, we use auxiliary variables usat≤t for every node t of T, that intuitively holds the information whether up to t, those parts of Π that have been encountered so far, are inconsistent. We define U := {usat≤t | t in T} and we construct Fk [Π, T ] := ∀(A ∪ U).Fup[Π, T ] ∧ Fu[Π, T ], where Fup[Π, T ] is defined by means of Formulas (8)-(11), resulting in a DNF.

Intuitively, Formulas (8) ignore cases for nodes t with Πt, where the inconsistency is not properly propagated from a node to its child nodes. Then, Formulas (9) do the same for nodes t with Πt ̸= ∅, i.e., inconsistency for a node t requires inconsistency below t or in t. Formulas (10) and (11) encode the other direction, where inconsistency is underclaimed, i.e., not set in a node or not propagated from a node to its parent.

Further, we encode Fu[Π, T ] in CNF, comprising a conjunction of Formulas (12).

Formulas (12) ensure that either the current assignment proves inconsistency or whenever an atom a ∈ A(Π) is known, it has to be set to true.

Theorem 10 (Correctness). Let Π be a tight ELP and T = (T, χ) be a TD of GΠ. Then, given any assignment α : K → {0, 1} we have that Fk [Π][α] is valid iff Fk [Π, T ][α] is valid.

Proof (Sketch). =⇒: Assume that Fk [Π][α] is valid. Then for any assignment β : A → {0, 1}, we have that Fk [Π][α][β] evaluates to true. From this we show that for any assignment β′ : U → {0, 1} we have Fk [Π, T ][α][β][β′ ] evaluates to true as well. Assume towards a contradiction that this is not the case. However, Formulas (8) and (9) ensure that assignments β′ are valid, where β′ (usat≤t) = 1 for a node t but neither β′ (usat≤t′) = 1 for any node t′ ∈ chldr(t), nor a rule in Πt is dissatisfied. Further, Formulas (10) and (11) ensure that whenever despite inconsistency up to a node t, β′ (usat≤t) = 0. Consequently, we only need to consider remaining cases, where usat≤t is maintained properly for every node t of T . Then, assuming that any Formula (12) is dissatisfied due to β′ , we have Fk [Π][β] is dissatisfied, contradicting our assumption. ⇐=: The other direction works similarly.

Further, we show that it is treewidth-aware and that the reduction causes at most a linear overhead.

Lemma 11 (Linear TW-Awareness). Let Π be a tight ELP and T = (T, χ) be a TD of GΠ. Then, the treewidth of GFk [Π,T ] is in O(width(T )).

Proof. We construct a TD T ′ = (T, χ′ ), where we define χ′ as follows. For every node t of T, we let χ′ (t) := χ(t) ∪ k(χ(t))∪{usat≤t, usat≤root(T)}∪{usat≤t′ | t′ ∈ chldr(t)}. Observe that T ′ is well-defined and that since |chldr(t)| ≤ 2, we have width(T ′ ) ∈ O(width(T )).

5.2 Encoding Possibility

In order to check whether an assumption on known atoms in K is fulfilled, it suffices to find counterexamples among all these modal atoms. This is different from the assumptions that are not known, since one has to find an individual witness model, over dedicated variables, as seen in the "possibility" part Fp[Π]. However, this is problematic for treewidth, since these (linearly) many models are not bounded by the treewidth. To resolve this issue, we are going to guide these witness models along the tree decomposition. In other words, in the following we are utilizing synergies between all witness models, restricted to the bags of a node.

Again, we focus on the easier case assuming that Π is tight. Towards defining Fp[Π, T ], we use auxiliary variables of the form It for every node t of T and every interpretation I ⊆ 2χ(t) restricted to χ(t), which we address by I⋆ := {It | t in T, I ⊆ 2χ(t) }. Observe that therefore the number of variables in I⋆ is exponential in the bag size |χ(t)|. However, since we do not use these variables under an innermost universal quantifier block, our approach therefore does not the complexity, as we will see later. Precisely, we construct Fp[Π, T ] := ∃I⋆.Fs[Π, T ], where Fs[Π, T ] is defined by means of Formulas (13)-(17) below.

Intuitively, our approach is to not maintain an individual assignment for every variable in K, which might increase the treewidth due to many copies. Instead, using I⋆, we store all potential assignments restricted to a bag, which indicates assignments that satisfy the program up to t. Then, Formulas (13) ensure that assignments not satisfying Πt cannot be claimed stable models. Formulas (14) additionally handles the case where the assignment of specific atoms in K is needed in order to reach satisfiability. Formulas (15) and (16) ensure that whenever an assignment I is claimed to hold, there is a corresponding matching assignment in every child node as well as parent node (if exist). Thereby, Formulas (15) propagate from a node t to compatible predecessor interpretations, and Formulas (16) propagate to the parent node. Finally, Formulas (17)

model the requirement that whenever ¬ka holds, some stable model that does not contain a is ultimately forced to hold.

Theorem 12 (Correctness). Let Π be a tight ELP and T = (T, χ) be a TD of GΠ. Then, given any assignment α : K → {0, 1} we have that Fp[Π][α] is valid iff Fp[Π, T ][α] is valid.

Proof (Sketch). =⇒: Assume that Fp[Π][α] is valid. Then, for every ka with α(ka) = 0, there is an assignment βa : A(Π) → {0, 1} such that SM[Π][α][βa] = COMP[Π][α][βa] evaluates to true. From this we construct an assignment β′ such that Fp[α][β′ ] evaluates to true. For every node t and a ∈ A(Π), we set β′ (It) := 1, whenever I = χ(t) ∩ β-1 a (1) and β′ (It) := 0 otherwise. Then, by construction of β′ , we have that Fp[Π, T ][α][β′ ] evaluates to true. ⇐=: The other direction works as follows. We assume an assignment β′ such that Fp[Π, T ][α][β′ ] evaluates to true and for every ka ∈ K with α(ka) = 0, we construct an assignment βa such that SM[Π][α][βa] = COMP[Π][α][βa] evaluates to true. To this end, we construct an assignment I, consisting of the union over one assignment It for every node t of T such that β′ (Itt) = 1 and It ∩ χ(t′ ) ∩ It′ ∩ χ(t) for every child node t′ ∈ chldr(t). Since Fp[Π, T ][α][β′ ] evaluates to true, such an assignment I with a /∈ I has to exist by construction of this formula. Consequently, one can show that then SM[Π][α][βa] = COMP[Π][α][βa] evaluates to true.

The reduction is treewidth-aware, i.e., while it causes an overhead in terms of treewidth, this is bounded by 2O(w) .

Lemma 13 (TW-Awareness (single exponential)). Let Π be a tight ELP and T = (T, χ) be a TD of GΠ. Then, the treewidth of GFp[Π,T ] is in 2O(width(T )) .

Proof. We construct a TD T ′ = (T, χ′ ), where we define χ′ as follows. For every node t of T, we let χ′ (t) := χ(t) ∪ k(χ(t)) ∪ {It | I ∈ 2χ(t) } ∪ {I ′ t′ | t′ ∈ chldr(t), I ′ ∈ 2χ(t′ ) , I ∈ 2χ(t) , I ∩ χ(t′ ) = I ′ ∩ χ(t)}. It is easy to see that T ′ is well-defined and that indeed since |chldr(t)| ≤ 2, we have that width(T ′ ) ∈ 2O(width(T )) .

5.3 Merging Consistency, Knowledge &Possibility Overall, we obtain the following runtime result.

Lemma 14 (Runtime). Let Π be any tight program and T = (T, χ) be a TD of GΠ of width w. Then, the formula F[Π, T ] can be computed in time 2O(w) · poly(|A(Π)|).

Proof. The runtime is due to the 2w many different variables of the form It in the construction of formula Fp[Π, T ].

The formula F[Π, T ] can then be used to solve world view existence and to obtain the following upper bound result.

Theorem 15 (Upper Bound for tight ELPs). Let Π be any tight program, whose treewidth of primal graph GΠ is w. Then, WV existence for Π can be decided in time 22O(w) · poly(|A(Π)|).

Proof. We construct both a TD T of GΠ of width 5 · w [Bodlaender et al., 2016] as well as the formula F[Π, T ], in time 2O(w) · poly(|A(Π)|). The constructed formula is an instance of 2-QSAT can be solved in the desired runtime, namely 2(2O(w) ) +2(2O(w) ) · 22O(w) · poly(|A(Π)|), see Proposition 1, since by Lemma 11 the treewidth over the inner-most (universally) quantified variables is linear in w.

However, for tight programs it is not expected that we can significantly improve this result, which we show below.

Theorem 16 (Lower Bound for tight ELPs). Let Π be any tight program, whose treewidth of the primal graph GΠ is w. Then, unless ETH fails, WV existence for Π cannot be decided in time 22o(w) · poly(|A(Π)|).

Proof. Let ∃X.∀Y.φ be any QBF with φ being in DNF and var(φ) = X ∪ Y . From this we construct an ELP Π over the set {sat, x, ˜x | x ∈ var(φ)} of atoms as follows. For every variable x ∈ X, we construct the rules x ← Kx, ˜x ← K ˜x, ⊥ ← x, ˜x, and ⊥ ← ¬x, ¬˜x. For every y ∈ Y , we construct rules y ← ¬˜ y and ˜ y ← ¬y. Further, we build the rule ⊥ ← ¬Ksat, which can be easily transformed to our narrow syntax using K without negation, by means of auxiliary atoms, as explained in the preliminaries. Then, for each term d ∈ φ consisting of literals l1, . . . , li, we construct: sat ← ˆl1, . . . ˆli, where for a literal l we let ˆl := ˜a if l = ¬a and ˆl := l otherwise. Observe that Π is normal and even tight. The reduction clearly runs in polynomial time.

Indeed, the reduction is correct. We show that there is a one-to-one correspondence between satisfying assignments over X of Q and world views of Π. Let I ∈ 2X be any assignment with Q[I] being valid. Then, we construct a WV W by defining W := {{sat} ∪ {˜x | I(x) = 0} ∪ {x | I(x) = 1}∪ {J | J ∈ 2Y }}. Assume towards a contradiction that W is not a WV of Π. But then, W does not coincide with set W ′ of stable models of ΠW . Take any J ∈ W. Observe that by construction of Π and since Q[I] is valid, we have that J is also an answer set of ΠW . Further, W ′ ⊆ W since W contains every subset over variables Y , which yields W = W ′ .

Take any WV W of Π. Then, by construction of Π, we have that sat ∈W ′ for everyW ′ ∈W and consequently, for any stable model N of ΠW , sat ∈ N. From this we construct an assignment I : X → {0, 1} from some W ′ ∈ W by I(x) := 1 for every x ∈ X with x ∈ W ′ and I(x) := 0 for every x ∈ X with ˜x ∈ W ′ . Assume towards a contradiction that Q[I] is invalid. Then, there is an assignment J : Y → {0, 1} with Q[I][J] = {∅}. As a consequence, we can define a stable model N ′ of ΠW with N ′ := (W ′ \ {sat}) ∪ {y | J(y) = 1} ∪ {˜ y | J(y) = 0}. This contradicts W being a WV.

Further, the reduction is treewidth-aware and it even linearly preserves the treewidth. To this end, take any TD T = (T, χ) of GQ. From this we construct a TD T ′ = (T, χ′ ) of GΠ as follows. For every node t of T, we define χ′ (t) := χ(t) ∪ {sat} ∪ {˜x | x ∈ χ(t)}. Observe that indeed T ′ is a welldefined TD of GQ. Obviously, we have that |χ′ (t)| ≤ 2 |χ(t)|+ 1 and therefore we follow that tw(Π) ∈ O(tw(Q)). Then, assuming WV existence on Π can be decided in time 22o(w) · poly(|A(Π)|) with w = tw(GΠ) contradicts Proposition 2.

5.4 Normal (HCF) and ι-Tight Programs

For HCF programs Π, we first construct a tight program Π′ , using a treewidth-aware translation R from k(Π) to Π′ =

R(k(Π)) [Fandinno and Hecher, 2021]. Then, the treewidth of GΠ′ is in O(tw(GΠ) · log(tw(GΠ))), an increase that is in line with known lower bounds under ETH [Hecher, 2022]. So, a significant improvement of this increase is unexpected.

After constructing tight program Π′ and obtaining an adapted TD T ′ of GΠ′ , we apply F[Π′ , T ′ ], as defined in the previous subsections, but where K = k(A(Π)).

Theorem 17 (Upper Bound for normal ELPs). Let Π be any normal ELP, whose treewidth of the primal graph GΠ is w. WV existence can be decided in time 22O(w·log(w)) · poly(|A(Π)|).

Proof (Sketch). Correctness of our approach follows from correctness of R and F. R increases treewidth from w to w · log(w) [Fandinno and Hecher, 2021]; applying Theorem 15 yields the result.

Theorem 18 (Tight Lower Bound for normal ELPs, ⋆3 ). Let Π be any normal program, whose treewidth of the primal graph GΠ is w. Then, unless ETH fails, WV existence for Π cannot be decided in time 22o(w·log(w)) · poly(|A(Π)|).

For ι-tight programs Π, the construction works analogously, but instead of R, we use an adapted reduction R′ [Hecher, 2023] to construct a tight program Π′ . There, the treewidth of GΠ′ is in O(tw(GΠ) · log(ι)). Consequently, we obtain results analogously to Theorems 17 and 18.

6 Discussion &Conclusion

We have focused here on the G94 semantics of ELPs by [Gelfond, 1994]. This was the original semantics that satisfy interesting properties from a knowledge representation point of view. Besides, many of our results carry on to the K15 semantics [Kahl et al., 2015] due to the existence of known translations [Fandinno et al., 2021]. For instance, any ELP interpreted under the K15 semantics can be understood as a different ELP under G94 semantics, which is obtained by replacing each expression of the form Ka by conjunction a ∧ Ka.

As a result the upper bounds for every non-tight category carry on to this semantics as well. Note that in general, if a program is objectively tight under the K15 semantics does not mean that the corresponding program to be used under the G94 semantics is also objectively tight. For instance, a ← Ka is objectively tight, but its corresponding program a ← a ∧ Ka is not. Conversely, an ELP under G94 semantics can be translated into a new program under the K15 semantics where expressions Ka are replaced by not k not k a and the rules

with not k not k a, k not k a, not k a and k a fresh auxiliary atoms. As a result, the lower bounds for every category not restricting the use of negation, carry on to these semantics.

In the future, we want to focus on implementations carrying out and comparing the presented QBF encodings. Since there is a known empirical correspondence between formulas of small treewidth and fast SAT solving [Atserias et al., 2011], this raises the question of whether similar observations can be drawn for such QBF encodings. Also, we expect further insights from comparisons with existing ELP solvers.

3 Proofs of statements marked with "⋆" are given in the appendix.

Acknowledgments

The work has been carried out while Hecher visited the Simons Institute for the Theory of Computing. It is supported by Austrian Science Fund (FWF) grants J4656 and P32830, by the Society for Research Funding Lower Austria (GFF) grant ExzF-0004, as well as by the Vienna Science and Technology Fund (WWTF) grant ICT19-065.