Body-Decoupled Grounding via Solving: A Novel Approach on the ASP Bottleneck

1 Introduction

Answer set programming (ASP) [Brewka et al., 2011; Gebser et al., 2019; Janhunen and Niemel¨a, 2016] is a modeling and solving framework that can be seen as an extension of propositional satisfiability (SAT), where knowledge is expressed by means of rules comprising a (logic) program, whose solutions are sets of atoms, called answer sets, that obey every rule. Its rich first-order like language made ASP an appealing tool for modeling industrial applications (see e.g., [Falkner et al., 2018]). Efficient systems are readily available ([Gebser et al., 2019; Calimeri et al., 2019]) and mainly build on a ground-and-solve technique, replacing variables by constants and feeding the resulting ground program into an ASP solver.

However, for certain types of problems, this ground-andsolve approach leads to the well-known ASP grounding bottleneck [Cuteri et al., 2020; Tsamoura et al., 2020], i.e., the instantiation of rules yields a program that is exponentially larger and thus too huge to be processed by the solver efficiently. We recall that the complexity for ground programs is relatively mild: consistency for disjunctive programs is located at the second level of the polynomial hierarchy, cf. [Eiter and Gottlob, 1995]; normal programs or tight programs yield NP-complete fragments [Bido´ıt and Froidevaux, 1991; Marek and Truszczy´nski, 1991]. Variables in rules increase the expressiveness and reflect the potentially huge costs of grounding: even for normal non-ground programs the complexity jumps up to NEXPTIME completeness [Dantsin et al., 2001]. While the standard grounding via rule instantation leads to an exponential blow up even for programs with bounded predicate arities, there are results that indicate that the costs of grounding can be decreased when assuming such a setting. In particular, Eiter et al. [2007] have shown that the complexity of consistency for non-ground normal programs is ΣP2 -complete. This indicates that assuming the predicate arity as fixed, there exists a polynomial translation to ground disjunctive programs, and thus an alternative grounding procedure that delegates certain efforts to the solving process.

Contributions. We provide an alternative grounding approach that utilizes the aforementioned complexity result, thereby decoupling rule bodies during grounding, which is rectified during solving. Our contributions are as follows.

1. We present a novel reduction from tight (non-ground) logic programs to disjunctive programs that encodes grounding via search, in order to identify unsatisfiable ground rules and unjustified (unfounded) atoms. In contrast to traditional grounding, our reduction allows us to decouple predicates occurring in the body of a rule, which might be particularly useful for larger bodies with a very dense structure.
2. We extend this approach to normal, non-ground programs, where for ensuring justifiability we additionally encode the idea of orderings (level mappings) in our reduction.
3. Finally, we present a prototype 1 that allows to translate critical parts of the program using our reduction, thereby empowering the grounding process by decoupling body predicates. Preliminary experiments indicate that this approach can lead to significant speed-ups, where the size of standard groundings would be excessively large.

Related Work. Efficient grounding is an active field of research and requires powerful rule initialization procedures trying to evade the intractable evaluation of non-ground programs. The literature distinguishes many approaches, ranging from traditional instantiation tactics [Gebser et al., 2019; Alviano et al., 2019; Kaminski and Schaub, 2021] over fruitful estimations [Hippen and Lierler, 2021] and lazy grounding [Bomanson et al., 2019; Weinzierl et al., 2020]. Besides, there are further attempts to avoid the grounding bottleneck, like constraint-programming or ASP modulo theory extensions, e.g., [Banbara et al., 2017; Janhunen et al., 2017; Cabalar et al., 2020], and methods based on graph invariants like treewidth [Bichler et al., 2020; Calimeri et al., 2019; Bliem et al., 2020; Mitchell, 2019]. Similar to our work, [Eiter et al., 2010] draws on the complexity of bounded arities to design space-efficient ASP evaluation methods, but their method is more in the spirit of meta-programming than on an alternative grounding procedure. Instead, we focus on decoupling body predicates and a translation to ground ASP.

1 Our system including supplemental material of this work is publicly available at https://github.com/viktorbesin/newground.

2 Preliminaries

We use mathematical vectors X=⟨x1, . . . , xm⟩, Y=⟨y1, . . . , yn⟩ in the usual way; we combine vectors by ⟨X, Y ⟩ := ⟨x1, . . . , xm, y1, . . . , yn⟩ and test whether x1 is contained in X by x1 ∈ X. Without loss of generality, we assume that elements of vectors are given in any fixed total order; for a given set S, we construct its unique vector by ⟨S⟩.

