Conflict-driven ASP Solving with External Sources and Program Splits

1 Introduction

Answer-Set Programming (ASP) is a declarative programming paradigm based on nonmonotonic programs [Gelfond and Lifschitz, 1991]. HEX-programs are an extension of ASP with external sources (ontologies, Web resources, etc). So-called external atoms pass information from the program to an external source, which returns values to the program. Notably, value invention allows for domain expansion. For instance, the external atom &synonym[car ](X) might be used to find the synonyms X of car , e.g. automobile. Also recursive data exchange between the program and external sources is supported, which leads to high expressiveness of the formalism. We use HEX as a representative for formalisms with expanding domains. Also well-known ASP extensions such as aggregates [Faber et al., 2010] and constraint ASP [Ostrowski and Schaub, 2012] correspond to special cases of HEX.

Suitable safety conditions guarantee the existence of a finite grounding which suffices for answer set computation; a grounding algorithm exists [Eiter et al., 2016b]. However, computing a grounding is often expensive as, in general, the grounder must evaluate external sources under up to exponentially many inputs to ensure that all relevant constants are respected. The situation is relieved by a model-building framework based on program splitting, where program components are arranged in a directed acyclic graph [Eiter et al., 2016a]. Then, at the time a component is grounded, its predecessors have already been evaluated and their answer sets can be exploited to skip evaluations. However, splitting deteriorates the performance of the conflict-driven solver since propagation throughout the whole program is inhibited. Therefore, current approaches suffer either a solving or a grounding bottleneck, depending on whether program splitting is used or not.

∗ Supported by the Austrian Science Fund (FWF) project P27730.

In this work we propose a novel learning technique for programs with multiple components, which is our main contribution. This allows for retaining the splitting technique for the sake of efficient grounding, but at the same time also propagate learned knowledge throughout the whole program. To this end, we identify reasons for inconsistencies in program components in terms of input from predecessors and propagate them back. The results are relevant beyond HEX as they carry over to special cases thereof; also ordinary ASP solving can benefit from splitting [Eiter et al., 2011] and is another possible application of our results.

In more detail, after the preliminaries (Section 2), the organization of the paper and our contributions are as follows:

• In Section 3 we use the notion of inconsistency reasons (IRs) for HEX-programs and present an algorithm for computing them for ground programs.
• In Section 4 we extend the algorithm to the nonground case, respecting possible optimizations by the grounder.
• In Section 5 we show how the techniques can be used to realize learning over multiple program components.
• In Section 6 we present our implementation and experimental results, which show a significant - in some cases even exponential - speedup.
• In Section 7 we discuss related work and conclude the paper.

Proofs are outsourced to the extended version at http://www. kr.tuwien.ac.at/research/projects/inthex/tulearning-ext.pdf.

2 Preliminaries

We follow Drescher et al. [2008] for basic concepts. We use as our alphabet mutually disjoint sets P of predicates, X of external predicats, C of constants, and V of variables. The set of all terms is given by T = C ∪ V.

An (ordinary) atom a is of form p(t1, . . . , tℓ) with predicate symbol p ∈ P and terms t1, . . . , tℓ ∈ T , abbreviated as p(t); for a list of terms t = t1, . . . , tℓ we write t ∈ t if t = ti for some 1 ≤ i ≤ ℓ. We call an atom (or other objects) ground if it does not contain variables. A (signed) literal is of type Ta or Fa, where a is an atom. We let σ denote the negation of a literal, i.e. Ta = Fa and Fa = Ta. An assignment A over the (finite) set A of ground atoms is a set of literals over A, where Ta ∈ A expresses that a is true, also denoted A |= a, and Fa ∈ A that a is false, also denoted A ̸|= a. A nogood is a set {L1, . . . , Ln} of ground literals Li, 1 ≤ i ≤ n. An assignment A is a solution to a nogood δ if δ ̸⊆ A, and to a set of nogoods ∆ if δ ̸⊆ A for all δ ∈ ∆. Note that according to this definition, partial assignments (i.e., assignments such that for some a ∈ A we have Ta ̸∈ A and Fa ̸∈ A) might be solutions to nogoods, even if supersets thereof are not. This definition is by intend and does not harm in the following.

