--- title: "Epistemic Logic Programs: Non-Ground and Counting Complexity" authors: - "Thomas Eiter" - "Johannes K. Fichte" - "Markus Hecher" - "Stefan Woltran" doi: "10.24963/ijcai.2024/369" url: "https://ijcai.org/proceedings/2024/369" pdf: "https://ijcai.org/proceedings/2024/0369.pdf" venue: "Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence" year: 2024 pages: "3333-3341" track: "Main Track" keywords: - "Knowledge Representation and Reasoning: KRR: Knowledge representation languages" - "Knowledge Representation and Reasoning: KRR: Logic programming" - "Knowledge Representation and Reasoning: KRR: Computational complexity of reasoning" - "Knowledge Representation and Reasoning: KRR: Non-monotonic reasoning" --- # Epistemic Logic Programs: Non-Ground and Counting Complexity Thomas Eiter, Johannes K. Fichte, Markus Hecher, Stefan Woltran *Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence*, pages 3333-3341. DOI: [10.24963/ijcai.2024/369](https://doi.org/10.24963/ijcai.2024/369) ## Abstract Answer Set Programming (ASP) is a prominent problem-modeling and solving framework, whose solutions are called answer sets. Epistemic logic programs (ELP) extend ASP to reason about all or some answer sets. Solutions to an ELP can be seen as consequences over multiple collections of answer sets, known as world views. While the complexity of propositional programs is well studied, the non-ground case remains open. This paper establishes the complexity of non-ground ELPs. We provide a comprehensive picture for well-known program fragments, which turns out to be complete for the class NEXPTIME with access to oracles up to SigmaP2. In the quantitative setting, we establish complexity results for counting complexity beyond #EXP. To mitigate high complexity, we establish results in case of bounded predicate arity, reaching up to the fourth level of the polynomial hierarchy. Finally, we provide ETH-tight runtime results for the parameter treewidth, which has applications in quantitative reasoning, where we reason on (marginal) probabilities of epistemic literals. ## Full text ## 1 Introduction Answer set programming (ASP) is a widely applied modeling and solving framework for hard combinatorial problems with roots in non-monotonic reasoning and logic programming [Brewka et al., 2011] and solving in propositional satisfiability [Fichte et al., 2023]. In ASP, knowledge is expressed by means of rules forming a (logic) program. Solutions to those programs are sets of atoms known as answer sets. Epistemic logic programs (ELPs) [Gelfond, 1991; Kahl et al., 2015; Shen and Eiter, 2016; Truszczy´nski, 2011a] extend ASP by allowing for modal operators K and M, which intuitively mean "known" or "provably true" and "possible" or "not provably false", respectively. These operators can be included into a program and allow for reasoning over multiple answer sets. Then, solutions to an ELP are known as world views. Interestingly, the complexity of decision problems, such as whether a ground ELP admits a world view, or whether a literal is true in all respectively some world view, reaches up to the fourth level of the polynomial hierarchy [Shen and Eiter, 2016]. Despite its hardness in the decision case, also counting world views is of vivid research interest today (see e.g., [Besin et al., 2021]), as it provides the connection of quantitative reasoning for ELPs and computing conditional probabilities by considering the proportion of world views compatible with a set of literals. State-of-the-art systems even allow for solving non-ground programs by either replacing variables with domain constants or structural guided grounding and then employing existing ASP solvers [Cabalar et al., 2020; Besin et al., 2022]. Despite the practical implementations and weak known lower bounds [Dantsin et al., 2001; Eiter et al., 2007], the actual complexity for non-ground ELPs - and thus the capabilites of today's non-ground ELP systems - remained entirely open. In particular, it is not known whether epistemic operators in combination with grounding lead to significant complexity amplifications or whether we see only a mild increase (reflected by a jump of one level in the PH - as in the ground case) compared to standard non-ground ASP. Contributions. In this paper, we study the precise computational complexity of qualitative and quantitative decision and reasoning problems for non-ground ELPs. Our contributions are detailed below. In addition, Table 1 surveys details and illustrates relations to existing results. 1. We provide a comprehensive picture of the non-ground ELP landscape, including common program fragments. We mitigate complexity by showing how complexity results drop if predicate arities are bounded - a typical assumption for solving. 2. We establish detailed complexity results for counting problems, which enables more fine-grained reasoning. To this end, we lift counting complexity notions to the weak-exponential hierarchy. 3. We analyze the impact of structural restrictions in form of bounded treewidth. If the predicate arities are bounded, we obtain precise upper bounds. Surprisingly, the complexity for tight and normal programs match in the nonground case, which is different to ground programs. We complete the upper bounds by conditional lower bounds assuming ETH 1 rendering significant runtime improve- 1 The exponential time hypothesis (ETH) implies 3-CNF satisfiability cannot be solved in time 2o(n) [Impagliazzo and Paturi, 2001]. ments for treewidth very unlikely. Interestingly, our results are based on two sophisticated techniques. First, a classical technique employing second-order logic with dependencies to descriptive complexity for the qualitative setting. Second, a direct approach relying solely on the validity problem for succinct quantified Boolean formulas, which enables results for the quantitative setting as well as when considering bounded treewidth. Broader Relation to AI. We see use cases and connections of our results in areas beyond the scope of logic programming. In particular, there are complex challenges in, e.g., conformant planning [Bonet, 2010] or in reasoning modes like abduction [Aliseda, 2017; Eiter and Gottlob, 1995b], which reach the third and the fourth level of the polynomial hierarchy. Such situations can be elegantly modeled via modal operators K and M, even in the non-ground setting. We expect that the interplay between introspection (i.e., K and M operator capabilities) and non-ground (first-order-like) rules will be of broader interest, as this is essential to formally model rational agents with different belief sets. Here, we provide precise complexity results, consequences of different modeling features, and insights in parameterized complexity. In addition, with the availability of efficient ELP solvers [Bichler et al., 2020; Cabalar et al., 2020], one obtains a first ELP modeling guide. Related Work. Eiter et al. (2007) establish the computational complexity for qualitative problems of non-ground ASP under bounded predicate arities. For ground ELP, Shen and Eiter (2016) show that qualitative problems are higher up in the Polynomial Hierarchy than for ASP, see Ground case in Table 1. In fact, the central decision problem, checking whether an ELP has a world view, is ΣP3 -complete. For treewidth and ground ELP, there are solvers that exploit treewidth [Bichler et al., 2020; Hecher et al., 2020] and also solvers for quantitative reasoning, which relate the the number of accepting literals to number of compatible world views [Besin et al., 2021]. Very recent works address the grounding bottleneck for solving with ELP solvers by grounding that exploits structure [Besin et al., 2023] and complexity of ground ELP when bounded by treewidth Fandinno and Hecher (2023). Our results reach beyond as we consider the non-ground quantitative and qualitative setting. While the non-ground case might seem somewhat expected, establishing results on the exponential hierarchy requires different techniques, especially for treewidth. Fichte et al. (2022b) consider plausibility reasoning in the ground setting for ASP without epistemic operators. ## 2 Preliminaries We assume familiarity with basics in Boolean satisfiability (SAT) [Kleine B¨uning and Lettman, 1999]. By exp(ℓ, k) we refer to k if ℓ ≤ 0 and to 2exp(ℓ-1,k) otherwise. Computational Complexity. We follow standard notions in computational complexity theory [Papadimitriou, 1994; Arora and Barak, 2009] and use the asymptotic notation O(·) as usual. Let Σ and Σ′ be some finite alphabets. We call I ∈ Σ∗ an instance and n denotes the size of I. A decision problem is some subset L ⊆ Σ∗ . Recall that P and NP are the complexity classes of all deterministically and non-deterministically polynomial-time solvable decision problems [Cook, 1971], respectively. We also need the Polynomial Hierarchy (PH) [Stockmeyer and Meyer, 1973; Stockmeyer, 1976; Wrathall, 1976]. In particular, ∆P0 := ΠP0 := ΣP0 := P and ∆Pi := P Σpi-1 , ΣPi := NPΣPi , and ΠPi := coNPΣPi for i > 0 where C D is the class C of decision problems augmented by an oracle for some complete problem in class D. The complexity class D Pk is defined as D Pk := {L1 ∩ L2 | L1 ∈ ΣPk ,L2 ∈ ΠPk } and D P = D P 1 [Lohrey and Rosowski, 2023]. The complexity class NEXP is the set of decision problems that can be solved by a non-deterministic Turing machine using time 2nO(1) , i.e., NEXPTIME = ⋃k∈N NTIME(2nk ). The complexity class NTIME(f(n)) is the set of decision problems that can be solved by a non-deterministic Turing machine which runs in time O(f(n)). Note that CO-NEXP is contained in NEXP NP . The weak EXP hierarchy (EXPH) is defined in terms of oracle complexity classes: ΣEXP 0 := EXP and ΣEXP i+1 := NEXPΣpi [Hemachandra, 1987]. We follow standard notions in counting complexity [Valiant, 1979; Durand et al., 2005; Hemaspaandra and Vollmer, 1995]. A counting problem is a function f : Σ∗ → N0. Then, #P is the class of all functions f : Σ∗ → N0 such that there is a polynomial-time non-deterministic Turing machine M, where for every instance I ∈ Σ∗ , f(I) outputs the number of accepting paths of the Turning machine's computation graph on input I. We will also make use of classes preceded with the sharp-dot operator '#·' defined using witness functions and respective decision problem in a decision complexity class. Answer Set Programming (ASP). Let (P, C) be a firstorder vocabulary of non-empty finite sets P of predicate and C of constant symbols, and let V be a set of variable symbols. Atoms a have the form p(t1, . . . , tn), where p ∈ P, n ≥ 0 is the arity of p, and each ti ∈ T , where T = C ∪ V is the set of terms. A logic program (LP) is a set P of rules r of the form where all ai are distinct atoms and 0≤k≤m≤n. We let Hr:={a1, . . . , ak}, B+ r :={ak+1, . . . , am}, and Br := {am+1, . . . , an}, and denote the set of atoms occurring in r and P by at(r):=Hr ∪ B+ r ∪Br , at(P):= ⋃r∈P at(r), and pnam(P) := {p | p(·) ∈ at(P) }. A program has bounded arity, if every predicate occurring in P has arity at most m for some arbitrary but fixed constant m. By bounded arity, refer to the class of programs that are of bounded arity. A rule r is a fact if B+ r ∪Br = ∅; a constraint if Hr = ∅; positive if Br = ∅; and normal if |Hr| ≤ 1. A program P is positive and normal, respectively, if each r ∈ P has the property. The (positive) dependency graph DP is the digraph with vertices ⋃r∈P Hr ∪B+ r , where for each rule r ∈ P two atoms a∈B+ r and b∈Hr are joined by edge (a, b). ProgramP is tight if DP has no directed cycle [Fages, 1994]. We let Full, Normal, and Tight be the classes of all, normal, and tight programs, respectively. Answer sets are defined via ground programs. The arguments and variables of an atom a = p(t1, . . . , tn) are the sets arg(a) := {t1, . . . , tn} and vars(a) := arg(a) ∩ V. This extends to sets A of atoms by arg(A) := ⋃a∈A arg(a) resp. Table 1: Complexity results of WV existence (counting/plausibility level) for ELP fragments, where each column states the corresponding fragment and each row gives the respective problem. "(b)" indicates fixed predicate arities. Entries indicate completeness results, runtimes are tight under ETH, omitting polynomial factors. d refers to the domain size and tw is the treewidth of the primal graph. "† ": The runtime bounds are for the counting case, as decision is easier due to classical complexity results. Here exp(0, n) = n and exp(k, n) = 2exp(k-1,n) , k ≥ 1. | | EHorn | Tight | Normal | Full | Result | |---------------------|-----------------------------------------|------------------------------|----------------------------------------|------------------------------|-----------------------------------------------| | Qualitative | | | | | | | Ground | P | ΣP2 | ΣP2 | ΣP3 | [Truszczy´nski, 2011b] [Shen and Eiter, 2016] | | Non-Ground | EXP | NEXP NP | NEXP NP | NEXPΣP2 | Theorem 4, Lemma 5 | | Non-Ground(b) | CONP | ΣP3 | ΣP3 | ΣP4 | Theorem 4, Lemma 5 | | Quantitative | | | | | | | Ground | #P | # · D P | # · D P | # · D P 2 | Lemma 15 | | Non-Ground | #EXP | #EXP NP | #EXP NP | #EXPΣP2 | Theorem 14 | | Non-Ground(b) | # · D P | # · D P 2 | # · D P 2 | # · D P 3 | Lemma 16 | | Parameterized | | | | | | | Ground [tw] Non-Gr. | exp(1, o(tw))† [tw](b) exp(1, do(tw) )† | exp(2,Θ(tw)) exp(2, dΘ(tw) ) | exp(2,Θ(tw · log(tw))) exp(2, dΘ(tw) ) | exp(3,Θ(tw)) exp(3, dΘ(tw) ) | [Fandinno and Hecher, 2023] Theorems 19,20 | vars(A) := ⋃a∈A vars(a) and likewise to rules and programs. An atom, rule or program φ is ground if vars(φ) = ∅ and propositional if arg(φ) = ∅. The Herbrand universe of a programP is the set UP := arg(P)∩C (if empty, UP := {c} for any c ∈ C), and its Herbrand base BP consists of all ground atoms with a predicate from P and constants from UP . A set M ⊆ BP of atoms satisfies (is a model of) a ground rule r resp. ground program P if (i) (Hr ∪Br )∩M ̸=∅ or (ii) B+ r \M ̸=∅ resp. M satisfies each r ∈ P. Furthermore, M is an answer set of P if M is a ⊆-minimal model of P M := ⋃r∈P {Hr ← B+ r | Br ∩M = ∅}, i.e., the GL-reduct of P [Gelfond and Lifschitz, 1991] w.r.t. M; AS(P) denotes the set of all answer sets of P. The answer sets of a general program P are those of its grounding grd(P) := ⋃r∈P grd(r), where grd(r) is the set of all rules obtained by replacing each v ∈ vars(r) with some element from UP . We assume safety, i.e., each rule r ∈P satisfies vars(Hr ∪ Br ) ⊆ vars(B+ r ). We can ensure it by a unary domain predicate dom with facts dom(c), c ∈ UP and adding dom(x) in the body of r for each x ∈ vars(r). To select rules in grd(P) with the same head D, we define def(D, P) := {r ∈ grd(P) | Hr = D} and to select nonground rules in P that define atoms with predicate p, we let pdef(p, P) := { r ∈ P | p(t1, . . . , tn) ∈ Hr }. Deciding whether a program P has an answer set (called consistency) is ΣP2 -complete for ground programs [Eiter and Gottlob, 1995a] and NEXP NP for non-ground programs [Eiter et al., 1994]. Epistemic Logic Programs (ELPs). Epistemic logic programs extend LPs with epistemic literals in rule bodies. A literal is either an atom a (positive literal) or its negation ¬a (negative literal). A set L of literals is consistent if for every ℓ ∈ L, ¬ℓ ̸∈ L assuming that ¬¬ℓ = ℓ. For a set A of atoms, we define ¬A := {¬a | a ∈ A} and lits(P) := at(P)∪¬at(P). An epistemic literal an expression not ℓ where ℓ is a literal. Following common convention, we use Kℓ as shorthand for ¬ not ℓ and Mℓ for not ¬ℓ. An epistemic atom is an atom that is used in an epistemic literal. For a set S consisting of atoms, literals, and/or epistemic literals, we denote by at(S) and lits(S), the set of atoms and literals, respectively, that occur in S. These notations naturally extend to rules and programs. Definitions for logic programs such as classes of programs naturally extend to ELP. The dependency graph DP of an ELP P is as for ASP, but for every rule r ∈ P and b ∈ Hr, we also add an edge (a, b) if r contains a body literal not ¬a or ¬ not a. Properties are similar to ASP. In addition, we define EHorn with no negations (neither ¬ nor not) and no disjunctions, however, Ka and Ma are allowed. There are different semantics for ELPs , e.g. [Gelfond, 1991; Truszczy´nski, 2011b; Kahl et al., 2015; Fari ˜nas del Cerro et al., 2015; Shen and Eiter, 2016]; see [Fandinno et al., 2022] for an overview. We consider [Shen and Eiter, 2016], which provides a reduct-based framework and offers highest problem solving capacity. In what follows, let P be a ground ELP. A world view interpretation (WVI) for P is a consistent set I ⊆ lits(P). Intuitively, every ℓ ∈ I is considered "known" and every a ∈ at(P) with {a, ¬a} ∩ I = ∅ is treated as "possible". The epistemic reduct [Shen and Eiter, 2016; Morak, 2019] of program P under WVI I is PI := {rI | r ∈ P}, where rI results by replacing in r each epistemic literal not ℓ with ¬ℓ if ℓ ∈ I and with ⊤ otherwise; double negation cancels. This amounts to FLP-semantics for nested negation; we omit HT-semantics, for which similar complexity results can be obtained. Note that PI has no epistemic negations. AWVI I over lits(P) is compatible with a set I of WVIs if (i) I ̸= ∅ and for each atom a, (ii) a ∈ I implies a ∈ ⋂J∈I J; (iii) ¬a ∈ I implies {J ∈ I | a ∈ J} = ∅; and (iv) a ∈ at(P) \ at(I) implies that a ∈ J and a ̸∈ J ′ . for some J, J ′ ∈ I. I is a candidate world view (WV) of P if I is compatible with the set AS(PI ). WV existence is ΣP3 -complete [Truszczy´nski, 2011b; Shen and Eiter, 2016]. The counting problem#WV asks to output the number of WVs. Semantics of non-ground ELPs is defined by grounding, as for LPs. Example 1 (cf. Gelfond 1991). Take the well-known scholarship eligibility problem encoding, which is as follows: ``` P1 ={ lowGPA(mark); highGPA(mia); lowGPA(maya) ∨ highGPA(maya); inelig(X) ← lowGPA(X); elig(X) ← highGPA(X); ⊥ ← elig(X), inelig(X); interview(X) ← not elig(X), not inelig(X) }. Then, the set of WVs of the program is { {¬interview(mark), lowGPA(mark), inelig(mark), ¬elig(mark), interview(maya), ¬interview(mia), highGPA(mia), elig(mia), ¬inelig(mia)} }. ``` First- and Second-Order Logic. We assume familiarity with logic and follow standard definitions [Gr¨adel et al., 2007] (see also the supplemental material). Throughout we assume that σ is a signature, which we omit if it is clear from context. The class Σ1k [σ] consists of all prenex second-order formulas Φ ∈ SO[σ], i.e., Φ = Q1R1Q2R2 · · ·QkRk.φ where Qi ∈ {∀, ∃} and Qi ̸= Qi+1 for 1 ≤ i < k, the Ri are disjoint nonempty sets of SO-variables, and φ ∈ FO[σ]; Φ is existential if Q1 = ∃. We say that Φ is in CDNF if free(φ) = ∅ and (i) k is even and φ = ∃⃗xψ with ψ in DNF, or (ii) k is odd and φ = ∀⃗xψ with ψ in CNF. ## 3 Complexity of Non-ground ELP Reasoning In this section, we establish results on the classical complexity of reasoning with non-ground ELPs. Our first insight is on qualitative reasoning. Therefore, we need Proposition 2, which states the relationship between second-order logic and the exponential hierarchy for combined and data complexity. Proposition 2 (Gottlob et al. 1999). Given a sentence Φ ∈ Σ1k and a finite structure A, deciding whether A |= Φ is (i) NEXPΣPk-1 -complete (combined complexity) and (ii) ΣPk - complete if Φ is fixed (data complexity). Next, in Lemma 3, we show a connection between the existing result on second-order logic and the exponential hierarchy in the general case and in case predicates have bounded arity. Lemma 3 (⋆2 ). Given a sentence Φ ∈ Σ1k [σ] in CDNF and a finite structure A, deciding whether A |= Φ is (i) NEXPΣPk-1 - complete and (ii) ΣPk+1 -complete if every predicate Ri in Φ has arity at most m for some arbitrary but fixed integer m ≥ 1. ## 3.1 Qualitative Reasoning With the help of the results above, we are ready to establish the following central insight into the complexity of non-ground ELPs. While it turns out that world view existence on a limited fragment is already complete for a class beyond NEXP, luckily, for bounded predicate arity we obtain completeness results for the fourth level of the polynomial hierarchy. Theorem 4. Let P be an ELP and (a) i = 2 if P ∈ Full, and (b) i = 1 if P ∈ Normal ∪ Tight. Then, deciding whether P admits a world view is NEXPΣPi -c for non-ground P and ΣPi+2 - c for non-ground of bounded arity. 2 We prove (⋆)-statements in an extended version [Eiter et al., 2024]. Proof (Sketch). Membership: For the non-ground cases, the result follows immediately from the Σpi+1 -completeness in the ground (propositional) case [Shen and Eiter, 2016], as grounding an ELP P leads to an exponentially larger program grd(P) and Σpj becomes NEXPΣPj-1 [Gottlob et al., 1999]. For the bounded arity cases. If predicate arities are bounded by a constant, a guess for a WVI I of an epistemic program P has polynomial size. We can emulate the epistemic reduct PI by replacing in P each epistemic literal not ℓ where ℓ = L(⃗t), L ∈ {p, ¬p} by an atom qnot L(⃗t), where not L is a fresh predicate of arity |⃗t|, and add the following fact or rule, for each tuple ⃗c of constants (having arity |⃗t|: (1) qnot L(⃗c), if L(⃗c) /∈ I, and (2) qnot L(⃗c) ← ¬L(⃗c) otherwise (double negation cancels). Then the answer sets of the resulting program PI,not correspond to the answer sets of PI , as (1) and (2), respectively, can be unfolded with rules in the grounding of P that contain not L(⃗c). In particular, I is compatible with AS(PI ) iff I is compatible with AS(PI,not). As PI,not has bounded predicate arity, brave and cautious reasoning from PI,pnot is in Σp3 and Πp3 , respectively, [Eiter et al., 2007]. Consequently, we can check in polynomial time with an Σp3 oracle whether I fulfills conditions (i)-(ii) of compatibility with AS(PI ), i.e., whether I is a WVI of P. This shows membership in Σp4 , i.e., P ∈ Full. If P ∈ Tight ∪Normal, brave and cautious reasoning from PI,pnot is in Σp2 and Πp2 , respectively, [Eiter et al., 2007], as program PI,pnot is normal/tight, if program P is so. This shows membership in Σp3 . Hardness: We construct from a given sentence Φ ∈ Σ1k and finite structure A an ELP P, thereby, we reduce deciding whether A |= Φ (model checking) to deciding whether P admits a world view (world-view-existence). In our reduction, we lift the existing ELP encoding that solves QBF validity to SO [Shen and Eiter, 2016]. In detail, Case P ∈ Full: let A = (A, σA) and Φ = ∃R1∀R2∃R3.φ ∈ Σ1k where φ = ∀⃗xψ and ψ = ∧mj=1 ∨ℓj h=1 Lj,h is in CNF, i.e., as in Lemma 3. We take u and v as propositional atoms and for each relation symbol R ∈ R1 ∪ R2 ∪ R2, we introduce predicates R and R. Then, we construct programs P1, . . . , P5 as follows. Let e(⃗x) = (e(x1), e(x2), . . . , e(xm)) and e(v) := v, if v is an FO-variable and e(v) := cA if v is a constant symbol. Intuitively, P1 selects with epistemic negation a candidate world view corresponding to a guess for each relation symbol R1,i in R1 using an auxiliary relation symbol R1,i for its complement. Program P2 generates then answer sets for each possible relation R2,i in R2. Programs P3 guesses for each such valuation of R2 a valuation of R3 such that ∀⃗xψ is true. The program P4 checks then using the saturation technique that ∀⃗xψ is not violated, i.e., ∃⃗x¬ψ is false; any violation makes u true and saturates the guess. The last rule in P4 eliminates the candidate world view if ¬u cannot be derived. where s(R(·)) := ¬R(·) if R /∈ σ, s(R(·)) := R(·) otherwise and s(¬R(·)) := R(·). Program P5 represents atoms of the input structure A as facts. Notably, we treat equality as the other relations. Finally, we build the program P = ⋃5i=1 Pi. Then P is constructible in polynomial time and it has a world view iff A |= Φ. Case P ∈ Tight ∪ Normal: We encode evaluating an SO sentence Φ = ∃P1∀P2∃⃗xψ over A. We assume ψ = ∨mj=1 ∧ℓj h=1 Lj,h is a DNF, drop P3, and replace P4 with the following rules: For each valuation of P1 and P2, we have then a unique answer set that contains u iff (A,RA 1 ,RA 2 ) |= ∃⃗xψ. Then P ′ = P - (P3 ∪ P4) ∪ P ′4 has a world view iff A |= P . As P ′4 is tight, the reduction applies for tight programs as well. Lemma 5 (⋆). Let P ∈ EHorn. Then, deciding whether P admits a world view is in P if P is ground, CONP-complete if P is non-ground and has bounded arity, and EXP-complete if P is non-ground. ## 3.2 Counting Complexity Beyond NEXP Before we can turn our attention to the quantitative setting, we need to define counting classes for classifying counting problems, whose corresponding decision problems are in NEXPC for a decision class C. Following, we provide canonical problems, followed by completeness results for ELPs. Generalizing Counting Classes. For counting solutions of problems in NEXP, the corresponding counting complexity class #EXP [Papadimitriou and Yannakakis, 1986] has been defined. However, classes based on oracle machine models, as in the #· complexity classes [Hemaspaandra and Vollmer, 1995] have been left out for exponential time. Below, we generalize counting complexity to the realm of exponential time. This allows us to describe in analogy to decision problems the complexity of counting problems beyond NEXP. Definition 6 (Exp-Oracle Classes). Let C be a decision complexity class. Then, #EXPC is the class of counting problems, whose solution is obtained by counting the number of accepting paths of a non-deterministic Turing machine in exponential time with access to a C oracle. Observe that by construction #EXP = #EXP P . To demonstrate these classes, we define a family of counting problems serving as canonical representatives. Succinct Quantified Boolean Formulas. To define succinct formula representation, we vastly follow existing ideas [Williams, 2008]. For a circuit C with a set I of n inputs, where C has size poly(n), we let T(C) be the truth table of the Boolean function represented by C. Formally, T(C) is the 2n -bit string such that T(C)[i] = C(Bi), where Bi is the i-th of all n-bit strings in lexicographic order; intuitively, T(C)[i] is bit i of a string that encodes a problem instance. For a 3CNF φ, we define such a circuit Cφ ("clause circuit") over sign-bits sj for j ∈ [1, 3] and variable-bits bkj for k ∈ [1, vφ], where vφ = ⌈log(| var(φ)|)⌉. More precisely, Cφ has 3(vφ + 1) input bits s1, ⃗ b1, s2, ⃗ b2, s3, ⃗ b3, where sj tells whether the j-th literal ℓj in a 3CNF clause, whose variable is encoded by the bits ⃗ bj = b1j , . . . , bvφ j , is positive (sj = 1) or negative (sj = 0). That is, ℓ1 ∨ ℓ2 ∨ ℓ3 ∈ φ if and only if Cφ(sgn(ℓ1), ⃗ b1, sgn(ℓ2), ⃗ b2, sgn(ℓ3), ⃗ b3) = 1. For φ in 3DNF, a circuit Cφ ("term circuit") is defined analogously. Example 7. Let (a∨ b ∨¬c) ∧ (¬b ∨a∨d) ∧ (¬b ∨ c ∨¬d) be a Boolean formula in 3CNF. Using 2 = ⌈(log(4))⌉ bits, we can succinctly represent this formula as a circuit. For QBFs, we must also succinctly represent quantifiers. While we could merge this into the clause or term circuit, for the sake of readability, we use a second circuit. For a QBF Q = ∃V1.∀V2. . . .QℓVℓ.φ with alternating quantifier blocks Qi ∈{∃, ∀}, we define a quantifier circuit CQ with ⌈log(l)⌉+vφ many input bits ⃗q,⃗b, where ⃗q =q1 , . . . , q⌈log(l)⌉ and ⃗b=b1 , . . . , bvφ . Intuitively, v ∈ var(φ) is in Vι iff CQ(bin(ι), bin(v)) = 1, where bin(·) is the binary representation. Q is closed if every v ∈ var(φ) is in Vι for some ι; otherwise Q is open and its (set of) free variables var(φ) \ (⋃1≤ι≤ℓ Vι). Definition 8 (Succinct QBF). A succinct QBF Q with ℓ alternating quantifier blocks (alternation depth) is given by a quantifier circuit CQ and a clause circuit Cφ. Problem SUCCQVALℓ is deciding whether a closed succinct QBF Q evaluates to true; #SUCCQVALℓ asks to count assignments θ over the free variables of Q such that Qθ evaluates to true. The following complexity result is known. Proposition 9 (Complexity of SUCCQVALℓ [Gottlob et al., 1999; Stewart, 1991]). For succinct QBFs Q of alternation depth ℓ ≥ 1, SUCCQVALℓ is NEXPΣPℓ-1 -complete. This immediately yields corresponding counting complexity. Proposition 10 (Complexity of #SUCCQVALℓ). For succinct QBFs Q of alternation depth ℓ ≥ 0, counting the number of assignments over its free variables under which Q evaluates to true is #EXPΣPℓ -complete. We will utilize this result by defining a parsimonious reduction to our counting problems of interest. A parsimonious reduction is a polynomial-time reduction from one problem to another that preserves the number of solutions, i.e., it induces a bijection between respective sets of solutions of two problems. ## 3.3 Quantitative Reasoning Next, we discuss how quantitative aspects enable more finegrained reasoning. Indeed, deciding whether a world view exists concerns only a single world view. Instead, if we aim for stable results towards consensus among different world views, one would prefer computing levels of plausibility for certain observations (assumptions). This is achieved by quantitative reasoning, where we quantify the number of world views satisfying a given query Q. Thereby we compute the level of plausibility for Q. We need the following notation. Definition 11. An (epistemic) query is a set of expressions of the formMℓ or Kℓ, where ℓ is a literal. Intuitively, we can then quantify the plausibility of queries. To this end, we define the union of an ELP P and a query Q, which is a set of expressions as defined above, by P ⊔ Q := P ∪ {v ← not v, ¬q | q ∈ Q} for a fresh atom v. Definition 12 (Plausibility Level). Let Q be an epistemic query and P be an ELP. The plausibility level of Q is defined as L(P,Q) :=#WV(P⊔Q). We define probabilities via two counting operations and therefore study the complexity of computing plausibility levels. Definition 13 (Probability). Let Q be an epistemic query and P be an ELP. The probability of Q is defined as L(P,Q) max(1,L(P,∅)) . Observe that the empty query has probability 1.0 and inconsistent queries or ELPs both have probability 0.0 (implausible). Complexity of Computing Plausibility Levels. For establishing the complexity of counting, we reduce from #SUCCQVALℓ and use Proposition 10. Indeed, computing plausibility levels is already hard for empty queries. Theorem14 (⋆). Let P be an ELP and (a) i = 2 if P∈Full, (b) i = 1 if P∈Normal ∪Tight, and (c) i = 0 if P∈EHorn. Then, computing plausibility level L(P, ∅) is #EXPΣPi -complete. Proof. Membership: This follows immediately from the ground case (propositional) where we have Σpi+1 -completeness [Shen and Eiter, 2016]. With the same argument as in the proof of Theorem 14, meaning, grounding an ELP P leads to an exponentially larger program grd(P), and Σpj becomes NEXPΣPj-1 cf. [Gottlob et al., 1999], we conclude the result. Hardness for P ∈ EHorn: We reduce from a restricted fragment of #SUCCQVAL0, taking a positive Boolean formula φ defined by a clause circuit C over 3 · (1 + n) many input gates, and constructing an ELP P. First, the evaluation of C is inductively constructed, starting from the input gates of C to the output gate of C. Thereby, for every gate g we construct a rule defining a predicate of arity 3 · (1 + n), depending on the result of the predicates for the input gates of g. By ⃗vi we refer to a sequence of n many variables v1 i , . . . , vn i . Also, we define the facts b(0) and b(1). For an input gate gj of C with 1 ≤ j ≤ 3·(1+n), we construct the fact gj(v1 , . . . , v3·(1+n) ). if and only if vj = 1. Without loss of generality, we assume that negation only appears at the input gates (negation normal form). for disjunction gate g∨ with inputs g1, . . . , go, we define for every 1 ≤ k ≤ o: We refer to the predicate of the final output gate of the construction by gC. Additionally, we construct the following rules below. First, we guess an assignment over the variables, where we decide whether a variable will be set to false: Then, we check whether there is an unsatisfied clause. It is easy to see that there is a bijection between satisfying assignments of φ and world views of P. Hardness for P ∈ Tight ∪ Normal: We reduce from #SUCCQVAL1, taking a QBF Q = ∀U.φ over free variables V , with 3DNF φ given by a term circuit C over 3 · (1 + n) many input gates and a quantifier circuit D over n input gates. From this, we construct ELP P . First, C is inductively constructed as above. We refer to the predicate of the output gate of the construction by gC. Then, similar to above, we define for every gate of the circuit D a predicate of arity n + 1 from the input gates to the output gate of D. For a negation gate g¬ with input g, we define for a conjunction gate g∧ with inputs g1, . . . , go, we define for disjunction gate g∨ with input gates g1, . . . , go, we define for every 1 ≤ k ≤ o: g∨(ι,⃗v1) ← gk(ι,⃗v1). The predicate of the final output gate of D is given by gD. Additionally, we construct the following rules below, thereby following ¬∃U.φ over the inverse formula of φ. First, we guess an assignment over the variables: ``` A(v1 , . . . , vn ) ← not ˙A(v1 , . . . , vn ), gD(1, v1 , . . . , vn ). ˙A(v1 , . . . , vn ) ← not A(v1 , . . . , vn ), gD(1, v1 , . . . , vn ). A(v1 , . . . , vn ) ← ¬ ˙A(v1 , . . . , vn ), gD(2, v1 , . . . , vn ). ˙A(v1 , . . . , vn ) ← ¬A(v1 , . . . , vn ), gD(2, v1 , . . . , vn ). Then, we check whether all terms are dissatisfied. usat(1,⃗v1, s2,⃗v2, s3,⃗v3) ← ˙A(⃗v1), gC(1,⃗v1, s2,⃗v2, s3,⃗v3) usat(0, ⃗v1, s2, ⃗v2, s3, ⃗v3) ← A(⃗v1), gC(0, ⃗v1, s2, ⃗v2, s3, ⃗v3) usat(s1,⃗v1, 1,⃗v2, s3,⃗v3) ← ˙A(⃗v2), gC(s1,⃗v1, 1,⃗v2, s3,⃗v3) usat(s1, ⃗v1, 0, ⃗v2, s3, ⃗v3) ← A(⃗v2), gC(s1, ⃗v1, 0, ⃗v2, s3, ⃗v3) usat(s1,⃗v1, s2,⃗v2, 1,⃗v3) ← ˙A(⃗v3), gC(s1,⃗v1, s2,⃗v2, 1,⃗v3) usat(s1, ⃗v1, s2, ⃗v2, 0, ⃗v3) ← A(⃗v3), gC(s1, ⃗v1, s2, ⃗v2, 0, ⃗v3). ``` We prohibit WVs with an answer set satisfying a term. sat ← gC(s1, ⃗v1, s2, ⃗v2, s3, ⃗v3), ¬usat(s1, ⃗v1, s2, ⃗v2, s3, ⃗v3) v ← not v, not ¬sat. It is easy to see that there is a bijection between satisfying assignments over V of Q and world views of P. Hardness for normal programs follows immediately from the reduction above, since the resulting programs are already normal. Hardness for P ∈ Full: We provide details in an extended version [Eiter et al., 2024]. Similarly, we conclude the following statement. Lemma 15 (⋆). Let P be a ground ELP and i = 2 if P ∈ Full, and i = 1 if P ∈ Normal ∪ Tight, and i = 0 if P ∈ EHorn. Then, computing plausibility level L(P, ∅) is # · D P i -complete. If the arity is a fixed constant, we obtain the following. Lemma 16 (⋆). Let P be a non-ground ELP of bounded arity and i = 2 if P ∈ Full, and i = 1 if P ∈ Normal ∪ Tight, and i = 0 if P ∈ EHorn. Then, computing plausibility level L(P, ∅) is # · D P i+1 -complete. ## 4 Non-Ground ELPs of Bounded Treewidth Before we discuss consequences of evaluating non-ground ELPs for treewidth, we recall tree decompositions (TDs) for which we need the following definition. Definition 17 (TD [Robertson and Seymour, 1985]). Let G = (V,E) be a graph. A pair T = (T, χ), where T is a rooted tree with root r(T) and χ is a labeling function that maps every node t of T to a subset χ(t) ⊆ V called bag, is a tree decomposition (TD) of G if (i) for each v ∈ V some t in T exists s.t. v ∈ χ(t); (ii) for each {v,w} ∈ E some t in T exists s.t. {v,w} ⊆ χ(t); and (iii) for each r, s, t of T s.t. s lies on the unique path from r to t, χ(r) ∩ χ(t) ⊆ χ(s). The width of T is the largest bag size minus one and the treewidth of G is the smallest width among all TDs of G. To simplify case distinctions in the algorithms, we use nice TDs in a proof (see extended version), which can be computed in linear time without increasing the width [Kloks, 1994]. To capture atom (predicate) dependencies of programs, we use the following primal graph GP = (V,E) of a program P defined as follows. For ground P, we let V := at(P) and {a, b} ∈ E if atoms a ̸= b jointly occur in a rule of P , while for non-ground P, we let V := pnam(P) and {p1, p2} ∈ E if predicates p1 ̸= p2 jointly occur in a rule of P. Tree decompositions allow us to establish tight complexity bounds for WV existence under ETH. To this end, we resort to quantified CSP (QCSP), which, intuitively, is analogous to quantified Boolean formulas, but over arbitrary finite domains instead of domain {0, 1}. To this end, we define primal graph PQ for a QCSP Q similarly to programs, but on the formula's matrix. Further, exp(0, n) = n and exp(k, n) = 2exp(k-1,n) , k ≥ 1, denotes the k-fold exponential function of n. The following bounds are known. Proposition 18 (Fichte et al. 2020). Given any QCSP Q with constraints C over finite domain D and alternation depth ℓ ≥ 1, where each constraint has at most s ≥ 3 variables. Then, under ETH the validity of Q cannot be decided in time exp(ℓ-1, |D|o(k) ) · poly(|C|), where k is the treewidth of PC. With his result at hand, we obtain the following. Theorem 19 (⋆). Let P be an arbitrary ELP of bounded arity a over domain size d = |dom(P)|, where the treewidth of GP is k. Furthermore, let (a) i = 2 if P ∈ Full, (b) i = 1 if P ∈ Normal ∪ Tight, and (c) i = 0 if P ∈ EHorn. Then, under ETH, WV existence of grd(P ) cannot be decided in time exp(i + 1, do(k) )· poly(|at(P )|). Indeed, one can obtain a runtime adhering to this lower bound. Theorem 20 (⋆). Let P be an arbitrary ELP of bounded arity a over domain size d = |dom(P)|, where the treewidth of GP is k. Furthermore, let (a) i = 2 if P ∈ Full and (b) i = 1 if P ∈ Normal ∪ Tight. Then, deciding world view existence as well as computing plausibility level L(P, ∅) of grd(P ) can be done in time exp(i + 1, dO(k) )· poly(|at(P )|). ## 5 Conclusion and Outlook We consider non-ground ELP, a popular concept to enable reasoning about answer sets. We settle the complexity landscape of qualitative and quantitative reasoning tasks for non-ground ELPs, including common program fragments. In particular, we establish that deciding whether a program admits a world view ranges between NEXP and NEXPΣP3 . We mitigate resulting high complexity by bounding predicate arities. Then, the complexity drops, ranging fromΣP2 to ΣP4 . In the quantitative setting, we consider levels of plausibility by quantifying the number of world views that satisfy a given query Q. We show completeness results for all common settings and classes of programs, namely, ground programs, non-ground programs, and non-ground programs of bounded arity. We complete these results by incorporating treewidth and establish results ranging up to four-fold exponential runtime in the treewidth, including ETH-tight lower bounds. Due to the techniques, our proofs also work for other common ELP-semantics. Our results contribute to several avenues for future research. First, we have an indication that well-known problems from the AI domains with high complexity are amenable to ELPs. In particular, we now have an understanding that epistemic operators and fixed predicate arities provide a suitable target formalism for problems on the second, third, or fourth level of the PH, as certain variants of the diagnosis problem [Eiter and Gottlob, 1995b; Eiter et al., 1997], counterfactual reasoning [Eiter and Gottlob, 1996], or default logic [Fichte et al., 2022c]. Modeling such problems using epistemic operators might yield elegant and instructive ASP encodings.Second, they indicate alternative ways for solver design: so far, standard non-ground ELP systems ground the ELP first and then solve the resulting ground ELP. Our results justify that epistemic operators can be reduced on the non-ground level without the exponential blowup. Recall that non-ground, normal ELPs and propositional, disjunctive LPs are of similar complexity (see Table 1). This makes alternative grounding techniques such as lazy grounding [Weinzierl et al., 2020] or body-decoupled grounding [Besin et al., 2022] immediately accessible for ELPs. Also, our results from Section 4 build a theoretical foundation for structure-aware ELP grounders. This could also be interesting for structure-guided reductions to ELP [Hecher, 2022]. Finally, extending the complexity landscape of non-ground ELPs is on our agenda. Finding natural NP-fragments would be interesting, since the complexity beyond EHorn almost immediately jumps two levels in PH for the Shen-Eiter semantics. A comprehensive complexity picture in ELP similar to ASP could be of interest in this setting [Truszczy´nski, 2011b; Fichte et al., 2015]. We have left aside the case of maximal world views so far, although we expect that the complexity increases by one level on the PH for reasoning problems. It might also be interesting to consider complementary aspects in ELPs where modal operators require some literals to be present in answer sets [Fichte et al., 2022a] or where we compute quantitative aspects approximately [Kabir et al., 2022]. Restrictions on epistemic atoms that might be of interest or other structural restrictions on programs, for example, fractional hyper-treewidth [Grohe and Marx, 2014], is subject of future research. ## Acknowledgements Authors are ordered alphabetically. The work has been carried out while Hecher visited the Simons Institute at UC Berkeley. Research is supported by the Austrian Academy of Sciences ( ¨OAW), DOC Fellowship; the Austrian Science Fund (FWF), grants P30168 and J4656; ELLIIT funded by the Swedish government; Humane AI Net (ICT-48-2020-RIA / 952026); the Society for Research Funding in Lower Austria (GFF) grant ExzF-0004; and Vienna Science and Technology Fund (WWTF) grants ICT19-065 and ICT22-023. ## References 1. [Aliseda, 2017] Atocha Aliseda. The Logic of Abduction: An Introduction, pages 219-230. Springer, Cham, 2017. 2. [Arora and Barak, 2009] Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cam- bridge University Press, 2009. 3. [Besin et al., 2021] Viktor Besin, Markus Hecher, and Stefan Woltran. Utilizing Treewidth for Quantitative Reasoning on Epistemic Logic Programs. TPLP, 21(5):575-592, 2021. 4. [Besin et al., 2022] Viktor Besin, Markus Hecher, and Stefan Woltran. Body-Decoupled Grounding via Solving: A Novel Approach on the ASP Bottleneck. In IJCAI'22, pages 2546- 2552. ijcai.org, 2022. 5. [Besin et al., 2023] Viktor Besin, Markus Hecher, and Stefan Woltran. On the structural complexity of grounding -tack- ling the ASP grounding bottleneck via epistemic programs and treewidth. In ECAI'23, pages 247-254. IOS Press, 2023. 6. [Bichler et al., 2020] Manuel Bichler, Michael Morak, and Stefan Woltran. selp: A single-shot epistemic logic pro- gram solver. TPLP, 20(4):435-455, 2020. 7. [Bonet, 2010] Blai Bonet. Conformant plans and be- yond: Principles and complexity. Artificial Intelligence, 174(3):245-269, 2010. 8. [Brewka et al., 2011] Gerhard Brewka, Thomas Eiter, and Mirosław Truszczyński. Answer set programming at a glance. Comm. of the ACM, 54(12):92-103, 2011. 9. [Cabalar et al., 2020] Pedro Cabalar, Jorge Fandinno, Javier Garea, Javier Romero, and Torsten Schaub. eclingo : A Solver for Epistemic Logic Programs. TPLP, 20(6):834- 847, 2020. 10. [Cook, 1971] Stephen A. Cook. The Complexity of Theorem- Proving Procedures. In STOC'71, pages 151-158. ACM, 1971. 11. [Dantsin et al., 2001] Evgeny Dantsin, Thomas Eiter, Georg Gottlob, and Andrei Voronkov. Complexity and expres- sive power of logic programming. ACM Comput. Surv., 33(3):374-425, 2001. 12. [Durand et al., 2005] Arnaud Durand, Miki Hermann, and Phokion G. Kolaitis. Subtractive reductions and complete problems for counting complexity classes. Theoretical Computer Science, 340(3):496-513, 2005. 13. [Eiter and Gottlob, 1995a] Thomas Eiter and Georg Gottlob. On the computational cost of disjunctive logic program- ming: Propositional case. Annals of Mathematics and Artificial Intelligence, 15(3-4):289-323, 1995. 14. [Eiter and Gottlob, 1995b] Thomas Eiter and Georg Gottlob. The Complexity of Logic-Based Abduction. Journal of the ACM, 42(1):3-42, 1995. 15. [Eiter and Gottlob, 1996] Thomas Eiter and Georg Gottlob. The complexity of nested counterfactuals and iterated knowledge base revisions. J. Comput. Syst. Sci., 53(3):497- 512, 1996. 16. [Eiter et al., 1994] Thomas Eiter, Georg Gottlob, and Heikki Mannila. Adding disjunction to datalog (extended abstract). In PODS '94, pages 267-278, New York, NY, USA, 1994. ACM. 17. [Eiter et al., 1997] Thomas Eiter, Georg Gottlob, and Nicola Leone. Abduction from logic programs: Semantics and complexity. Theor. Comput. Sci., 189(1-2):129-177, 1997. 18. [Eiter et al., 2007] Thomas Eiter, Wolfgang Faber, Michael Fink, and Stefan Woltran. Complexity results for answer set programming with bounded predicate arities and impli- cations. Annals of Mathematics and Artificial Intelligence, 51(2-4):123-165, 2007. 19. [Eiter et al., 2024] Thomas Eiter, Johannes K. Fichte, Markus Hecher, and Stefan Woltran. Epistemic logic programs: Non-ground and counting complexity. CoRR, 2024. Ex- tended Version of a paper that has been accepted for publi- cation at IJCAI'24. 20. [Fages, 1994] Franc ¸ois Fages. Consistency of Clark's com- pletion and existence of stable models. Logical Methods in Computer Science, 1(1):51-60, 1994. 21. [Fandinno and Hecher, 2023] Jorge Fandinno and Markus Hecher. Treewidth-aware complexity for evaluating epis- temic logic programs. In IJCAI'23, pages 3203-3211. ij- cai.org, 2023. 22. [Fandinno et al., 2022] Jorge Fandinno, Wolfgang Faber, and Michael Gelfond. Thirty years of epistemic specifications. TPLP, pages 1043-1083, 2022. 23. [Fariñas del Cerro et al., 2015] Luis Fariñas del Cerro, An- dreas Herzig, and Ezgi Iraz Su. Epistemic equilibrium logic. In IJCAI, pages 2964-2970, 2015. 24. [Fichte et al., 2015] Johannes K. Fichte, Mirosław Truszczyński, and Stefan Woltran. Dual-normal logic programs -the forgotten class. TPLP, 15(4-5):495-510, 2015. 25. [Fichte et al., 2020] Johannes Klaus Fichte, Markus Hecher, and Maximilian F. I. Kieler. Treewidth-Aware Quantifier Elimination and Expansion for QCSP. In CP'20, pages 248-266. Springer, 2020. 26. [Fichte et al., 2022a] Johannes K Fichte, Sarah Alice Gaggl, and Dominik Rusovac. Rushing and strolling among an- swer sets -navigation made easy. In AAAI'2022, 2022. 27. [Fichte et al., 2022b] Johannes K. Fichte, Markus Hecher, and Mohamed A. Nadeem. Plausibility reasoning via pro- jected answer set counting -a hybrid approach. In IJCAI'22, pages 2620-2626. IJCAI Organization, July 2022. 28. [Fichte et al., 2022c] Johannes K. Fichte, Markus Hecher, and Irina Schindler. Default logic and bounded treewidth. Information and Computation, 2022. 29. [Fichte et al., 2023] Johannes K. Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r)evolution of sat. Commun. ACM, 66(6):64-72, May 2023. 30. [Gelfond and Lifschitz, 1991] Michael Gelfond and Vladimir Lifschitz. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9(3/4):365-386, 1991. 31. [Gelfond, 1991] Michael Gelfond. Strong Introspection. In AAAI'91, pages 386-391. AAAI Press / The MIT Press, 1991. 32. [Gottlob et al., 1999] Georg Gottlob, Nicola Leone, and Hel- mut Veith. Succinctness as a source of complexity in logical formalisms. Annals of Pure and Applied Logic, pages 231- 260, 1999. 33. [Grädel et al., 2007] Erich Grädel, Phokion G Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y Vardi, Yde Venema, Scott Weinstein, et al. Finite Model Theory and its applications. Springer, 2007. 34. [Grohe and Marx, 2014] Martin Grohe and Dániel Marx. Constraint solving via fractional edge covers. ACM Trans- actions on Algorithms (TALG), 11(1):1-20, 2014. 35. [Hecher et al., 2020] Markus Hecher, Michael Morak, and Stefan Woltran. Structural Decompositions of Epistemic Logic Programs. In AAAI'20, pages 2830-2837. AAAI Press, 2020. 36. [Hecher, 2022] Markus Hecher. Treewidth-aware reductions of normal ASP to SAT -is normal ASP harder than SAT after all? Artificial Intelligence, 304:103651, 2022. 37. [Hemachandra, 1987] Lane A. Hemachandra. The strong ex- ponential hierarchy collapses. In STOC'87, pages 110-122, New York, New York, USA, 1987. ACM. 38. [Hemaspaandra and Vollmer, 1995] Lane A. Hemaspaandra and Heribert Vollmer. The Satanic Notations: Counting Classes Beyond #P and Other Definitional Adventures. SIGACT News, 26(1):2-13, March 1995. 39. [Impagliazzo and Paturi, 2001] Russell Impagliazzo and Ra- mamohan Paturi. On the Complexity of k-SAT. Journal of Computer and System Sciences, 62(2):367-375, 2001. 40. [Kabir et al., 2022] Mohimenul Kabir, Flavio O Everardo, Ankit K Shukla, Markus Hecher, Johannes Klaus Fichte, and Kuldeep S Meel. ApproxASP -a scalable approximate answer set counter. In AAAI'22, pages 5755-5764. AAAI Press, 2022. 41. [Kahl et al., 2015] Patrick Thor Kahl, Richard Watson, Ev- genii Balai, Michael Gelfond, and Yuanlin Zhang. The Language of Epistemic Specifications (Refined) Including a Prototype Solver. J. Logic Comput., 25, 2015. 42. [Kleine Büning and Lettman, 1999] Hans Kleine Büning and Theodor Lettman. Propositional Logic: Deduction and Algorithms, volume 48 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1999. 43. [Kloks, 1994] Ton Kloks. Treewidth, Computations and Ap- proximations, volume 842 of LNCS. Springer, 1994. 44. [Lohrey and Rosowski, 2023] Markus Lohrey and Andreas Rosowski. On the complexity of diameter and related problems in permutation groups. In ICALP'23, pages 134:1- 134:18. Dagstuhl Publishing, 2023. 45. [Morak, 2019] Michael Morak. Epistemic Logic Programs: A Different World View. In ICLP'19, pages 52-64, 2019. 46. [Papadimitriou and Yannakakis, 1986] Christos H. Papadim- itriou and Mihalis Yannakakis. A Note on Succinct Repre- sentations of Graphs. Inf. Control., 71(3):181-185, 1986. 47. [Papadimitriou, 1994] Christos H. Papadimitriou. Computa- tional Complexity. Addison-Wesley, 1994. 48. [Robertson and Seymour, 1985] Neil Robertson and Paul D. Seymour. Graph Minors -a Survey. In Surveys in Combi- natorics 1985, London Mathematical Society Lecture Note Series, pages 153-171. Cambridge University Press, 1985. 49. [Shen and Eiter, 2016] Yi-Dong Shen and Thomas Eiter. Evaluating epistemic negation in answer set programming. Artificial Intelligence, 237:115-135, 2016. 50. [Stewart, 1991] Iain A. Stewart. Complete Problems Involv- ing Boolean Labelled Structures and Projection Transac- tions. J. Logic Comput., 1(6):861-882, 12 1991. 51. [Stockmeyer and Meyer, 1973] Larry J. Stockmeyer and Al- bert R. Meyer. Word problems requiring exponential time. In STOC'73, pages 1-9. ACM, 1973. 52. [Stockmeyer, 1976] Larry J. Stockmeyer. The polynomial- time hierarchy. Theoretical Computer Science, 3(1):1-22, 1976. 53. [Truszczyński, 2011a] Miroslaw Truszczyński. Revisiting Epistemic Specifications. In Logic Programming, Knowl- edge Representation, and Nonmonotonic Reasoning -Es- says Dedicated to Michael Gelfond on the Occasion of His 65th Birthday, LNCS, pages 315-333. Springer, 2011. 54. [Truszczyński, 2011b] Miroslaw Truszczyński. Trichotomy and dichotomy results on the complexity of reasoning with disjunctive logic programs. TPLP, 11(6):881-904, 2011. 55. [Valiant, 1979] Leslie G. Valiant. The complexity of com- puting the permanent. Theoretical Computer Science, 8(2):189-201, 1979. 56. [Weinzierl et al., 2020] Antonius Weinzierl, Richard Taupe, and Gerhard Friedrich. Advancing lazy-grounding ASP solving techniques -restarts, phase saving, heuristics, and more. TPLP, 20(5):609-624, 2020. 57. [Williams, 2008] Ryan Williams. Non-Linear Time Lower Bound for (Succinct) Quantified Boolean Formulas. Elec- tron. Colloquium Comput. Complex., TR08-076, 2008. 58. [Wrathall, 1976] Celia Wrathall. Complete Sets and the Polynomial-Time Hierarchy. Theoretical Computer Sci- ence, 3(1):23-33, 1976.