Ground ASP. Let ℓ, m, n be non-negative integers such that ℓ ≤ m ≤ n; a1, . . ., an be distinct propositional atoms. A (disjunctive) program P is a set of (disjunctive) rules

For a rule r, we let Hr :={a1, . . . , aℓ}, B+ r :={aℓ+1, . . . , am}, and Br :={am+1, . . . , an}. We denote the sets of atoms occurring in a rule r or in a program P by at(r) :=Hr ∪ B+ r ∪ Br and at(P) := ⋃r∈P at(r). A rule r is normal if |Hr| ≤ 1 and a program P is normal if all its rules are normal. The dependency graph DP is the directed graph defined on the set ⋃r∈P Hr∪B+ r of atoms, where for every rule r ∈ P two atoms a ∈ B+ r and b ∈ Hr are joined by an edge (a, b). A program P is tight if DP has no directed cycle [Fages, 1994].

An interpretation I is a set of atoms. I satisfies a rule r if (Hr ∪Br )∩I ̸=∅ or B+ r \ I ̸=∅. I is a model of P if it satisfies all rules of P. The Gelfond-Lifschitz (GL) reduct of P under I is the program PI obtained from P by first removing all rules r with Br ∩I ̸= ∅ and then removing all ¬z where z ∈ Br from the remaining rules r [Gelfond and Lifschitz, 1991]. I is an answer set of a program P if I is a minimal model (w.r.t. ⊆) of PI . The problem of deciding whether an ASP program has an answer set is called consistency, which is ΣP 2 -complete [Eiter and Gottlob, 1995]. If the input is restricted to normal programs, the complexity drops to NP-complete [Bido´ıt and Froidevaux, 1991; Marek and Truszczy´nski, 1991]. The following characterization of answer sets is often applied for normal programs [Lin and Zhao, 2003; Janhunen, 2006]. Let I be a model of a normal program P and φ be a function (ordering) φ : I → {0, . . . , |I| - 1} over I. We say a rule r ∈ P is suitable for justifying a ∈ I if (i) a ∈ Hr, (ii) B+ r ⊆ I, (iii) I ∩Br = ∅, as well as (iv) I ∩(Hr \{a}]) = ∅. An atom a ∈ I is founded if there is a rule r ∈ P justifying a, which is the case if r is suitable for justifying a and φ(b) < φ(a) for every b ∈ B+ r , and unfounded otherwise. Then, I is an answer set of P if (i) I is a model of P, and (ii) I is founded, i.e., every a ∈ I is founded. For tight programs, the ordering φ is not needed.

Non-ground ASP. Let p1, . . . pn be predicates, where each takes arity |pi| many variables for 1 ≤ i ≤ n. A (non-ground) program Π is a set of (non-ground) rules of the form

where for every variable vector Xi we have |Xi|=|pi|, and whenever x ∈ ⟨X1, . . . ,Xℓ,Xm+1, . . . ,Xn⟩, then x ∈ ⟨Xℓ+1, . . . ,Xm⟩ (safeness). For a non-ground rule r, we let Hr :={p1(X1), . . . , pℓ(Xℓ)}, B+ r :={pℓ+1(Xℓ+1), . . . , pm(Xm)}, Br :={pm+1(Xm+1), . . . , pn(Xn)}, and var(r) :={x ∈ X | p(X) ∈ Hr ∪ B+ r ∪ Br }. We use heads(Π) :={p(X) ∈ Hr | r ∈ Π}, hpreds(Π) :={p | p(X) ∈ heads(Π)}. Without loss of generality, we assume that variables are unique per rule, i.e., for every two rules r, r′ ∈ Π, we have var(r) ∩ var(r′ ) = ∅. Attributes disjunctive, normal, and tight naturally carry over to nonground rules (programs). The rule size corresponds to ∥r∥ := |B+ r | + |Br | + |Hr| and program size ∥Π∥ := ∑r∈Π ∥r∥.

In order to ground Π, we require a given set F of facts, i.e., atoms of the form p(D) with p being a predicate of Π and D being a vector over domain values of size |D| = |p|. We say that D is part of the domain of Π, defined by dom(Π) := {d ∈ D | p(D) ∈ F}. We refer to the domain vectors over dom(Π) for a variable vector X of size |X| by dom(X). Let D be a domain vector over variable vector X and vector Y contain only variables of X. We refer to the domain vector of D restricted to Y by DY . The grounding G(Π) consists of F and ground rules obtained by replacing each rule r of Form (1) for every domain vector D ∈ dom(⟨var(r)⟩) by p1(DX1 ) ∨ . . . ∨ pℓ(DXℓ ) ← pℓ+1(DXℓ+1 ), . . . , pm(DXm ),