HEX-Programs. We briefly recall HEX-programs, which generalize (disjunctive) logic programs under the answer set semantics [Gelfond and Lifschitz, 1991]; for more details and background, see Eiter et al. [2016a].

Syntax. HEX-programs extend ordinary ASP-programs by external atoms, which enable a bidirectional interaction between a program and external sources of computation. An external atom is of the form &g[Y](X), where &g ∈ X is an external predicate, Y = p1, . . . , pk is a list of input parameters (predicate names from P or constants 1 from C ∪ V), called input list, and X = t1, . . . , tl are output terms.

Definition 1. A HEX-program P consists of rules

a1 ∨ · · · ∨ ak ← b1, . . . , bm, not bm+1, . . . , not bn (1) where each ai is a ground atom and each bj is either an ordinary atom or an external atom.

The head of a rule r is H(r) = {a1, . . . , ak}, its body is B(r) = {b1, . . . , bm, not bm+1, . . . , not bn}, and its positive resp. negative body is B+(r) = {b1, . . . , bm} resp. B-(r) = {bm+1, . . . , bn}.

Semantics. We first define the semantics of ground programs. In the following, assignments are over the set A(P ) of ordinary atoms that occur in the program P at hand. The semantics of a ground external atom &g[y](x) wrt. an assignment A is given by the value of a 1+k+l-ary Boolean oracle function f&g that is defined for all possible values of A, y and x. Thus, &g[y](x) is true relative to A iff f&g(A, y, x) = T. In extension of the semantics by Gelfond and Lifschitz [1991], a ground rule r of form (1) is satisfied under A, denoted A |= r, if A |= ai for some 1 ≤ i ≤ k, or A ̸|= bi for some 1 ≤ i ≤ m, or A |= bi for some m+ 1 ≤ i ≤ n. A ground program P is satisfied under A, denoted A |= P, if each r ∈ P is satisfied under A. The answer sets of a ground HEX-program P are defined using the FLP-reduct of P wrt. an assignment A, which is the set fP A = {r ∈ P | A |= b for all b ∈ B(r)} of all rules whose body is satisfied by A:

1 Also variables become constants after the grounding step.

Definition 2. An assignment A is an answer set of a ground HEX-program P, if A is a subset-minimal model of fP A. 2

The set of all answer sets of a program P is denoted AS(P ).

Example 1. Consider the program P = {p ← &id[p]()}, where &id[p]() is true iff p is true. Then P has the answer set A1 = ∅; indeed it is a subset-minimal model of fP A1 = ∅.

The answer sets of a (possibly) nonground program P are given by the answer sets AS(grndC(P)) of its grounding grndC(P) = {ρ(r) | ρ: V → C}, which results from P if all variables are replaced by all constants from C in all possible ways using variable substitutions ρ: V → C; for a composed object x (atom, rule, program, etc), ρ(x) denotes x after replacing each variable V ∈ vars(x) in x by ρ(V ).

While grndC(P) may be infinite in general, suitable safety criteria guarantee that a finite subset suffices to compute the answer sets, cf. Eiter et al. [2016b]. In this paper, all programs are assumed to satisfy these criteria.

Grounding and solving algorithm. For the general understanding of this paper it is not necessary to introduce the grounding procedure in detail. Some details about the solving algorithm are introduced later on. However, it is important to know the following properties of the algorithms.

The existing grounding algorithm [Eiter et al., 2016b] is typically slow whenever an external atom depends on atoms other than facts and this dependency is neither monotonic nor antimonotonic. Then already the construction of a single rule instance is exponential in the number of atoms. Intuitively, this is because the grounder does not yet know the relevant inputs to the external atom and must evaluate it under exponentially many possibilities to ensure that all relevant output elements are respected. After grounding, the solving algorithm [Eiter et al., 2014a] is applied, which uses conflict-driven learning similar to SAT and ordinary ASP solving [Gebser et al., 2012]; the search is interleaved with the evaluation of external sources. Efficiency strongly depends on learning additional nogoods during solving, which are only implicitly in the program. In addition, an evaluation framework has been developed, which allows for splitting the program into components [Eiter et al., 2016a]; while splitting may speed up grounding since the grounder already knows parts of the answer set computed by previous components, it is barrier for conflict-driven learning.

