# epistemic_logic_programs_nonground_and_counting_complexity__8974b446.pdf Epistemic Logic Programs: Non-Ground and Counting Complexity Thomas Eiter1 , Johannes K. Fichte2 , Markus Hecher3 , Stefan Woltran1 1Institute of Logic and Computation, TU Wien 2Department of Computer and Information Science (IDA), Link oping University 3Computer Science & Artificial Intelligence Laboratory, Massachusetts Institute of Technology thomas.eiter@tuwien.ac.at, johannes.fichte@liu.se, hecher@mit.edu stefan.woltran@tuwien.ac.at, 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 wellknown program fragments, which turns out to be complete for the class NEXPTIME with access to oracles up to ΣP 2 . 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. 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 ETH1 rendering significant runtime improve- 1The exponential time hypothesis (ETH) implies 3-CNF satisfiability cannot be solved in time 2o(n) [Impagliazzo and Paturi, 2001]. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24) 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 ΣP 3-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, P 0 := ΠP 0 := ΣP 0 := P and P i := P Σp i 1, ΣP i := NPΣP i, and ΠP i := co NPΣP i for i > 0 where CD is the class C of decision problems augmented by an oracle for some complete problem in class D. The complexity class DP k is defined as DP k := { L1 L2 | L1 ΣP k, L2 ΠP k } and DP = DP 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 2n O(1), i.e., NEXPTIME = S 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 NEXPNP. The weak EXP hierarchy (EXPH) is defined in terms of oracle complexity classes: ΣEXP 0 := EXP and ΣEXP i+1 := NEXPΣp i [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 a1 . . . ak ak+1, . . . , am, am+1, . . . , an, where all ai are distinct atoms and 0 k m n. We let Hr:={a1, . . . , ak}, B+ r :={ak+1, . . . , am}, and B r := {am+1, . . . , an}, and denote the set of atoms occurring in r and P by at(r):=Hr B+ r B r , at(P):= S 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 B r = ; a constraint if Hr = ; positive if B r = ; 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 S 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). Program P 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) := S a A arg(a) resp. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24) EHorn Tight Normal Full Result Qualitative Ground P ΣP 2 ΣP 2 ΣP 3 [Truszczy nski, 2011b] [Shen and Eiter, 2016] Non-Ground EXP NEXPNP NEXPNP NEXPΣP 2 Theorem 4, Lemma 5 Non-Ground(b) CONP ΣP 3 ΣP 3 ΣP 4 Theorem 4, Lemma 5 Quantitative Ground #P # DP # DP # DP 2 Lemma 15 Non-Ground #EXP #EXPNP #EXPNP #EXPΣP 2 Theorem 14 Non-Ground(b) # DP # DP 2 # DP 2 # DP 3 Lemma 16 Parameterized Ground [tw] exp(1, o(tw)) exp(2, Θ(tw)) exp(2, Θ(tw log(tw))) exp(3, Θ(tw)) [Fandinno and Hecher, 2023] Non-Gr. [tw](b)exp(1, do(tw)) exp(2, dΘ(tw)) exp(2, dΘ(tw)) exp(3, dΘ(tw)) Theorems 19,20 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. vars(A) := S 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 program P 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 B r ) 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 := S r P { Hr B+ r | B r 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) := S 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 B r ) 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 ΣP 2-complete for ground programs [Eiter and Gottlob, 1995a] and NEXPNP 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 := {r I | r P}, where r I 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. A WVI 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 T 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 ΣP 3-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. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24) Example 1 (cf. Gelfond 1991). Take the well-known scholarship eligibility problem encoding, which is as follows: P1 = { low GPA(mark); high GPA(mia); low GPA(maya) high GPA(maya); inelig(X) low GPA(X); elig(X) high GPA(X); elig(X), inelig(X); interview(X) not elig(X), not inelig(X) }. Then, the set of WVs of the program is { { interview(mark), low GPA(mark), inelig(mark), elig(mark), interview(maya), interview(mia), high GPA(mia), elig(mia), inelig(mia)} }. Firstand 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 Σ1 k[σ] consists of all prenex second-order formulas Φ SO[σ], i.e., Φ = Q1R1Q2R2 Qk Rk.φ 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 Φ Σ1 k and a finite structure A, deciding whether A |= Φ is (i) NEXPΣP k 1-complete (combined complexity) and (ii) ΣP kcomplete 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 Φ Σ1 k[σ] in CDNF and a finite structure A, deciding whether A |= Φ is (i) NEXPΣP k 1complete and (ii) ΣP k+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ΣP i-c for non-ground P and ΣP i+2c 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 Σp i+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 Σp j becomes NEXPΣP j 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 Σp 3 and Πp 3, respectively, [Eiter et al., 2007]. Consequently, we can check in polynomial time with an Σp 3 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 Σp 4, i.e., P Full. If P Tight Normal, brave and cautious reasoning from PI,pnot is in Σp 2 and Πp 2, respectively, [Eiter et al., 2007], as program PI,pnot is normal/tight, if program P is so. This shows membership in Σp 3. Hardness: We construct from a given sentence Φ Σ1 k 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.φ Σ1 k where φ = xψ and ψ = Vm j=1 Wℓ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) := c A 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. P1 = {R1,i(e( x1,i)) not R1,i(e( x1,i)); R1,i(e( x1,i)) not R1,i(e( x1,i)) | R1,i R1}. Program P2 generates then answer sets for each possible relation R2,i in R2. P2 = {R2,i(e( x2,i)) R2,i(e( x2,i)); R2,i(e( x2,i)) R2,i | R2,i R2} Programs P3 guesses for each such valuation of R2 a valuation of R3 such that xψ is true. P3 = {R3,i(e( x3,i)) R3,i(e(x3,i)) | R3,i R3} The program P4 checks then using the saturation technique that xψ is not violated, i.e., x ψ is false; any violation Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24) makes u true and saturates the guess. The last rule in P4 eliminates the candidate world view if u cannot be derived. P4 = {u s(Lj,1), . . . , s(Lj,ℓj) | 1 j m} {R3,i(e( x3,i)) u; R3,i(e( x3,i)) u | R3,i R3} {v not v, not u}. 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. P5 = {Ri( c) | c RA i , c U | c|, 1 i k}. Notably, we treat equality as the other relations. Finally, we build the program P = S5 i=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 ψ = Wm j=1 Vℓj h=1 Lj,h is a DNF, drop P3, and replace P4 with the following rules: P 4 = {u Lj,1, . . . , Lj,ℓj | 1 j m} {v not v, not u}. 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 = #EXPP. 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 bk j 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 = b1 j, . . . , 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(φ) \ (S 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, Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24) 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 form Mℓ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. Theorem 14 ( ). 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ΣP i-complete. Proof. Membership: This follows immediately from the ground case (propositional) where we have Σp i+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 Σp j becomes NEXPΣP j 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 a conjunction gate g with inputs g1, . . . , go, we define g (s1, v1, s2, v2, s3, v3) g1(s1, v1, s2, v2, s3, v3), . . . , go(s1, v1, s2, v2, s3, v3); for disjunction gate g with inputs g1, . . . , go, we define for every 1 k o: g (s1, v1, s2, v2, s3, v3) gk(s1, v1, s2, v2, s3, v3). We refer to the predicate of the final output gate of the construction by g C. 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: V (v1, . . . , vn) M V (v1, . . . , vn), b(v1), . . . , b(vn). Then, we check whether there is an unsatisfied clause. V ( v1), g C(1, v1, s2, v2, s3, v3), V ( v2), g C(s1, v1, 1, v2, s3, v3), V ( v3), g C(s1, v1, s2, v2, 1, v3). 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 g C. 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 g ( v1) g(ι, v1), b(ι), b(v1 1), . . . , b(vn 1 ); for a conjunction gate g with inputs g1, . . . , go, we define g (ι, v1) g1(ι, v1), . . . , go(ι, v1); 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 g D. 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), g D(1, v1, . . . , vn). A(v1, . . . , vn) not A(v1, . . . , vn), g D(1, v1, . . . , vn). A(v1, . . . , vn) A(v1, . . . , vn), g D(2, v1, . . . , vn). A(v1, . . . , vn) A(v1, . . . , vn), g D(2, v1, . . . , vn). Then, we check whether all terms are dissatisfied. usat(1, v1, s2, v2, s3, v3) A( v1), g C(1, v1, s2, v2, s3, v3) usat(0, v1, s2, v2, s3, v3) A( v1), g C(0, v1, s2, v2, s3, v3) usat(s1, v1, 1, v2, s3, v3) A( v2), g C(s1, v1, 1, v2, s3, v3) usat(s1, v1, 0, v2, s3, v3) A( v2), g C(s1, v1, 0, v2, s3, v3) usat(s1, v1, s2, v2, 1, v3) A( v3), g C(s1, v1, s2, v2, 1, v3) usat(s1, v1, s2, v2, 0, v3) A( v3), g C(s1, v1, s2, v2, 0, v3). We prohibit WVs with an answer set satisfying a term. sat g C(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 # DP i -complete. If the arity is a fixed constant, we obtain the following. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24) 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 # DP 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, d O(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ΣP 3. We mitigate resulting high complexity by bounding predicate arities. Then, the complexity drops, ranging from ΣP 2 to ΣP 4. 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. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24) 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 Exz F-0004; and Vienna Science and Technology Fund (WWTF) grants ICT19-065 and ICT22-023. [Aliseda, 2017] Atocha Aliseda. The Logic of Abduction: An Introduction, pages 219 230. Springer, Cham, 2017. [Arora and Barak, 2009] Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. [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. [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. [Besin et al., 2023] Viktor Besin, Markus Hecher, and Stefan Woltran. On the structural complexity of grounding - tackling the ASP grounding bottleneck via epistemic programs and treewidth. In ECAI 23, pages 247 254. IOS Press, 2023. [Bichler et al., 2020] Manuel Bichler, Michael Morak, and Stefan Woltran. selp: A single-shot epistemic logic program solver. TPLP, 20(4):435 455, 2020. [Bonet, 2010] Blai Bonet. Conformant plans and beyond: Principles and complexity. Artificial Intelligence, 174(3):245 269, 2010. [Brewka et al., 2011] Gerhard Brewka, Thomas Eiter, and Mirosław Truszczy nski. Answer set programming at a glance. Comm. of the ACM, 54(12):92 103, 2011. [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. [Cook, 1971] Stephen A. Cook. The Complexity of Theorem Proving Procedures. In STOC 71, pages 151 158. ACM, 1971. [Dantsin et al., 2001] Evgeny Dantsin, Thomas Eiter, Georg Gottlob, and Andrei Voronkov. Complexity and expressive power of logic programming. ACM Comput. Surv., 33(3):374 425, 2001. [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. [Eiter and Gottlob, 1995a] Thomas Eiter and Georg Gottlob. On the computational cost of disjunctive logic programming: Propositional case. Annals of Mathematics and Artificial Intelligence, 15(3 4):289 323, 1995. [Eiter and Gottlob, 1995b] Thomas Eiter and Georg Gottlob. The Complexity of Logic-Based Abduction. Journal of the ACM, 42(1):3 42, 1995. [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. [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. [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. [Eiter et al., 2007] Thomas Eiter, Wolfgang Faber, Michael Fink, and Stefan Woltran. Complexity results for answer set programming with bounded predicate arities and implications. Annals of Mathematics and Artificial Intelligence, 51(2-4):123 165, 2007. [Eiter et al., 2024] Thomas Eiter, Johannes K. Fichte, Markus Hecher, and Stefan Woltran. Epistemic logic programs: Non-ground and counting complexity. Co RR, 2024. Extended Version of a paper that has been accepted for publication at IJCAI 24. [Fages, 1994] Franc ois Fages. Consistency of Clark s completion and existence of stable models. Logical Methods in Computer Science, 1(1):51 60, 1994. [Fandinno and Hecher, 2023] Jorge Fandinno and Markus Hecher. Treewidth-aware complexity for evaluating epistemic logic programs. In IJCAI 23, pages 3203 3211. ijcai.org, 2023. [Fandinno et al., 2022] Jorge Fandinno, Wolfgang Faber, and Michael Gelfond. Thirty years of epistemic specifications. TPLP, pages 1043 1083, 2022. [Fari nas del Cerro et al., 2015] Luis Fari nas del Cerro, Andreas Herzig, and Ezgi Iraz Su. Epistemic equilibrium logic. In IJCAI, pages 2964 2970, 2015. [Fichte et al., 2015] Johannes K. Fichte, Mirosław Truszczy nski, and Stefan Woltran. Dual-normal logic programs the forgotten class. TPLP, 15(4 5):495 510, 2015. [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. [Fichte et al., 2022a] Johannes K Fichte, Sarah Alice Gaggl, and Dominik Rusovac. Rushing and strolling among answer sets navigation made easy. In AAAI 2022, 2022. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24) [Fichte et al., 2022b] Johannes K. Fichte, Markus Hecher, and Mohamed A. Nadeem. Plausibility reasoning via projected answer set counting - a hybrid approach. In IJCAI 22, pages 2620 2626. IJCAI Organization, July 2022. [Fichte et al., 2022c] Johannes K. Fichte, Markus Hecher, and Irina Schindler. Default logic and bounded treewidth. Information and Computation, 2022. [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. [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. [Gelfond, 1991] Michael Gelfond. Strong Introspection. In AAAI 91, pages 386 391. AAAI Press / The MIT Press, 1991. [Gottlob et al., 1999] Georg Gottlob, Nicola Leone, and Helmut Veith. Succinctness as a source of complexity in logical formalisms. Annals of Pure and Applied Logic, pages 231 260, 1999. [Gr adel et al., 2007] Erich Gr adel, 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. [Grohe and Marx, 2014] Martin Grohe and D aniel Marx. Constraint solving via fractional edge covers. ACM Transactions on Algorithms (TALG), 11(1):1 20, 2014. [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. [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. [Hemachandra, 1987] Lane A. Hemachandra. The strong exponential hierarchy collapses. In STOC 87, pages 110 122, New York, New York, USA, 1987. ACM. [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. [Impagliazzo and Paturi, 2001] Russell Impagliazzo and Ramamohan Paturi. On the Complexity of k-SAT. Journal of Computer and System Sciences, 62(2):367 375, 2001. [Kabir et al., 2022] Mohimenul Kabir, Flavio O Everardo, Ankit K Shukla, Markus Hecher, Johannes Klaus Fichte, and Kuldeep S Meel. Approx ASP a scalable approximate answer set counter. In AAAI 22, pages 5755 5764. AAAI Press, 2022. [Kahl et al., 2015] Patrick Thor Kahl, Richard Watson, Evgenii Balai, Michael Gelfond, and Yuanlin Zhang. The Language of Epistemic Specifications (Refined) Including a Prototype Solver. J. Logic Comput., 25, 2015. [Kleine B uning and Lettman, 1999] Hans Kleine B uning and Theodor Lettman. Propositional Logic: Deduction and Algorithms, volume 48 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1999. [Kloks, 1994] Ton Kloks. Treewidth, Computations and Approximations, volume 842 of LNCS. Springer, 1994. [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. [Morak, 2019] Michael Morak. Epistemic Logic Programs: A Different World View. In ICLP 19, pages 52 64, 2019. [Papadimitriou and Yannakakis, 1986] Christos H. Papadimitriou and Mihalis Yannakakis. A Note on Succinct Representations of Graphs. Inf. Control., 71(3):181 185, 1986. [Papadimitriou, 1994] Christos H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994. [Robertson and Seymour, 1985] Neil Robertson and Paul D. Seymour. Graph Minors a Survey. In Surveys in Combinatorics 1985, London Mathematical Society Lecture Note Series, pages 153 171. Cambridge University Press, 1985. [Shen and Eiter, 2016] Yi-Dong Shen and Thomas Eiter. Evaluating epistemic negation in answer set programming. Artificial Intelligence, 237:115 135, 2016. [Stewart, 1991] Iain A. Stewart. Complete Problems Involving Boolean Labelled Structures and Projection Transactions. J. Logic Comput., 1(6):861 882, 12 1991. [Stockmeyer and Meyer, 1973] Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time. In STOC 73, pages 1 9. ACM, 1973. [Stockmeyer, 1976] Larry J. Stockmeyer. The polynomialtime hierarchy. Theoretical Computer Science, 3(1):1 22, 1976. [Truszczy nski, 2011a] Miroslaw Truszczy nski. Revisiting Epistemic Specifications. In Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning - Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday, LNCS, pages 315 333. Springer, 2011. [Truszczy nski, 2011b] Miroslaw Truszczy nski. Trichotomy and dichotomy results on the complexity of reasoning with disjunctive logic programs. TPLP, 11(6):881 904, 2011. [Valiant, 1979] Leslie G. Valiant. The complexity of computing the permanent. Theoretical Computer Science, 8(2):189 201, 1979. [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. [Williams, 2008] Ryan Williams. Non-Linear Time Lower Bound for (Succinct) Quantified Boolean Formulas. Electron. Colloquium Comput. Complex., TR08-076, 2008. [Wrathall, 1976] Celia Wrathall. Complete Sets and the Polynomial-Time Hierarchy. Theoretical Computer Science, 3(1):23 33, 1976. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)