Example 1. Consider the non-ground program Π :={r} with r=a(X, Y ) ← b(X), c(Y,Z) and F := {b(1). c(1, 2).}. Observe that dom(X)={1} and dom(Y )= dom(Z)={1, 2}. The grounding P = G(Π) of Π consists of:

The only answer set of P is {b(1), c(1, 2), a(1, 1)}.

3 Body-Decoupled Grounding via Search

In this section, we introduce our concept of body-decoupled grounding, whose idea is to reduce the grounding size by decoupling dependencies between different predicates of rule bodies. We briefly motivate the potential of this idea.

Example 2. Assume the following non-ground program Π′ that decides in (13) for each edge (e) of a given graph, whether to pick it (p) or not (¯ p). Then, in (14) it is ensured that the choice of edges does not form triangles.

The typical grounding effort of (14) is in O(|dom(Π′ )|3 ). Our approach grounds body predicates of (14) individually, yielding linear bounds in the size of facts, i.e., O(|dom(Π′ )|2 ).

Guess Answer Set Candidates

Body-Decoupled Grounding for Tight ASP. First, we present our approach for cycle-free programs without disjunction. To this end, we assume a given non-ground, tight program Π and a set F of facts. For each predicate p(X) in heads(Π), we use every instantiation of p(X) and its negation ¯ p(X) over dom(Π), resulting in atoms AtPred := {p(D), ¯ p(D) | p(X) ∈ heads(Π),D ∈ dom(X)}; the atoms over ¯ p(X) are for technical reasons only, and are not needed when emplyoing e.g., choice rules [Simons et al., 2002].

In addition to AtPred and in accordance with the semantics of ASP, we require to ensure (i) satisfiability and (ii) foundedness. For (i) computing models of rules, we require atoms AtSat :={sat, satr, satx(d) | r ∈ Π, x ∈ var(r), d ∈ dom(x)}, where sat (satr) indicates satisfiability (of non-ground rule r), respectively. An atom of the form satx(d) indicates that for checking satisfiability, we assign variable x of non-ground rule r to domain value d ∈ dom(x). For (ii) ensuring foundedness, we use variables AtUf := {ufr(DX), ufy(D⟨X,y⟩) | r ∈ Π,D ∈ dom(⟨var(r)⟩), h(X) ∈ Hr, y ∈ var(r), y /∈ X}. Intuitively, ufr(D) indicates that r fails to justify h(D) for head predicate h(X) ∈ Hr and domain vector D ∈ dom(h), where ufy(D⟨X,y⟩) refers to the assigned domain value d that variable y gets in this foundedness check for h(D). Overall, the number |AtPred ∪ AtSat ∪ AtUf | of auxiliary atoms is in O(∥Π∥ · |dom(Π)|a+1 ), where a is the largest predicate arity.

Next, we are in position to explain our reduction for tight programs. The overall idea consists of three parts and is part of the reduction R, which transforms the non-ground, tight program Π into a ground, disjunctive program R(Π) consisting of F and the rules given in Figure 1. Rules (2) take care of guessing answer set candidates, then Rules (3)-(8) ensure (i) satisfiability, and Rules (9)-(12) model (ii) foundedness.

Interestingly, the only disjunction that is indeed crucial and cannot be modeled via choice rules, is the disjunction part of Rules (3) for (i) satisfiability, which is responsible for guessing and saturating assignments of variables to domain values. The construction is such that whenever for a non-ground rule r ∈ Π, there is an assignment of variables to domain values such that the resulting ground rule is satisfied, Rules (4) or (5) yield satr. If such an atom satr can be derived for all non-ground rules of r ∈ Π, we follow sat by Rules (6), which is mandatory (cf. Rules (8)). Then, Rules (7) apply saturation, which causes the assignment of all domain values to every variable. Assuming that a grounding of a rule r ∈ Π was not satisfied, then there would exist a ⊆-smaller model of the reduct, invalidating the answer set candidate. Intuitively, the construction takes care that there is an answer set of R(Π), only if the grounding of Π admits an answer set.

Rules (9) are for (ii) preventing unfoundedness, ensuring that for each head atom h(D) contained in a model of R(Π), variables get assigned domain values for proving foundedness. Unjustifiability of a rule r ∈ Π for atom h(D) is derived by Rules (10) and (11), which is prevented by Rules (12).

