--- title: "Bypassing the ASP Bottleneck: Hybrid Grounding by Splitting and Rewriting" authors: - "Alexander Beiser" - "Markus Hecher" - "Kaan Unalan" - "Stefan Woltran" doi: "10.24963/ijcai.2024/360" url: "https://ijcai.org/proceedings/2024/360" pdf: "https://ijcai.org/proceedings/2024/0360.pdf" venue: "Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence" year: 2024 pages: "3250-3258" track: "Main Track" keywords: - "Knowledge Representation and Reasoning: KRR: Computational complexity of reasoning" - "Knowledge Representation and Reasoning: KRR: Non-monotonic reasoning" - "Knowledge Representation and Reasoning: KRR: Applications" - "Knowledge Representation and Reasoning: KRR: Logic programming" --- # Bypassing the ASP Bottleneck: Hybrid Grounding by Splitting and Rewriting Alexander Beiser, Markus Hecher, Kaan Unalan, Stefan Woltran *Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence*, pages 3250-3258. DOI: [10.24963/ijcai.2024/360](https://doi.org/10.24963/ijcai.2024/360) ## Abstract Answer Set Programming (ASP) is a key paradigm for problems in artificial intelligence and industrial contexts. In ASP, problems are modeled via a set of rules. Over the time this paradigm grew into a rich language, enabling complex rule types like aggregate expressions. Most practical ASP systems follow a ground-and-solve pattern, where rule schemes are grounded and resulting rules are solved. There, the so-called grounding bottleneck may prevent from solving, due to sheer grounding sizes. Recently body-decoupled grounding (BDG) demonstrated how to reduce grounding sizes by delegating effort to solving. However, BDG provides limited interoperability with traditional grounders and only covers simple rule types. In this work, we establish hybrid grounding — based on a novel splitting theorem that allows us to freely combine BDG with traditional grounders. To mitigate huge groundings in practice, we define rewriting procedures for efficiently deferring grounding effort of aggregates to solving. Our experimental results indicate that this approach is competitive, especially for instances, where traditional grounding fails. ## Full text ## 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. 2. 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. 3. 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 Table 1: Number of solved instances for Scenarios S1-S4. | Scen. #Insts. | Scen. #Insts. | Total #Solved | Total #Solved | Total #Solved | Total #Solved | |-----------------|-----------------|-----------------|-----------------|-----------------|-----------------| | S1 | 50 | gringo idlv 26 | 50 | NaGG-gringo 50 | NaGG-idlv 50 | | S2 | 3500 | 250 | 980 | 1057 | 1000 | | S3-T4 | 3500 | 491 | 489 | 2526 | 2420 | | S3-T6 | 3500 | 204 | 204 | 2078 | 1997 | | S3-T8 | 3500 | 156 | 156 | 1718 | 1666 | | S4-T4 | 3500 | 231 | 439 | 1274 | 1168 | | S4-T6 | 3500 | 143 | 197 | 907 | 890 | | S4-T8 | 3500 | 121 | 156 | 756 | 700 | Figure 2: Cactus plot (S2, S3, S4), number of grounded (G), and combined (grounded and solved) (S) instances, for gringo, idlv, NaGG-gringo, and NaGG-idlv. ![Image](https://ijcai.org/proceedings/2024/fulltext/360/image_000000_4333b726faef45187a22fa4b240f28330c11ba514442645273f466041b787cf1.png) ## 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. Figure 3: Combined solving profile of NaGG-gringo/NaGG-idlv (top row) and gringo/idlv (bottom row). S2 (grounding-time; first column; top: NaGG-gringo, bottom: gringo), S3-T6 (grounding-time; second column; top: NaGGgringo, bottom: gringo), S4-T4 (combined-time; third column; top: NaGG-idlv, bottom: idlv). Circles mark instances solved (grounded) within 1800s and 32GB RAM. ![Image](https://ijcai.org/proceedings/2024/fulltext/360/image_000001_72d44117440fdb077979a1a8bfe832ca5d66cb4fb3daa575189bb0fd5fe49274.png) Figure 4: Grounding size for S1 per instance. ![Image](https://ijcai.org/proceedings/2024/fulltext/360/image_000002_bf77c77bf2cffe5c0f9d3a52f73a6766c5feb2e466dcbd0a868f425cf8045ae3.png) 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. ## References 1. [Alviano and Faber, 2018] Mario Alviano and Wolfgang Faber. Aggregates in answer set programming. KI - Künstliche Intelligenz, 32(2-3):119-124, 2018. 2. [Alviano et al., 2019] Mario Alviano, Giovanni Amendola, Carmine Dodaro, Nicola Leone, Marco Maratea, and Francesco Ricca. Evaluation of Disjunctive Programs in WASP. In LPNMR'19, volume 11481 of LNCS, pages 241-255. Springer, 2019. 3. [Banbara et al., 2017] Mutsunori Banbara, Benjamin Kauf- mann, Max Ostrowski, and Torsten Schaub. Clingcon: The next generation. Theory Pract. Log. Program., 17(4):408- 461, 2017. 4. [Bartholomew et al., 2011] Michael Bartholomew, Joohyung Lee, and Yunsong Meng. First-order se- mantics of aggregates in answer set programming via modified circumscription. In Papers from the 2011 AAAI Spring Symposium, 2011. 5. [Ben-Eliyahu and Dechter, 1994] Rachel Ben-Eliyahu and Rina Dechter. Propositional Semantics for Disjunctive Logic Programs. Annals of Mathematics and Artificial In- telligence, 12(1):53-87, 1994. 6. [Besin et al., 2022] Viktor Besin, Markus Hecher, and Ste- fan Woltran. Body-Decoupled Grounding via Solving: A Novel Approach on the ASP Bottleneck. In IJCAI'22, pages 2546-2552. ijcai.org, 2022. 7. [Besin et al., 2023] Viktor Besin, Markus Hecher, and Ste- fan Woltran. On the Structural Complexity of Ground- ing -Tackling the ASP Grounding Bottleneck via Epis- temic Programs and Treewidth. In 26th European Confer- ence on Artificial Intelligence (ECAI 2023), volume 372 of Frontiers in Artificial Intelligence and Applications, pages 247-254. IOS Press, 2023. 8. [Bichler et al., 2020] Manuel Bichler, Michael Morak, and Stefan Woltran. lpopt: A Rule Optimization Tool for An- swer Set Programming. Fundamenta Informaticae, 177(3- 4):275-296, 2020. 9. [Bomanson et al., 2014] Jori Bomanson, Martin Gebser, and Tomi Janhunen. Improving the normalization of weight rules in answer set programs. In Eduardo Fermé and João Leite, editors, JELIA'14, pages 166-180. Springer-Verlag, 2014. 10. [Brass and Dix, 1999] Stefan Brass and Jürgen Dix. Seman- tics of (disjunctive) logic programs based on partial evalu- ation. J. Log. Program., 40(1):1-46, 1999. 11. [Brewka et al., 2011] G. Brewka, T. Eiter, and M. Truszczyński. Answer set programming at a glance. Comm. of the ACM, 54(12):92-103, 2011. 12. [Calimeri et al., 2019] Francesco Calimeri, Simona Perri, and Jessica Zangari. Optimizing answer set computation via heuristic-based decomposition. Theory Pract. Log. Program., 19(4):603-628, 2019. 13. [Calimeri et al., 2020] Francesco Calimeri, Wolfgang Faber, Martin Gebser, Giovambattista Ianni, Roland Kaminski, Thomas Krennwallner, Nicola Leone, Marco Maratea, Francesco Ricca, and Schaub Torsten. ASP-Core-2 in- put language format. Theory Pract. Log. Program., 20(2):294-309, 2020. 14. [Corrêa et al., 2023] Augusto B. Corrêa, Markus Hecher, Malte Helmert, Davide Mario Longo, Florian Pommeren- ing, and Stefan Woltran. Grounding Planning Tasks Using Tree Decompositions and Iterated Solving. In ICAPS'23, pages 100-108. AAAI Press, 2023. 15. [Cuteri et al., 2017] Bernardo Cuteri, Carmine Dodaro, Francesco Ricca, and Peter Schüller. Constraints, lazy constraints, or propagators in ASP solving: An empirical analysis. Theory Pract. Log. Program., 17(5-6):780-799, 2017. 16. [Cuteri et al., 2020] Bernardo Cuteri, Carmine Dodaro, Francesco Ricca, and Peter Schüller. Overcoming the grounding bottleneck due to constraints in ASP solving: Constraints become propagators. In IJCAI'20, pages 1688-1694. ijcai.org, 2020. 17. [Dantsin et al., 2001] Evgeny Dantsin, Thomas Eiter, Georg Gottlob, and Andrei Voronkov. Complexity and expres- sive power of logic programming. ACM Comput. Surv., 33(3):374-425, 2001. 18. [Dodaro et al., 2023] Carmine Dodaro, Giuseppe Mazzotta, and Francesco Ricca. Answer Set Programming as SAT modulo Acyclicity. In ECAI'23. IOS Press, 2023. In Press. 19. [Eiter and Gottlob, 1995] Thomas Eiter and Georg Gottlob. On the computational cost of disjunctive logic program- ming: Propositional case. Annals of Mathematics and Ar- tificial Intelligence, 15(3-4):289-323, 1995. 20. [Eiter et al., 2007] Thomas Eiter, Wolfgang Faber, Michael Fink, and Stefan Woltran. Complexity results for answer set programming with bounded predicate arities and impli- cations. Annals of Mathematics and Artificial Intelligence, 51(2-4):123-165, 2007. 21. [Faber et al., 2011] Wolfgang Faber, Gerald Pfeifer, and Nicola Leone. Semantics and complexity of recursive aggregates in answer set programming. Artificial Intelli- gence, 175(1):278-298, 2011. 22. [Falkner et al., 2018] Andreas A. Falkner, Gerhard Friedrich, Konstantin Schekotihin, Richard Taupe, and Erich Christian Teppan. Industrial applications of answer set programming. Künstliche Intell., 32(2-3):165-176, 2018. 23. [Ferraris, 2011] Paolo Ferraris. Logic programs with propo- sitional connectives and aggregates. ACM Transactions on Computational Logic, 12(4):Article 25 (40 pages), 2011. 24. [Gebser et al., 2018] Martin Gebser, Nicola Leone, Marco Maratea, Simona Perri, Francesco Ricca, and Torsten Schaub. Evaluation techniques and systems for answer set programming: A survey. In Jérôme Lang, editor, IJ- CAI'18, pages 5450-5456. ijcai.org, 2018. 25. [Gebser et al., 2019] Martin Gebser, Roland Kaminski, Ben- jamin Kaufmann, and Torsten Schaub. Multi-shot ASP solving with clingo. Theory Pract. Log. Program., 19(1):27-82, 2019. 26. [Gelfond and Zhang, 2019] Michael Gelfond and Yuanlin Zhang. Vicious circle principle, aggregates, and forma- tion of sets in ASP based languages. Artificial Intelligence, 275:28-77, 2019. 27. [Hecher and Kiesel, 2023] Markus Hecher and Rafael Kiesel. The impact of structure in answer set counting: Fighting cycles and its limits. In KR'23, 2023. In Press. 28. [Hecher, 2022] Markus Hecher. Treewidth-aware reductions of normal ASP to SAT -Is normal ASP harder than SAT after all? Artif. Intell., 304:103651, 2022. 29. [Hippen and Lierler, 2021] Nicholas Hippen and Yuliya Lierler. Estimating grounding sizes of logic programs un- der answer set semantics. In JELIA'21, volume 12678 of LNCS, pages 346-361. Springer, 2021. 30. [Janhunen, 2006] Tomi Janhunen. Some (in)translatability results for normal logic programs and propositional the- ories. Journal of Applied Non-Classical Logics, 16(1- 2):35-86, 2006. 31. [Kaminski and Schaub, 2022] Roland Kaminski and Torsten Schaub. On the foundations of grounding in answer set programming. Theory Pract. Log. Program., pages 1-60, 2022. 32. [Lifschitz and Turner, 1994] Vladimir Lifschitz and Hudson Turner. Splitting a Logic Program. In ICLP'94, pages 23- 37. MIT Press, 1994. 33. [Lin and Zhao, 2003] Fangzhen Lin and Jicheng Zhao. On tight logic programs and yet another translation from nor- mal logic programs to propositional logic. In IJCAI'03, pages 853-858. 34. Morgan Kaufmann, 2003. [Marek and Truszczyński, 1991] 35. Wiktor Marek and Mirosław Truszczyński. Autoepistemic logic. Jour- nal of the ACM, 38(3):588-619, 1991. 36. [Mitchell, 2019] David Mitchell. Guarded constraint models define treewidth preserving reductions. In CP'19, volume 11802 of LNCS, pages 350-365. Springer, 2019. 37. [Pelov et al., 2003] Nikolay Pelov, Marc Denecker, and Maurice Bruynooghe. Translation of aggregate programs to normal logic programs. In Marina De Vos and Alessan- dro Provetti, editors, International Workshop on Answer Set Programming (ASP'03), pages 29-42, 2003. 38. [Tsamoura et al., 2020] Efthymia Tsamoura, Víctor Gutiérrez-Basulto, and Angelika Kimmig. Beyond the grounding bottleneck: Datalog techniques for infer- ence in probabilistic logic programs. In AAAI'20, pages 10284-10291. AAAI Press, 2020. 39. [Weinzierl et al., 2020] Antonius Weinzierl, Richard Taupe, and Gerhard Friedrich. Advancing lazy-grounding ASP solving techniques -restarts, phase saving, heuristics, and more. Theory Pract. Log. Program., 20(5):609-624, 2020. 40. [Zaniolo et al., 2017] Carlo Zaniolo, Mohan Yang, Ariyam Das, Alexander Shkapsky, Tyson Condie, and Matteo In- terlandi. Fixpoint semantics and optimization of recur- sive datalog programs with aggregates. Theory Pract. Log. Program., 17(5-6):1048-1065, 2017.