Bypassing the ASP Bottleneck: Hybrid Grounding by Splitting and Rewriting

1 Introduction

Answer set programming (ASP) [Brewka et al., 2011; Gebser et al., 2019] is a prominent modeling and solving framework, where problems are modeled by means of rules that form a (logic) program. The solutions of such programs are called answer sets, which are sets of atoms that fulfill every rule. A huge contribution to the success story and practical relevance of ASP is the availability of efficient systems [Gebser et al., 2019; Alviano et al., 2019]. These systems are based on a ground-and-solve pattern, where a grounder replaces firstorder like variables by domain constants, thereby creating a ground program that is solved by means of an ASP solver.

Over the time, the ground-and-solve pattern enabled ASP to grow into a rich and expressive language supporting complex expressions like aggregates [Alviano and Faber, 2018]. This makes ASP a convenient tool for formulating problems in domains like knowledge representation, artificial intelligence, and even in industrial contexts, see e.g., [Falkner et al., 2018]. Aggregates are particularly useful to compactly express complex scenarios and are implemented in modern grounders, such as gringo [Kaminski and Schaub, 2022] and idlv [Calimeri et al., 2019].

Undoubtedly, there is a huge downside to the groundand-solve pattern, as it may lead to the well-known ASP grounding bottleneck [Gebser et al., 2018; Cuteri et al., 2020; Tsamoura et al., 2020] - an issue, where the grounder creates an exponentially large program beyond solving capabilities. While this is a major source of inefficient encodings, this issue is far from surprising, as already the evaluation of normal programs is NEXPTIME-complete [Dantsin et al., 2001]. However, as shown by Eiter et al., [2007], for constant predicate arities the complexity of non-ground answer set existence increases by only one level in the polynomial hierarchy, compared to ground programs (i.e., hardness of deciding answer set existence grows for normal programs from NP [Marek and Truszczy´nski, 1991] to ΣP 2 and for disjunctive programs from ΣP 2 [Eiter and Gottlob, 1995] to ΣP 3 ).

These insights have been recently utilized to mitigate the grounding bottleneck, resulting in body-decoupled grounding (BDG) [Besin et al., 2022] and other variants [Dodaro et al., 2023] of shifting effort from the grounder to the solver. BDG provides an efficient alternative to cope with large rule bodies, as body elements are grounded independently, i.e., it is exponential only in the maximum predicate arity and not in the number of variables of the whole body. However, this technique comes with limitations, as for small rule bodies it is outperformed by traditional grounding. In practice, some combination of both concepts is therefore well desired. To date (i) BDG supports only very limited interoperability with traditional grounding (if programs Π1 and Π2 shall be grounded via BDG and traditional grounding, respectively, a predicate is prohibited to appear in rule heads of both programs), and crucially, (ii) BDG does not support aggregates yet, which are one of the main sources of huge groundings.

Contributions 1 . We address both shortcomings (i) and (ii):

1. First, we propose hybrid grounding, which aims at com-

1 Supplementary material including source code, benchmark instances and experimental results, are available online: https://github. com/alexl4123/newground/releases/tag/v2.0.0.

bining the best of both traditional grounding and BDG. We thereby develop a novel splitting theorem to enable arbitrary partitions of a non-ground normal program Π into a tight program 2 Πt with dense rule bodies 3 , and a potentially cyclic part Πc, forming the remainder. Program Πt is then grounded similar to BDG, where we avoid large grounding sizes caused by dense rule bodies and delay efforts to the ASP solver. In turn, Πc benefits from efficient traditional grounding of small rule bodies.

1. We define novel rewriting methods on translating hardto-ground aggregate expressions, such that we ease the grounding of aggregates with a dense body. We then utilize hybrid grounding, where the translated rules are subject to BDG, i.e., put into Πt. Thereby, we provide an alternative approach beyond traditional variable instantiation. To deal with aggregation in different contexts, we provide variants of our translation.
2. Finally, we present an implementation of our translationbased approach on the ASP grounding bottleneck in Python, where we provide support for commonly used ASP aggregates. In our experimental evaluation, we compare two rewritings, demonstrating that hybrid grounding on these translations is capable of grounding dense aggregates beyond the state-of-the-art.