See Appendix for reduction R(Π) on Π from Example 1.

Theorem 1 (Correctness). Let Π be any tight, non-ground program. Then, the grounding procedure R on Π is correct, i.e., the answer sets of R(Π) restricted to at(G(Π)) match the answer sets of G(Π). Precisely, for every answer set M ′ of R(Π) there is an answer set M ′ ∩ at(G(Π)) of G(Π).

Proof (Sketch). ⇐: Assume that M is an answer set of G(Π), but there is noM ′ ⊋M withM ′ ∩at(G(Π))=M∩at(G(Π)) that is an answer set of R(Π). This results in either (i) M being not a model of G(Π), or (ii) M being unfounded. ⇒: Let M ′ be an answer set of R(Π) and assume that M := M ′ ∩ at(G(Π)) is not an answer set of G(Π). Then, either (i) M ′ is not a model of R(Π), or (ii) M ′ is unfounded.

Notably, one can split the program and partially apply R.

Corollary 1 (Partial Reducibility). Given a tight, non-ground program Π and a partition of Π into programs Π1, Π2 with hpreds(Π1) ∩ hpreds(Π2) = ∅. Then, the answer sets of R(Π1) ∪ G(Π2) restricted to at(G(Π)) match those of G(Π).

The procedure R works in polynomial time, since our technique does not suffer from large rules (or large rule bodies).

Additional Rules for Foundedness of Normal Programs

Figure 2: (Top): More involved formalization of checking for unfounded atoms based on Observation 1, yielding alternative R′ of (cf. R of Figure 1). (Bottom): For normal, non-ground programs, we require additional rules for ensuring foundedness, yielding R′′ .

Theorem 2 (Polynomial Runtime and Grounding Size). Let Π be any tight, non-ground program, where every predicate has arity at most a. Then, the grounding procedure R on Π is polynomial, i.e., runs in time O(∥Π∥ · |dom(Π)|2·a ).

We do not expect a significant runtime improvement in the worst case. Further, the expressiveness increase from normal to disjunctive programs is inevitable (already for fixed arity).

Proposition 1 (Disjunctive Programs Inevitable). Let Π be any tight non-ground program, where every predicate has arity at most a. Then, unless NP = ΣP2 , there cannot be a polynomial grounding procedure R′ , where R′ (Π) is normal.

Proof (Idea). While consistency for normal ground programs is in NP, ΣP2 -hardness for disjunctive (head-cycle-free) nonground programs, cf. [Eiter et al., 2007, Lem. 6], can be lifted to tight non-ground programs, by observing tightness after converting disjunctive rules into normal ones via shifting.

Utilizing Variable Independencies. Having established the basic grounding procedure R, we provide an improvement based on reachable paths. For a non-ground program Π, we define the variable graph VΠ, whose vertices are the variables var(r) of rules r ∈ Π, with an edge between two x, y ∈ var(r) whenever there is a predicate p(X) in r with x, y ∈ X. Let X, Y be variable vectors. We refer by rch(Y, X) to those vertices in X that are reachable by some y ∈ Y in VΠ.

Observation 1 (Variable-Justification Independency). Given a non-ground program Π, any rule r ∈ Π with h(X) ∈ Hr and p(Y ) ∈ B+ r . Further, let I be a set of atoms over G(Π). Then, if r does not justify h(DX) ∈ I for D ∈ dom(⟨X, Y ⟩) due to p(DY ) /∈ I, we have that r fails to justify any h(D′ ) ∈ I with D′ ∈ dom(X) and D′⟨rch(Y,X)⟩ = D⟨rch(Y,X)⟩ as well.

Example 3. Recall Π of Example 1. Let I = {b(1)} and assume an arbitrary atom a(2, 1). The rule a(X, Y ) ← b(X), c(Y,Z) does not justify a(2, 1) due to b(2) /∈ I. Hence, this rule fails to justify any atom a(2, y) with y ∈ dom(Y ).

Based on the observation above, we provide an alternative of reduction R, which is preferred in case of more independent variables according to Observation 1. Instead of AtUf, we use atoms AtUfI := {ufrch(Y,X)(DX), ufy(D⟨X,y⟩)|r ∈ Π, D ∈ dom(⟨var(r)⟩), h(X) ∈ Hr, p(Y ) ∈ B+ r ∪Br , y ∈ Y, y /∈ X}. The updated reduction R′ is given in Figure 2 (top), where Rules (15) and (16) replace Rules (10) and (11) with the only difference that a different head predicate is used with a potentially smaller domain vector. Further, Rules (12) are replaced by Rules (17), which contain disjunctions in their bodies, as in the well-known weight rules [Gebser et al., 2011]. Alternatively, one can do the cross product among the sets of disjuncts of (17).