3 Inconsistency Analysis - Ground Case

In this section we consider programs P which are extended with facts FI over atoms I ⊆ D from a given (input) domain D, where FI = {a ←| a ∈ I}. This resembles a program (component) P evaluated under input I (e.g. from predecessor components, as discussed more extensively in Section 5).

Following Redl [2017b], we express reasons for inconsistency of P ∪ FI in terms of atoms which must resp. must not occur in I in order to make P ∪FI inconsistent. Formally:

Definition 3 (Inconsistency Reason (IR)). Let P be a HEXprogram and D be a set of atoms, called (input) domain, such that H(P) ∩ D = ∅. An inconsistency reason (IR) of P wrt. D is a pair R = (R+, R-) of sets of atoms R+ ⊆ D and R- ⊆ D with R+ ∩ R- = ∅ s.t. P ∪ FI is inconsistent for I ⊆ D with R+ ⊆ I and R- ∩ I = ∅.

2 For ordinary P , these are Gelfond & Lifschitz' answer sets.

Example 2. An IR of P = {← a, not c; d ← b.} wrt. D = {a, b, c} is R = ({a}, {c}) because P ∪FI is inconsistent for all I ⊆ D whenever a ∈ I and c ̸∈ I, while b can be in I or not without influencing (in)consistency.

Note that in contrast to work on ASP debugging, which we discuss in more detail in Section 7 and focuses on (humanreadable) explanations for inconsistency of single programs, out notion rather aims at identifying classes of program instances depending on the input facts, which are inconsistent. As a consequence, the techniques developed for ASP debugging cannot directly be used, which is intuitively expected because checking a single program for inconsistency is computationally easier than identifying IRs, cf. Redl [2017b].

Further note that although small IRs are preferred, we do not formally require them to be minimal. This is in view of the application in Section 5, which relies on a fast method for computing IRs, for which we give up minimality.

In general, programs may have no, one or multiple IRs. For instance, {← a;← b} has the inconsistency reasons R1 = ({a}, ∅) and R2 = ({b}, ∅)) wrt. D = {a, b}.

We introduce now a new technique for computing IRs. Since it is based on an extension of the evaluation algorithm for ground HEX-programs, we recapitulate it in the following paragraph; for details we refer to Eiter et al. [2014a]. However, we slightly adopt the presentation of the algorithm as a preparation for the extensions in the paragraph afterwards.

Evaluation of ground HEX-programs. The evaluation follows Algorithm 1. The initialization is at (a). The given HEX-program P is extended with facts FI and transformed to an ordinary ASP-program ˆ P by replacing each external atom &g[y](x) in P by an ordinary replacement atom e&g[y](x) and adding a rule e&g[y](x)∨ne&g[y](x) ← to guess its value. Program ˆ P is then represented as set of nogoods ∆, which consists of nogoods ∆ˆ P stemming from Clark's completion [Clark, 1977] and singleton loop nogoods [Gebser et al., 2012]; this set will be extended as the search space is traversed. The computed answer set ˆA of the guessing program ˆ P is initially empty; for the sake of the algorithm, assignments are seen as lists (i.e., the order of assignments is relevant). The decision level (dl) is initially 0 and incremented for every guess. We assume that dl(a) ∈ N0 stores the dl of each assigned atom. The initialization immediately assigns facts to true and atoms which do not appear in any heads to false (both at dl 0).

After the initialization, the algorithm performs deterministic propagation at (b) such as unit propagation; further propagation techniques such as unfounded set propagation can be added. Each implied literal is assigned at the maximum dl of the literals which implied it. The algorithm detects conflicts, learns additional nogoods and backtracks at (c). If the conflict is on dl 0, the instance is inconsistent and the callback function h is notified (with nogoods ∆ and assignment ˆA over P as input) to determine the return value in case of inconsistency; this callback serves as a preparation for our extension of the algorithm below and is instantiated with just h⊥(∆, ˆA) = ⊥ for answer set computation. If the assignment is complete at