Related Work. The literature distinguishes alternative grounding approaches, ranging from classical techniques [Alviano et al., 2019; Kaminski and Schaub, 2022], numerical techniques [Hippen and Lierler, 2021], lazy rule injection [Cuteri et al., 2017], and lazy grounding [Weinzierl et al., 2020], over ASP modulo theory, e.g., [Banbara et al., 2017], and methods based on structural measures, e.g., [Bichler et al., 2020; Mitchell, 2019; Calimeri et al., 2019]. There are existing works on translating aggregates, e.g., [Bartholomew et al., 2011; Zaniolo et al., 2017; Pelov et al., 2003; Bomanson et al., 2014]. Earlier works on splitting, e.g., [Lifschitz and Turner, 1994] do not focus on grounding strategies.

2 Preliminaries

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 a1∨ . . . ∨ aℓ ← aℓ+1, . . . , am, ¬am+1, . . . , ¬an. 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 vertices ⋃r∈P Hr ∪ B+ r , s.t. for every r∈P two atoms a∈B+ r and b∈Hr are joined by edge (a, b). A head-cycle of DP is an {a, b}-cycle 4 for two distinct atoms a, b ∈ Hr for some rule r ∈ P. P is head-cycle-free (HCF) or tight if DP contains no head-cycle or cycle, respectively.

2 We can relax this condition, which causes an additional subquadratic overhead in the form of level mappings [Janhunen, 2006].

3 A rule body is dense if it contains a large number of predicates

4 Let G = (V, E) be a digraph and W ⊆ V . Then, a (directed) cycle in G is a W-cycle if it contains all vertices fromW.

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 P I 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. I is an answer set of a program P if I is a minimal model (w.r.t. ⊆) of P I . Deciding whether a program has an answer set is called consistency, which is ΣP 2 -complete [Eiter and Gottlob, 1995]. For normal and HCF programs, its complexity drops to NP-complete [Marek and Truszczy´nski, 1991; Ben-Eliyahu and Dechter, 1994]. For an interpretation I, a level mapping ψ : I → {0, . . . , |I| - 1} assigns every atom in I a unique value [Lin and Zhao, 2003; Janhunen, 2006]. Given an interpretation I of an HCF program Π and a level mapping ψ of I. An atom a ∈ I is founded if for an r ∈ Π with a ∈ Hr, we have B+ r ⊆ I, ψ(b) < ψ(a) for every b ∈ B+ r , and I ∩ Br = I ∩ (Hr \ {a}) = ∅. I is an answer set of Π if (i) I is a model of Π, and (ii) all atoms in I are founded.

Non-ground ASP. We use 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 in X by x1 ∈ X. Elements of vectors are in any fixed total order. For a set S, we construct its unique vector by ⟨S⟩.

A term is a constant, or a variable. Let p1, . . . , pn be predicates; each one takes arity |pi| many variables for 1 ≤ i ≤ n. A comparison is a predicate of the form t ≺ u, where t, and u are terms, and ≺∈ {<, ≤, >, ≥, =, ̸=}, in their usual meaning. A literal is a predicate, or its negation. 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 nonground rule r, we define Hr :={p1(X1), . . . , pℓ(Xℓ)}, B+ r :={pℓ+1(Xℓ+1), . . . , pm(Xm)}, as well as Br :={pm+1(Xm+1), . . . , pn(Xn)}. We furthermore define Br :=B+ r ∪Br , var(r) :={x ∈ X | p(X) ∈ Hr∪Br}, and use hpred(Π) :={p(X) ∈ Hr | r ∈ Π} and pred(Π) :={p(X) ∈ (Hr ∪ Br) | r ∈ Π}. For brevity, we assume variables are unique per rule, i.e., for every two rules r, r′∈Π, var(r) ∩ var(r′ )=∅. Attributes disjunctive, normal, and tight carry over to rules (programs). 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 containing only variables of X. We refer to the domain vector D restricted to Y by DY. The grounding G(Π) comprises F and rules obtained by replacing each rule r of Form (1) for every D ∈ dom(⟨var(r)⟩) by p1(DX1 ) ∨ . . . ∨ pℓ(DXℓ ) ← pℓ+1(DXℓ+1 ), .., pm(DXm ), ¬pm+1(DXm+1 ), .., ¬pn(DXn ). The dependency graph DΠ of the non-ground program Π is defined over the ground program G(Π); scc(Π) refers to the set of strongly-connected components (vertices) of DΠ.