Body-Decoupled Grounding for Normal ASP. The idea of our reduction R can be also lifted to normal, non-ground programs. To this end, one can rely on orderings. To simplify the presentation, we only show a variant that uses a quadratic number of auxiliary atoms for comparison, instead of encoding orderings. We therefore use for every two distinct ground atoms p(D), p′ (D) of Π, an additional auxiliary predicate [p(D) ≺ p′ (D′ )] responsible for storing precedence in the order of derivation. Then, given R of Figure 1, for normal programs we just need to add those rules of Figure 2 (bottom), resulting in R′′ . Intuitively, Rules (18) determine precedence among different atoms and Rules (19) take care of transitivity of "≺". In addition to (15) and (16), Rules (20) add a case of unfoundedness, if precedence is not suitable for justifying.

Analogously to Theorem 1, one can show correctness of R′′ for normal, non-ground programs, including when applied to program parts as in Corollary 1. To this end, we capture predicate dependencies as follows. The dependency graph DΠ has as vertices the predicates hpreds(Π) with a directed edge from p to q whenever there is a rule r∈Π with p(X) ∈ B+ r and q(Y )∈Hr. Then, a set C⊆ hpreds(Π) of predicates is a strongly-connected component (SCC) if C is a ⊆-largest set such that for every two distinct predicates p, q in C there is a directed path from p to q in DΠ. Then, SCCs yield sufficient conditions for partially applying R′′ .

Theorem 3. Given a normal, non-ground program Π, a partition Π1,Π2 with hpreds(Π1)∩hpreds(Π2)=∅ s.t. for any SCCs C1 of DΠ1 , C2 of DΠ2 : C1∩C2=∅. The answer sets of R′′ (Π1)∪G(Π2) restricted to at(G(Π)) match those of G(Π).

4 Implemented Prototype &Experiments

We implemented a software tool, called newground, realizing body-decoupled grounding via search as described above. The system newground is written in Python3 and uses, among others, the API and of clingo 5.5 and its ability to efficiently parse logic programs via syntax trees. As Corollary 1 suggests, we opted for an implementation enabling partial reducability, allowing users to select program parts that shall be reduced and others that are (traditionally) grounded. Besides Figure 1, we utilize variable independencies, as highlighted in Figure 2 (top). Internally, we optimize by pre-compiling usual compare-operators for more compact programs. Notably, newground is not restricted to decision problems, which enables counting or (quantitative) reasoning.

In order to evaluate newground, we design a series of benchmarks. Clearly, we cannot beat highly optimized grounders in all imaginable scenarios. Instead, we discuss potential use cases, where body-decoupled grounding is preferrable, since this approach can be incorporated into every grounder. We consider these (directed) graph scenarios:

• S1 (coloring): Compute edge colorings over three colors s.t. no incoming or outgoing edges have the same color.
• S2 (paths): Find reachable paths between source and destination, where each node admits only one outgoing edge.
• S3 (clique): Obtain directed subgraphs containing cliques (fully connected subgraphs of size at least three).

S4 (nprc): Compute non-partition-removal colorings, whose encoding is taken from [Weinzierl et al., 2020].

S5 (stable marriage): Obtain so-called stable marriages; encoding taken from the ASP competition 2014.