Algorithm 1: HEX-CDNL

(d), the algorithm must check if the guesses of replacement atoms coincide with the real truth values of external atoms, and if it represents a model which is also subset-minimal wrt. the reduct. If this is not the case, the assignment is added as nogood in order to discard it. 3 Finally, the algorithmmay perform theory propagation at (e) or guess a truth value at (f) if no other case is applicable.

Soundness and completeness of Algorithm 1 was shown by Eiter et al. [2014a] as follows:

Proposition 1. Let P be a program and I ⊆ D be input atoms from a domain D. If HEX-CDNL(P, I, h⊥) returns (i) an assignment A, then A is an answer set of P ∪FI ; (ii) ⊥, then P ∪FI is inconsistent.

Computing inconsistency reasons. We now extend the existing evaluation algorithm for ground HEX-programs from the previous paragraph to an algorithm for computing IRs. Our approach is based on implication graphs, which represent the current status and assignment history of the solver following Algorithm 1, cf. e.g. Biere et al. [2009]. Intuitively, the nodes of the graph represent (already assigned) literals or conflicts, their decision levels, and the nogoods which implied them. Predecessor nodes represent implicants. Nodes without predecessors represent guesses. Formally:

Definition 4. An implication graph is a directed graph 〈V, E〉, where V is a set of triplets 〈L, dl , δ〉, denoted L@dl/δ, where L is a signed literal or ⊥, dl ∈ N0 is a decision level, δ ∈ ∆ ∪ {⊥} is a nogood, and E is a set of unlabeled edges.

3 This is for simplicity, actual implementations are more involved.

Algorithm 2: InconsistencyAnalysis

a guess on dl 1, Fb@1/δ1 is implied by Ta using δ1, Tc@1/δ2 is implied by Ta and Fb using δ2, Td@2/⊥ is a guess on dl 2, and Te@2/δ3 is implied by Tc and Td using δ3.

In order to compute an IR wrt. a domain D in case of inconsistency, we reuse Algorithm 1 but let it call Algorithm 2 after an inconsistency is detected by using InconsistencyAnalysis(D,∆, ˆA) instead of h⊥.

Observe that for answer set computation (i.e., using h = h⊥), soundness of Algorithm 1 implies that h(∆, ˆA) is called at some point because it is the only way to return ⊥. Note that this can only happen after a violated nogood has been identified on decision level 0. But this implies that at the time the inconsistency of an instance is detected, all assignments are deterministic.

Now the basic idea of Algorithm 2 is as follows. We start at (a) with a nogood δ ∈ ∆ which is currently violated; such a nogood always exists because otherwise Algorithm 1 would not have called h(∆, ˆA). Since each literal σa in this nogood was assigned on decision level 0, each of them was assigned by unit propagation as a consequence of previously assigned literals. Algorithm 2 resolves this nogood at (c) with the cause of one of its literals σa, i.e., with the nogood ϵ which implied literal σa. The loop at (b) repeats this step until the nogood contains only literals over explanation atoms from D. The iterative resolution corresponds to the replacement of the literal by its predecessors in the implication graph (where the implication graph itself is implicitly represented by the nogoods that implied literals). The iteration steps when the nogood δ contains only literals from D; since these literals imply the originally violated nogood and are thus responsible for inconsistency, δ represents an IR which we return at (d).

Using hDanalyse (∆, ˆA) = InconsistencyAnalysis(D,∆, ˆA) allows then for exploiting Algorithm 1 to compute IRs:

Proposition 2. Let P be a program and I ⊆ D be input atoms froma domainD. If HEX-CDNL(P, I, hDanalyse ) returns (i) an assignment A, then A is an answer set of P ∪ FI ; (ii) a pair R = (R+,R-) of sets of atoms, then P ∪ FI is inconsistent and R is an inconsistency reason of P wrt. D.

4 Inconsistency Analysis - Nonground Case

We now extend the above approach to nonground programs.