Example 1. Consider the non-ground program Π1 :={r1} with r1 = a(X, Y ) ← b(X), c(Y, Z), d(Y ) and F1 :={b(1); c(1, 2); c(2, 1); d(1)}. Observe that dom(X)={1} and dom(Y )=dom(Z)={1, 2}. Grounding G(Π1) comprises: {b(1); c(1, 2); c(2, 1); d(1); a(1, 1)←b(1), c(1, 1), d(1); a(1, 1)←b(1), c(1, 2), d(1); a(1, 2)←b(1), c(2, 1), d(2); a(1, 2)←b(1), c(2, 2), d(2)} The answer set of Π1 is {b(1); c(1, 2); c(2, 1); a(1, 1); d(1)}.

Aggregates. We denote aggregates as specified in the ASPCore-2 standard [Calimeri et al., 2020]. Let T = ⟨t1, . . . , to⟩ be a term vector and L = ⟨l1(Y 1), ..., lk(Y k)⟩ be a literal vector. An (aggregate) element e is of the form T : L, where T is the head of e of length o and L is its body. We require variables in T to occur in a non-negated predicate of L. We refer to E = {e1, . . . , eα} as the element multiset (|E| = α). An aggregate is of the form aggr{E} ≺ u, aggr ∈ {count,sum,min,max}, u is a term, and ≺∈ {<, ≤, >, ≥, =, ̸=}. An aggregate may occur in Br of a non-ground rule r; a variable X of some body of an element ej ∈ E that also occurs in Br, is a global variable, i.e., the aggregate has a variable dependency on X.

To evaluate an aggregate aggr{E}≺u, it is grounded, thereby replacing variables by domain values. Then, those ground element heads in E, whose element body hold, are collected, resulting in a set R of domain vectors. We apply aggr on R, where count(R), sum(R), min(R), and max(R) are evaluated under the usual semantics. Finally, we determine aggr(R) ≺ u.

Example 2. Consider the non-ground program Π2 :={r2} with r2 = ← e(X, Y ), count{A, B : e(A, B), f(A, X); A : g(A), e(A, Y ); A : h(A)} ≥ 3. and F2 :={e(1, 1); f(1, 1); g(1); g(2); h(1); h(3)}. Note that the element tuple sets are R1 = {(1, 1)}, R2 = {(1)}, and R3 = {(1), (3)}. Further, the combined one is R = R1 ∪ R2 ∪ R3. Grounding G(Π2) results in the following program, which has no answer set: {e(1, 1); f(1, 1); g(1); g(2); h(1); h(3); ←e(1, 1), count{(1, 1), (1), (3)} ≥ 3}

In general, we rewrite aggregate expressions to non-ground programs, for enabling efficient hybrid grounding. Still, we define for aggregate programs the dependency graph DΠ, and scc(Π) analogously. Further, we require a rule r containing an aggregate that the corresponding pi(DXi ) ∈ Hr, and pj(DXj ) ∈ B+ r are not contained in a cycle in DΠ. However, there are proposals for recursive aggregate semantics, e.g., [Ferraris, 2011; Faber et al., 2011; Gelfond and Zhang, 2019]. However, these are not contained in the agreed ASPCore-2 standard, as supported by current ASP systems.

3 A Splitting Theorem for Hybrid Grounding