S1 aims at providing a basic coloring problem. The decision of S2 is in P, but it can be extended; counting such paths is hard (#P-complete problem [Valiant, 1979]). Deciding S3 is polynomial-time computable, but ready to be used as part of more expressive problems. S4 (nprc) and S5 (stable marriage) are known ASP scenarios. We study Hypotheses H1-H4:

• H1: In contrast to traditional grounding, newground suffers less from increased instance density and instance size.
• H2: Body-decoupled grounding can massively reduce grounding sizes and grounding times of large instances.

H3: Body-decoupled grounding can improve overall (+solving) performance on crafted and application instances.

H4: The idea of body-decoupled grounding, where suitable, efficiently interoperates with other approaches.

Benchmark Instances. For answering the hypotheses, we use crafted (random) and applicable ASP competition instances. Note that competition instances are not designed to run into grounding bottlenecks. Therefore, we randomly generate instances for S1-S4, from 100 to 1500 vertices, with an edge probability (density) from 0.1 to 1.0. These are particularly useful to answer H1-H3. For S5, we took competition instances (plus crafted ones), which aid in analyzing H2-H4.

Benchmark Setting. We only study the performance of the following exact (full) grounders (e.g., no lazy grounding).

• gringo version 5.5.1; idlv version 1.1.6
• newground: Body-decoupled grounding is applied on certain (manually fixed, see Appendix) non-ground rules of the respective programs that potentially cause grounding overhead. The remaining part is grounded with gringo.
• newground*: newground with idlv instead of gringo.

We measure grounding sizes, grounding times, and solving capabilities of groundings. For full intercomparability, grounding size measures the size of the corresponding text output without I/O operations. The reason is that newground can be interleaved with other program parts, which fails to work with smodels or aspif formats out-of-the-box. Anyway, relative orders of magnitude of measured grounding sizes unambiguously stand. For comparing overall performance, we use solver clingo 5.5.1 with "-q --stats=2", i.e., we compute one answer set; for newground we add "--project" to ensure answer sets are over the same atoms. We limit main memory (RAM) to 16GB and overall runtimes (grounding & solving) to 1800s. Plots use cut-off grounding sizes of 10GB or 30GB.

Results: Grounding Scalability Study. For systematically studying the grounding of S1-S5, we use crafted instances and create for each solver a grounding profile. Figure 3 depicts the grounding profiles of S1 for gringo (left) and newground (right), showing grounding times and sizes, depending on the instance size (x-axis) and density (y-axis). Interestingly, for newground grounding times and sizes for a fixed instance size (column) of Figure 3 (right) are quite similar. This is in contrast to Figure 3 (left), suggesting that compared to gringo, newground is not that sensitive to instance density. Further, the rows of Figure 3 (right) are also similar. Overall, we confirm H1 (see Appendix for more data).

Results: Grounding Performance. In Figure 4 (left), we show a cactus plot of grounding times over S1-S4 for all grounders. Interestingly, newground clearly outperforms here; gringo performs second-best, except for S4 (nprc), where treewidth-based grounding seems promising. The grounding sizes over all instances for S1-S4 are given in the scatter plot Figure 4 (middle), which shows that newground massively reduces sizes (almost all dots above diagonal). Interestingly, newground solves instances, where gringo and idlv output groundings beyond 30GB. Figure 4 (right) shows a scatter plot revealing that newground improves grounding times (blue/green dots above diagonal). Among those below the diagonal, most dots are below 250s (y-axis), suggesting a portfolio that uses gringo or idlv for 250s and switches to newground if unsuccessful. The orange dots represent overall runtimes among solved instances, showing that no instance below the diagonal (where newground falls behind) can be solved in more than 250s. Overall, we confirm H2.

Results: Overall Performance. For a deeper study of overall (solving) performance, we refer to the cactus plot of Figure 5 (left), showing runtimes for S1-S4. While newground performs best, we still see a clear difference between solving and grounding performance (cf. Figure 4). One could believe that analyzing combined grounding and solving is unfair for gringo and idlv, since newground grounds faster. However, Figure 4 (left) shows that for, e.g., S2 and S3, there are many instances grounded by gringo within 200s. Interestingly, Figure 5 (left) reveals that only a small amount of those can then actually be solved by clingo within the remaining 1600s. This is also visible in Figure 5 (right), which depicts a cactus plot for S5 over grounding as well as overall runtime. We expect potential to optimize clingo's internal handling of large programs (big data) for better utilizing newground's grounding performance. However, we confirm H3; and H4 due to the integration of newground with gringo and idlv.

5 Conclusion, Discussion &FutureWork

This work introduces a technique on body-decoupled grounding, where grounding-intense ASP rules are treated by means of a novel reduction. The reduction translates tight (normal) non-ground rules into disjunctive ground rules, thereby being exponential only in the maximum predicate arity. Our empirical evaluation shows an advantage: Compared to state-ofthe-art exact grounders, body-decoupled grounding applied on crucial program parts massively reduces grounding size.

We plan on integrating our approach into (intelligent) grounders, aiming for heuristics that automatically estimate program parts where newground likely pays off. Further, our approach could be extended to disjunctive non-ground programs, which unfortunately is ΣP3 -complete for bounded arity [Eiter et al., 2007]. However, we expect "almost tightness" notions, e.g., [Fandinno and Hecher, 2021; Hecher, 2022], to aid in reducing heavy rules for disjunctive atoms.

Acknowledgments

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