Simulating Sets in Answer Set Programming

1 Introduction

The success of answer set programming (ASP) is in no small part due to its declarative approach to computation, which allows users to encode complex problems in a clean, direct manner [Brewka et al., 2011; Lifschitz, 2019]. Plain ASP can express problems up to the second level of the polynomial hierarchy [Dantsin et al., 2001], and highly optimised ASP solvers often lead to efficient solutions in such cases. However, not all problems can be expressed in this way, and ASP has therefore been extended with more complex terms that support function symbols [Bonatti, 2004], list, and sets [Calimeri et al., 2009].

The ability to encode sets (of constants) in terms is of particular interest here, since it preserves - in contrast to function symbols and lists - the decidability of reasoning. Moreover, sets and related predicates like ∈ and ⊆ support a very declarative modelling style. For example, the rules in Figure 1 define maximal strongly connected components (scc) on a graph described by edges e(X, Y ) and vertices v(X). The rules for c show how sets can be constructed iteratively using suitable functions, while the last two rules provide an elegant description of maximal sets. Such elegance presumably was the main motivation for implementations of sets

Figure 1: Strongly connected components in ASP with sets

in ASP solvers [Calimeri et al., 2009], but sets have further computational advantages in boosting expressive power, as noted already for the case of Datalog [Ortiz et al., 2010; Carral et al., 2019b].

Surprisingly, the extension of ASP with sets remains poorly understood, regarding both its theoretical properties and its practical potential. Most notably, Calimeri et al. [2008; 2009] discuss set terms in combination with functions and lists, and provide a first implementation in DLV-complex. However, to our knowledge, even the complexity of reasoning in ASP with sets has not been established yet, and its utility for solving computationally hard problems has never been discussed or evaluated. One may also wonder whether formalisms that are even more powerful, such as rules with function symbols or value invention, could be exploited to implement sets, but research on feasible implementation methods is similarly scarce. Significant potential for using ASP and related tools therefore remains unexplored.

To address this, we take a closer look at the extension of ASP with set terms, investigate possible implementation methods in theory, and evaluate their practical feasibility in solving problems that are beyond the expressive power of plain ASP. Our main contributions are:

• We define DLP(S), the extension of disjunctive logic programs with set terms, and establish relevant reasoning complexities under the stable model semantics.
• We show how DLP(S) reasoning can be reduced to reasoning in disjunctive logic programs with function symbols while still ensuring finite stable models.
• We show that existing lazy ASP solvers can handle these programs, whereas traditional ASP engines will fail.
• We develop another alternative grounding approach

based on a technique for modelling sets in existential rules [Carral et al., 2019b].

• We evaluate the ability of our new methods and the existing set implementation DLV-complex to solve complex real-world problems from ontology engineering.

Full proofs, datasets, and source code for our prototype implementations can be accessed through the online repository https://github.com/knowsys/eval-2022-IJCAI-asp-with-sets.

2 ASP with Sets

We now introduce the extension of non-monotonic disjunctive logic programs with finite sets (DLP(S)). This will allow us to write rules as in Figure 1.

Syntax. Formally, we consider two sorts: a sort of objects obj and a sort of sets set. A signature of DLP(S) is based on countably infinite sets of object constants Cobj (typically a, b, c), object variables Vobj (typically X, Y , Z), set variables Vset (typically S, U, V ), and predicate names P including special predicates {∈,⊆} ⊆ P. The signature of a predicate symbol p is a tuple sig(p) = 〈S1, . . . , Sn〉 of sorts, and n is called its arity. We have sig(∈) = 〈obj, set〉 and sig(⊆) = 〈set, set〉. An object term is any object constant or object variable. A set term is any set variable, the special constant ∅, an expression {t} where t is an object term, or, recursively, an expression (s1 U s2) where s1, s2 are set terms. We use {t1, . . . , tn} as abbreviation for ({t1} U ({t2} U . . . U {tn} . . .)) and omit parentheses for U. An term or formula is ground if it contains no variables.