First, we provide new insights into a hybrid grounding strategy that allows us to significantly strengthen body-decoupled grounding (BDG) [Besin et al., 2022]. More concretely, we split a program into parts, which enables to individually combine body-decoupled grounding on dense tight rules, with classical grounding for the remainder of the program. This yields a stronger result, which we call hybrid grounding, where we provide a way to freely split a non-ground program Π into two parts: A dense tight program Πt and the remainder Πc = Π \ Πt. This flexibility will then pave the way towards the efficient grounding of dense aggregates, using different translations to a (tight) program.

Example 3. We demonstrate the potential of hybrid grounding by a small example. Consider the non-ground program Π3 :={r3a; r3b} with r3a =a(X) ← b(X), r3b =a(X) ← c(X), e(A,B), e(A,C), e(B,C), and facts F3 :={b(1);c(2)}∪G, whereG is a graph given by edge facts (e). Rule r3b uses 4 (densely) interacting variables, i.e., intuitively r3b is denser than r3a. In practice, one would therefore ground r3a with state-of-the-art grounders and r3b with BDG, avoiding groundings that are cubic in the domain size.

BDG, in contrast to hybrid grounding, explicitly prohibits shared predicates (here: a) and the result would be indeed wrong. We derive a(1) from r3a using fact b(1). Crucially, r3b can never derive a(1), as there is no fact c(1). Since a(1) was derived, but can not be justified by BDG (rule r3b), the constructed program does not have an answer set.

In order to ensure correctness of hybrid grounding for any partitioning into two programs Πc, Πt, despite the fact that (shared) atoms can be derived by both programs (individually), we use auxiliary predicates p′ for predicates p appearing in the head of the rules in Πt. This will allow us to distinguish the (potentially interleaving) cases, where an atom is founded by Πc and those where the atom is derived due to Πt.

Hybrid Grounding Procedure. First, we discuss a simplified variant of hybrid grounding, where we only permit cyclic dependencies within Πc, but not between Πt and Πc. Crucially, we ensure that atoms are correctly derived, despite shared predicates between Πc and Πt, thereby bijectively preserving all answer sets.

Figure 1 depicts hybrid grounding procedure H. First, by Rules (2) we guess whether an atom can be derived by means of Πt. Further, these rules ensure that atoms over auxiliary predicates h′ (i.e., those derived by means of Πt) are copied to atoms over h. This is crucial, as these rules ensure the link between Πt and Πc, but also contribute to rule satisfiability of Πt, as discussed below. Then, Rules (3) ground Πc by classical means (i.e., rule instantiation). Note that in this step, practical grounders might simplify or remove rules of Πc. However, this can be avoided by grounding Πc together with (non-ground versions of) Rules (2).

Then, Rules (4)-(8) ensure rule satisfiability of Πt. This is achieved by guessing every potential instantiation in Rules (4), applying the saturation technique in Rules (8), and deriving rule satisfiability via avoiding rule body combinations due to Rules (5)-(7). Observe that the latter rules only use a single (body) predicate of Πt. After that, rule satisfiability can be derived for all rules of Πt by Rules (4), which is mandatory due to (8).

Finally, Rules (9)-(12) of Figure 1 ensure that, in addition to satisfiability of rules in Πt, every atom that is guessed via Rules (2) is indeed founded. To this end, it is sufficient to find a suitable rule instantiation via Rules (9) for such an atom, and derive unfoundedness for a rule, again, by decoupling body atoms due to Rules (10) and (11), such that not every rule yields unfoundedness for that atom, see Rules (12). Note that the latter rules are relaxed such that these rules are only generated for atoms that are derived due to Πt, i.e., if the atom over the auxiliary predicate p′ holds.

Despite Rules (2), we bijectively preserve all answer sets.

Lemma 1. Given a partition of any non-ground HCF program Π into a program Πc and a tight program Πt=Π \ Πc, such that for every S ∈ scc(Π), we have |E(SΠt )| = 0, where E(SΠt ) is the edge set of the subgraph SΠt of DΠt induced by S ∩ at(Πt). Then, the answer sets of H(Πc, Πt) restricted to at(G(Π)) bijectively match those of G(Π).