Grounding algorithms for ASP and HEX do not use the naive grounding grndC(P) which substitutes variables V in P by constants in C in all possible ways. Instead, optimizations are performed to keep the grounding small. However, the exact algorithms for performing such optimizations, and therefore the output, depend on the used grounder. In fact, a correct grounding procedure can output any optimized ground program ogC(P) as long as AS(ogC(P)) = AS(P) holds; it does not even be a subset of grndC(P), which allows for optimizations within rules and introducing auxiliary rules. This is why one cannot give a precise definition of an optimized grounding. However, while multiple valid groundings exist in general, we assume that an arbitrary but fixed algorithm is used, which makes ogC(P) unique; similarily for pogC,I(P) introduced in the following.

This prohibits the direct reduction of the computation of an IR for a (possibly) nonground program P wrt. a domain D to the ground case. Let Pg = ogC,I(P) be an optimized grounding of P ∪ FI for some I ⊆ D, where we assume that the facts FI themselves are not included in the grounding. Then, if HEX-CDNL(Pg, I, hDanalyse ) returns a pair R = (R+, R-), we have by Proposition 2 that R is an IR for Pg, i.e., Pg ∪ FJ is inconsistent for all J ⊆ D with R+ ⊆ J and R- ∩ J = ∅. However, R is not necessarily an IR for P wrt. D because for a different set of facts I ′ ⊆ D we may have ogC,I ′ (P) ̸= Pg.

Example 4. Consider P = {q(X) ← p(X); ← not q(1)} and D = {p(1)}. For input I = ∅, Pg ∪ FI = {← not q(1)} is a valid grounding for evaluation because AS(P ∪ FI ) = AS(Pg ∪ FI) = ∅. However, for inconsistency analysis of P , the grounding Pg ∪ FI is not sufficient: R = (∅, ∅) is an IR of Pg wrt. D but not of P wrt. D as P ∪ F{p(1)} is consistent.

We thus use a partially optimized grounding pogC,I(P) for a specific input I ⊆ D with the properties that (i) pogC,I (P ) ⊆ grndC(P) and (ii) AS(pogC,I(P)) = AS(P ∪ FI). That is, optimization is restricted to the elimination of rules, while changes within or additions of rules are prohibited. A grounding procedure for HEX-progams with these properties was presented by Eiter et al. [2016b].

The idea is to use pogC,I(P) for the inconsistency analysis, but respect that unknown rules might provide additional support for atoms. To this end, we introduce for each atom a in pogC,I(P) a rule a ← a′ , where a′ is a new atom, to represent the situation that a is supported by rules not in pogC,I(P). While structural information of the programmight be exploited to further restrict the set of atoms that can have further support by rules that are missing in the current grounding, this is not a trivial task; we leave it for future work in order to focus on the main idea in this paper. Then, if an IR does not contain any a′ , possibly missing rules are not relevant and it carries over to program P. Formally:

Proposition 3. Let P be a program and I ⊆ D be input atoms from a domain D. Then an IR R = (R+,R-) of pogC,I(P)∪{a ← a′ | a ∈ A(pogC,I(P))} wrt. D∪{a′ | a ∈ A(pogC,I(P))} s.t. (R+ ∪R-)∩{a′ | a ∈ A(pogC,I(P))} = ∅ is an IR of P wrt. D.

5 Trans-Unit Propagation

Current evaluation techniques are in particular bad for programs with guesses that are separated from constraints by nonmonotonic external atoms; we focus on programs of this form in the following. While monotonic and antimonotonic external atoms can be efficiently grounded without splitting, grounding nonmonotonic external atoms, which do not depend only on facts, requires exponentially many calls to external sources. Splitting can solve this grounding bottleneck, but it introduces a solving bottleneck because subsequent constraints cannot be propagated back.

Example 5. Suppose we want to form a committee of employees. Some pairs of persons should not be together in the committee due to conflicts of interests (cf. independent sets of a graph). The competences of the committee depend on the persons involved. For instance, it can decide in technical questions only if a certain number of members has expert knowledge in the field. The competences can depend nonmonotonically on the members. For instance, while overrepresentation of a department might not be forbidden in principle, it can make it lose authorities such as assigning more resources to this department. Constraints define the competences the committee should have. This is encoded as follows:

r4 : ← not comp(technical), not comp(financial).} Here, we do not want committees which can neither decide in technical nor financial affairs.

When grounding P as a whole, since the external atom in r3 depends nonmonotonically on the guessed committee, the grounder must evaluate it under all possible guesses as each one could introduce other competences. However, many guesses are not relevant because they are already eliminated by r2. In contrast, an existing evaluation framework for HEXprograms allows for splitting it into components which are separately grounded and solved [Eiter et al., 2016a]. More precisely, based on the dependencies between rules, the program is partitioned into subprograms such that the resulting dependencies between the subprograms form an acyclic evaluation graph (cyclically depending rules must be in one component); an example is shown in Figure 2. For the evaluation, the framework first computes the answer sets of components without predecessors. The successor components are then extended with the answer sets of predecessor components (one at a time), grounded and solved. This procedure is repeated recursively; the final answer sets are extracted from the leaf components. For details we refer to Eiter et al. [2016a].

Example 6 (cont'd). Program P from Example 5 can be partitioned into P1 and P2, where P2 depends on P1, cf. Figure 2.

However, then r4 is separated from the guess and a conflict with r4 during the evaluation of P2 cannot be propagated to exclude guesses. Hence, with current evaluation techniques, there is a bottleneck either in the grounding phase (if the program is not split) or in the solving phase (if it is split).

Propagating inconsistency reasons. The main idea is to associate an IR R = (R+, R-) of a later program component with a constraint cR =← R+, {not a | a ∈ R-} which we propagate to predecessors. Recall that for a domain D of explanation atoms and an inconsistency reason R = (R+, R-) wrt. a program P , all programs P ∪ FI with I ⊆ D such that R+ ⊆ I and R- ∩ I = ∅ are inconsistent. Thus:

Proposition 4. For all HEX-programs P and IRs R = (R+, R-) of P wrt. a domain D, we have that AS(P ∪FI ) = AS(P ∪ {cR} ∪ FI ) for all I ⊆ D.

Such a constraint can also be added to predecessor components in order to eliminate wrong guesses earlier, which we call trans-unit (tu-)propagation.

Proposition 5. For a program component P and IRs R = (R+, R-) of P wrt. a domain D, we have that cR can be added to a predecessor component P ′ , if all atoms appearing in cR are defined in P ′ or one of its own transitive predecessors.

Example 7 (cont'd). Assume that joe and sue are the only technicians and alyson is the only economist. Then, P2 is always inconsistent if none of these three persons is selected, independent of other choices. If the current input to component P2 is I = {in(jack), in(joseph)}, then by exploiting nogoods learned from the external source &competences, the IR R = (∅, {in(joe), in(sue), in(alyson)}) wrt. P2 ∪ FI can be determined, and the constraint cR =← not in(joe), not in(sue), not in(alyson) can be added to P1.

According to Proposition 5, a constraint constructed in this way can be added to a predecessor component P ′ , if all atoms appearing in cR are defined in P ′ . That is, it can be added to all predecessors which fulfill this criterion. In our implementation and experiments, we add it to the top-most one. This in order to eliminate invalid candidates as early as possible. For analytical reasons, this is always better than adding them to later program components since it eliminates possibly more candidates, while costs for adding the constraint are the same for all components.

6 Implementation and Experiments

For the experiments, we integrated our techniques into the reasoner DLVHEX 4 with GRINGO 4.5.4 and CLASP 3.1.4 as backends. All benchmarks were run on a Linux machine with two 12-core AMD Opteron 6176 SE CPUs and 128 GB RAM; timeout was 300 secs and memout 8 GB per instance. We used the HTCondor load distribution system (http://research.cs. wisc.edu/htcondor) to ensure robust runtimes (i.e., deviations of runs on the same instance are negligible).

Setting and hypotheses. Based on the program class we want to assess, we selected our benchmarks such that guessing and checking is separated by nonmonotonic external atoms. For each benchmark we compare three configurations: (i) evaluation as a monolithic program, (ii) evaluation using splitting, and (iii) evaluation with trans-unit (tu-)propagation. Our hypothesis is that (i) suffers a grounding and (ii) suffers (also) a solving bottleneck, whereas (iii) outperforms the other two approaches as it can restrict the grounding and propagate throughout the whole program at the same time. In the tables we show the overall runtime, grounding and solving time, averaged over all instances of the respective size; importantly, other computations besides grounding and solving (e.g. preprocessing and method-specific tasks such as splitting for (ii) and inconsistency analysis for (iii)) can cause the overall runtime to be higher than the sum of grounding and solving time. Numbers in parantheses show the number of timeout instances. The encodings of all presented benchmarks can be found in the official benchmark suite of the system. 5

4 http://www.kr.tuwien.ac.at/research/systems/dlvhex

Configuration Problem. Consider the following configuration problem. We assemble a server cluster consisting of various components. For a given component selection the cluster has different properties such as its efficiency, power consumption, etc. Properties may depend not only on individual components but also on their interplay, and this dependency can be nonmonotonic (e.g. the selection of an additional component might make it lose the property of low energy consumption). We want the cluster to have certain properties.

In order to capture also similar configuration problems (such as Example 5), we use a more abstract formalization as a quadruple (D, P,m, C), where D is a domain, P is a set of properties, m is a function which associates each selection S ⊆ D with a set of properties m(S) ⊆ P, and C is a set of constraints of form Ci = (C + i ,C - i ), where C + i ⊆ 2P and C - i ⊆ 2P define sets properties which must resp. must not be simultaneously given; a selection S ⊆ D is a solution if for all (C + i ,C - i ) ∈ C we have C + i ̸⊆m(S) or m(S) ∩C - i ̸= ∅.

For the experiment we consider for each size n ten randomly generated instances with n domain elements, ⌊ n5 + 1⌋ properties, a random function m, and a random number of constraints, such that their count has an expected value of n.

The results are shown in Table 1. One can observe that for all shown instance sizes, the splitting approach is the slowest, monolithic evaluation is the second-slowest, and tupropagation is the fastest configuration. A look at the grounding and solving times shows that for the monolithic approach, the main source of computation costs is grounding, while for splitting it is the solving phase (although also the grounding costs are high due to repetitive instantiation of program components). In contrast, with tu-propagation both grounding and solving is fast, while most of the computation time is spent on other computations (most importantly, the inconsistency analysis). The observations are in line with our hypotheses.

Diagnosis Problem. Next, we consider the diagnosis problem 〈Od,Op,H, C, P〉, where sets Od and Op are definite resp. potential observations, H is a set of hypotheses, C is a set of constraints over the hypotheses, and P is a logic program which defines the observations which follow from given hypotheses. Each constraint C ∈ C forbids certain combinations of hypotheses. A solution consists of a set SH ⊆ H of hypotheses and a set of potential observations SO ⊆ Od such that (i) all answer sets of P ∪H, which contain all of SO ∪Od, contain also SH, and (ii) C ̸⊆ SH for all C ∈ C. Informally, SH are necessary hypotheses to explain the observations.

5 https://github.com/hexhex/core/tree/master/benchmarks

As a concrete medical example, definite observations are known symptoms and test results, potential observations are possible outcomes of yet unfinished tests and hypotheses are possible causes (e.g. diseases, nutrition behavior, etc). Constraints exclude certain (combinations of) hypotheses because it is known from anamnesis and the patient's declaration that they do not apply. A solution of the diagnosis problem corresponds to a set of possible observations which, if confirmed by tests, imply certain hypotheses (i.e., medical diagnosis), which can be exploited to perform the remaining tests goal-oriented.

We use 10 random instances for each instance size, where the size is given by the number of observations; observations are definite with a probability of 20% and potential otherwise.

The results are shown in Table 2. Unlike for the previous benchmark, monolithic is slower than splitting. This is because the evaluation of the external source (corresponding to evaluating P ) is much more expensive now; since monolithic grounding requires exponentially many evaluations, while during solving this is not necessarily the case, the evaluation costs have a larger impact to monolithic than to splitting. However, as before tu-propagation is clearly the fastest configuration. Again, the observations are in line with our hypotheses.

Analysis of Best-Case Potential. Finally, in order to analyze the potential of our approach in the best case, we use a synthetic program. Our program of size n is as follows:

It uses a domain of size n and guesses a subset thereof. It then uses an external atom to compute the complement set. The final constraint encodes that the guessed set and the complement must not be nonempty at the same time, i.e., there are only two valid guesses: either all elements are in or all are out.

The results are shown in Table 3. While splitting separates the rules in the third line from the others and must handle each guess independently, the monolithic approach must evaluate the external atom under all possible extensions of out . Both approaches are exponential. In contrast, tu-propagation learns for each non-empty guess a constraint which excludes all guesses that set someIn to true; after learning a linear number of such constraints, only the two valid guesses remain.

7 RelatedWork and Conclusion

RelatedWork. Previous work on inconsistency analysis was mainly in the context of answer set debugging and faulty systems in general, based on symbolic diagnosis [Reiter, 1987]. For instance, Syrj¨anen [2006] computes inconsistency explanations in terms of either minimal sets of constraints which need to be removed to regain consistency, or of odd loops (in the latter case the program is called incoherent). The realization is based on another program. Also the more general approaches by Brain et al. [2007] and Gebser et al. [2008] rewrite the program to debug into a meta-program using dedicated control atoms. The goal is to support human users to find reasons for undesired program behavior. Possible queries are, for instance, why a certain assignment is not an answer set. These approaches are based on meta-programming while our approach is based on an analysis of the implication graph. The extension to the nonground case, which is crucial for our application, requires further techniques. The challenges arise from the fact that, unlike the approaches mentioned above, we do not only compute reasons for inconsistency of a fixed program, but rather inconsistency wrt. a set of possible extensions by facts. Another difference concerns the goal of the approaches: while the aforementioned ones aim at answer set debugging and therefore at human-readable explanations of the inconsistency, we aim at an explanation in terms of atoms, which can be transformed into a constraint more easily.

Also related are previous evaluation algorithms for HEXprograms. While the previous state-of-the-art algorithm corresponds to Algorithm 1 using h⊥(∆, ˆA) = ⊥ for parameter h, alternative algorithms have been developed as well. One of them was presented by Eiter et al. [2014b], who used support sets [Darwiche and Marquis, 2002] to represent sufficient conditions to make an external atom true. Such support sets are used speed up the compatibility check at (d). However, as this technique shows its benefits only during the solving phase, it does not resolve the grounding issue addressed in this paper. Later, another evaluation approach based on support sets was developed; in contrast to the previous one it compiles away external atoms altogether [Redl, 2017a]. However, the size of the resulting rewritten program strongly depends on the type of external sources and is exponential in general. Thus, the technique is only practical for certain external sources which are known to have a small representation by support sets (which is not the case for the benchmarks discussed in this paper).

Conclusion. Our experiments show that inconsistency analysis is a promising technique for realizing conflict-driven learning over multiple program components. For programs where evaluation as a whole causes a grounding bottleneck (e.g. due to presence of value invention in programs with expanding domains), splitting is useful for efficient grounding but introduces a barrier for propagation and a solving bottleneck. Inconsistency analysis is the basis for combining the advantages of both: splitting for the sake of efficient grounding but still propagating throughout the whole program. The results show a significant, potentially exponential speedup for the addressed class of programs.

An interesting starting point for future work is the generalization of nogood propagation to general, not necessarily inconsistent program components. In this work, typical solver optimizations have been disabled for tu-propagation as they can harm soundness of the algorithm in general; although the other approaches used them and tu-propagation was still the fastest, an important extension is the identification of specific solver optimizations which are compatible with inconsistency analysis and might lead to an even greater improvement. Another starting point for future work is to exploit structural information of the program to further restrict the set of atoms that can have further support by rules that are missing in the current grounding. Since this decision must reasonably be made without computing the full grounding