An atom is an expression p(t1, . . . , tn) where p ∈ P with sig(p) = 〈S1, . . . , Sn〉 and ti is a term of sort Si. We write ∈(t, s) as t ∈ s, and ⊆(s1, s2) as s1 ⊆ s2. A literal is an atom α or a negated atom not α. We sometimes treat conjunctions or disjunctions of literals as sets of literals. For a formula F, preds(F) denotes the set of all predicates in F.

Definition 1. A DLP(S) rule is an expression r of the form H ← B+ ∧B-, where the head H is a disjunction of atoms, the positive body B+ is a conjunction of atoms, and the negative body B- is a conjunction of negated atoms, such that:

1. every object variable in r occurs in B+,
2. every set variable S in r occurs in B+ as an argument ti = S (1 ≤ i ≤ n) of an atom p(t1, . . . , tn) ∈ B+ with non-special predicate p ∈ P \ {∈, ⊆}, and
3. the special predicates ∈ and ⊆ do not occur in H.

A fact is a disjunction-free rule with empty body, i.e., a ground atom. A DLP(S) program P is a set of DLP(S) rules. A rule, fact, or program is DLP if it contains only object terms. We also consider the extension of DLP with arbitrary (object) function symbols, which we will denote DLPf .

Some restrictions in Definition 1 could be relaxed without fundamentally changing the properties of DLP(S). Our selection is also motivated by practical concerns, e.g., since a rule q(S) ← p(S U T) (which violates condition 2) would produce exponentially many derivations in the size of any set R for which p(R) holds.

A substitution σ is a sort-preserving partial mapping from variables to terms. Fσ denotes the result of applying σ to all variables in the formula or term F for which it is defined.

Semantics. We define a stable model semantics for DLP(S) by interpreting set terms as finite sets over the (object) domain. Given a program P, let obj(P) be the set of all object constants in P (including those used in set terms), and let set(P) be a set of terms of the form {t1, . . . , tn} that bijectively correspond to the powerset of obj(P). The grounding ground(P) of P consists of all rules that can be obtained from a rule r of P by (1) uniformly replacing object and set variables in r by terms from obj(P) and set(P), respectively; and (2) replacing each of the resulting set terms s by the corresponding term from set(P) that represents the same set under the usual interpretation of ∅, {·}, and U.

An interpretation I for P is a set of ground facts that only uses terms from obj(P) and set(P), and that contains exactly those facts c∈t (resp. s⊆t) for which c occurs in the set term t (resp. for which all constants in s occur in t). I satisfies (or is a model of ) a ground atom α if α ∈ I. I satisfies a ground conjunction B (disjunction H) if B ⊆ I (H∩I ̸= ∅), and a positive ground rule H ← B if it satisfies H or does not satisfy B. The reduct P I of P with respect to I is obtained from ground(P) by (1) deleting every negated atom notα with α /∈ I and (2) deleting every rule with a negated atom notα with α ∈ I. I is a stable model of P if it is a subsetminimal model of P I . A fact α is (cautiously) entailed by P if every stable model of P contains the fact α′ , obtained by replacing set terms in α with their representative in set(P).

Since there are exponentially many sets over a given object domain, groundings, reducts, and stable models can also be exponential for DLP(S), even in the size of the data:

Theorem 1. Deciding whether P entails α is CONEXPTIME NP -complete. If P does not contain ∨, the problem is CONEXPTIME-complete. In either case, hardness holds even if only facts are allowed to vary while all other rules are fixed (data complexity).

Proof sketch. The data complexities of the considered problems are ΠP 2 -complete respectively CONP-complete for DLP [Dantsin et al., 2001]. Hardness can be shown, e.g., by reducing from the word problem of polynomial-time alternating Turing machines with one quantifier alternation. The claims for DLP(S) follow by simulating an exponentially time-bounded alternating Turing machine instead.

The encoding is standard once an exponentially long chain (of time points or tape cells) is inferred. Given input facts succ(1, 2), . . . , succ(ℓ - 1, ℓ), a chain of length 2ℓ is characterised by a predicate c, defined as follows:

Here we use for anonymous variables. The encoding is adapted from Carral et al. [2019b]. Predicates n(S, T, X, V ) express that (1) T is the successor of S if both sets are taken as binary numbers with elements from {1, . . . , ℓ} encoding active digits, (2) X is the largest number (most significant bit) in T, and (3) T \ {X} = V . With this in mind, (4) and (5) increment numbers with the highest bit staying the same or being increased by one, respectively.

Membership is also derived from known results by reducing the DLP(S) problems to propositional logic programming problems via grounding, which incurs an exponential blowup in the presence of set terms.

3 Reducing DLP(S) to DLP

Answer Set Programming over DLP(S) could be implemented by similar techniques as normal ASP, taking the semantics of sets into account when applying rules (operational extension APIs like clingo's @-terms or DLV's external atoms could be used). However, this is rarely done so far, and we therefore explore alternative approaches. A first idea is to reduce DLP(S) to DLP with arbitrary function symbols (DLPf ), which is known to be computationally very powerful [Bonatti, 2004; Eiter and Simkus, 2010]. In this section, we show how this can be done and establish the correctness of the translation. Its computational properties and possible implementation in current solvers are discussed later.

We encode sets using a constant c∅ (the empty set) and a function f∪, such that, e.g., f∪(a, f∪(b, c∅)) represents the set {a, b}. However, we cannot generally represent {c} ∪ s by f∪(c, s), since this would lead to redundant representations like f∪(a, f∪(a, c∅)). Instead, we use facts of the form su(c, s, t) - where su stands for singleton union - to express {c} ∪ s = t, where t might be different from f∪(c, s). In particular, su(c, s, s) means c ∈ s, which we abbreviate by in(c, s). Finally, to ensure that only necessary set encodings are derived, we use facts get su(c, s) to express that a representation of {c} ∪ s is needed. The following DLPf rules implement these ideas:

We can exercise this machinery to define rules that compute arbitrary unions using analogous predicates u and get u:

Here, (11) is the base and (12) the recursive case, and (13) and (14) ensure the computation of necessary auxiliary facts. We are now ready to transform a single DLP(S) rule r = H ← B to a set of DLPf rules dlpf (r). For every DLP(S)

predicate p of arity n, let ˆ p be a unique fresh predicate of arity n and signature sig(p) = 〈obj, . . . , obj〉, and for every set term s, let Vs be a fresh object variable. We construct H′ and B′ fromH and B, respectively, by replacing each atom t ∈ s by in(t, s), each atom s ⊆ u by sub(s, u), every predicate p by ˆ p, and every set term s by Vs. Moreover, let B+ be the conjunction of positive literals in B′ . Now let s1, . . . , sk be a list of all terms and subterms in r of the form {t} or s U u, ordered such that subterms occur before their superterms. Then dlpf (r) consists of the following rules:

where we define, for v = {t}, α(v) = get su(t, c∅) and β(v) = su(t, c∅, Vv); and, for v = s U u, α(v) = get u(Vs, Vu) and β(v) = u(Vs, Vu, Vv).

Example 1. Consider the DLP(S) rule r : p(S) ← q(S, x) ∧ r(S U {x}) ∧ not x ∈ S. The required list of set terms is s1 = {x}, s2 = S U {x}. We have H′ = ˆ p(VS), B+ = ˆ q(VS, x) ∧ ˆ r(VSU{x}), and B′ = B+ ∧ not in(x, VS). Now dlpf (r) consists of the rules:

Note how B+ is used to ensure that the auxiliary rules that define only some of the variables Vs are safe in the sense of Definition 1 (1).

As Example 1 suggests, we could sometimes use get su and su instead of get u and u. This optimisation can be useful in practice since it may make rules (11)-(12) obsolete, but we omit it from our formal description for simplicity.