Proof (Sketch). Correctness of BDG under the assumption hpred(Πc) ∩ hpred(Πt) = ∅ has been shown in [Besin et al., 2022]. In this case, predicates hpred(Πc), hpred(Πt) can only appear in rule bodies of Πt, Πc, respectively. Therefore, foundedness of atoms over predicates hpred(Πt) is checked by Rules (9)-(12) and foundedness of atoms over hpred(Πc) is derived directly by Rules (3). Satisfiability of Πt is ensured by Rules (4)-(8); satisfiability of Πc is treated by Rules (3).

Suppose hpred(Πc) ∩ hpred(Πt) ̸= ∅. As now atoms over hpred(Πc), hpred(Πt) may be derived in Πc, Πt but may also appear in rule heads of Πt, Πc, respectively, this might lead to incorrect results. We rename all head predicates h(X) ∈ hpred(Πt) to h′ (X). This (again) ensures foundedness of atoms over hpred(Πt) and satisfiability of Πt, only by Rules (9)-(12) and (4)-(8) , respectively, while Πt continues to use atoms derived by Πc in its rule bodies. However, Πt has to inform Πc about atoms derived in Πt, ensured by Rules (2). This still applies if Πc is cyclic, as long as there is no shared cycle between Πc and Πt.

It remains to argue, why despite Rules (2), every answer set M of H(Πc, Πt) has a unique answer set M ∩at(Π) of Π. Consider an arbitrary h(D) ∈ at(G(Π)). If h(D) /∈ M, h′ (D) /∈ M due to Rules (2) , making M ∪ {h(D)} unique.

Suppose h(D)∈M. Case h′ (D)∈M: Then, h(D) has to be founded by Πt. Hence, there is an r∈Πt with satr ∈M due to Rules (7). So, there is no answer set M ′ ̸=M identical toM over at(G(Π)), s.t. h′ (D) /∈M ′ , since satr /∈M ′ .

Case h′ (D)∈M: There is no answer set M ′ ̸=M identical to M over at(G(Π)), s.t. h′ (D)∈M ′ , as M ′ violates (12).

Results. Next, we strengthen Lemma 1. Indeed, compared to BDG as presented in [Besin et al., 2022], our hybrid strategy enables to freely split a non-ground HCF program Π into a tight program Πt and the remainder Π \ Πt. This yields the theorem below, which is the key result of hybrid grounding, permitting the (potentially cyclic) sharing of predicates between split programs Πc, Πt.

With level mappings, we can extend H to work despite cycles over Πc and Πt. This yields reduction Hlv (Appendix Figure 7), where we use auxiliary predicates to encode level mappings over each two atoms p1(D1), p2(D2) for any domain vectors D1, D2 of a shared SCC, so that one of the atoms has precedence over the other one. We formalize that this precedence is transitive, to avoid cyclic precedence via level mappings. Crucially, we then ensure that a head atom h(D) of a rule r is unfounded, if a body atom over a predicate in pred(r)\hpred(r) does not precede h(D). This prevents abusing cyclic foundedness between both Πc and Πt.

Theorem 1 (Grounding-Splitting Theorem). Given a partition of any non-ground HCF program Π into a HCF program Πc and a tight program Πt = Π \ Πc. The answer sets of Hlv(Πc, Πt) restricted to at(G(Π)) match those of G(Π).

Note that Hlv can be further extended, such that Πt is any normal (HCF) program. This requires level mappings as above, thereby also excluding cyclic foundedness within Πt.

We still obtain polynomial runtimes for small domains, without considering traditional grounding, i.e., Rules (3).

Proposition 1 (Runtime). Let Π be any tight non-ground program, where predicate arities are bounded by a. Then, Hlv(∅, Π) runs in time O((|Π| + |at(Π)|) · |dom(Π)|2·a ).

4 Aggregate Rewriting for Hybrid Grounding

State-of-the-art grounders easily run into the groundingbottleneck in case of dense aggregates, whose body contains a large number of variables. With the help of hybrid grounding, it is possible to efficiently ground tight ASP programs, but utilizing this approach for aggregates requires further considerations. To this end, we present ideas behind our aggregate rewriting techniques. While these are presented along the lines of the count aggregate, they work for all aggregates, as detailed in the appendix.

4.1 Warm-up: How to Rewrite Aggregates

According to Proposition 1, the grounding time is mainly influenced by the maximum arity. Hence, the rewritten program should have a low maximum arity. Consider the simple monotonic count aggregate: count{X : p(X, Y )} ≥ 3. Intuitively this aggregate holds whenever we derive at least three different element heads, i.e., three different instantiations for variable X. We implement this by (i) copying the element's body (p(X, Y )) three times and by (ii) adding an alldiff predicate to ensure that the tuple-heads (X) differ:

To ensure low maximum arity, we encode alldiff by pairwise difference checks, i.e., Xi ̸=Xj, for all pairs i, j.

As a first step towards generalizing the example, we provide a generalization for rules containing a single monotonic count aggregate (count≺) in the positive body of a rule r (count≺ ∈ B+ r ). Further, we require count≺ to have an integer bound ≥ u and a single element e = T e : Be, comprising head Te = ⟨t1, ..., to⟩ and body Be = l1(Y 1), . . . , lk(Y k). By extending our idea from above, we ensure that whenever u different element heads T e exist, the aggregate holds. Therefore, we (i) add u many Be,i's, with variable indexing as described above, and (ii) add alldiff constraints for all (indexed, 1 ≤ i ≤ u) Te,i's. The resulting rewritten rule is depicted in Equation (13), where B+ rc := B+ r \ {count≺}, yielding rewriting procedure RMcount (Rewriting Monotonic Count).

Glue Πc to Πt and Ground Πc

r

Satisfiability of Πt

Prevent Unfoundedness of Atoms in Πt

Figure 1: Hybrid grounding procedure H(Πc, Πt), which creates a disjunctive ground program from a given non-ground HCF program Πc ∪Πt such that Πt is tight. We thereby interleave classical grounding on Πc with body-decoupled grounding on Πt.

Rewriting Procedure RMcount

Results. Let h = |T | be the length of the element's head, and ϕr be the maximum arity of r (before rewriting). Then, Lemma 2 upper bounds the rewritten rule's arity.

Lemma 2 (Maximum arity of RMcount ). Let r be a rule containing a single count aggregate, with a singleton element set, with u being an integer constant and ≺ being ≥. The maximum arity of RMcount (r) is bounded by max{2 · |h|, ϕr}.

4.2 Generalizing the Idea

To this end, we need to address several issues: (i) multiple elements, (ii) variable dependencies, (iii) variable bounds, (iv) different comparison operators, and (v) different aggregate types. Many of these issues are interdependent and there is no single approach to address all issues at once. For brevity, we give an idea of how the generalization works for the count aggregate, by addressing issue (i) (and partly (iv)). For issues (ii), (iii), (iv) and (v), we refer to the appendix.

First we address issue (i), where we observe that a simple extension of RMcount to multiple elements fails for two reasons: On the one hand, for the count aggregate to hold in general, we need to consider every combination of u different element heads. On the other hand, element heads might have varying arity. We address both by introducing a combined element, which combines all elements into one conceptual element E. Element E has a combined head (T ′ ), and a single body predicate (tp(T ′ )), i.e., E = T ′ : tp(T ′ ). Note that the arity of the combined element head T ′ has to be the maximum arity over all elements e′ (|T ′ | = maxe′Te′ ). Intuitively, a ground atom over predicate tp holds, whenever there is at least one aggregate element that founds it. Therefore, we introduce for each element e = Te : Be a new rule: tp(Te) ← Be. However, this rule fails in case of different head element arities. Note, for each element e, its head arity |Te| fulfills |Te| ≤ |T ′ |. So we adapt this idea in the following way: If for an element e we have |T ′ | - |T e| > 0 we fill up the difference with fresh dummy constants cj . The full rule is depicted in Equation (14a) below.