The transformation needs one more ingredient, since our set representations are not unique. For example, f∪(a, f∪(b, c∅)) and f∪(b, f∪(a, c∅)) both represent {a, b}. We therefore explicitly compute equality of sets as follows:

Definition 2. Given a DLP(S) program P , the DLPf program dlpf (P) consists of the following rules:

• the rules (7)-(12) and (17)-(20);
• for every predicate ˆ p in P of arity n, the rules

• p(X1, · · ·, Xn) ∧ eq(Xi, Y )

where [Xi/Y ] is the substitution replacing Xi by Y ;

• for every rule r ∈ P, the rules dlpf (r).

The next result is a pre-condition for the practical utility of our translation. It can be shown directly but also follows from Theorem 5 below.

Theorem 2. All stable models of dlpf (P) are finite.

We can convert ground terms s that contain c∅ or f∪ to canonical set terms [s] ∈ set(P) in the obvious way: [c∅] = ∅ and [f∪(t, s)] is the representation of {t} U [s] in set(P). Moreover, let [t] = t for other terms (not representing sets). Then, for every stable model J of dlpf (P), we find an interpretation [J ] = {p([t1], · · · , [tn]) | ˆ p(t1, · · · , tn) ∈ J}.

Theorem 3. The set of stable models of a DLP(S) program P is exactly the set {[J ] | J is a stable model of dlpf (P)}.

4 Lazy Grounding

A popular approach towards reasoning in ASP is "ground & solve", where one first computes a set of ground instances of rules that are then turned into a propositional logic problem to which an ASP solver can be applied [Gebser et al., 2018; Faber, 2020]. To ensure that the grounding stage produces enough rule instances, it is common to disregard negative body literals when applying rules during grounding. Optimisations can further reduce the number of rule applications, e.g., using predicate dependencies to compute a stratification. A classical algorithm that combines several such ideas was proposed by Calimeri et al. [2008], who defined FG as the class of all DLPf programs on which their grounding is finite. However, although our programs dlpf (P ) have finite stable models (Theorem 2), such classical grounding approaches will usually not work for them:

Proposition 4. If P contains a fact p(∅) and a rule p(S U {a}) ← p(S), then dlpf (P) /∈ FG.

Indeed, it can be verified in practice that grounders such as gringo and iDLV do not terminate on dlpf (P) for programs P as in Proposition 4. A challenge that grounders are facing in this case is that negation in the rules (7)-(10) of dlpf (P) is not stratified. To avoid groundings that are too small, most classical grounders will therefore ignore the negated literal in rule (7), which leads to a program that has no finite model.