Example 4. For example, given an aggregate count{X1 : p(X1);X2, Y2 : k(X2, Y2);X3, Y3,Z3 : l(X3, Y3,Z3)} ≥ u, we get |T ′ | = 3, and for elements 1, 2 and 3: |T1| = 1, |T2| = 2 and |T3| = 3. By applying our updated Equation (14a) we obtain the following three rules (c1, and c2 are fresh constants): {tp(X1, c1, c2) ← p(X1); tp(X2, Y2, c2) ← k(X2, Y2); tp(X3, Y3, Z3) ← l(X3, Y3, Z3)}

Having the encoding of E, we are ready to put together the pieces. To this end, we partly take into account issue (iv), thereby introducing a count≺ predicate and an appropriate new rule (Equation (14b)) such that count≺ holds whenever the aggregate holds. The encoding of Equation (14b) states u variable disjoint tp(T ′ ) predicates and the alldiff predicate to ensure pairwise differing T ′ . Finally, in the original rule we replace the aggregate by predicate count≺ (Equation (14c)):

Rewriting Procedure RS count

5 Implementation and Experimental Results

We implemented both hybrid grounding and aggregate rewritings, resulting in the system Novel AggreGate Grounder (NaGG). Our prototypical grounder is based on Python3 and the clingo 5.6 API. Efficient parsing of the input program is achieved by the clingo Abstract Syntax Tree (AST) library.

The main part of NaGG implements hybrid grounding according to the grounding-splitting theorem (Theorem 1). Thereby, NaGG provides the flavors NaGG-gringo (NaGGidlv) indicating that NaGG takes care of the program part Πt and gringo (idlv) grounds the remainder Πc, respectively. By design, NaGG is most beneficial if Πt comprises only rules of larger bodies (with many variable dependencies), whereas Πc only contains rules of slim bodies. So, hybrid grounding avoids large groundings of Πt, caused by exhaustive rule instantiation or auxiliary predicates of high arity.

Aggregates are handled by NaGG with a preprocessor, which implements multiple rewriting strategies (Appendix Table 2). Note that by construction our aggregate rewritings generate rules of large bodies (and many variable dependencies). The translation of aggregates therefore is one crucial use case that demonstrates the potential of this technique well.

5.1 Experimental Setup

We compared NaGG against state-of-the-art grounders gringo 5.6.2 and idlv 1.1.6. We compare four experimental setups, gringo, idlv, NaGG-gringo, and idlvgringo. While we consider lazy grounding related, we only compare NaGG to exact grounders. However, we expect that our approach is of interest for lazy grounding, as available systems do not support aggregates.

Benchmark Setting. We mainly measure grounding sizes (times) and combined times (grounding and solving). Grounding size thereby refers to the output size, which is either in smodels or aspif format for idlv and gringo, respectively. In our benchmarks, we limit available main memory (RAM) to 32GB (for each grounding or solving), and the overall runtime for both grounding and solving to 1800s. Plots only show grounding sizes up to 32GB. We used a benchmark system with an AMD Opteron 6272 with 225GB RAM on Debian10 with kernel 4.19.0-16-amd64. To rule out random results, we ran benchmark jobs multiple times.

Benchmark Scenarios. In order to evaluate NaGG, we design a series of benchmarks. The goal of these experiments is to demonstrate application areas and use cases for hybrid grounding strategies on dense aggregates. This seems to be particularly useful, as our approach can be readily incorporated into every grounder, making a portfolio-based grounder. We consider the following benchmark scenarios:

• S1 Polygamy Stable Matching: We adapt the stable marriage problem (ASP Competition 2014), where we add an aggregate to permit polygamy for some individual(s).
• S2 Relaxed NPRC: We relax non-partition-removal colorings [Weinzierl et al., 2020], by adding an aggregate to permit some deleted node causing a disconnected graph.
• S3 Traffic Connector: Decide whether there are connected subgraphs reaching at least a certain number of the nodes, s.t. we use at most one central node of degree ≥ k (traffic connector). k ranges from 4 (S3-T4), 6 (S3-T6), to 8 (S3-T8).
• S4 Count Traffic Connectors: This is based on S3, where we count the number of traffic connectors via aggregates, thereby storing the aggregate result in a predicate. As above, k ranges from 4 (S4-T4), 6 (S4-T6) to 8 (S4-T8).

Benchmark Instances. We use both random and application instances. For S1, we take instances from the ASP competition (2014). We generate graphs with varying instance density (edge probability) and instance size for S2, S3 and S4, to discuss the impact of instance scalability on NaGG. For S3 and S4 we model different rule densities k, i.e., number of different body variables, allowing us to study rule scalability.

Hypotheses. We study Hypotheses H1-H3:

• H1: NaGG improves overall solving performance on crafted and application instances.
• H2: For NaGG, the overall solving performance suffers less from increased rule density, instance density, and instance size.
• H3: NaGG reduces grounding sizes and grounding times for dense scenarios and instances.

5.2 Experimental Results

We confirm H1 via Table 1 and Figure 2. On application instances gringo is only capable of grounding and solving 26 instances of S1, which is increased to 50 by NaGG-gringo. On crafted instances, e.g., S3-T6, gringo and idlv ground and solve 204 instances, which increases to 2078 and 1997 for NaGG-gringo and NaGG-idlv, respectively.

We continue with H2 and refer to Table 1 and Figure 3. Note that the rule densities for S3-T4 to S3-T8 are strictly monotonically increasing. For S3-T4, gringo and idlv ground and solve fewer than 500 instances, which increases to more than 2400 for NaGG, so the relative factor between standard grounders and NaGG is about 5. For S3-T8 gringo and idlv ground and solve fewer than 160 instances, which increases to more than 1600 for NaGG, so a relative factor of about 10. Therefore, the relative factor approximately doubles. Additionally, observe that in Figure 3 our approach (first row) remains relatively stable with increased instance density, compared to other grounders (second row). Further, we are able to ground and solve larger instances, as seen in Figure 3.

Lastly, we confirm H3 (using Figures 2-4). In Figure 3 (second column), it can be seen that, e.g., for instance size 100, density 10, the grounding size is reduced by a factor of about 1000. For these instances, also grounding time is reduced from between 600 and 800 to a value between 0 and 100. Further, in S1 (Figure 4), we also reduce the grounding size by about a factor of 10. Lastly, Figure 2 confirms a reduction in grounding time, which gives a general trend. There, our approach grounds about 10000 instances, whereas standard grounders manage about 3000 instances.

6 Discussion and Conclusion

Aggregates are a crucial part of many ASP programs. In this work, we improved developments in the area of alternative grounding techniques. Our approach enables hybrid grounding, where we approach the grounding of dense aggregates by shifting efforts to solving, while still applying traditional grounding techniques for the remainder of the program. In order to do so, we establish a flexible and novel splitting theorem on interleaving these techniques with existing traditional groundings. Further, we present different rewriting techniques to translate non-ground aggregates to non-ground rules such that these rules can be efficiently treated by hybrid grounding. Our results show that state-of-the-art grounders can still be improved, despite years of development.

In upcoming works, we plan to tightly integrating our approach into standard grounders like gringo and idlv. Further, we expect hybrid grounding to be useful in the context of lazy grounding and big data. Especially for hard-to-ground instances and application areas, hybrid grounding might be an alternative to traditional approaches; recent work in planning [Corrˆea et al., 2023] underlines this perspective. Finally, we want to investigate rewriting techniques (e.g., [Brass and Dix, 1999]) for hybrid grounding. What about structural measures beyond treewidth, see, e.g., [Hecher, 2022; Hecher and Kiesel, 2023; Besin et al., 2023]?

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 Science Fund (FWF), grant J4656; the Society for Research Funding in Lower Austria (GFF) grant ExzF-0004; and Vienna Science and Technology Fund (WWTF) grant ICT19-065.