Fortunately, this problem can be avoided by lazy grounding approaches, which interleave grounding and solving to produce rule instances only when relevant to the search for a stable model. Notable systems of this type include Alpha [Weinzierl, 2017; Taupe et al., 2019] and ASPeRiX [Lef`evre et al., 2017]. We analyse the former to show that such approaches are applicable to our task:

Theorem 5. The algorithm of Alpha terminates on every program of the form dlpf (P).

Alpha therefore produces a complete set of (necessarily finite) stable models of dlpf (P), which correspond to the stable models of P by Theorem 3. The essence of our proof of this claim is the fact that Alpha eagerly applies a form of unit propagation where it exhaustively applies rules (8)-(10) before considering further choice points obtained by grounding rule (7). Since the propagation will derive facts for in, rule (7) is only potentially applicable to values of X that are not in the set represented by S, and sets can only be enlarged a finite number of times before no such elements are left.

5 Grounding with Existential Rules

Instead of relying on lazy grounding, an alternative approach towards reasoning in DLP(S) is to develop a setaware grounder whose output can be combined with existing solvers. Since classical grounders are mostly Datalog engines (with some support for stratified negation), we essentially need an engine for Datalog(S), the extension of Datalog with sets. To obtain this, we follow an approach by Carral et al. [2019b] who used a reasoning algorithm from databases (the standard chase) to simulate Datalog(S) reasoning, and we argue that it can safely be combined with stratified negation, which is not immediate in this context.

We first explain grounding based on Datalog(S) with stratified negation. Given a DLP(S) program P , a stratification s : P →Nmaps rules to natural numbers such that, for all pairs of rules r1, r2 ∈ P of form ri : Hi ←B+ i ∧Bi ∈ P, and all p ∈ preds(H2): (1) if p ∈ preds(B+ 1 ), then s(r1) ≥ s(r2), and (2) if p ∈ preds(B1 ), then s(r1) > s(r2). This induces a partitioning P1, . . . , Pn of P such that Pi = {r ∈ P | s(r) = i}. A program P is stratified if it has a stratification.

Now for any program P, let P ! ⊆ P be the largest disjunction-free, stratified subset of P such that predicates in heads of P \P ! do not occur in P ! . 1 A predicate is certain if it occurs only in P ! . The Datalog(S) program grnd(P ) contains all facts in P and, for each non-fact rule H ← B+ ∧B- ∈ P , the rules

where ruler is a dedicated fresh predicate for r, X is a list of all variables in r, and B! = ∧{notα ∈ B- | the predicate of α is certain}. For a ground atom of the form ruler(c), the ground rule r[c] is obtained by applying the substitution X ↦→ c to r. We get a simple but correct grounding: Proposition 6. For any DLP(S) program P, grnd(P) is a stratified Datalog(S) program. If I is the (unique) stable model of grnd(P), then the stable models of {r[c] |

ruler(c) ∈ I} are exactly the stable models of P .

To compute the stable model of grnd(P), we simulate reasoning in stratified Datalog(S) by generalising an approach for existential rules (also know as tuple-generating dependencies), which we extend by negation (which will be stratified in the same sense as defined above). Such rules have the form ∃Y .H ← B+ ∧ B-, where H and B+ are conjunctions of atoms, B- is a conjunction of negated atoms, Y is a list of existentially quantified variables, and all other (implicitly universally quantified) variables also occur in B+ (safety). Existential quantifiers may lead to new domain elements, represented by named nulls, which play the role of anonymous constants. We can apply an existential rule ∃Y .H ← B+ ∧ B- to a set I of facts (using constants and possibly nulls) if (1) there is a substitution θ with B+θ ⊆ I and B- ∩ I = ∅, and (2) the rule is not already satisfied under θ, i.e., I ̸|= ∃Y .(Hθ). If this holds, we apply the rule by extending I with Hθ′ , where θ′ is an extension of θ that maps each Y ∈ Y to a fresh null.

For existential rules without negation, a (standard) chase is a possibly infinite set I obtained by exhaustive, fair application of rules. For a set of existential rules with negation that has a stratification P1, . . . , Pn, the stratified chase I is ⋃ni=1 Ii, where I0 = ∅ and Ii (1 ≤ i ≤ n) is the possibly infinite set obtained by exhaustive, fair application of rules Pi to Ii-1. Note that this only leads to a practical (and overall fair) procedure if each Ii is finite, which may depend on the chosen order of rule applications. 2 We follow Carral et al. [2019b] and require that, within each stratum Pi, rules without existential variables are applied first (the so-called Datalog-first chase). This assumption simplifies presentation and is justified for the system used in our evaluation.

1 This can be viewed as a kind of split program in the sense of Lifschitz and Turner [1994].

Example 2. Contrary to expectations in normal logic programming, the stratified chase does not yield a unique result, not even up to homomorphic renaming of nulls. Consider the fact q(a) and the rules

A stratification s must satisfy s(q(a)) ≤ s(r1) ≤ s(r3), s(q(a)) ≤ s(r2) ≤ s(r3), and s(r3) < s(r4). A valid partitioning would be {q(a), r1}, {r2, r3}, {r4}, which yields a stratified chase {q(a), r(a, a), e(a, a)}. Note that r2 is not applicable since r(a, a) is already derived before r2 is considered. However, if we consider the partition {q(a), r2}, {r1, r3}, {r4}, which is also a valid stratification, then the stratified chase is {q(a), r(a, n), r(a, a), e(a, a), e(n, n), p()}, where n is a named null introduced when applying r2 in the first stratum (as it is not satisfied at this point).

Now we can simulate sets in a similar way as in Definition 2, but using existential rules and nulls instead of DLPf rules and function terms. To this end, we replace rule (7) by

while all other auxiliary rules remain as before. The translation of Datalog(S) rules to existential rules likewise remains the same as in Definition 2. This produces existential rules with negation if the input rules contain negation but no disjunction. However, stratification can be lost if auxiliary predicates like get su are needed in every stratum. To address this, each stratum Pi will use distinct copies of each auxiliary rule, using indexed predicates such as sui and get sui. The resulting set of existential rules with negation is denoted nex(Pi), and for Datalog(S) program P with negation and stratification P1, . . . , Pn, we define nex(P ) = nex(P1) ∪ ⋃ni=2 nex(Pi) ∪ {sui(X, S,U) ← sui-1(X, S,U)}. Then nex(P) is stratified. Since every null n that is introduced by a chase over nex(P) first appears in a fact su(t, s, n), we can extend the notation introduced before Theorem 3 and associate n with the set [n] := [f∪(t, s)].

Theorem 7. If P is a stratified Datalog(S) program with negation, then every stratified, Datalog-first chase I of nex(P) is finite and [I] := {p([t1], · · · , [tn]) | ˆ p(t1, · · · , tn) ∈ I} is the unique stable model of P.

2 This is typical for the standard chase; Kr¨otzsch et al. [2019] give an introductory discussion.

Figure 2: Rules for transitive reduction

Figure 3: Rules for maximal antichains

The previous result is remarkable in the light of Example 2, since it identifies a case where a classical stratification can safely be applied to existential rules with negation.

This completes our approach of using existential rule reasoners for DLP(S)-reasoning: for a DLP(S) program P, we conduct a stratified chase over nex(grnd(P)) to infer facts of the form ruler(t) and in(c, n), from which we can construct ground instances of DLP(S) rules as in Proposition 6.

6 Evaluation

To evaluate the practical feasibility of our approaches, we developed prototypical implementations of the necessary procedures and combined them with existing reasoning engines to compute stable models. The first approach (LAZY) uses the transformation dlpf (P) and the lazy ASP solver Alpha 3 [Weinzierl, 2017]. The second approach (EXRULES) implements grounding with existential rules using the Rulewerk library with the VLog reasoner 4 [Carral et al., 2019a] to produce a grounded file in aspif format, to which we apply the ASP solver clasp v3.2.1 [Gebser et al., 2007]. Our prototype code will be published as open source as soon as possible (after double-blind review). As a third scenario DLVCOMP, we use the native implementation of sets provided in DLVcomplex [Calimeri et al., 2009].

As a challenging task for set-based reasoning, we use a rule-based reasoning method for the expressive description logic Horn-ALC by Carral et al. [2019b]. Given an ontology that is syntactically transformed into facts, the rules compute the inferred subclass relationships that follow from the ontology - a problem that is EXPTIME-complete in data complexity. Following Carral et al., we omit auxiliary rules (11)-(20)

3 https://github.com/alpha-asp/Alpha, master, 29 Aug 2021

4 https://github.com/karmaresearch/vlog, master, 30 Aug 2021

from dlpf (P ) and the corresponding existential rules version, since they would not contribute new derivations here. The rules define a binary predicate sc that represents the inferred subclass hierarchy, and a unary predicate class that marks class names in the ontology.

On top of this basic classification task, we specified two tasks that require additional expressive power of DLP(S). First, we compute the transitive reduction of the class hierarchy, i.e., a directed graph that contains only direct subclass relations without the transitive bridges (Task A). The additional rules in Figure 2 were used for this task. While Task A is inherently non-monotonic, these rules are still stratified and lead to a unique stable model.

As a second task, we compute maximal antichains (i.e., sets of incomparable classes) in the class hierarchy (Task B). This task admits many solutions, each a stable model, and we asked systems to compute five stable models in this case. The rules we used are shown in Figure 3.

Experiments were executed with eight different ontologies from the Oxford Ontology Repository 5 as shown in Table 1. In each case, we deleted axioms that are not supported in the description logic Horn-ALC and normalised the remaining axioms as required by the classification rules [Carral et al., 2019b]. Our final evaluation data sets are provided in the auxiliary material. Our evaluation computer is a mid-end server (Debian Linux 9.13; Intel Xeon CPU E5-2637v4@3.50GHz; 384GB RAM DDR4; 960GB SSD), though most experiments did not use more than 8GB of RAM. A timeout of 15min was used in all experiments. We report results of single runs, as we observed almost no time variations across runs.

5 https://www.cs.ox.ac.uk/isg/ontologies/

The results of scenarios DLVCOMP and EXRULES on both tasks are shown in Figure 4, with missing values indicating a timeout. Scenario LAZY is omitted from the figure since it did not succeed in any of the tasks. The most difficult problem that we could solve with method LAZY was the basic classification (without any of the additional rules for tasks A or B) of the vaccine ontology 00668, which took 248sec (vs. <4sec needed in the other approaches).

Overall, we find that ASP with set terms can be used to solve complex problems on large real-world inputs. Both the native implementation in DLV-complex and our new existential-rule grounding performed well across a range of inputs. Contrary to our expectations, the lazy grounding approach was much less effective. Since Alpha solved instances of the base task, which already contains (7) as the only rule that can create infinitely many domain elements, we speculate that the algorithm behaves correctly in principle but is sometimes affected by additional optimisations or heuristics.

DLVCOMP and EXRULES often showed similar performance on Task A, though we can see some differences, most notably an order of magnitude advantage for VLog+clasp on 00395. Interestingly, EXRULES showed almost the same performance on Task B, whereas times for DLVCOMP increased such that only smaller problems could be solved. Again, this might be caused by a particular weakness of the implementation that is not conceptual. For EXRULES, most of the time was spent in the grounding phase, whereas solving the grounded files was relatively quick. Overall, we see promise in the performance of our existential grounding prototype, but the absolute run times should not be considered the main outcome of our experiments, given the diversity of the underlying systems in terms of maturity and recency.

7 Conclusions

Set terms are a natural and intuitive modelling construct, and clearly a useful addition to practical ASP tools. This seems to be the first work, however, that highlights their expressive advantages and puts them to concrete use on real-world problems that (due to their computational complexity) cannot be solved with plain ASP. Our work indicates that various existing ASP systems can feasibly be applied to these new kinds of tasks. The competitive performance of our prototypical existential-rule grounder encourage further research into combinations of existential rules and ASP.

We were surprised by the weak performance of lazy grounding approaches in our experiments, but we still consider them promising. Our programs can serve as benchmarks for further improving such implementations. An operational alternative to DLV-complex would to implement own set datatypes through extension points of modern ASP solvers, such as clingo's @-terms or DLV's external atoms. Finally, there is potential for investigating further uses of set terms in ASP for improving performance or readability. Candidate applications can be found, e.g., in the area of abstract argumentation, where ASP has been successfully applied [Gaggl et al., 2015]. Our experiments with description logics (DLs) also suggest the use of sets for a native integration of DLs and ASP, e.g., in the style of dl-programs [Eiter et al., 2004].

Acknowledgments

We thank an anonymous reviewer of IJCAI'22 for pointing out the potential utility of clingo @-terms and DLV external atoms for implementing complex-value extensions of ASP. This work was partly supported by Deutsche Forschungsgemeinschaft (DFG) in project 389792660 (TRR 248, Center for Perspicuous Systems), by the Bundesministerium f¨ur Bildung und Forschung (BMBF) in projects 01IS20056 NAVAS and ScaDS.AI (Center for Scalable Data Analytics and Artificial Intelligence), and by the Center for Advancing Electronics Dresden (cfaed).