# efficient_hexprogram_evaluation_based_on_unfounded_sets__ca0bb60b.pdf

Journal of Artiﬁcial Intelligence Research 49 (2014) 269 321 Submitted 09/13; published 02/14

Efﬁcient HEX-Program Evaluation Based on Unfounded Sets

Thomas Eiter EITER@KR.TUWIEN.AC.AT Michael Fink FINK@KR.TUWIEN.AC.AT Thomas Krennwallner TKREN@KR.TUWIEN.AC.AT Christoph Redl REDL@KR.TUWIEN.AC.AT Institut f ur Informationssysteme Technische Universit at Wien Favoritenstraße 9-11, A-1040 Vienna, Austria

Peter Sch uller PETERSCHUELLER@SABANCIUNIV.EDU Faculty of Engineering and Natural Sciences Sabanci University Orhanli, Tuzla, 34956 Istanbul, Turkey

HEX-programs extend logic programs under the answer set semantics with external computations through external atoms. As reasoning from ground Horn programs with nonmonotonic external atoms of polynomial complexity is already on the second level of the polynomial hierarchy, minimality checking of answer set candidates needs special attention. To this end, we present an approach based on unfounded sets as a generalization of related techniques for ASP programs. The unfounded set detection is expressed as a propositional SAT problem, for which we provide two different encodings and optimizations to them. We then integrate our approach into a previously developed evaluation framework for HEX-programs, which is enriched by additional learning techniques that aim at avoiding the reconstruction of the same or related unfounded sets. Furthermore, we provide a syntactic criterion that allows one to skip the minimality check in many cases. An experimental evaluation shows that the new approach signiﬁcantly decreases runtime.

1. Introduction

Answer Set Programming (ASP) is a declarative problem solving approach. Due to expressive extensions and efﬁcient systems like SMODELS (Simons, Niemel a, & Soininen, 2002), DLV (Leone, Pfeifer, Faber, Eiter, Gottlob, Perri, & Scarcello, 2006) and CLASP (Gebser, Kaufmann, & Schaub, 2012), it has been gaining popularity for many applications (Brewka, Eiter, & Truszczy nski, 2011). However, current trends in computing, such as context awareness or distributed systems, raised the need for access to external sources in a program. For instance, external sources on the Web range from light-weight data access (e.g., XML, RDF, or data bases) to knowledge-intensive formalisms (e.g., OWL ontologies). To cater for this need, Eiter, Ianni, Schindlauer, and Tompits (2005) deﬁned HEX-programs as an extension of ASP with so-called external atoms, through which the user can couple any external information source with a logic program. Roughly, such atoms pass information, given by predicate extensions, from the program to an external source which returns output values of an (abstract) function that it computes. For example, a rule nb(X, Y ) &neighbor[ map , X](Y ) may informally import for a point X on a map that is stored in the ﬁle map (in a particular data format), each point Y in the neighborhood of X into the predicate nb. Such convenient external access has been

c 2014 AI Access Foundation. All rights reserved.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

exploited for many applications, including querying data and ontologies (Eiter et al., 2008b; Hoehndorf et al., 2007; Marano et al., 2010), e-government (Zirtiloˇglu & Yolum, 2008), fuzzy answer set programming (Nieuwenborgh, Cock, & Vermeir, 2007a), multi-context reasoning (Brewka & Eiter, 2007; Eiter et al., 2012b), (Nieuwenborgh et al., 2007b; Basol et al., 2010). The formalism is highly expressive as recursive data exchange between the rules and external sources is possible. The semantics of HEX-programs is model-based and given by answer sets following the approach of Faber, Leone, and Pfeifer (2011), which extends the answer set semantics of logic programs (Gelfond & Lifschitz, 1991) to logic programs with aggregates; the Faber et al. approach (known as the FLP semantics) preserves the property that answer sets have, in the spirit of the closed world assumption, smallest positive information content, which is formally captured by a minimality condition on models. The current approach for the evaluation of HEX-programs (Eiter et al., 2006a, 2011) is to rewrite a given HEX-program to an answer set program by (i) eliminating external atoms in favor of auxiliary atoms using so called replacement atoms, and (ii) introducing auxiliary rules such that the answer sets of the HEX-program Π correspond to a subset of the answers sets of the resulting program ˆΠ in which the auxiliary atoms faithfully represent the values of the external atoms; this compatibility condition of an answer set of ˆΠ is tested in a postcheck. For computing the answer sets of a (disjunctive) logic program P like ˆΠ, different methods have been proposed. An immediate one is to implement the deﬁnition of an answer set and test whether a given interpretation is a minimal model of the so called reduct of the program P wrt. the interpretation; to this end, a suitable candidate answer set might be guessed or generated by heuristics. This approach was essentially adopted for the solvers GNT (Janhunen et al., 2006) and CMODELS (Lierler, 2005), which use for this test a logic program, respectively a SAT encoding. A different approach was presented by Leone et al. (1997) based on the notion of unfounded set (Van Gelder, Ross, & Schlipf, 1991), which they extended from normal (non-disjunctive) to disjunctive logic programs. Intuitively, a set U of atoms is unfounded wrt. to a model of a program P, if switching all atoms in U to false does not lead to violated rules; the answer sets of P are then its models that are unfounded-free, i.e., the models disjoint from all respective unfounded sets. For checking (un)foundedness of a given candidate answer set, Koch et al. (2003) presented a SAT encoding. Drescher et al. (2008) later exploited ﬁndings of them and Leone et al. to extend the technique of conﬂict-driven clause learning used by the CLASP solver to disjunctive logic programs. In all the quoted works, however, access to external sources was not an issue, and thus they cannot be deployed to HEX-programs. In fact, in addition to the compatibility check of an answer set of the replacement program ˆΠ, the current HEX evaluation must in a second step test the minimality of the interpretation induced for the HEX-program Π wrt. the program reduct. This method, which we refer to as the explicit FLP check, turns out to be less efﬁcient in practice, and it often dominates the total runtime; thus a more efﬁcient method is desirable. Motivated by this and the seminal approach of Leone et al., we consider in this paper the use of unfounded sets as an alternative to the explicit FLP check for HEX-programs, which we refer to as the unfounded set check. To this end, we extend the notion of unfounded sets for disjunctive logic programs to HEX-programs, following the lines of Faber (2005), where unfounded sets for logic programs with aggregates were deﬁned, and consider their use in combination with clause learning techniques. Our main contributions are summarized as follows:

We present a basic encoding of unfounded set existence to a set of nogoods, i.e., constraints that have to be satisﬁed, and we show that its solutions are in 1-1 correspondence with the

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

unfounded sets. The latter can thus be computed running a SAT solver, followed by a postprocessing step which checks that the values of replacement atoms are compatible with the external call results. Benchmarks show that this strategy is already more efﬁcient than the explicit FLP check.

We then present an advanced encoding of unfounded set existence that is reusable for any interpretation. Compared to our ﬁrst encoding, it is conceptually more involved and has (slightly) higher initialization cost, but it has the advantage that it can be reused for all unfounded set checks and needs no separate initialization for each check. Our benchmarks show that the advanced encoding is superior to the ﬁrst one for many practical problems.

Next, we consider optimizations which hinge on dependencies between external and ordinary atoms that are determined in careful analysis. These optimizations can be integrated into our encodings by adding further nogoods which restrict the search space to relevant parts.

We consider how to exploit information gained in the unfounded set check of a candidate answer set in answer set candidate generation, i.e., in the evaluation of the program ˆΠ. Adopting a Conﬂict Driven Clause Learning approach (Drescher et al., 2008), this step has been recently enhanced by external behavior learning (Eiter et al., 2012a), in which nogoods describing the external source behavior are learned during the search to guide model generation towards proper guesses. We show how to learn in the candidate generation step additional nogoods from unfounded sets that avoid the reconstruction of the same or related unfounded sets, yielding further gain.

We present a syntactic decision criterion that can be used to decide whether a program possibly has unfounded sets. If the result of this check is negative, then the computationally expensive search for unfounded sets can be skipped entirely. The criterion is based on atom dependency and, loosely speaking, says that there are no cyclic dependencies of ground atoms through external atoms. This property can be efﬁciently checked for a given ground HEXprogram using standard methods. In fact it applies to a range of applications, in particular for input-stratiﬁed programs, where external sources are accessed in a workﬂow to produce input for the next stage of computation. However, advanced applications of HEX-programs can have cycles through external atoms, e.g., in natural encodings of problems on multi-context systems (Brewka & Eiter, 2007) or abstract argumentation systems (Dung, 1995), for which the FLP check can not be simply skipped.

In further elaboration, we then consider a program decomposition based on the dependency graph that is induced by a program Π (note that exploiting syntactic modularization of unfounded sets can be traced back to Leone et al., 1997; Koch et al., 2003). We show that Π has some unfounded set wrt. a candidate answer set A exactly if some of the components ΠC in its decomposition has some unfounded set wrt. A; as computing the decomposition can be realized efﬁciently and does not incur large overhead, we can apply the decision criterion for skipping the FLP check efﬁciently on a ﬁner-grained level, and the search for unfounded sets can be guided to relevant program parts.

An experimental evaluation on advanced reasoning applications shows that unfounded sets checking combined with learning methods of Eiter et al. (2012a) improves HEX-program evaluation considerably, sometimes drastically. More speciﬁcally, the benchmark applications

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

include reasoning tasks in Multi-Context Systems (Brewka & Eiter, 2007; Eiter et al., 2012b), abstract argumentation (Dung, 1995), terminological default reasoning over description logic knowledge bases (Baader & Hollunder, 1995), and conformant planning (Goldman & Boddy, 1996; Smith & Weld, 1998). The experiments have been carried out with DLVHEX version 2.3.0, a prototype solver for HEX-programs, which was extended to support the techniques developed in this paper. The decomposition approach can yield a considerable gain, as it appears e.g. for the HEX-encoding of a Dung-style argumentation semantics (Dung, 1995) and DL-programs (Eiter et al., 2008a). On the other hand, for the terminological default reasoning benchmark, our syntactic criterion lets us conclude that the FLP check is obsolete. In conclusion, the new approach enables signiﬁcant speedup and thus enlarges the scope of

HEX applicability.

1.1 Organization

The rest of this paper is organized as follows. The next section provides preliminaries on HEXprograms and their evaluation via answer sets of a transformed ASP program without external atoms. In Section 3, we deﬁne unfounded sets and present a basic and a uniform encoding of unfounded set search using nogoods. Section 4 considers reﬁnements and optimizations of the encodings, as well as external behavior learning to prevent reconstruction of unfounded sets. In Section 5, we give a syntactic decision criterion to avoid the FLP check and a program decomposition method exploiting it. Experimental results of a prototype implementation are reported in Section 6. In Section 7, we consider related work and extensions of our approach. In Section 8, we conclude and point out issues for further research.

2. Preliminaries

In this section, we start with some basic deﬁnitions, and then introduce HEX-programs. In accordance with Gebser et al. (2012) and Eiter et al. (2012a), a (signed) literal is a positive or a negative formula Ta resp. Fa, where a is a ground atom of form p(c1, . . . , cℓ), with predicate p and constants c1, . . . , cℓ, abbreviated p(c). For a literal σ = Ta or σ = Fa, let σ denote its opposite, i.e., Ta = Fa and Fa = Ta. An assignment A over a (ﬁnite) set of atoms A is a consistent set of signed literals Ta or Fa, where Ta expresses that a A is true and Fa that it is false; A is complete, also called an interpretation, if no assignment A A exists. We denote by AT = {a | Ta A} and AF = {a | Fa A} the set of atoms that are true resp. false in A, and by ext(q, A) = {c | Tq(c) A} the extension of a predicate q in A. Furthermore, A|q is the set of all literals over atoms with predicate q in A. For a list q = q1, . . . , qk of predicates, we write p q iff qi = p for some 1 i k, and let A|q = S j A|qj. A nogood is a set {L1, . . . , Ln} of signed literals Li, 1 i n. An interpretation A is a solution to a nogood δ (resp. to a set of nogoods), iff δ A (resp. δ A for all δ ).

Example 1 The interpretation A = {Ta, Fb, Tc} is a solution to the nogood {Ta, Tb, Tc} but not to {Ta, Fb, Tc}.

2.1 HEX-Programs

Next, we recall syntax and semantics of HEX-programs.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

2.1.1 HEX-PROGRAM SYNTAX

As introduced by Eiter et al. (2005), HEX-programs are a generalization of (disjunctive) extended logic programs under the answer set semantics (Gelfond & Lifschitz, 1991). HEX-programs extend ASP programs by external atoms, which enable a bidirectional interaction between a program and external sources of computation. External atoms have a list of input parameters (constants or predicate names) and a list of output parameters. Informally, to evaluate an external atom, the reasoner passes the constants and extensions of the predicates in the input tuple to the external source associated with the external atom. The external source computes output tuples which are matched with the output list. Syntactically, a ground external atom is of the form

&g[p](c), (1)

where &g is an external predicate, p = p1, . . . , pk are the input list consisting of predicate names or object constants, and c = c1, . . . , cl are the output list consisting of constant terms. Predicates in the input list are sometimes called input predicates. A default literal is a formula b or not b, where b is a ground ordinary atom of form p(c1, . . . , cℓ) with constants ci, 1 i ℓ, or and external atom. For every set S of ordinary and external atoms, we let not S = {not b | b S}. Ground HEX-programs are then deﬁned similar to ground ASP programs.

Deﬁnition 1 (Ground HEX-programs) A ground HEX-program consists of rules

a1 ak b1, . . . , bm, not bm+1, . . . , not bn , (2)

where each ai is an ordinary ground atom, each bj is either an ordinary ground atom or a ground external atom, and k + n > 0.1

For a rule r, the head is H(r) = {a1, . . . , ak} and the body is B(r) = B+(r) not B (r), where B+(r) = {b1, . . . , bm} is the positive body, B (r) = {bm+1, . . . , bn} is the negative body. If B(r) = , then r is a fact, and we omit . For a program Π, let A(Π) be the set of all ordinary atoms and EA(Π) be the set of all external atoms occurring in Π. For a default literal b, let tb = Ta if b = a for an atom a, and tb = Fa if b = not a. Furthermore, fb = Fa if b = a and fb = Ta if b = not a. We call a rule r a constraint, if B(r) = .

Example 2 For rule r = a b c, not d we have H(r) = {a, b}, B+(r) = {c} and B (r) = {d}. We further have tc = Tc, fc = Fc, t not d = Fd and f not d = Td.

We will also consider non-ground programs (i.e., with variables allowed in place of object constants) in our examples. In particular, external atoms &g[X](Y) may contain variables in their input list X and output list Y. For such programs, suitable safety conditions allow for using a grounding procedure which transforms the program to a variable-free program with the same answer sets (Eiter, Ianni, Schindlauer, & Tompits, 2006). However, we limit our formal investigation to ground programs.

1. For simplicity, we do not formally introduce strong negation but view, as customary, classical literals a as new atoms together with a constraint which disallows that a and a are simultaneously true.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

Example 3 The program

domain(a); domain(b)

sel(X) domain(X), not nsel(X)

nsel(X) domain(X), not sel(X)

encodes the problem of partitioning two domain elements a and b into two sets sel and nsel.

2.1.2 HEX-PROGRAM SEMANTICS

An ordinary ground atom a is true relative to assignment A, denoted A |= a, if Ta A and false otherwise. A default-negated ground atom not a is true relative to assignment A, denoted A |= not a, if Fa A and false otherwise. The semantics of a ground external atom of form (1) wrt. an interpretation A is given by the value of a 1+k+l-ary Boolean oracle function f&g that is deﬁned for all possible values of A, p and c, such that &g[p](c) is true relative to A, denoted A |= &g[p](c), if and only if f&g(A, p, c) = 1.

Example 4 (Set Partitioning) Consider the program Π

sel(a) domain(a), &diﬀ[domain, nsel](a)

nsel(a) domain(a), &diﬀ[domain, sel](a)

where for predicates p and q, &diﬀ[p, q](X) computes the set of all elements X which are in the extension of p but not in the extension of q. Informally, this program implements a choice from sel(a) and nsel(a).

Satisfaction of ordinary rules and ASP programs (Gelfond & Lifschitz, 1991) is then extended to

HEX-rules and programs in the obvious way: a rule r is satisﬁed by assignment A, denoted A |= r, iff A |= h for some h H(r), or A |= b for some b B+(r), or A |= b for some b B (r). A program Π is satisﬁed by assignment A iff A |= r for all r Π. An interpretation A is a model of a program Π, denoted A |= Π, iff A |= r for all r Π. The notion of extension ext( , A) for external predicates &g with input lists p is naturally deﬁned by ext(&g[p], A) = {c | f&g(A, p, c) = 1}.

Deﬁnition 2 (FLP-Reduct (Faber et al., 2011)) For an interpretation A over a program Π, the FLP-reduct of Π wrt. A is the set fΠA = {r Π | A |= b, for all b B(r)} of all rules whose body is satisﬁed by A.

An assignment A1 is smaller or equal to another assignment A2 wrt. a program Π, denoted A1 Π A2, iff {Ta A1 | a A(Π)} {Ta A2 | a A(Π)}.

Deﬁnition 3 (Answer Set) An answer set of Π is a Π-minimal model A of fΠA.

Example 5 Consider the program Π:

where f&id(A, p) = 1 iff Tp A is true. Then Π has the answer set A1 = ; indeed it is a Π-minimal model of fΠA1 = . Note that A2 = {Tp, Tq} is not an answer set of Π, as it is not a minimal model of fΠA2 = Π.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

2.2 Evaluation of HEX-Programs

A possible way to determine the answer sets of a HEX-program Π is to use a transformation to an ASP program without external atoms whose answer sets encompass all answer sets of Π. We now describe such a transformation. Each external atom a = &g[p](c) in a rule r Π is replaced by an ordinary ground replacement atom ˆa = e&g[p](c) (resulting in a rule ˆr), and an additional rule e&g[p](c) ne&g[p](c) is added to the program. The answer sets of the resulting guessing program ˆΠ are determined by an ASP solver and projected to non-replacement atoms. However, the resulting assignments might be spurious answer sets of Π, as the values of &g[p] and e&g[p](c) relative to an interpretation may not coincide. Each answer set of ˆΠ is thus merely a candidate which must be checked against the external sources. If no discrepancy is found, the model candidate is a compatible set of Π. More precisely,

Deﬁnition 4 (Compatible Set) A compatible set of a program Π is an assignment ˆA such that

(i) ˆA is an answer set (Gelfond & Lifschitz, 1991) of the guessing program ˆΠ, and (ii) f&g( ˆA, p, c) = 1 iff Te&g[p](c) ˆA for all external atoms &g[p](c) in Π, i.e., the guessed values coincide with the values of the oracle functions.

A subset of the compatible sets of Π represents the answer sets of Π, where each answer set A of Π is given by the restriction of a unique compatible set ˆA to the non-replacement atoms. More formally, an answer set A of a program Π corresponds to the compatible set

κ(Π, A) = A {Tea, Fnea | a is an external atom in Π, A |= e}

{Fea, Tnea | a is an external atom in Π, A |= e} .

To ﬁlter out those compatible sets that do not yield answer sets, each compatible set ˆA has to be checked against models of the FLP reduct. To be more speciﬁc, a procedure called explicit FLP check constructs the reduct fΠA and checks whether it has a model A smaller than A; if such an A is found, it rejects A, otherwise outputs A as an answer set. The explicit FLP check rewrites the HEX-program to an ASP program without external atoms and amounts to the search for answer sets of the following program, in which the truth values of all replacement atoms coincide with the according oracle function values:

Check(Π, A) = f ˆΠ ˆA { a | a A(Π), Ta ˆA} {a a | Ta ˆA} { not smaller} {smaller not a | a A(Π), Ta ˆA} .

It consists of the reduct f ˆΠ ˆA and rules that restrict the search to proper subinterpretations of ˆA, where smaller is a new atom. Moreover, as we actually need to search for models and not just compatible sets, rules of the form a a (where a is a new atom for each Ta ˆA) make sure that atoms can be arbitrarily true without having a justifying rule in Π.

Proposition 1 Let A be an interpretation extracted from a compatible set ˆA of program Π. Then the program Check(Π, A) has an answer set A such that f&g(A , p, c) = 1 iff Te&g[p](c) A

for all external atoms &g[p](c) in Π, if and only if A is not an answer set of Π.

Because of the guessing rules, we can rewrite all rules in f ˆΠ ˆA except the guesses on replacement atoms to constraints as follows:

Check Optimized(Π, A) = f ˆΠ ˆA { a | a A(Π), Ta ˆA} {a a | Ta ˆA} { not smaller} {smaller not a | a A(Π), Ta ˆA}.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

External Atom Evaluation

Π add external replacement atoms + guessing rules

Main Search (CDNL) Plugin 1

check unveriﬁed external atom guesses

FLP Check (Unfounded Set Check)

Plugin k Answer Sets

Model Candidates

Compatible Sets

Figure 1: Overview of the framework for evaluating HEX-programs.

where f ˆΠ ˆA denotes the FLP reduct of ˆΠ wrt. interpretation ˆA with each rule of form (2) except guessing rules for replacement atoms being rewritten to

not a1, . . . , not ak, b1, . . . , bm, not bm+1, . . . , not bn .

Proposition 2 Let A be an interpretation extracted from a compatible set ˆA of program Π. Then the program Check Optimized(Π, A) has an answer set A such that f&g(A , p, c) = 1 if and only if Te&g[p](c) A for all external atoms &g[p](c) in Π, if and only if A is not an answer set of Π.

This program is more efﬁcient for evaluation. Our comparison in Section 6 uses this optimized version of the explicit check, but still demonstrates a signiﬁcant performance gain by our novel approach.

Example 6 (cont d) Reconsider the program Π = { p &id[q](); q p } from above. Then the corresponding guessing program is ˆΠ = {p e&id[q](); q p; e&id[q]() ne&id[q]() } and yields the compatible sets ˆA1 = and ˆA2 = {Tp, Tq, Te&id[p]}. While A1 = is also a Π-minimal model of fΠA1 = , A2 = {Tp, Tq} is not a Π-minimal model of fΠA2 = Π. Indeed, the program

Check(Π, A2) = ˆΠ {p p ; q q ; e&id[q]() e &id[q]() } { not smaller}

{smaller not p} {smaller not q; smaller not e&id[q]()}

has the answer set A = n Fp, Tp , Fq, Tq , Fe&id[q](), Tne&id[q](), Te &id[q](), Tsmaller o and

f&id(A , q, ϵ) = 0 and Fe&id[q]() A .

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

Basic Encoding

Uniform Encoding Assumptions

search for UFS candidates

verify candidate

External Atom Evaluation

Main Search (CDNL) unfounded free

compatible set ˆA

Figure 2: FLP Check based on Unfounded Sets

The complete prodedure of computing answer sets of HEX-programs has been described by Eiter et al. (2012a) and is shown as a block diagram in Figure 1; the ﬁrst version introducing this approach was DLVHEX version 2.1.0. Step S1 enumerates compatible sets; we reuse this part of the evaluation process from prior work and do not modify it. Step S2 checks whether a compatible set is indeed a

HEX answer set. The improvement of the efﬁciency of S2 is the focus of this work. S1 transforms the input program Π into ˆΠ by introducing replacement atoms and guesses for replacement atoms. The main search enumerates model candidates, i.e., answer sets of ˆΠ. (Depending on heuristics, this search can evaluate external atoms for guiding the search.) Model candidates are veriﬁed against the semantics of external atoms. If this check fails, the main search continues to enumerate model candidates; if the check succeeds, then the model candidate is a compatible set. S2 checks whether a compatible set is an answer set of Π. Previous work realized this step using an explicit FLP check. In this work we propose two alternatives to carry out this FLP check based on unfounded sets.

Figure 2 depicts a block diagram of the FLP checks proposed in this work, called basic and uniform encoding. Both encodings are SAT theories. The basic encoding builds on the program Π and the compatible set ˆA. The uniform encoding is based only on Π (hence we can reuse it for all compatible sets), however it requires us to set solver assumptions based on ˆA. The encoding (and assumptions) are used to search for unfounded set (UFS) candidates (by a SAT solver). A UFS candidate has to be veriﬁed against the values of external atoms (these are guessed in the UFS encoding). If all UFS candidates fail the external atom check, or if there are no UFS candidates, then ˆA is an unfounded-free compatible set and hence an answer set of Π. Otherwise the FLP check found an unfounded set wrt. ˆA and the main search continues looking for a new model candidate.

We next describe our encodings for UFS-checking.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

3. Unfounded Set Detection

As described in Section 2.2, the minimality check, also called the explicit FLP check, is computationally costly and involves much overhead: all models of Check(Π, A) must be enumerated, and calls to the external sources to test compatibility must be made. Even worse, as we need to search for a smaller model and not just for a smaller compatible set, Check(Π, A) usually (to our experience) has even more models than the original program. Moreover, it appears that in many current application scenarios there is no smaller model of the reduct fΠA, i.e., most assignments extracted from compatible sets ˆA pass the FLP check. There are two possible reliefs: developing a cheaper minimality check or to avoid the minimality check if possible. While this section targets at the former idea, the latter one is addressed in Section 5. To this end, we present a novel FLP check algorithm based on unfounded sets (UFS). Instead of explicitly searching for smaller models of the reduct, we check whether the candidate answer set is unfounded-free. To this end, we use unfounded sets for HEX-programs akin to those by Faber (2005) for programs with arbitrary aggregates.

Deﬁnition 5 (Unfounded Set) Given a program Π and an assignment A, let X be any set of ordinary ground atoms appearing in Π. Then, X is an unfounded set for Π wrt. A if, for each rule r having some atoms from X in the head, at least one of the following conditions holds, where A . .X = (A \ {Ta | a X}) {Fa | a X}:

(i) some literal of B(r) is false wrt. A,

(ii) some literal of B(r) is false wrt. A . .X, or

(iii) some atom of H(r) \ X is true wrt. A.

Intuitively, an unfounded set is a set of atoms which only circularly support each other; by assigning all of them false, no violation of any rule will be introduced. As for answer sets, their minimality enforces now that no subset of the atoms that are true in an answer set can form an unfounded set; in fact, answer sets can be characterized in terms of unfounded sets, using the following notion.

Deﬁnition 6 (Unfounded-free Interpretations) An interpretation A of a program Π is unfoundedfree, iff AT X = , for every unfounded set X of Π wrt. A.

The following result is a generalization of a respective result for ordinary (disjunctive) logic programs (Leone et al., 1997) and logic programs with aggregates (Faber, 2005).

Theorem 3 (Characterization of Answer Sets) A model A of a HEX-program Π is an answer set of Π iff it is unfounded-free.

Example 7 Consider the program Π and A1 from Example 6. Trivially, A1 is unfounded-free, and thus A1 is an answer set of Π. On the other hand, the set X = {p, q} is an unfounded set w.r.t. A2, since X intersects with the head of p &id[q]() and A . .X |= &id[q](). Therefore A2 is not unfounded-free and not an answer set of Π.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

3.1 Basic Encoding of the Unfounded Set Search

We realize the search for unfounded sets using nogoods, i.e., for a given Π and an assignment A we construct a set of nogoods, such that solutions to this set correspond to (potential) unfounded sets; we then use a SAT solver to search for such unfounded sets. More speciﬁcally, our encoding of unfounded set detection uses a set

ΓA Π = NA Γ,Π OA Γ,Π ,

of nogoods where NA Γ,Π contains all necessary constraints and the set OA Γ,Π are optional optimization nogoods that prune irrelevant parts of the search space; the latter is related to the one of Drescher et al. (2008) but respects external atoms. The idea is that the set of ordinary atoms of a solution to ΓA Π represents a (potential) unfounded set U of Π wrt. A, while the replacement atoms encode the truth values of the corresponding external atoms under A . .U. For a rule r, let B+ o (r) B+(r) consist of all ordinary atoms, and let Be(r) B(r) consist of all external replacement atoms. Then, ΓA Π is built over atoms A(ΓA Π) = A(ˆΠ) {hr, lr | r Π}, where hr, and lr are new atoms for every rule r in Π. The necessary part

NA Γ,Π = {{Fa | Ta A}} S r Π Rr,A

of ΓA Π consists of a nogood {Fa | Ta A}, which eliminates unfounded sets that do not intersect with true atoms in A, and of nogoods Rr,A = Hr,A Cr,A for every r Π where

Hr,A = {{Thr} {Fh | h H(r)}} {{Fhr, Th} | h H(r)}, called the head criterion, encodes that hr is true for a rule r iff some atom of H(r) is in the unfounded set; and

{{Thr} {Fa | a B+ o (r), A |= a} {ta | a Be(ˆr)} {Th | h H(r), A |= h}} if A |= B(r), {} otherwise, called the conditional part Cr,A, encodes that Condition (i), (ii) or (iii) of Deﬁnition 5 must hold if hr is true. More speciﬁcally, for an unfounded set U and a rule r with H(r) U = (hr is true) it must not happen that A |= B(r) (Condition (i) fails), no a B+ o (r) with A |= a is in the unfounded set and all a Be(ˆr) are true under A . .U (Condition (ii) fails), and all h H(r) with A |= h are in the unfounded set (Condition (iii) fails). Concrete instances for OΓ,A Π are deﬁned in Section 4.

Example 8 Consider Π = {r1 : p &id[p]()} and the compatible set ˆA = {Tp, Te&id[p]}. The nogood set NA2 Γ,Π is {{Thr1, Fp}, {Fhr1, Tp}, {Thr1, Te&id[p](), Tp}}.

Towards computing unfounded sets, observe that every unfounded set can be extended to a solution to the nogood set ΓA Π over A(ΓA Π). Conversely, the solutions to ΓA Π include speciﬁc extensions of the unfounded sets, given for each unfounded set U by assigning true to all atoms in U, to all hr such that H(r) intersects with U, and to all replacement atoms e&g[p](c) such that &g[p](c) is true under A . .U, and assigning false to all other atoms in A(ΓA Π). More formally,

Deﬁnition 7 (Induced Assignment of an Unfounded Set wrt. ΓA Π) Let U be an unfounded set of a program Π wrt. assignment A. The assignment induced by U wrt. ΓA Π, denoted IΓ(U, ΓA Π, Π, A), is IΓ(U, ΓA Π, Π, A) = I0 Γ(U, Π, A) {Fa | a A(ΓA Π), Ta I0 Γ(U, Π, A)} ,

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

I0 Γ(U, Π, A) = {Ta | a U} {Thr | r Π, H(r) U = } {Te&g[p](c) | &g[p](c) EA(Π), A . .U |= &g[p](c)} .

We call a set N of nogoods conservative, if it holds for every unfounded set U of Π wrt. A that IΓ(U, ΓA Π, Π, A) is a solution to N. We then show that the solutions to ΓA Π include all assignments induced by unfounded sets of Π wrt. A, assuming that OΓ,A Π is conservative.

Proposition 4 Let U be an unfounded set of a program Π wrt. assignment A such that AT U = . Then IΓ(U, ΓA Π, Π, A) is a solution to ΓA Π.

Note that the converse does not hold, i.e., not every solution corresponds to some induced assignment; intuitively this is because it does not reﬂect the semantics of external sources. Regardless of this we immediately obtain from Proposition 4 a useful test for unfounded-freeness.

Corollary 5 If ΓA Π has no solution, then U AT = for every unfounded set U of Π.

Using the following result, we can ﬁnd the unfounded sets of Π wrt. A among all solutions to ΓA Π by using a postcheck on the external atoms.

Theorem 6 Let S be a solution to ΓA Π such that

(a) Te&g[p](c) S and A |= &g[p](c) implies A . .U |= &g[p](c); and

(b) Fe&g[p](c) S and A |= &g[p](c) implies A . .U |= &g[p](c)

where U = {a | a A(Π), Ta S}. Then U is an unfounded set of Π wrt. A.

Informally, the proposition states that the non-replacement atoms in S that are true and also appear in Π form an unfounded set, provided that truth of the replacement atoms e&g[p](c) in S coincides with the truth of the corresponding &g[p](c) under A . .U (as in Deﬁnition 7). However, this check is just required if the truth values of e&g[p](c) in S and of &g[p](c) under A differ. This gives rise to an important optimization for the implementation: external atoms, whose (known) truth value of &g[p](c) under A matches the truth value of e&g[p](c) in S, do not need to be postchecked. It follows immediately from Deﬁnition 7 that this postcheck does not eliminate unfounded sets, as formalized by the following proposition.

Proposition 7 Let U be an unfounded set of a program Π wrt. assignment A such that AT U = . Then IΓ(U, ΓA Π, Π, A) fulﬁlls Conditions (a) and (b) of Theorem 6.

Example 9 Reconsider program Π = {r1 : p &id[p]()} from Example 8 and the compatible set ˆA2 = {Tp, Te&id[p]}. The nogood set NA2 Γ,Π = {{Thr1, Fp}, {Fhr1, Tp}, {Thr1, Te&id[p](), Tp}} has solutions S {Thr1, Tp, Fe&id[p]()}, which correspond to the unfounded set U = {p}. Here, Fe&id[p]() represents that A2 . .U |= &id[p]().

Note that due to the premises in Conditions (a) and (b) of Theorem 6, the postcheck is faster if Te&g[p](c) S whenever A |= &g[p](c) holds for many external atoms in Π. This can be exploited during the construction of S as follows: if it is not absolutely necessary to set the truth value of e&g[p](c) differently, then carry over the value from &g[p](c) under A. Speciﬁcally, this is successful if e&g[p](c) does not occur in ΓA Π.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

3.2 Uniform Encoding of the Unfounded Set Search

The encoding ΓA Π presented in the previous subsection has the disadvantage that it depends on the current assignment A. Therefore it needs to be generated separately for every unfounded set check if the assignment changed (which is very likely). As this causes signiﬁcant overhead, we present now an advanced encoding which can be reused for any assignment. We introduce some additional variables which represent the truth values of the atoms in the current assignment. Prior to an unfounded set check, the current assignment is injected by setting the values of these variables to ﬁxed values, which can be done using assumptions as supported by modern SAT solvers such as CLASP. Changing assumptions is much easier than changing the encoding, which leads to an additional speedup in some cases, especially for programs which need many unfounded set checks. Our advanced encoding uses a set ΩΠ of nogoods. As before, the idea is that the set of ordinary atoms of a solution to ΩΠ represents a (potential) unfounded set U of Π wrt. some assignment A, while the replacement atoms encode the truth values of the corresponding external atoms under A . .U. The encoding ΩΠ is conceptually more complex than ΓA Π; the initialization is computationally (slightly) more costly, hence the advantages of our new encoding become visible for instances with many compatible sets (thus many unfounded set checks), while it might be counterproductive for small instances. The nogood set ΩΠ is built over the atoms of ˆΠ and and further fresh atoms not occurring in ˆΠ: hr and lr, for every rule r in Π, a A for every ordinary atom a A(ˆΠ) (i.e. ordinary atoms in Π and replacement atom auxiliaries), and a A . .U, a A U, a A U for every ordinary atom a A(Π). The auxiliary atoms a A, a A . .U, a A U, a A U are used to make the encoding usable for any assignment A. Only during the unfounded set check with respect to a certain assignment, we will temporarily add assumptions to the solver which force certain truth values of the atoms a A for all a A(ˆΠ) depending on the current assignment A. Intuitively, a A represents the truth value of a in A and a A . .U of a in A . .U (where U is the current unfounded set), a A U represents that a is true in A and is contained in U, and a A U represents that a is false in A or it is contained in U. To this end, a set of assumptions is a consistent set A of signed literals. A solution A to a nogood δ resp. a set of nogoods satisﬁes A, if A A. That is, assumptions ﬁx the truth value of some atoms. Modern ASP and SAT solvers support assumptions natively, and they can be easily undone without a complete reset of the reasoner and recreating the whole problem instance. This is an essential feature for efﬁciently implementing our improved encoding. Our encoding ΩΠ is then ΩΠ = NΩ,Π OΩ,Π ,

where NΩ,Π = {{Fa | a A(Π)}} S a A(Π) Da S r Π(Hr Cr) is the necessary part and

{Fa | a A(Π)} encodes that we search for a nonempty unfounded set;

{Fa A U, Ta A, Ta}, {Ta A U, Fa A}, {Ta A U, Fa} {Fa A U, Fa A}, {Fa A U, Ta}, {Ta A U, Ta A, Fa} {Ta A . .U, Fa A}, {Ta A . .U, Ta}, {Fa A . .U, Ta A, Fa}

encodes that a A U is true iff a A and a are both true, a A U is true iff a A is false or a is true, and a A . .U is true iff a A is true and a is false;

Hr = {{Thr} {Fh | h H(r)}} {{Fhr, Th} | h H(r)} encodes that hr is true for a rule r iff some atom of H(r) is in the unfounded set; and

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

{{Thr} {Ta A | a B+(ˆr)} {Fa A | a B (ˆr)} (i) {Fa A U | a B+ o (r)} {ta | a Be(ˆr)} (ii) {Th A U | h H(r)}} (iii)

encodes that if hr is true, then one of (i), (ii) or (iii) in Deﬁnition 5 must hold.

More speciﬁcally, for an unfounded set U and a rule r with H(r) U = (hr is true) it must not happen that A |= B(r) (Condition (i) fails), no a B+ o (r) with A |= a is in the unfounded set and all a Be(ˆr) are true under A . .U (Condition (ii) fails), and all h H(r) with A |= h are in the unfounded set (Condition (iii) fails).

Example 10 For Π = {r1 : p &id[p]() } in Example 6, the constructed nogood set is

ΩΠ = {{Fp}, {Fp A U, Tp A, Tp}, {Tp A U, Fp A}, {Tp A U, Fp},

{Fp A U, Fp}, {Fp A U, Tp}, {Tp A U, Tp A, Fp}, {Tp A . .U, Fp A},

{Tp A . .U, Tp}, {Fp A . .U, Tp A, Fp},

{Thr1, Fp}, {Fhr1, Tp}, {Thr1, Te&id[p]()A, Te&id[p](), Tp A U}} .

Towards computing unfounded sets, observe that every unfounded set can be extended to a solution to the set of nogoods ΩΠ over A(ΩΠ). Conversely, the solutions to ΩΠ include speciﬁc extensions of all unfounded sets, which are again characterized by induced assignments; that is, by assigning true to all atoms in U, to all hr such that H(r) intersects with U, and to all replacement atoms e&g[p](c) such that &g[p](c) is true under A . .U, appropriate truth values to the auxiliary atoms according to their intuitive meaning, and assigning false to all other atoms in A(ΩΠ). More formally, this leads us to the following assignment:

Deﬁnition 8 (Induced Assignment of an Unfounded Set wrt. ΩΠ) Let U be an unfounded set of a program Π wrt. assignment A. The assignment induced by U wrt. ΩΠ, denoted IΩ(U, ΩΠ, Π, A), is IΩ(U, ΩΠ, Π, A) = I0 Ω(U, Π, A) {Fa | a A(ΩΠ), Ta I0 Ω(U, Π, A)} , where I0 Ω(U, Π, A) = {Ta | a U} {Thr | r Π, H(r) U = } {Te&g[p](c) | &g[p](c) EA(Π), A . .U |= &g[p](c)} {Ta A | a A(Π), Ta A} {Tˆa A | a EA(Π), A |= a} {Ta A U | a A(Π), Ta A, a U} {Ta A . .U | a A(Π), Ta A, a U} {Ta A U | a A(Π), Fa A or a U} .

If we adopt for an assignment A the assumption set

AA = {Ta A | a A(Π), Ta A} {Fa A | a A(Π), Fa A}

{Tˆa A | a EA(Π), A |= a} {Fˆa A | a EA(Π), A |= a} ,

then all assignments induced by unfounded sets of Π wrt. A are solutions to ΩΠ wrt. AA (but not conversely, because intuitively the latter do not reﬂect the semantics of external sources). As before, we call a set of nogoods N conservative, if IΩ(U, ΩΠ, Π, A) is a solution to N for every unfounded set U of Π wrt. A. Under this property, those interpretations are solutions of the whole nogood set which comply with the assumptions from A.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

Proposition 8 Let U be an unfounded set of a program Π wrt. assignment A such that AT U = . If OΩ,Π is conservative, then IΩ(U, ΩΠ, Π, A) is a solution to ΩΠ that satisﬁes AA.

Corollary 9 If ΩΠ has no solution which satisﬁes AA, then U AT = for every unfounded set U of Π (assuming OΩ,Π is conservative).

The next property allows us to ﬁnd the unfounded sets of Π wrt. A among all solutions to ΩA that satisfy AA by using a postcheck on the external atoms.

Theorem 10 Let S be a solution to ΩΠ (with conservative OΩ,Π) that satisﬁes AA such that

(a) Te&g[p](c) S and A |= &g[p](c) implies A . .U |= &g[p](c); and

(b) Fe&g[p](c) S and A |= &g[p](c) implies A . .U |= &g[p](c),

where U = {a A(Π) | Ta S}. Then U is an unfounded set of Π wrt. A.

As for ΓA Π, the proposition states that the non-replacement atoms in S that are true and appear in Π form an unfounded set, provided that each replacement atom e&g[p](c) in S has the same truth value as &g[p](c) under A . .U (as in Deﬁnition 8). Again, this check is just required if the truth value of e&g[p](c) in S is different from the one of &g[p](c) under A. Similarly as for the encoding Γ, it follows immediately from Deﬁnition 8 that this postcheck does not eliminate unfounded sets, as formalized by the following proposition.

Proposition 11 Let U be an unfounded set of a program Π wrt. assignment A such that AT U = . Then IΩ(U, ΩΠ, Π, A) fulﬁlls Conditions (a) and (b) of Theorem 10.

Example 11 Reconsider program Π = {r1 : p &id[p]()} from Example 6 and the compatible set A2 = {Tp, Te&id[p]}. The nogood set

ΩΠ = {{Fp}, {Fp A U, Tp A, Tp}, {Tp A U, Fp A}, {Tp A U, Fp},

{Fp A U, Fp}, {Fp A U, Tp}, {Tp A U, Tp A, Fp}, {Tp A . .U, Fp A},

{Tp A . .U, Tp}, {Fp A . .U, Tp A, Fp},

{Thr1, Fp}, {Fhr1, Tp}, {Thr1, Te&id[p]()A, Te&id[p](), Tp A U}}

with assumptions AA2 = {Tp A} has solutions S {Thr1, Tp, Tp A, Fe&id[p], Tp A U, Tp A U, Fp A . .U}, which correspond to the unfounded set U = {p}. Here, Fe&id[p]() represents that A2 . .U |= &id[p]().

We will see in Section 6 that the encoding ΩΠ is superior to ΓA Π for many practically relevant programs. The effect becomes especially visible if they need many unfounded set checks, which intuitively is the case when many answer sets exist; here reusability of the encoding is very beneﬁcial, while for small programs with few answer sets, the incurred overhead does not lead to savings.

4. Optimization and Learning

In this section we ﬁrst discuss some reﬁnements and optimizations of our nogood encodings for UFS search. In particular, we present nogoods which prune irrelevant parts of the search space; they can be integrated into both encodings ΓA Π and ΩΠ under suitable adjustments. After that, we propose a strategy for learning nogoods from detected unfounded sets, avoiding that the same unfounded set is generated later again.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

4.1 Optimization

We present now three optimizations which turned out to be effective in improving UFS search, where the second and the third exclude each other, i.e., they can not be used simultaneously.

4.1.1 RESTRICTING THE UFS SEARCH TO ATOMS IN THE COMPATIBLE SET

First, not all atoms in a program are relevant for the unfounded set search: atoms that are false under A can be ignored.

Proposition 12 Suppose U is an unfounded set of Π wrt. an interpretation A such that A |= a for some a U. Then U \ {a} is an unfounded set of Π wrt. A.

The nogoods for this optimization are simple. In the encoding ΓA Π, we add the conservative nogood {Ta} for each a A(Π) with A |= a to the optimization part OA Γ,Π and in the encoding ΩΠ the conservative nogood {Fa A, Ta} for each a A(Π) to the optimization part OΩ,Π.

4.1.2 AVOIDING GUESSES OF REPLACEMENT ATOMS

In some situations, the truth value of a replacement atom b in a solution S to ΓA Π resp. ΩΠ with assumptions AA is irrelevant. That is, both STb = (S \ {Tb, Fb}) {Tb} and SFb = (S \ {Tb, Fb}) {Fb} are solutions to ΓA Π resp. ΩΠ that satisfy AA, and they represent the same unfounded set. We then can set the truth value of b to an (arbitrary) ﬁxed value instead of inspecting both alternatives. The next proposition states a sufﬁcient criterion for this irrelevance.

Proposition 13 Let b be a replacement atom, and let S be a solution to ΓA Π resp. ΩΠ satisfying AA. If for every rule r Π such that b B+(ˆr) B (ˆr) and A |= B(r), either

(a) for some a B+ o (r) such that A |= a, it holds that Ta S, or

(b) for some a H(r) such that A |= a, it holds that Fa S,

then both STb and SFb are solutions to ΓA Π resp. ΩΠ that satisfy AA.

This property can be utilized by adding conservative nogoods. Recall that A(ΓA Π) and A(ΩΠ) contain atoms lr for every r Π. They intuitively serve to encode for a solution S to ΓA Π resp. ΩΠ with assumptions AA whether the truth values of the replacement atoms in B(r) are relevant or can be set arbitrarily. The following nogoods label relevant rules r, forcing lr to be false iff some of the conditions in Proposition 13 holds. For the encoding ΓA Π, we add to OA Γ,Π for each rule r:

LA Γ,r ={{Tlr, Ta} | a B+ o (r), A |= a} {{Tlr, Fa} | a H(r), A |= a} {{Flr} {Fa | a B+ o (r), A |= a} {Ta | a H(r), A |= a}} .

For the encoding ΩΠ, we add to OΩ,Π for each rule r:

LΩ,r ={{Tlr, Ta, Ta A} | a B+ o (r)} {{Tlr, Fa, Ta A} | a H(r)} {{Flr} {Fa A U | a B+ o (r)} {Ta A U | a H(r)}} . These constraints exclusively enforce either Tlr or Flr. Hence, the truth value of lr deterministically depends on the other atoms, i.e., the nogoods do not cause additional guessing. By Proposition 13 we can set the truth value of a replacement atom b arbitrarily, if lr is false for all r such that b B+(ˆr) or b B (ˆr). However, it must be ensured that changing the truth

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

value of replacement atoms does not harm the satisfaction of the conditions in Theorem 6 (resp. Theorem 10). As mentioned after Theorem 6, it is beneﬁcial to set the truth value of e&g[p](c) to the one of &g[p](c) under A, because this can reduce the number of external atoms that must be checked. Importantly, this also relaxes the antecedence of the conditions in Theorem 6 (resp. Theorem 10), and guarantees that they are not harmed. The following nogoods enforce a coherent interpretation of the replacement atoms. For the encoding ΓA Π we add to OA Γ,Π for each rule r:

F A Γ,r = {Flr | b B+(ˆr) B (ˆr)} {Fb} | b Be(ˆr), A |= b {Flr | b B+(ˆr) B (ˆr)} {Tb} | b Be(ˆr), A |= b ,

while for the encoding ΩΠ we add to OΓ,Π for each rule r:

FΩ,r = {Flr | b B+(ˆr) B (ˆr)} {Tb A, Fb} | b Be(ˆr) {Flr | b B+(ˆr) B (ˆr)} {Fb A, Tb} | b Be(ˆr) .

In summary, the encoding ΓA Π has the optimization part OA Γ,Π = S r Π LA Γ,r F A Γ,r and the encoding ΩΠ the optimization part OΩ,Π = S r Π LΩ,r FΩ,r. We give now an example for this optimization using our encoding Γ.

Example 12 Consider the program Π = {r1 : p &id[p](); r2 : q &id[q]()}, and the compatible set ˆA = {Tp, Tq, Te&id[p](), Te&id[q]()}. Then the necessary part of encoding ΓA Π has solutions S1 {Thr1, Tp, Fe&id[p](), Fhr2, Fq, Fe&id[q]()} and S2 {Thr1, Tp, Fe&id[p](), Fhr2, Fq, Te&id[q]()} (which represent the same unfounded set U = {p}). Here, the optimization part for r2, LA r2 F A r2 = {{Tlr2, Fq}, {Flr2, Tq}, {Flr2, Te&id[q]()}}, eliminates solutions S2 for ΓA Π. This is beneﬁcial as for solutions S1 the postcheck is easier (e&id[q]() in S1 and &id[q]() have the same truth value under A).

Note that if this optimization is not used, then for all rules r the atom lr is in fact not needed and thus unconstrained. To avoid an exponential increase of the number of UFS candidates, these atoms should then be set to a ﬁxed value.

4.1.3 EXCHANGING NOGOODS BETWEEN UFS AND MAIN SEARCH

The third optimization allows for the exchange of learned knowledge about external atoms between the UFS check and the main search for compatible sets. For this purpose, we ﬁrst deﬁne nogoods which correctly describe the input-output relationship of external atoms.

Deﬁnition 9 A nogood of the form N = {Tt1, . . . , Ttn, Ff1, . . . , Ffm, σe&g[p](c)}, where σ is T or F, is a valid input-output-relationship, if for every assignment A such that N \{σe&g[p](c)} A it holds that A |= &g[p](c) if σ = F, and A |= &g[p](c) if σ = T.

Here, the signed literals with atoms ti, 1 i n, resp. fj, 1 j m, reﬂect the relevant true resp. false atoms in the interpretation A, built over predicates which occur in the input list p. Techniques for learning such nogoods have been described by Eiter et al. (2012a) and exploit properties of external sources (such as monotonicity and functionality) to restrict the size of N. Let N be a nogood which is a valid input-output-relationship learned during the main search, i.e., for compatible sets of ˆΠ, and let F = T and T = F.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

Deﬁnition 10 (Nogood Transformation TΓ) For a valid input-output relationship N = {Tt1, . . . , Ttn, Ff1, . . . , Ffm, σe&g[p](c)} and an assignment A, the nogood transformation TΓ is deﬁned as

if Fti A for some 1 i n, { {Ft1, . . . , Ftn} {σe&g[p](c)} {Tfi | 1 i m, A |= fi} } otherwise.

The next result states that TΓ(N, A) can be considered, for all valid input-output relationships N under all assignments A, without losing unfounded sets.

Proposition 14 Let N be a valid input-output relationship, and let U be an unfounded set wrt. Π and A. If OA Γ,Π contains only conservative nogoods, then IΓ(U, ΓA Π, Π, A) is a solution to TΓ(N, A) (i.e., also nogoods TΓ(N, A) are conservative).

Hence, all valid input-output relationships for external atoms that are learned during the search for compatible sets can be reused (applying the above transformation) for the UFS check. Moreover, during the evaluation of external atoms in the postcheck for candidate unfounded sets (i.e., solutions to ΓA Π), further valid input-output relationships might be learned. They can in turn be used by (further) unfounded set checks (in transformed form) but also in the search for compatible sets.

Example 13 (Set Partitioning) For the program Π from Example 4, consider the compatible set ˆA = {Tdomain(a), Tsel(a), Te&diﬀ[nsel](a)}. Suppose the main search has learned the inputoutput relationship N = {Tdomain(a), Fnsel(a), Fe&diﬀ[nsel](a)}. Then the transformed nogood is a TΓ(N,A)={{Fdomain(a), Fe&diﬀ[nsel](a)}}; it intuitively encodes that if domain(a) is not in the unfounded set U, then e&diﬀ[nsel](a) is true under A . .U. This holds because e&diﬀ[nsel](a) is true under A and can only change its truth value if domain(a) becomes false.

This learning technique can be adopted for our encoding ΩΠ as follows.

Deﬁnition 11 (Nogood Transformation TΩ) For a valid input-output relationship N, the nogood transformation TΩis deﬁned as

TΩ(N) = {{σe&g[p](c)} {Tt1A, Ft1, . . . , Ttn A, Ftn, Ff1A . .U, . . . , Ffm A . .U}} .

Compared to TΓ(N, A), the main difference is that TΩ(N) is reusable for every assignment, similar to the deﬁnition of our unfounded set detection problem ΩΠ. The next result states that TΩ(N) can be considered, for all valid input-output relationships N under all assignments A, without losing unfounded sets.

Proposition 15 Let N be a valid input-output relationship, and let U be an unfounded set wrt. Π and A. If OΩ,Π contains only conservative nogoods, then IΩ(U, ΩΠ, Π, A) is a solution to TΩ(N) (i.e., also nogoods TΩ(N) are conservative).

Hence, also with encoding ΩΠ all valid input-output relationships for external atoms that are learned during the search for compatible sets can be reused and vice versa.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

Example 14 (cont d) Reconsider the program Π from Example 4 and the compatible set ˆA = {Tdomain(a), Tsel(a), Te&diﬀ[domain,nsel](a)}. Suppose the main search has learned the inputoutput relationship N = {Tdomain(a), Fnsel(a), Fe&diﬀ[domain,nsel](a)}. The transformed nogood is

TΩ(N)={{Tdomain(a)A, Fdomain(a), Fnsel(a)A . .U, Fe&diﬀ[domain,nsel](a)A . .U}} ;

it intuitively encodes that if domain(a) is true in the assignment A but not in the unfounded set U, and if nsel(a) is false in A . .U, then e&diﬀ[domain,nsel](a) is true under A . .U. This holds as e&diﬀ[domain,nsel](a) is true under A and can only change its truth value if domain(a) gets false.

The nogood exchange also beneﬁts from our advanced encoding. With our previous encoding ΓA Π, we needed to build the SAT instance from scratch for every unfounded set check. Thus, nogoods learned in the main search for compatible sets need to be transformed and added to the UFS detection problem for every check (otherwise they are lost). With our new encoding ΩΠ, this is done only once because learned nogoods are kept for multiple unfounded set checks. This also allows us to make use of advanced forgetting heuristics in SAT solvers more effective. Finally, an important note is that the optimizations presented in Section 4.1.2 and 4.1.3 can not be used simultaneously (differently from the optimizations in Section 4.1.1 and 4.1.2 resp. 4.1.1 and 4.1.3), as this can result in contradictions due to (transformed) learned nogoods. We thus disabled the optimization for avoiding guesses of replacement atoms (Section 4.1.2) in our experiments.

4.2 Learning Nogoods from Unfounded Sets

Until now we have considered merely detecting unfounded sets. A strategy to learn from detected unfounded sets for the main search for compatible sets is missing. We next develop such a strategy which we call unfounded set learning (UFL).

Example 15 Consider the program Π = { p &id[p](); x1 x2 xk }. As we know from Example 7, U = {p} is a UFS of the subprogram Π = { p &id[p]() } wrt. A = {Tp, Te&id()}. The same is true for Π and moreover for every A A; i.e., p must never be true.

The program in Example 15 has many compatible sets, and half of them (all where p is true) will fail the UFS check for the same reason. We thus develop a strategy for generating additional nogoods to guide the search for compatible sets in a way such that the same unfounded sets are not reconsidered. We present two such strategies, but will focus on the ﬁrst one because our experiments have shown that the ﬁrst one is superior for all our instances.

4.2.1 UFS-BASED LEARNING

For an unfounded set U of Π wrt. A we deﬁne a set L1(U, Π, A) of learned nogoods as follows. Suppose that r1, . . . , rj are all rules r in Π such that H(r) U = and U B+ o (r) = , i.e., the set of all external rules of Π wrt. U (rules which do not directly depend positively on U). Then

L1(U, Π, A) = {{σ0, σ1, . . . , σj} | σ0 {Ta | a U}, σi Hi for all 1 i j)} ,

where Hi = {Th | h H(ri) \ U, A |= h} {Fb | b B+ o (ri), A |= b}. Formally we can show that adding this set of nogoods is correct, i.e., does not prune answer sets:

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

Proposition 16 If U is an unfounded set of Π wrt. A, then every answer set of Π is a solution to the nogoods in L1(U, Π, A).

Example 16 Consider the program Π from Example 15 and suppose we have found the unfounded set U = {p} wrt. the interpretation A = {Tp, Tx1} {Fxi | 1 < i k}. Then the learned nogood L1(U, A, Π) = {Tp} immediately guides the search to the part of the search tree where p is false, i.e., roughly half of the guesses are avoided.

4.2.2 REDUCT-BASED LEARNING

A different learning strategy is based on the models of fΠA rather than the unfounded set U itself, hinging on the observation that for every unfounded set U, A . .U is a model of fΠA; hence U = refutes A as a minimal model of fΠA. This was noted by Faber (2005) for aggregates. We exploit this to construct nogoods from a nonempty U wrt. a model A as follows. The interpretation A . .U is not only a model of fΠA, but of all programs Π fΠA. Hence, if an assignment A falsiﬁes at least the rules of Π which A falsiﬁes, and A T (A . .U)T, then A

is not an answer set of Π. This yields the following nogood set L2(U, Π, A). Suppose r1, . . . , rn are all rules r of Π which are not in its FLP-reduct wrt. A (i.e., A |= B(ri). Then

L2(U, Π, A) = {{Ta | a (A . .U)T} {σ0, σ1, . . . , σn}

| σ0 {Ta | a U}, σi Hi for all 1 i n} ,

where Hi = {ta | a B(ˆr), ˆA |= a}, 1 i n. That is, each nogood consists of the true-part of the smaller model A . .U of the reduct fΠA, an unfounded atom σ0 (i.e. true in A but not in A . .U), and a false body literal σi (1 i n) for each rule of Π with unsatisﬁed body wrt. A.

Example 17 Let Π = {p &id[p](); q &id[q]()}, where &id[a]() evaluates to true iff a is true. Suppose A = {Tp, Tq}. Then U = {Tp, Tq} is an unfounded set wrt. A. In the above construction rule we have A . .U = {}, σ0 {Tp, Tq} and n = 0 (because both rule bodies are satisﬁed wrt. A). The learned nogoods are L2(U, Π, A) = {{Tp}, {Tq}}.

In Example 17, the learned nogoods will immediately guide the search to the interpretation {Fp, Fq}, which is the only one which becomes an answer set. Formally, we can show:

Proposition 17 If U is an unfounded set of Π wrt. A and A |= Π, then each answer set of Π is a solution to all nogoods in L2(U, Π, A).

However, L2(U, Π, A) appeared to be clearly inferior to L1(U, Π, A) from Section 4.2.1. Informally, its nogoods overﬁt the detected unfounded set and do not generalize well to other ones.

5. Deciding the Necessity of the Minimality Check

Although the minimality check based on unfounded sets is more efﬁcient than the explicit minimality check, the computational costs are still high. Moreover, during the evaluation of ˆΠ for computing the compatible set ˆA, the ASP solver has already made an unfounded set check, and we can safely assume that it is founded from the perspective of the ASP solver. Hence, all remaining unfounded sets which were not discovered by the ASP solver must involve external sources, as their behavior is not fully captured by the ASP solver.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

In this section we pursue these ideas and give a decision criterion for deciding whether a further UFS check is necessary. We eventually deﬁne a class of programs which needs no additional UFS check. Intuitively, we show that every unfounded set that is not already detected during the construction of ˆA contains input atoms of external atoms involved in cycles. If the program has no such input atom, then the UFS check is superﬂuous. Afterwards, we show how to apply this criterion, which holds in practically relevant cases, to program components; this often yields additional speedup. However, there are also cases where the UFS check can not be skipped; e.g., recursive URL retrieval from a web resource (which requires cyclic use of an external atom).

5.1 Basic Decision Criterion

We start with a deﬁnition of atom dependency.

Deﬁnition 12 (Atom Dependency) For a ground program Π, and ground atoms p(c) and q(d), we say that

(i) p(c) depends on q(d), denoted p(c) q(d), if for some rule r Π we have p(c) H(r) and q(d) B(r);

(ii) p(c) depends externally on q(d), denoted p(c) e q(d), if some rule r Π and external atom &g[q1, . . . , qn](e) B+(r) B (r) exist such that p(c) H(r) and q {q1, . . . , qn}.

In the following, we consider dependency graphs GR Π = (V, E) for a ground program Π, whose vertices V are the ground atoms and whose edges E are given by a binary relation R over ground atoms (E = R). We call p(c) q(d) also an ordinary edge and p(c) e q(d) an e-edge. We establish a lemma that allows us to restrict our attention to the core of an unfounded set, i.e., its most essential part; we can disregard atoms in a cut of GR Π, which is deﬁned as follows.

Deﬁnition 13 (Cut) Let U be an unfounded set of Π wrt. A. A set of atoms C U is a cut of GR Π, if

(i) b e a / GR Π, for all a C and b U (C has no incoming e-edge from U),

(ii) b a GR Π and a b GR Π, for all a C and b U \ C (there are no ordinary edges between C and U \ C).

We ﬁrst prove that cuts can be removed from unfounded sets and the resulting set is still an unfounded set.

Lemma 18 (Unfounded Set Reduction Lemma) Let U be an unfounded set of Π wrt. a complete assignment A, and let C be a cut of GR Π. Then, Y = U \ C is an unfounded set of Π wrt. A.

Example 18 Consider the following program:

Π = {r &id[r](); p &id[r](); p q; q p} .

Then we have p q, q p, r e r and p e r. Π has the unfounded set U = {p, q, r} wrt. A = {Tp, Tq, Tr}. Observe that C = {p, q} is a cut of GR Π, and therefore U \ C = {r} is an unfounded set of Π wrt. A.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

Next we prove that intuitively, for each unfounded set U of Π, either the input to some external atom is unfounded itself, or U is already detected when ˆΠ is evaluated.

Lemma 19 (EA-Input Unfoundedness) Let U be an unfounded set of Π wrt. an assignment A. If GR Π has no edge x e y such that x, y U, then U is an unfounded set of ˆΠ wrt. ˆA.

Example 19 Reconsider the program Π from Example 18. Then the unfounded set U = {p, q} wrt. A = {Tp, Tq, Fr} is already detected when

ˆΠ = { e&id[r]() ne&id[r]() ; r e&id[r](); p e&id[r](); p q; q p }

is evaluated by the ASP solver because no edges p e q and q e p exist. In contrast, the unfounded set U = {p, q, r} wrt. A = {Tp, Tq, Tr} is not detected by the ASP solver because p, r U and p e r.

Thus, the unfounded sets of Π wrt. A that are not recognized during the evaluation of ˆΠ have cyclic dependencies over input atoms of some external atom. Programs with acyclic dependencies do not need additional UFS checks. Recall that a cycle wrt. a binary relation R is a sequence C = c0, c1, . . . , cn, cn+1 of elements, n 0, such that (ci, ci+1) R for all 0 i n and c0 = cn+1. A set S contains a cycle wrt. R, if there is a cycle C = c0, c1, . . . , cn, cn+1 wrt. R such that ci S for all 0 i n + 1. Informally, the next proposition states that each unfounded set of Π wrt. A which contains no cycle through the input atoms to some external atom corresponds to some unfounded set of ˆΠ wrt. ˆA, i.e., the unfoundedness is already detected when ˆΠ is evaluated. Let d = e, where is the inverse of (i.e. = {(x, y) | (y, x) }). A cycle c0, c1, . . . , cn, cn+1 under d is called an e-cycle, if it contains an e-edge, i.e., ci e ci+1 for some 0 i n.

Theorem 20 (Relevance of e-cycles) Let U = be an unfounded set of Π wrt. an interpretation A which does not contain any e-cycle under d. Then ˆΠ has a nonempty unfounded set wrt. ˆA.

Corollary 21 If a program Π has no e-cycle under d and ˆΠ has no unfounded set wrt. an interpretation ˆA, then A is unfounded-free for Π.

This corollary can be used to increase the performance of an evaluation algorithm as follows: if there is no cycle under d containing e-edges, then an explicit unfounded set check is not necessary because the unfounded set check during the evaluation of ˆΠ is sufﬁcient. Note that this test can be done efﬁciently (in fact in linear time, similar to deciding stratiﬁability of an ordinary logic program). Moreover, in practice one can abstract from d by using analogous relations on the level of predicate symbols instead of atoms. Clearly, if there is no e-cycle in the predicate dependency graph, then there can also be no e-cycle in the atom dependency graph. Hence, the predicate dependency graph can be safely used to decide whether the unfounded set check can be skipped.

Example 20 All example programs so far need an UFS check, but the program Π = {out(X) &diﬀ[set1, set2](X)} F, where diﬀcomputes the set difference of unary predicates set1 and set2 and F is any set of facts, needs no UFS check as there is no e-cycle under d. Also the program Π = {str(Z) dom(Z), str(X), str(Y ), not &concat[X, Y ](Z)} (where &concat takes two constants and computes their string concatenation) needs no UFS check; there is a cycle over an external atom, but no e-cycle under d.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

Unfortunately, the converse of Theorem 20 does not hold, that is, ˆΠ may fail to be unfoundedfree wrt. ˆA but no unfounded set of Π wrt. A contains an e-cycle; thus, the condition in Corollary 21 is not necessary for unfounded-freeness of Π wrt. A. However, the following generalization of Theorem 20 allows us to conclude that if ˆΠ is unfounded-free wrt. ˆA, then every unfounded set U of Π wrt. A must contain an atom that provides input to an external atom on a cycle under d.

Deﬁnition 14 (Cyclic Input Atoms) For a program Π, an atom a is a cyclic input atom, if some edge b e a with a path from a to b under d exists.

Let CA(Π) denote the set of all cyclic input atoms of program Π.

Theorem 22 (Unfoundedness of Cyclic Input Atom) Let U = be an unfounded set of Π wrt. A such that U CA(Π) = . Then, ˆΠ has a nonempty unfounded set wrt. ˆA.

As a consequence of Theorem 22, we can add the nogood {Fa | a CA(Π)} to ΓA Π. Again using predicate symbols instead of atoms reduces the overhead of the dependency graph.

Example 21 Reconsider Π in Example 18. Then U = {p, q} is an unfounded set wrt. A = {Tp, Tq, Fr}; as U is disjoint from CA(Π) = {r}, it is detected during the evaluation of ˆΠ.

5.2 Program Decomposition

The usefulness of the decision criterion can be increased by decomposing the program into components, such that the criterion can be applied componentwise. This allows us to restrict the UFS check to components with e-cycles, while e-cycle-free components can be ignored. Let C be a partitioning of the ordinary atoms A(Π) of Π into subset-maximal strongly connected components under e. We deﬁne for each partition C C the subprogram ΠC associated with C as ΠC = {r Π | H(r) C = }. We next show that if a program has an unfounded set U wrt. A, then U C is an unfounded set wrt. A for the subprogram of some strongly connected component C.

Theorem 23 Let U = be an unfounded set of Π wrt. A. Then, for some C C it holds that U C is a nonempty unfounded set of ΠC wrt. A.

Note that constraints (i.e., rules with empty head) do not harm this proposition. Each constraint r of kind B(r) can be rewritten to p B(r), not p for a new atom p, and C = {p} is a strongly connected component with ΠC = {r}, which does not contain an e-cycle. Thus, for the rewritten constraints the according subprograms ΠC can be ignored anyways. This proposition states that a search for unfounded sets can be done independently for the subprograms ΠC for all C C. If there is an unfounded set of Π wrt. an assignment, then there is also an unfounded set of at least one program component wrt. this assignment. We know by Corollary 21 that programs Π without e-cycles can only contain unfounded sets that are already detected when ˆΠ is solved. If we apply Theorem 23 to the subprograms ΠC, we can safely ignore e-cycle-free program components.

Example 22 Reconsider the program Π from Example 18. Then C contains the components C1 = {p, q} and C2 = {r} and we have ΠC1 = {p &id[r](); p q; q p} and ΠC2 = {r &id[r]()}. By Theorem 23, each unfounded set of Π wrt. some assignment A gives rise to an

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

unfounded set of either ΠC1 or ΠC2. E.g., consider U = {p, q, r} and A = {Tp, Tq, Tr}; then U {r} = {r} is an unfounded set of ΠC2 wrt. A. As ΠC1 has no e-cycles, we conclude from Corollary 21 that all unfounded sets of ΠC1 are already detected when ˆΠ (resp., ˆΠC1) is evaluated. Hence, only ΠC2 needs an additional UFS check. Indeed, the only unfounded set of ˆΠ that is not detected when ˆΠ is evaluated is {r}, which is unfounded wrt. each interpretation A {Tr} for ΠC2 and Π.

Finally, we show that splitting, i.e., the component-wise check for foundedness, does not lead to spurious unfounded sets.

Proposition 24 If U is an unfounded set of ΠC wrt. A such that U C, then U is an unfounded set of Π wrt. A.

The results can be generalized to subprograms that are larger than strongly connected components; however, we leave a detailed study of this for future work.

6. Implementation and Evaluation

For implementing our technique, we integrated CLASP into our prototype system DLVHEX; we use

CLASP as an ASP solver for computing compatible sets and as a SAT solver for solving the nogood set of the UFS check. In our experiments, we will also use external behavior learning (EBL) as developed by Eiter et al. (2012a). The basic idea is to learn additional nogoods from evaluations of external atoms, which capture (parts of) the behavior of external sources. Thus, these nogoods eliminate model candidates which violate the known semantics of external atoms. Regarding a concrete setting, there is a large number of combinations of EBL and the techniques presented in this paper. Indeed, we may either activate or deactivate external behavior learning and use either the explicit or the UFS-based minimality check. In the latter case, we can further use unfounded set learning (UFL), the decision criterion for skipping the unfounded set check can be exploited or ignored, and program decomposition might be used or not. Moreover, we can choose between the encodings Γ and Ω. In total, these are 34 different settings. However, we will restrict our discussion to some interesting conﬁgurations. In general, we will activate the developed features stepwise such that in our tables the efﬁciency increases from left to right. We will start with the traditional algorithm based on an explicit minimality check without any learning techniques of Eiter et al. (2012a) and from this paper (i.e., only conﬂict-driven learning inside CLASP is used). In the next step we will add external behavior learning, while UFL is not possible with the explicit check. Then we switch from the explicit minimality check to the UFS-based check without learning and without exploiting the decision criterion and program decomposition. Nevertheless, this naive kind of UFS-based minimality checking is often more efﬁcient than the explicit minimality check with EBL. In the next step, we add the decision criterion and program decomposition. In the following, monolithic (mol) means that both the decision criterion and the program decomposition are off, and modular (mod) that they are on. Next we add EBL and UFL to the UFS-based minimality check, and ﬁnally we switch the encoding from Γ to Ω(including EBL, UFL and modular decomposition). However, we might skip some of the steps for speciﬁc benchmarks and argue why they are uninteresting in the respective cases. Detailed instance information and results with all combinations of parameters are available.2

2. http:/www.kr.tuwien.ac.at/research/projects/hexhex/ufs

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

Brieﬂy, our results show a clear improvement, for both synthetic and application instances, by the UFS check and EBL. Moreover, a closer analysis shows that the UFS check decreases in some cases not only the runtime but also the number of enumerated candidates (UFS resp. model candidates of the FLP reduct) and the number of external atom evaluations. We evaluated the implementation on a Linux server with two 12-core AMD 6176 SE CPUs with 128GB RAM running DLVHEX version 2.3.0. The evaluated techniques were conﬁgured using commandline arguments. To the best of our knowledge, DLVHEX is the only implementation of the

HEX semantics. In each test run the CPU usage was limited to two CPU cores, running a Condor load distribution system which ensures robust runtimes (i.e., multiple runs of the same instance have negligible deviations). The timeout was uniformly set to 300 seconds for each instance; for each parameter value, the average runtime over all instances is printed where timeouts, whose number is shown in parentheses, are fully taken into account.

6.1 Detailed Benchmark Description and Experimental Results

We give now a detailed description of the benchmarks used in our experiments, and present the results of our experimental evaluation.

6.1.1 SET PARTITIONING

This benchmark extends the program from Example 4 by the additional constraint

sel(X), sel(Y ), sel(Z), X = Y, X = Z, Y = Z

and varies the size of domain. The results are shown in Table 1. Here we see a big advantage of the UFS check over the explicit check, for both computing all answer sets and ﬁnding the ﬁrst one. A closer investigation shows that the improvement is mainly due to the optimizations in Section 4, which make the UFS check investigate signiﬁcantly fewer candidates than the explicit FLP check. Furthermore the UFS check requires fewer external computations. Both the explicit and the UFS-based minimality check beneﬁt from EBL if we compute all answer sets, but the results show that the UFS-based check beneﬁts more. In contrast, UFL (not shown in the table) does not lead to a further speedup as no unfounded sets are found in this program. The decision criterion and program decomposition improve the runtime slightly for small instances. However, for large instances the decision criterion cannot avoid the UFS check in most components of the program because of its cyclic structure. Thus a single UFS check over the whole program is replaced by multiple UFS checks over individual program components, which involves more overhead that becomes visible when computing all answer sets. If we compute only one answer set, then EBL turns out to be counter-productive. This is because learning is involved with additional overhead, while we cannot proﬁt much from the learned knowledge if we abort after the ﬁrst answer set, hence the costs exceed the beneﬁt. Using the encoding Ωinstead of Γ increases the efﬁciency in this case, because there is not only a large number of answer sets but also a large number of answer set candidates. Thus, a reusable encoding is very beneﬁcial, even if we compute only one answer set. Since in the evaluation of this program no unfounded sets are encountered, it is obvious that additional unfounded set checks over partial interpretations increase the overhead at no beneﬁt; hence we do not discuss respective results.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

all answer sets ﬁrst answer set explicit +EBL UFS Γ UFS Γ +EBL Ω explicit +EBL UFS Γ UFS Γ +EBL Ω mol mod mol mod

5 (1) 300.00 (1) 300.00 (1) 0.33 (0) 0.32 (0) 0.09 (0) 0.07 (0) 54.02 (0) 53.80 (0) 0.05 (0) 0.05 (0) 0.05 (0) 0.05 (0) 6 (1) 300.00 (1) 300.00 (1) 0.77 (0) 0.81 (0) 0.12 (0) 0.10 (0) 300.00 (1) 300.00 (1) 0.04 (0) 0.05 (0) 0.06 (0) 0.06 (0) 7 (1) 300.00 (1) 300.00 (1) 1.73 (0) 1.78 (0) 0.20 (0) 0.13 (0) 300.00 (1) 300.00 (1) 0.06 (0) 0.06 (0) 0.06 (0) 0.07 (0) 8 (1) 300.00 (1) 300.00 (1) 4.35 (0) 4.17 (0) 0.31 (0) 0.16 (0) 300.00 (1) 300.00 (1) 0.07 (0) 0.06 (0) 0.07 (0) 0.07 (0) 9 (1) 300.00 (1) 300.00 (1) 10.42 (0) 10.21 (0) 0.47 (0) 0.23 (0) 300.00 (1) 300.00 (1) 0.08 (0) 0.07 (0) 0.08 (0) 0.09 (0) 10 (1) 300.00 (1) 300.00 (1) 26.31 (0) 25.13 (0) 0.53 (0) 0.29 (0) 300.00 (1) 300.00 (1) 0.09 (0) 0.09 (0) 0.11 (0) 0.12 (0) 15 (1) 300.00 (1) 300.00 (1) 300.00 (1) 300.00 (1) 2.83 (0) 0.79 (0) 300.00 (1) 300.00 (1) 0.19 (0) 0.15 (0) 0.27 (0) 0.26 (0) 20 (1) 300.00 (1) 300.00 (1) 300.00 (1) 300.00 (1) 12.98 (0) 1.95 (0) 300.00 (1) 300.00 (1) 0.38 (0) 0.29 (0) 0.57 (0) 0.57 (0) 25 (1) 300.00 (1) 300.00 (1) 300.00 (1) 300.00 (1) 45.18 (0) 4.11 (0) 300.00 (1) 300.00 (1) 0.70 (0) 0.47 (0) 1.09 (0) 1.08 (0)

Table 1: Set Partitioning Benchmark Results

Note that the results are not comparable to those by Eiter et al. (2012a), because previous work focused on the computation of subset-minimal compatible sets and did not perform a minimality check wrt. the reduct, i.e., the semantics was different.

6.1.2 NONMONOTONIC MULTI-CONTEXT SYSTEMS

Nonmonotonic Multi-Context-Systems (MCSs) (Brewka & Eiter, 2007) are a generic formalism for aligning knowledge bases called contexts, which emerged from an approach by Ghidini and Giunchiglia (2001). The contexts are interlinked via bridge rules which enable belief exchange across contexts; the MCS semantics requires that local belief sets are compliant with the bridge rules. Such compliance can be impossible to achieve; that is, the MCS is inconsistent. To understand the reasons for the latter, Eiter et al. (2012b) deﬁned inconsistency explanations (IEs) for a MCS, which can be computed with a HEX-program encoding. This encoding is based on Saturation, which is a general technique for solving Σp 2 problems in disjunctive answer set programming (cf., Leone et al., 2006). Intuitively, a quantiﬁed Boolean formula (QBF) of the form X YΦ(X, Y) is evaluated using this technique as follows. Disjunctions are used to guess whether a variable v is true or false. A spoil atom is made true whenever Φ evaluates to true given truth assignments to X and Y. Finally whenever spoil is true, all literals over Y are set to true; this creates a unique assignment of the respective atoms. Given a guess on X, its unique spoil extension is an answer set if and only if all guesses of truth assignments Y make the spoil atom true and saturate the guess to become the unique extension this holds due to the minimality condition on answer sets of the reduct (see Deﬁnition 3). We use the HEX-encoding for computing IEs as a benchmark, as the saturation is rich in cycles through external atoms and disjunctive rule heads. External atoms in this benchmark evaluate semantics of contexts in the MCS (i.e., the local belief sets or models). We use random instances of different MCS topologies, i.e., connection graphs of contexts, created with our MCS benchmark generator.3 Note that the topologies are by their structure bound to certain system sizes (number of contexts), and that the difﬁculty of the instances varies among topologies; thus larger instances may have shorter runtimes. Our instances have up to 10 contexts, each consisting of a randomly generated consistent normal answer set program.

3. Described at http:/www.kr.tuwien.ac.at/research/systems/dmcs/experiments.html, online available at https:/dmcs. svn.sourceforge.net/svnroot/dmcs/dmcs/trunk

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

#ctx explicit +EBL UFS Γ UFS Γ +EBL +UFL Ω mol mod

3 (6) 4.78 (0) 3.97 (0) 2.96 (0) 2.97 (0) 1.65 (0) 0.08 (0) 0.08 (0) 4 (10) 51.90 (1) 45.91 (1) 48.71 (1) 48.59 (1) 23.48 (0) 0.10 (0) 0.11 (0) 5 (8) 149.53 (3) 137.95 (3) 150.80 (3) 150.64 (3) 94.45 (1) 0.10 (0) 0.12 (0) 6 (6) 159.41 (3) 154.69 (3) 157.62 (3) 157.72 (3) 151.89 (3) 0.12 (0) 0.15 (0) 7 (12) 231.23 (9) 227.45 (9) 234.74 (9) 234.63 (9) 216.75 (8) 0.17 (0) 0.20 (0) 8 (5) 244.39 (4) 204.92 (3) 246.42 (4) 246.34 (4) 190.60 (3) 0.17 (0) 0.21 (0) 9 (8) 300.00 (8) 278.44 (7) 300.00 (8) 300.00 (8) 264.65 (6) 0.22 (0) 0.24 (0) 10 (11) 300.00 (11) 268.78 (9) 300.00 (11) 300.00 (11) 247.16 (8) 0.25 (0) 0.31 (0)

Table 2: Consistent MCSs Benchmark Results

#ctx all answer sets explicit +EBL UFS Γ UFS Γ +EBL +UFL Ω mol mod

3 (9) 3.29 (0) 2.70 (0) 2.44 (0) 2.34 (0) 1.09 (0) 0.14 (0) 0.14 (0) 4 (14) 41.57 (1) 17.94 (0) 37.04 (1) 37.03 (1) 6.05 (0) 2.71 (0) 0.61 (0) 5 (11) 154.55 (5) 148.11 (5) 154.17 (5) 153.94 (5) 108.87 (2) 3.65 (0) 1.28 (0) 6 (18) 130.90 (7) 102.57 (6) 128.26 (7) 128.12 (7) 87.75 (4) 10.61 (0) 1.55 (0) 7 (13) 166.14 (5) 118.04 (5) 157.67 (5) 157.06 (5) 107.50 (4) 84.08 (2) 29.47 (0) 8 (6) 261.96 (5) 143.75 (2) 262.95 (5) 263.00 (5) 118.36 (2) 55.86 (1) 51.13 (1) 9 (14) 286.74 (13) 206.10 (9) 287.10 (12) 287.32 (12) 189.48 (8) 124.34 (5) 130.56 (6) 10 (12) 300.00 (12) 300.00 (12) 300.00 (12) 300.00 (12) 290.18 (11) 290.69 (11) 277.05 (11)

ﬁrst answer set #ctx explicit +EBL UFS Γ UFS Γ +EBL +UFL Ω mol mod

3 (9) 0.09 (0) 0.09 (0) 0.08 (0) 0.08 (0) 0.08 (0) 0.08 (0) 0.09 (0) 4 (14) 0.13 (0) 0.14 (0) 0.11 (0) 0.12 (0) 0.12 (0) 0.11 (0) 0.13 (0) 5 (11) 0.16 (0) 0.17 (0) 0.14 (0) 0.14 (0) 0.14 (0) 0.14 (0) 0.16 (0) 6 (18) 0.18 (0) 0.19 (0) 0.16 (0) 0.16 (0) 0.15 (0) 0.15 (0) 0.18 (0) 7 (13) 0.19 (0) 0.17 (0) 0.17 (0) 0.17 (0) 0.15 (0) 0.15 (0) 0.17 (0) 8 (6) 0.23 (0) 0.20 (0) 0.21 (0) 0.20 (0) 0.17 (0) 0.17 (0) 0.19 (0) 9 (14) 0.32 (0) 0.27 (0) 0.28 (0) 0.28 (0) 0.22 (0) 0.23 (0) 0.28 (0) 10 (12) 0.44 (0) 0.33 (0) 0.39 (0) 0.39 (0) 0.29 (0) 0.29 (0) 0.34 (0)

Table 3: Inconsistent MCSs Benchmark Results

The number of candidates for smaller models of the FLP reduct equals the number of unfounded set candidates as each unfounded set corresponds to a smaller model. However, as we stop the enumeration as soon as a smaller model respectively an unfounded set is found, the explicit and the UFS check may consider depending on the speciﬁc program and solver heuristics different numbers of interpretations. This explains why the UFS check is sometimes slightly slower than the explicit check. However, the delay between different UFS candidates was always smaller, which sometimes makes it faster even if it visits more candidates.

The results for consistent and inconsistent MCSs are shown in Table 2 and 3, respectively, where the number of instances of of each system size is given in parentheses. Intuitively, consistent and inconsistent MCSs are dual, as for each candidate the explicit resp. UFS check fails (i.e., stops early), vs. for some (or many) candidates the check succeeds (stops late). However, the mixed results do not permit us to draw solid conclusions on the computational relationship of the evaluation

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

methods. Nonetheless, we can see that the UFS check based on Ωwas often much faster than the explicit check (up to three orders of magnitude). As consistent MCSs have no IEs and hence no answer sets, we need not distinguish for them between computing one or all answer sets. The effects of external behavior learning (Eiter et al., 2012a) and of unfounded set learning are clearly evident in the MCS benchmarks, for both computing the ﬁrst and all answer sets. The UFS check proﬁts more from EBL than the explicit check, further adding to its advantage. By activating UFL (which is not possible in the explicit check) we gain another signiﬁcant speedup. We now discuss the effects of the syntactic decision criterion and program decomposition. Due to saturation, the encoding contains cycles where nearly all cycles in the HEX-program contain at least one external atom. Therefore, the decision criterion can reduce the set of atoms, for which the UFS check needs to be performed, only by the atoms that are deﬁned in the EDB. This does not yield signiﬁcant efﬁciency improvements. However, the benchmark results for MCS instances conﬁrm that the syntactic check is cheap and does not hurt performance. Over all 186 instances, the total runtime with decision criterion and program decomposition was 11,695 seconds compared to 11,702 seconds without, and the number of instance timeouts was the same. If we use encoding Ωinstead of Γ, we can observe another signiﬁcant speedup for computing all IEs of inconsistent MCSs. This is because there usually exist many answer sets (often thousands), and thus a reusable encoding is very beneﬁcial. In contrast, if we compute only the ﬁrst answer set or the MCS is consistent (no answer set exists), then the check with the more involved encoding Ω is slightly slower; its reusability does not pay off if we abort after the ﬁrst answer set. In summary, we can observe that the encoding Ωleads to a signiﬁcant performance gain over encoding Γ, while the decision criterion and decomposition do not help. In our next benchmark we will observe opposite effects.

6.1.3 ABSTRACT ARGUMENTATION

In this benchmark we compute ideal set extensions (Dung, Mancarella, & Toni, 2007) for randomly generated instances of abstract argumentation frameworks (AFs) (Dung, 1995) of different sizes. The problem of checking whether a given set of arguments is an ideal set of an AF is co-NPcomplete (Dunne, 2009). In this benchmark we use a HEX encoding that mirrors this complexity: it guesses such a set and checks its ideality using the Saturation technique involving an external atom (see Appendix A.1). Table 4 shows the results for different numbers of arguments, where each entry is the average of 30 benchmark instances. We compare the following conﬁgurations for both computing all and the ﬁrst answer set. In the ﬁrst column we do an explicit minimality check without learning techniques. The second column shows that learning (EBL) leads to almost the same runtime results. This can be explained by the structure of the encoding, which does not allow for effectively reusing learned nogoods. In the third column, we perform an UFS-based minimality check using our encoding Γ, but without applying the decision criterion and decomposition. We can observe that this is already a signiﬁcant improvements compared to the explicit minimality check, illustrating the effectiveness of our new approach. Similar as in the MCS benchmark, the number of reduct model candidates is equal to the number of UFS candidates in most cases, but the UFS check again enumerates its candidates faster; this explains the observed speedup.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

all answer sets explicit +EBL UFS Γ UFS Γ +EBL Ω mol mod +UFL

1 (30) 0.06 (0) 0.06 (0) 0.05 (0) 0.05 (0) 0.05 (0) 0.05 (0) 2 (30) 0.08 (0) 0.07 (0) 0.06 (0) 0.06 (0) 0.06 (0) 0.07 (0) 3 (30) 0.11 (0) 0.10 (0) 0.08 (0) 0.08 (0) 0.08 (0) 0.09 (0) 4 (30) 0.19 (0) 0.19 (0) 0.14 (0) 0.12 (0) 0.12 (0) 0.13 (0) 5 (30) 0.32 (0) 0.32 (0) 0.26 (0) 0.18 (0) 0.18 (0) 0.19 (0) 6 (30) 0.71 (0) 0.72 (0) 0.55 (0) 0.33 (0) 0.33 (0) 0.36 (0) 7 (30) 1.58 (0) 1.66 (0) 1.16 (0) 0.52 (0) 0.51 (0) 0.56 (0) 8 (30) 4.75 (0) 5.04 (0) 3.06 (0) 1.09 (0) 1.08 (0) 1.15 (0) 9 (30) 14.02 (0) 14.97 (0) 8.65 (0) 1.86 (0) 1.84 (0) 1.95 (0) 10 (30) 41.10 (0) 44.38 (0) 24.53 (0) 4.73 (0) 4.58 (0) 4.79 (0) 11 (30) 129.35 (1) 139.80 (2) 51.39 (0) 9.34 (0) 9.34 (0) 9.48 (0) 12 (30) 250.16 (12) 258.82 (17) 119.44 (0) 12.49 (0) 12.38 (0) 12.39 (0) 13 (30) 294.91 (27) 296.67 (27) 274.65 (19) 24.26 (0) 24.33 (0) 24.44 (0) 14 (30) 290.01 (29) 290.01 (29) 290.00 (29) 51.38 (3) 51.65 (3) 51.98 (3) 15 (30) 290.01 (29) 290.01 (29) 290.00 (29) 79.93 (3) 78.00 (3) 78.19 (3) 16 (30) 300.00 (30) 300.00 (30) 300.00 (30) 80.10 (4) 77.91 (4) 77.95 (4) 17 (30) 300.00 (30) 300.00 (30) 300.00 (30) 81.90 (5) 77.04 (5) 76.85 (5) 18 (30) 300.00 (30) 300.00 (30) 300.00 (30) 127.43 (8) 126.57 (8) 125.91 (8) 19 (30) 300.00 (30) 300.00 (30) 280.39 (28) 173.16 (13) 148.13 (10) 147.62 (10) 20 (30) 300.00 (30) 300.00 (30) 278.20 (27) 167.72 (12) 167.02 (12) 166.07 (12)

ﬁrst answer set explicit +EBL UFS Γ UFS Γ +EBL Ω mol mod +UFL

1 (30) 0.05 (0) 0.05 (0) 0.05 (0) 0.05 (0) 0.05 (0) 0.05 (0) 2 (30) 0.07 (0) 0.07 (0) 0.06 (0) 0.06 (0) 0.06 (0) 0.06 (0) 3 (30) 0.09 (0) 0.09 (0) 0.08 (0) 0.08 (0) 0.07 (0) 0.08 (0) 4 (30) 0.14 (0) 0.14 (0) 0.12 (0) 0.10 (0) 0.10 (0) 0.12 (0) 5 (30) 0.22 (0) 0.22 (0) 0.21 (0) 0.15 (0) 0.15 (0) 0.17 (0) 6 (30) 0.46 (0) 0.47 (0) 0.42 (0) 0.27 (0) 0.27 (0) 0.29 (0) 7 (30) 0.76 (0) 0.79 (0) 0.68 (0) 0.37 (0) 0.37 (0) 0.40 (0) 8 (30) 2.34 (0) 2.44 (0) 1.98 (0) 0.89 (0) 0.90 (0) 0.94 (0) 9 (30) 7.35 (0) 7.82 (0) 5.76 (0) 1.36 (0) 1.28 (0) 1.34 (0) 10 (30) 19.47 (0) 21.05 (0) 15.37 (0) 3.54 (0) 3.53 (0) 3.68 (0) 11 (30) 63.39 (1) 67.39 (1) 26.30 (0) 4.61 (0) 4.66 (0) 4.69 (0) 12 (30) 119.65 (4) 126.18 (4) 60.88 (0) 6.11 (0) 6.11 (0) 6.13 (0) 13 (30) 197.04 (14) 201.27 (15) 149.25 (3) 16.34 (0) 16.49 (0) 16.50 (0) 14 (30) 227.27 (22) 227.72 (22) 218.00 (17) 41.28 (2) 41.68 (2) 41.76 (2) 15 (30) 260.02 (26) 260.02 (26) 260.01 (26) 40.92 (2) 41.38 (2) 41.62 (2) 16 (30) 230.04 (23) 230.04 (23) 230.02 (23) 40.63 (3) 40.69 (3) 40.84 (3) 17 (30) 250.03 (25) 250.03 (25) 250.01 (25) 35.24 (2) 35.60 (2) 35.57 (2) 18 (30) 270.02 (27) 270.02 (27) 270.01 (27) 74.89 (5) 75.47 (5) 75.10 (5) 19 (30) 230.06 (23) 230.06 (23) 211.12 (21) 66.58 (4) 67.03 (4) 67.04 (4) 20 (30) 220.07 (22) 220.07 (22) 200.29 (20) 81.81 (5) 82.33 (5) 82.45 (5)

Table 4: Argumentation Benchmark Results

When we enable the decision criterion and program decomposition, we can observe a further speedup. This is because cycles in argumentation instances usually involve only small parts of the overall program; thus the UFS search can be signiﬁcantly simpliﬁed by excluding large program parts. We further have observed that program decomposition without the decision criterion is counter-productive (not shown in the table), because a single UFS search over the whole program is replaced by many UFS searches over program components (without the decision criterion, no such check is excluded). This incurs more overhead.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

In the ﬁfth column we enable EBL and UFL, which leads to a small speedup in some cases. However, as already mentioned above, no effective reuse of learned nogoods is possible.

Switching the encoding from Γ to Ωleads to a small speedup in some cases, but is also counterproductive in others. This is because the programs in this benchmark have usually only very few compatible sets, and only few unfounded set checks need to be performed. Hence the lower initialization overhead of the encoding Ωdoes not inﬂuence the runtime dramatically. On the other hand, the higher complexity of the encoding Ωincreases the runtime of small instances.

6.1.4 DEFAULT REASONING OVER DESCRIPTION LOGICS

A prominent instance of HEX-programs are DL-programs, which combine description logic ontologies with rules; they result by using a special external atom that is available as DL-plugin in

DLVHEX. Via DL-programs, we obtain an encoding of terminological default reasoning over description logic ontologies in the approach of Baader and Hollunder (1995) into HEX-programs, in which defaults require cyclic dependencies over external atoms. However, as all such dependencies involve default negated atoms, we have no cycles according to Deﬁnition 12, which respects only positive dependencies. Hence, the decision criterion comes to the conclusion that no UFS check is required.

We used variants of the benchmarks presented by Eiter et al. (2012a), which query wines from an ontology and classify them as red or white wines, where a wine is assumed to be white unless the ontology explicitly entails the opposite. In this scenario, the decision criterion eliminates all unfounded set checks. However, as there is only one compatible set per instance, there would be only one unfounded set check anyway, hence the speedup due to the decision criterion is not signiﬁcant. But the effect of the decision criterion can be increased by slightly modifying the scenario such that there are multiple compatible sets. This can be done, for instance, by nondeterministic default classiﬁcations, e.g., if a wine is not Italian, then it is either French or Spanish by default. Our experiments have shown that with a small number of compatible sets, the performance enhancement due to the decision criterion is marginal, but increases with larger numbers of compatible sets. For instance, for 243 compatible sets (and thus 243 unfounded set checks) we could observe a speedup from 13.59 to 12.19 seconds.

6.1.5 CONFORMANT PLANNING

In classical AI planning, a planning domain contains a description of actions with their preconditions and effects in the world. Finding a plan means to ﬁnd a sequence of actions that reaches from a given initial state a state fulﬁlling a given goal condition. Conformant planning (Goldman & Boddy, 1996; Smith & Weld, 1998) is the same problem but where the initial state is only partially speciﬁed and/or the domain is nondeterministic, such that by executing the plan we reach the goal regardless of the action outcomes and the actual initial state.

We here experimented on a very simple conformant planning domain: two robots with a limited sensor range patrol an area, in which is an object at an unknown initial location. The goal is to ﬁnd a sequence of movements of the two robots such that they detect the object in all cases. For experiments we used an encoding which realizes conformant planning using Saturation (see above) and contains an external atom for computing whether the patrol robots detect object (cf. Appendix A.2). In general, deciding the existence of a short (polynomial length bounded) conformant plan is Σp 3-

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

plan length

all answer sets

explicit UFS Γ UFS Γ +EBL +UFL Ω Ω mol mod -EBL-UFL +EBL+UFL

3 4 (10) 1 7.10 (0) 0.12 (0) 0.11 (0) 0.11 (0) 0.12 (0) 0.12 (0) 0.14 (0) 4 4 (10) 1 10.66 (0) 0.16 (0) 0.15 (0) 0.15 (0) 0.15 (0) 0.15 (0) 0.18 (0) 5 4 (10) 1 10.69 (0) 0.15 (0) 0.15 (0) 0.14 (0) 0.14 (0) 0.13 (0) 0.15 (0) 6 4 (10) 2 206.45 (2) 1.98 (0) 1.38 (0) 1.67 (0) 1.69 (0) 1.09 (0) 1.35 (0) 7 4 (10) 2 258.82 (5) 2.85 (0) 1.79 (0) 2.44 (0) 2.43 (0) 1.50 (0) 1.84 (0) 8 4 (10) 3 300.00 (10) 36.80 (0) 16.41 (0) 40.94 (0) 40.99 (0) 10.42 (0) 13.88 (0) 9 4 (10) 3 300.00 (10) 43.20 (0) 19.53 (0) 78.11 (0) 77.10 (0) 13.91 (0) 19.62 (0) 10 4 (10) 4 300.00 (10) 300.00 (10) 274.53 (5) 300.00 (10) 300.00 (10) 203.70 (2) 252.31 (5) 11 4 (10) 4 300.00 (10) 299.76 (9) 239.61 (5) 300.00 (10) 300.00 (10) 174.86 (2) 209.41 (3) 12 4 (10) 5 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 13 4 (10) 5 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 14 4 (10) 6 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 15 4 (10) 6 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 16 4 (10) 7 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10)

plan length

ﬁrst answer set

explicit UFS Γ UFS Γ +EBL +UFL Ω Ω mol mod -EBL-UFL +EBL+UFL

3 4 (10) 1 0.89 (0) 0.05 (0) 0.05 (0) 0.05 (0) 0.05 (0) 0.06 (0) 0.06 (0) 4 4 (10) 1 1.36 (0) 0.06 (0) 0.05 (0) 0.05 (0) 0.06 (0) 0.06 (0) 0.06 (0) 5 4 (10) 1 2.23 (0) 0.06 (0) 0.07 (0) 0.06 (0) 0.06 (0) 0.07 (0) 0.07 (0) 6 4 (10) 2 7.21 (0) 0.22 (0) 0.15 (0) 0.14 (0) 0.14 (0) 0.12 (0) 0.13 (0) 7 4 (10) 2 17.39 (0) 0.34 (0) 0.22 (0) 0.21 (0) 0.20 (0) 0.17 (0) 0.18 (0) 8 4 (10) 3 139.26 (1) 6.07 (0) 2.73 (0) 2.73 (0) 2.69 (0) 1.45 (0) 1.78 (0) 9 4 (10) 3 150.50 (3) 3.24 (0) 1.47 (0) 1.69 (0) 1.70 (0) 0.89 (0) 1.16 (0) 10 4 (10) 4 255.89 (7) 92.19 (2) 47.58 (0) 82.84 (2) 82.52 (2) 24.23 (0) 31.36 (0) 11 4 (10) 4 300.00 (10) 97.11 (2) 39.99 (0) 84.08 (1) 83.85 (1) 19.53 (0) 25.85 (0) 12 4 (10) 5 287.76 (9) 198.75 (5) 143.52 (4) 184.81 (5) 184.78 (5) 131.46 (4) 136.64 (4) 13 4 (10) 5 300.00 (10) 287.07 (9) 211.97 (5) 277.79 (9) 277.71 (9) 165.64 (4) 185.84 (4) 14 4 (10) 6 300.00 (10) 300.00 (10) 244.33 (7) 300.00 (10) 300.00 (10) 213.89 (5) 232.85 (6) 15 4 (10) 6 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 285.36 (9) 296.10 (9) 16 4 (10) 7 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10)

Table 5: Conformant Planning Benchmark Results

complete, see Turner (2002), but if action executability is decidable in polynomial time, the problem is in Σp 2; our example domain enjoys the property. Our results are displayed in Table 5, which shows averages over 10 instances per size. The instances consist of n 4 grids with n {3, . . . , 16}, the plan length required for ﬁnding a solution increases with larger instance sizes. (This is because the number of robots does not increase while the two robots must still cover the whole area.) Instances were generated by randomly placing robots in opposite quarters of the map. As expected we observe that the explicit FLP check performs worst, followed by the monolithic UFS check with Γ encoding, and the modular UFS Γ encoding; the UFS Ωencoding (without external behavior nor unfounded set learning) performs best. External behavior learning (EBL) and unfounded set learning (UFL) do not improve the performance, on the contrary it increases the run times signiﬁcantly for the modular UFS Γ check and slightly for the Ωcheck. EBL does not change times signiﬁcantly for the explicit check, therefore we omit results for explicit +EBL. By looking into proﬁling information and at the domain we found the reasons: (a) the external atoms depend on a large part of the interpretation (locations of all robots) so EBL cannot cut away

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

signiﬁcant portions of the search space; (b) evaluating the external atom takes a negligible amount of time, so beneﬁcial effects of EBL will be outweighed by is computational overhead. For UFL we observed that the benchmark instances contain only few unfounded sets (pruning less than half of the answer set candidates) and thus UFL cannot improve performance given the overhead it incurs. We conclude that in some scenarios, using EBL and UFL can reduce efﬁciency. As in the Ωcheck the UFS check encoding is constructed only once, the overhead for EBL and UFL observed with the Γ encoding no longer has such a big impact. Nevertheless Ωwithout learning slightly outperforms Ωwith UFL and EBL. An analysis of the number of UFS checks and the number of external atom evaluations (not shown in table) revealed that UFL and EBL decreases (i) the number of unfounded set checks needed and (ii) the number of external atoms evaluated (in one 9 4 instance, from 5132 to 3341). Thus if external computations would be more costly, the positive effects of UFL and EBL on Ωwould outweigh their computational overhead and it would be beneﬁcial to activate UFL and EBL in this domain. Interestingly, for small map sizes we see that with the Ωencoding, the 3 4 instances actually seem to be harder to solve than the larger 4 4 and 5 4 instances. This is because all these instances require plan length 1 to ﬁnd a solution; so the larger instances are more constrained than the smaller instances because there robots have less freedom to move around while still detecting all objects. Hence, for 5 4 maps the solver ﬁnds solutions faster than for 4 4 maps. The conclusion from this benchmark is that depending on the computational task in external atoms, UFL and EBL can be beneﬁcial or harmful for efﬁciency of reasoning.

6.2 Summary

Our experiments have shown that the learning technique EBL developed by Eiter et al. (2012a) and the techniques introduced in this paper lead to signiﬁcant performance improvements in most cases, with few exceptions for speciﬁc benchmarks. The effects of external behavior learning (EBL) are clearly evident both for the explicit minimality check and for the unfounded set-based check, but are even more prominent with the latter. Independently of whether EBL is used or not, unfounded set checking pushes the efﬁciency of HEX-program evaluation compared to explicit minimality checking. Moreover, it allows for learning of additional nogoods, which is also advantageous in most of our benchmarks. Regarding the two problem encodings, the benchmarks show that the UFS check is usually faster with the Ωencoding than with the Γ encoding, however the former UFS check involves more initialization overhead, which might be counterproductive for small programs. The decision criterion may lead to an additional speedup and does not introduce notable overhead, thus it can always be activated. Finally, program decomposition often leads to an additional performance gain, but should only be used in combination with the decision criterion because otherwise a single UFS check is replaced by multiple UFS checks, which involves more overhead.

7. Discussion

We now discuss related work and outline some possible starting points for extensions.

7.1 Related Work

Constraint answer set solving (Gebser, Ostrowski, & Schaub, 2009) can be seen as a special case of HEX-programs. It extends ASP by dedicated constraint atoms in rule bodies (comparisons of

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

numeric constraint variables) that allow for a bidirectional exchange of information between the logic program and the constraint solver. While the constraint solver is a concrete instance of an external source, HEX-programs support arbitrary external sources. The idea of external behavior learning (EBL), introduced by Eiter et al. (2012a) is further related to the work of Drescher and Walsh (2012) since both approaches generate nogoods on-the-ﬂy. Besides grounding, one of the main differences between ASP and SAT solving is foundedness, i.e., the truth of each atom in an answer set is justiﬁed by a non-circular derivation from rules and facts. To account for circularity, the notion of unfounded set has been introduced by van Gelder et al. (1991) for deﬁning the well-founded semantics of logic programs with negation, by constructing the least ﬁxpoint of a monotone operator on partial assignments; the total ﬁxpoints of this operator correspond to the stable models of the logic program. This actually allows to give a characterization of the stable models in terms of unfounded sets. In fact, unfounded set checking turned out to be a fruitful model-based approach in ASP solving, which has an equally successful syntactic counterpart known as loop formulas (Lin & Zhao, 2004; Lee & Lifschitz, 2003; Lee, 2005). Different kinds of unfounded set checks with different complexities have been developed for various program classes. The computation of answer sets by a model generate and test approach, which is pursued by many ASP solvers, requires that a form of minimality check or unfounded set check is carried out already for ordinary logic programs (i.e., in absence of external atoms). However, for normal program this test is tractable and it is frequently realized using source pointers (Simons et al., 2002). Intuitively, the reasoner stores for each atom a pointer to a rule which possibly supports this atom. The list of source pointers is updated during propagation. If at some point there is no supporting rule for an atom, then it can conclude that this atom must be false. In the context of ASP, the notion of unfounded set has been explicitly formulated and extended to disjunctive logic programs by Leone et al. (1997), who proved that the stable models of a disjunctive logic program are its models that are unfounded-free. This results was the basis for the architecture of the DLV solver, which generates answer set candidates that are checked for unfounded-freeness. This test, which like answer set checking for disjunctive answer set programs, is co-NP-complete (Faber, 2005), has been reduced by Koch et al. (2003) to unsatisﬁability testing of a SAT instance. This approach has been later extended to conﬂict-driven learning and unfounded set checking by Drescher et al. (2008), where two instances for the CLASP solver, an ASP instance and a SAT instance, are used to generate and check answer set candidates, respectively. In parallel to our work, this technique was recently reﬁned by exploiting assumptions such that the encoding of the unfounded set search does not need to be adopted to the current assignment (Gebser, Kaufmann, & Schaub, 2013). This is related to our uniform encoding of the unfounded set search, but still restricted to disjunctive ASP without external sources. For HEX-programs, the unfounded set search needs to respect the semantics of external atoms and is thus a more general problem. Alviano, Calimeri, Faber, Leone, and Perri (2011) consider normal logic programs with monotone and antimonotone aggregate atoms, and deﬁned unfounded sets for such programs. Based on this, they extended the well-founded semantics of Van Gelder et al. (1991), which although closely related is weaker than the general FLP semantics (Faber et al., 2011). We now considered unfounded set checking in the presence of external sources and for FLP answer sets, for which the results by Drescher et al. (2008) do not immediately carry over. Indeed, already for ground Horn programs, the presence of nonmonotonic external atoms that are decidable in polynomial time makes unfoundedness checking intractable (more precisely, co-NP-complete), such that deciding the existence of an FLP answer set is a Σp 2-complete problem in the ground case.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

For computationally harder external atoms, the complexity may increase relative to an oracle for the external function (see Faber, 2005). However, the results from this paper do still apply in such cases. Drescher et al. (2008) employed also a splitting technique, which goes back to the work of Leone et al. (1997); it is related to our program decomposition, but works for ASP programs without external sources only. Note that our notion of splitting is different from the well-known splitting sets by Lifschitz and Turner (1994), as we consider only positive dependencies for ordinary atoms. While we consider e-cycles, which are speciﬁc for HEX-programs, the interest of Drescher et al. (2008) was with head-cycles, which may arise with disjunctive rule heads. In fact, our approach may be regarded as an extension of the one of Drescher et al., since the evaluation of ˆΠ follows their principles of performing UFS checks in case of head-cycles. For the evaluation of the FLP semantics, an unfounded set check or explicit FLP check is instrumental. we just mention that other semantics of HEX-programs may not involve such a step which is intractable in general (as follows from Leone et al., 2006, already for ground Horn programs with nonmonotonic external atoms that are decidable in polynomial time). For instance, Shen (2011) and Shen and Wang (2011) present a well-justiﬁed semantics where unfounded set checking is essentially replaced by a ﬁxpoint iteration which, intuitively, tests if a model candidate reproduces itself but excludes circular justiﬁcations. However, the complexity of answer set computation does not decrease by this approach in general, and in particular deciding well-justiﬁed answer set existence for ground Horn programs with nonmonotonic external atoms that are decidable in polynomial time is Σp 2-complete, and thus as hard as deciding the existence of answer sets as in Deﬁnition 3.

7.2 Extensions

We have designed our unfounded set check as a postcondition test; that is like the explicit FLP check, it is carried out only after a complete assignment has been generated as an answer set candidate. However, in certain cases it might be obvious that a partial interpretation (in which some truth values are open) can be extended to an answer set, because the existence of an unfounded set is guaranteed for any extension to a complete assignment. One can then backtrack earlier, which intuitively leads to a saving for certain classes of instances. Exploring this idea, we have generalized our framework with a control component which decides, based on a heuristics, when an unfounded set check is carried out; in the standard setting, this is whenever an assignment in the model generation is complete (i.e., a complete assignment is given). A UFS check on partial assignments, that is sound with respect to any extension to a complete assignment, is possible if the ASP solver has ﬁnished unit propagation over a maximal subset of the program such that the interpretation is already complete on it, and all guessed values of external atom replacements are correct. We thus used this criterion, which is easy to test, for a greedy heuristics to issue UFS checks in our prototype system. However, in contrast to our initial expectation, we found that for all our benchmarks the UFS check wrt. partial assignments was not productive. A closer look reveals that this is essentially because nogood learning from unfounded sets (UFL) effectively avoids the reconstruction of the same unfounded set anyway. It therefore rarely happens that UFS checking wrt. a partial interpretation identiﬁes an unfounded set earlier than UFS checking wrt. complete interpretations. Therefore, we believe that UFS checking wrt. a partial interpretation rarely identiﬁes an unfounded set earlier than UFS checking wrt. complete assignments. As UFS checking for HEX-programs involves the evalu-

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

all answer sets ﬁrst answer set Ω Ωpartial (periodic) Ωpartial (max) Ω Ωpartial (periodic) Ωpartial (max) +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL

5 (1) 0.07 (0) 0.09 (0) 0.11 (0) 0.05 (0) 0.06 (0) 0.07 (0) 6 (1) 0.10 (0) 0.13 (0) 0.15 (0) 0.06 (0) 0.07 (0) 0.09 (0) 7 (1) 0.13 (0) 0.15 (0) 0.19 (0) 0.07 (0) 0.08 (0) 0.11 (0) 8 (1) 0.18 (0) 0.20 (0) 0.26 (0) 0.08 (0) 0.10 (0) 0.14 (0) 9 (1) 0.24 (0) 0.26 (0) 0.35 (0) 0.09 (0) 0.12 (0) 0.17 (0) 10 (1) 0.29 (0) 0.33 (0) 0.47 (0) 0.11 (0) 0.14 (0) 0.21 (0) 15 (1) 0.80 (0) 0.96 (0) 1.61 (0) 0.24 (0) 0.38 (0) 0.73 (0) 20 (1) 1.96 (0) 2.46 (0) 4.92 (0) 0.51 (0) 0.97 (0) 2.30 (0) 25 (1) 4.15 (0) 5.52 (0) 11.25 (0) 0.97 (0) 1.98 (0) 4.50 (0)

Table 6: Set Partitioning with UFS Checking over Partial Assignments

Ω Ωpartial (periodically) Ωpartial (max) +EBL+UFL +EBL+UFL +EBL+UFL

3 (6) 0.08 (0) 0.09 (0) 0.10 (0) 4 (10) 0.11 (0) 0.11 (0) 0.12 (0) 5 (8) 0.12 (0) 0.12 (0) 0.13 (0) 6 (6) 0.15 (0) 0.15 (0) 0.16 (0) 7 (12) 0.20 (0) 0.20 (0) 0.21 (0) 8 (5) 0.21 (0) 0.21 (0) 0.22 (0) 9 (8) 0.24 (0) 0.24 (0) 0.27 (0) 10 (11) 0.31 (0) 0.31 (0) 0.32 (0)

Table 7: Consistent MCSs Benchmark Results with UFS Checking over Partial Assignments

all answer sets ﬁrst answer set Ω Ωpartial (periodic) Ωpartial (max) Ω Ωpartial (periodic) Ωpartial (max) +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL

3 (9) 0.14 (0) 0.13 (0) 0.16 (0) 0.09 (0) 0.09 (0) 0.10 (0) 4 (14) 0.61 (0) 0.64 (0) 0.88 (0) 0.13 (0) 0.13 (0) 0.14 (0) 5 (11) 1.28 (0) 1.36 (0) 1.81 (0) 0.16 (0) 0.16 (0) 0.17 (0) 6 (18) 1.55 (0) 1.67 (0) 2.49 (0) 0.18 (0) 0.18 (0) 0.18 (0) 7 (13) 29.47 (0) 31.54 (0) 44.90 (1) 0.17 (0) 0.17 (0) 0.18 (0) 8 (6) 51.13 (1) 51.22 (1) 51.66 (1) 0.19 (0) 0.20 (0) 0.21 (0) 9 (14) 130.56 (6) 130.99 (6) 133.84 (6) 0.28 (0) 0.27 (0) 0.28 (0) 10 (12) 277.05 (11) 277.20 (11) 278.21 (11) 0.34 (0) 0.35 (0) 0.36 (0)

Table 8: Inconsistent MCSs Benchmark Results with UFS Checking over Partial Assignments

ation of external sources and compatibility testing, this easily leads to costs that are higher than the potential savings. A more detailed analysis requires further studies; since the results do not seem to be promising, we leave this for possible future work.

Table 6 10 show the benchmark results if UFS checking wrt. partial assignments is enabled when computing all or the ﬁrst answer set only.

The ﬁrst column shows the runtime with UFS checking wrt. complete interpretations only, using encoding Ω, EBL and UFL (equivalent to the last column in the tables in Section 6). The second column shows the results with UFS checking wrt. partial assignments, using a heuristics which performs the UFS check periodically (periodic). The third column shows the runtimes if the UFS check is always performed, if no other propagation technique can derive further truth values (max).

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

all answer sets ﬁrst answer set Ω Ωpartial (periodic) Ωpartial (max) Ω Ωpartial (periodic) Ωpartial (max) +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL

1 (30) 0.05 (0) 0.05 (0) 0.05 (0) 0.05 (0) 0.05 (0) 0.05 (0) 2 (30) 0.07 (0) 0.06 (0) 0.07 (0) 0.06 (0) 0.07 (0) 0.07 (0) 3 (30) 0.09 (0) 0.09 (0) 0.10 (0) 0.08 (0) 0.08 (0) 0.09 (0) 4 (30) 0.13 (0) 0.14 (0) 0.16 (0) 0.12 (0) 0.12 (0) 0.14 (0) 5 (30) 0.19 (0) 0.20 (0) 0.22 (0) 0.17 (0) 0.16 (0) 0.18 (0) 6 (30) 0.36 (0) 0.36 (0) 0.39 (0) 0.29 (0) 0.29 (0) 0.31 (0) 7 (30) 0.56 (0) 0.56 (0) 0.59 (0) 0.40 (0) 0.40 (0) 0.42 (0) 8 (30) 1.15 (0) 1.15 (0) 1.19 (0) 0.94 (0) 0.94 (0) 0.96 (0) 9 (30) 1.95 (0) 1.94 (0) 2.01 (0) 1.34 (0) 1.35 (0) 1.39 (0) 10 (30) 4.79 (0) 4.80 (0) 4.96 (0) 3.68 (0) 3.67 (0) 3.75 (0) 11 (30) 9.48 (0) 9.49 (0) 9.71 (0) 4.69 (0) 4.71 (0) 4.74 (0) 12 (30) 12.39 (0) 12.42 (0) 12.79 (0) 6.13 (0) 6.11 (0) 6.23 (0) 13 (30) 24.44 (0) 24.45 (0) 25.32 (0) 16.50 (0) 16.46 (0) 16.80 (0) 14 (30) 51.98 (3) 52.03 (3) 52.57 (3) 41.76 (2) 41.80 (3) 41.98 (3) 15 (30) 78.19 (3) 78.14 (3) 79.81 (3) 41.62 (2) 41.53 (2) 42.02 (2) 16 (30) 77.95 (4) 77.99 (4) 79.52 (4) 40.84 (3) 40.79 (3) 41.04 (3) 17 (30) 76.85 (5) 76.86 (5) 77.82 (5) 35.57 (2) 35.53 (2) 35.58 (2) 18 (30) 125.91 (8) 126.17 (8) 128.83 (8) 75.10 (5) 75.32 (5) 75.37 (5) 19 (30) 147.62 (10) 147.51 (10) 149.62 (10) 67.04 (4) 66.88 (4) 67.59 (4) 20 (30) 166.07 (12) 165.96 (12) 168.53 (12) 82.45 (5) 82.27 (5) 82.90 (5)

Table 9: Argumentation with UFS Checking over Partial Assignments

It can be observed that UFS checking wrt. partial assignments does not lead to a further speedup in any case. Quite the contrary, some instances have signiﬁcantly higher runtimes with more frequent unfounded set checks. This is best visible in the set partitioning benchmark (Table 6), when computing all explanations for inconsistent MCSs with 5, 6 or 7 contexts (Table 9), and when computing all answer sets in the conformant planning benchmark (Table 10). In the set partitioning benchmark the effects are especially signiﬁcant, which is as expected because every compatible set is unfounded-free. Thus, additional UFS checks are always counterproductive. In the consistent multi-context systems, reasoning is fast anyway, thus the frequency of UFS checking has no significant impact (Table 7). In the argumentation benchmark we can also observe a slight slowdown by more frequent UFS checking, although it is less dramatic than in the other benchmarks because the other propagation methods are applicable more frequently and thus fewer UFS checks are performed even with setting max (Table 9). On the other hand, for ASP solving (where no such extra costs incur), UFS checks over partial interpretations may still be beneﬁcial, as reported by Gebser et al. (2013). In conclusion, UFS checks on partial assignments of HEX-programs will require tailored heuristics that not only take the structure of the program, but also domain-speciﬁc knowledge into account, which remains for future work.

8. Conclusion

HEX-programs are an expressive extension of non-monotonic logic programs with access to external information via external atoms; supported by a plugin architecture they can be fruitfully deployed for a range of applications. External atoms however make the efﬁcient evaluation of HEX-programs a challenging task, and in particular to compute answer sets of a HEX-program Π, which are the models A of Π that are subset-minimal models of its FLP-reduct fΠA (which keeps all rules whose

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

all answer sets ﬁrst answer set ΩΩpartial (periodic) Ωpartial (max) ΩΩpartial (periodic) Ωpartial (max) +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL +EBL+UFL

3 4 (10) 1 0.14 (0) 0.14 (0) 0.16 (0) 0.06 (0) 0.06 (0) 0.08 (0) 4 4 (10) 1 0.18 (0) 0.17 (0) 0.20 (0) 0.06 (0) 0.06 (0) 0.08 (0) 5 4 (10) 1 0.15 (0) 0.15 (0) 0.18 (0) 0.07 (0) 0.07 (0) 0.09 (0) 6 4 (10) 2 1.35 (0) 1.35 (0) 1.48 (0) 0.13 (0) 0.13 (0) 0.15 (0) 7 4 (10) 2 1.84 (0) 1.83 (0) 2.03 (0) 0.18 (0) 0.18 (0) 0.21 (0) 8 4 (10) 3 13.88 (0) 14.23 (0) 17.27 (0) 1.78 (0) 1.86 (0) 2.36 (0) 9 4 (10) 3 19.62 (0) 19.96 (0) 23.75 (0) 1.16 (0) 1.18 (0) 1.42 (0) 10 4 (10) 4 252.31 (5) 257.18 (5) 289.20 (7) 31.36 (0) 33.40 (0) 49.36 (0) 11 4 (10) 4 209.41 (3) 214.72 (3) 244.84 (5) 25.85 (0) 27.15 (0) 37.64 (0) 12 4 (10) 5 300.00 (10) 300.00 (10) 300.00 (10) 136.64 (4) 137.22 (4) 142.74 (4) 13 4 (10) 5 300.00 (10) 300.00 (10) 300.00 (10) 185.84 (4) 188.73 (4) 209.44 (4) 14 4 (10) 6 300.00 (10) 300.00 (10) 300.00 (10) 232.85 (6) 235.06 (7) 243.73 (7) 15 4 (10) 6 300.00 (10) 300.00 (10) 300.00 (10) 296.10 (9) 297.42 (9) 300.00 (10) 16 4 (10) 7 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10) 300.00 (10)

Table 10: Conformant Planning with UFS Checking over Partial Assignments

bodies are satisﬁed). To improve on this expensive test (which was customary in implementations so far), we have presented an alternative test based on unfounded sets that we obtain by adapting the notion of unfounded set for aggregates by Faber (2005) to external atoms. Also Alviano et al. (2011) use a related notion of unfounded sets for programs with aggregates, but restrict the discussion to monotonic and antimonotonic aggregates. We have realized unfounded set (UFS) checking by a transformation to SAT solving, where the satisfying assignments of a constructed CNF generate candidate unfounded sets, which in turn are subject to a (rather simple) postcheck that takes external atom evaluation into account.

In particular, we have provided two SAT encodings for UFS checking: the conceptually simple encoding ΓA Π, which needs initialization for every UFS check, and the advanced encoding ΩΠ, which can be reused for all UFS checks. To further boost performance, we have shown how to learn from unfounded sets by deriving nogoods, i.e., constraints (possibly involving also external atoms) which guide future search in model generation and help to avoid that unfounded sets are regenerated. In further elaboration, we have reﬁned the basic approach by suitable program splitting, such that the UFS check can be carried out independently on program components, cutting down the complexity. Furthermore, we have presented a syntactic criterion that allows us to decide efﬁciently whether the UFS check can be safely skipped for a component or the whole program, exploiting that the answer set candidates from the model search have only special unfounded sets that involve cyclic input to external atoms; for HEX-programs in simple applications, this is usually not the case.

The experimental evaluation of our new approach, which considered different combinations of the techniques and comprised problems from various domains including multi-context systems, abstract argumentation, default reasoning over ontologies, and conformant planning, where HEXprograms serve for easy-cut declarative problem solving, has shown that it is more efﬁcient than the traditional minimal model check; it can lead to exponential gains and yields often drastic performance improvements, while it is not slower (except in very few cases by a marginal amount). Furthermore, the reusable encoding ΩΠ turned out to be beneﬁcial for programs that require many unfounded set checks, which includes all programs that have many answer sets.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

8.1 Future work

An issue for further improvement of the approach in this paper are other heuristics for UFS checking over partial assignments. While the natural heuristics that we considered are counterproductive, others might lead to additional speedup in some cases. However, this may require to incorporate domain-speciﬁc knowledge about external atoms; currently this is only done in the learning algorithms but not in the heuristics. In the same line, one might consider developing a heuristics for dynamically choosing between the UFS search encodings that we presented, and to study heuristics for guiding the unfounded set search, i.e., for variable selection by the SAT solver. Currently, our implementation applies the same heuristics for the unfounded set search as in the model generation process. However, our experimental comparison with the explicit minimality check in terms of the considered candidate sets suggests that there is room for improvement by employing suitable choices. Developing appropriate heuristics and validating their effectiveness on candidate set enumeration remains to be explored. Finally, an obvious issue are other criteria that allow to skip the UFS check or simplify it while they can be efﬁciently tested.

Acknowledgments

Preliminary results of this work have been presented at the 13th European Conference on Logics in Artiﬁcial Intelligence (JELIA 2012), September 26-28, 2012, Toulouse, France (Eiter, Fink, Krennwallner, Redl, & Sch uller, 2012c), and the 5th Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2012), September 4, 2012, Budapest, Hungary (Eiter, Fink, Krennwallner, Redl, & Sch uller, 2012b). We are grateful to the anonymous reviewers for their helpful and constructive comments. This work was supported by the Austrian Science Fund (FWF) via the projects P20840, P20841, P24090, and by the Vienna Science and Technology Fund (WWTF) project ICT08-020. Peter Sch uller was supported by TUBITAK Fellowship 2216.

Appendix A. Benchmark Encodings

In this appendix, we give details to some of the benchmark encodings (those which are not described in the references). We note that these encodings have not been developed and tuned for good performance and serve merely for an experimental comparison of the various FLP check realizations. Benchmark encodings and HEX-plugins are publicly available at https:/github.com/ hexhex/benchmarks.

A.1 Abstract Argumentation

The Abstract Argumentation benchmark results in Section 6.1 were obtained using the following encoding, which is derived from encodings for admissible and preferred set extensions of an argumentation framework (A, att) described by Egly, Gaggl, and Woltran (2010). Input instances of this benchmark are deﬁned over a set A of arguments encoded as facts arg(a) for each a A and a set att of attacks between arguments, encoded as facts att(a, b) for some (a, b) A A. The encoding consists of the following rules where x, y, z A; very similar encodings are explained in detail by Egly et al. (2010) (but without the use of external atoms). We deﬁne defeat from attacks.

defeat(x, y) att(x, y).

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

We guess a set S A using predicates in S and out S.

in S(x) not out S(x), arg(x). out S(x) not in S(x), arg(x).

We require that all arguments in S are conﬂict-free and defended from S.

in S(x), in S(y), defeat(x, y).

defeated(x) in S(y), defeat(y, x).

not Defended(x) defeat(y, x), not defeated(y).

in S(x), not Defended(x).

For saturation we deﬁne a linear order on arguments, including inﬁmum and supremum.

lt(x, y) arg(x), arg(y). (x < y)

nsucc(x, z) lt(x, y), lt(y, z).

succ(x, y) lt(x, y), not nsucc(x, y).

ninf (x) lt(y, x). nsup(x) lt(x, y).

inf (x) not ninf (x), arg(x). sup(x) not nsup(x), arg(x).

We perform a guess over a set T A using a disjunction.

in T(x) out T(x) arg(x).

We check each argument of T whether it is in S and spoil the answer set if S T.

s In T upto(y) inf (y), in S(y), in T(y).

s In T upto(y) inf (y), out S(y).

s In T upto(y) succ(z, y), in S(y), in T(y), s In T upto(z).

s In T upto(y) succ(z, y), out S(y), s In T upto(z).

s In T sup(y), s In T upto(y).

spoil s In T.

We also spoil the answer set if T is not a preferred extension, determined by an external atom with the semantic function f&arg Sem Ext such that f&arg Sem Ext(A, pref , arg, att, in T, unused, spoil) = 1 iff Fspoil A or the extension of predicate in T is a preferred set extension of the argumentation framework speciﬁed by the extension of predicates arg and att. Internally, the external atom uses another ASP program to compute the semantics. This check is performed using an ASP encoding for preferred extensions from Egly et al. (2010).

t Is Not Pref &arg Sem Ext[pref , arg, att, in T, unused, spoil]().

spoil t Is Not Pref .

Note that the parameters pref and unused support more general functionalities of f&arg Sem Ext which are not relevant for this benchmark. We create a unique answer set whenever spoil is true and require that only spoiled answer sets are returned.

in T(x) spoil, arg(x). out T(x) spoil, arg(x).

s In T spoil. t Is Not Pref spoil. not spoil.

Given an instance encoded as above, an answer set to the above program exists iff there exists an ideal set extension of the given argumentation framework.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

A.2 Conformant Planning

The Conformant Planning benchmark results in Section 6.1 were obtained using the following encoding. Input instances of this benchmark are deﬁned over a set R of robots, sets X and Y of valid x and y coordinates of the environment, and a maximum plan length l; an instance contains for each robot r R the initial position (x, y) as facts robo X(r, x, 0) and robo Y (r, y, 0). The encoding consists of the following rules where, unless stated otherwise, 0 t < l, r R, x X, y Y . For each robot we generate four possible moves in the environment.

move(r, x, y + 1, t) move(r, x, y + 1, t) robo X(r, x, t), robo Y (r, y, t). (y + 1 Y )

move(r, x, y 1, t) move(r, x, y 1, t) robo X(r, x, t), robo Y (r, y, t). (y 1 Y )

move(r, x + 1, y, t) move(r, x + 1, y, t) robo X(r, x, t), robo Y (r, y, t). (x + 1 X)

move(r, x 1, y, t) move(r, x 1, y, t) robo X(r, x, t), robo Y (r, y, t). (x 1 X)

We disallow moving to multiple locations and standing still (the latter is not strictly necessary but we obtained experimental results that way).

move(r, x1, y1, t), move(r, x1, y2, t). (x1, x2 X, x1 < x2, y1, y2 Y )

move(r, x, y1, t), move(r, x, y2, t). (y1, y2 Y, y1 < y2)

move (r, t) move(r, x, y, t).

not move (r, t).

The effect of moving is a deterministic change of location.

robo X(r, x, t + 1) move(r, x, y, t). robo Y (r, y, t + 1) move(r, x, y, t).

For saturation we guess the position of the object.

obj X(x) obj X(x) . obj X(y) obj Y (y) .

We spoil the answer set if the object is at multiple locations.

spoil obj X(x1), obj X(x2). (x1, x2 X, x1 < x2)

spoil obj Y (y1), obj Y (y2). (y1, y2 Y, y1 < y2)

We spoil the answer set if the object is at no location.

object Has No XUp To(1) obj X(1).

object Has No XUp To(x) object Has No XUp To(x 1), obj X(x). (x 1 X)

spoil object Has No XUp To(xmax). (xmax = max(X))

object Has No YUp To(1) obj Y (1).

object Has No YUp To(y) object Has No YUp To(y 1), obj Y (y). (y 1 Y )

spoil object Has No YUp To(ymax). (ymax = max(Y ))

We spoil the answer set if the object is sensed, which is determined by an external atom with the semantic function f&sense such that f&sense(A, robo X, robo Y , obj X, obj Y , range, spoil) = 1 iff

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

Tspoil A or the predicates robo X, robo Y , obj X, obj Y represent in A a state where the robot has a distance less than range to the object, i.e., the robot can detect the object. The implementation of this external atom was realized in C++ and consists of verifying range q

2x + 2y and bookkeeping code to extract x and y from A.

spoil &sense[robo X, robo Y , obj X, obj Y , range, spoil]().

We create a unique answer set whenever spoil is true and require that only spoiled answer sets are returned.

obj X(x) spoil. obj X(x) spoil.

obj Y (x) spoil. obj Y (x) spoil.

object Has No XUp To(x) spoil. object Has No YUp To(y) spoil.

Given an instance encoded as above, an answer set to the above program exists iff there exists a sequence of movements that ensures to detect the object no matter where it is located. Furthermore the movements required to detect the object, i.e., the conformant plan, is encoded in the answer set in the extension of the move predicate.

Appendix B. Proofs

Proof of Proposition 1. ( ) Let A be an answer set of Check(Π, A) such that f&g(A , p, c) = 1 iff Te&g[p](c) A for all external atoms &g[p](c) in Π. Since ˆA is a compatible set of Π, f&g(A, p, c) = 1 iff Te&g[p](c) ˆA for all external atoms

&g[p](c) in Π. Thus, f ˆΠ ˆA is the same as fΠA with replacement atoms in place of external atoms, and with additional guessing rules for replacement atoms. Since A is a model of Check(Π, A) it is also a model of f ˆΠ ˆA. Let A = {Ta A | a A(Π)} {Fa A | a A(Π)}. Since f&g(A , p, c) = 1 iff Te&g[p](c) A for all external atoms &g[p](c) in Π by assumption, A is a model of fΠA. Since A is an answer set of Check(Π, A), and a Check(Π, A) for all a A(Π) with Ta ˆA (and thus Ta A), {Ta A | a A(Π)} A. Finally, due to { not smaller} {smaller not a | a A(Π), Ta ˆA} Check(Π, A), there is at least one a A(Π) s.t. Ta ˆA (and thus also Ta A), but Fa A (and thus also Fa A ). Therefore {Ta A | a A(Π)} A is a model of Π, and thus A is not an answer set of Π. ( ) If A is not an answer set of Π, then there is a model A of fΠA which is smaller in the positive part, i.e., {Ta A } {Ta A}. Let

A = κ(Π, A ) {Ta | Ta ˆA, Fa A } {Fa | Ta ˆA, Ta A } {Tsmaller}.

We show that A is an answer set of Check(Π, A) such that f&g(A , p, c) = 1 iff Te&g[p](c) A

for all external atoms &g[p](c) in Π. Since A has been extracted from a compatible set ˆA of Π, f ˆΠ ˆA is the same as fΠA with replacement atoms in place of external atoms, and with additional guessing rules for replacement atoms. Since A is a model of fΠA, and the truth values of all replacement atoms in A coincide

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

with the oracle functions by deﬁnition of κ(Π, A ), and set exactly one of ea or nea for each external atom a in Π to true (and thus satisfy the guessing rules for replacement atoms), A is a model of f ˆΠ ˆA. Since {Ta A } {Ta A} and thus also {Ta A | a A(Π)} {Ta A | a A(Π)}, the corresponding constraint a in Check(Π, A) is not violated. Moreover, for each a with Ta ˆA we have either Ta A or Ta A , thus the corresponding rule a a in Check(Π, A) is satisﬁed. Finally, since Tsmaller A , the rules {smaller not a | a A(Π), Ta ˆA} are satisﬁed and the constraint not smaller does not ﬁre. Thus A is a model of Check(Π, A). We show now that A is also a subset-minimal model of f Check(Π, A)A . Observe that

f Check(Π, A)A = f ˆΠ ˆA {a a | Ta ˆA}

{smaller not a | a A(Π), Ta ˆA}.

However, if any atom a A(f Check(Π, A)A ) with Ta A is changed to false, then the interpretation is not a model anymore because the corresponding rule a a is violated, as only one of a and a is true in A by deﬁnition; thus no interpretation with smaller positive part than A can be a model of f Check(Π, A)A . Hence A is an answer set of Check(Π, A). Finally, f&g(A , p, c) = 1 iff Te&g[p](c) A for all external atoms &g[p](c) in Π by deﬁnition of κ(Π, A ). 2

Proof of Proposition 2. The result follows from Proposition 1 and the fact that the programs Check(Π, A) and Check Optimized(Π, A) have the same answer sets. Indeed, by construction the programs have the same models; consequently, every answer set A of Check(Π, A) (which is a model of Check(Π, A)) is a model of f Check Optimized(Π, A)A . As A is a minimal model of f Check(Π, A)A , due to the guessing rules a a , for Ta ˆA, and ea nea , for all external atoms a in Check(Π, A), we have either {Ta, Fa } A or {Fa, Ta } A (but not both) and either {Tea, Fnea} A or {Fea, Tnea} A (but not both); furthermore, due to the constraints a for every a A(Π) such that Ta / ˆA, we have Fa A for each such a. As the same guessing rules and constraints are also in Check Optimized(Π, A), in every model A

of Check Optimized(Π, A)A such that A Check Optimized(Π,A) A all atoms a, a , ea, and nea must thus have the same value as in A ; consequently, also smaller must have the same value as in A . It follows that A is a minimal model of f Check Optimized(Π, A)A , i.e., A is an answer set of Check Optimized(Π, A). The argument that every answer set of Check Optimized(Π, A) is an answer set of Check(Π, A) is analogous. 2

Proof of Theorem 3. The argument that proves Corollary 3 by Faber (2005) can be used mutatis mutandi to prove this statement, with external atoms in place of aggregates. 2

Proof of Proposition 4. We proceed by contraposition and show that if IΓ(U, ΓA Π, Π, A) is not a solution to ΓA Π, then U cannot be an unfounded set such that AT U = . First observe that the nogoods in Hr,A demand Thr to be true for a rule r Π in a solution to ΓA Π if and only if some head atom h H(r) of this rule is in U. As the truth values of hr and all h H(r) are deﬁned in IΓ(U, ΓA Π, Π, A) exactly to this criterion, no nogood from Hr,A can be involved in a contradiction. Furthermore, the nogood {Fa | Ta A} NA Γ,Π is violated by IΓ(U, ΓA Π, Π, A) only if AT U = ; hence, if IΓ(U, ΓA Π, Π, A) is not a solution to ΓA Π and

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

AT U = , as OA Γ,Π is conservative, then for some rule r Π the nogood in Cr,A must be violated. That is, we know the following: Thr IΓ(U, ΓA Π, Π, A) (and therefore H(r) U = ), Fa IΓ(U, ΓA Π, Π, A) for all a B+ o (r), ta IΓ(U, ΓA Π, Π, A) for all a Be(ˆr), and Th IΓ(U, ΓA Π, Π, A) for all h H(r) with A |= h. Moreover, we have Cr,A = . We now show that this implies that none of the conditions (i) (iii) of Deﬁnition 5 holds for r wrt. U and A, which means that U is not an unfounded set. Condition (i) does not hold for r because A |= B(r) (otherwise Cr,A = ). Condition (ii) does not hold for r. Suppose to the contrary that it holds. Then there must be some b B(r) s.t. A . .U |= b. Because Cr,A = , we know that A |= b. We make a case distinction on the type of b:

If b is a positive default literal from A(Π), then Fb IΓ(U, ΓA Π, Π, A) and therefore b U. Consequently A . .U |= b. Contradiction. If b is a negative default literal over A(Π) , then A |= b implies A . .U |= b. Contradiction. If b is a positive or default-negated replacement atom, then tb IΓ(U, ΓA Π, Π, A). But this implies, by deﬁnition of IΓ(U, ΓA Π, Π, A), that A . .U |= b. Contradiction. Condition (iii) does not hold for r because Th IΓ(U, ΓA Π, Π, A) and thus, by deﬁnition of IΓ(U, ΓA Π, Π, A), h U for all h H(r) with A |= h. Thus A |= a for all a H(r) \ U. 2

Proof of Theorem 6. Suppose U is not an unfounded set. Then there is an r Π s.t. H(r) U = and none of the conditions (i) (iii) in Deﬁnition 5 is satisﬁed. We show now that S cannot be a solution to ΓA Π that satisﬁes conditions (a) and (b), which proves the result. Because Condition (i) does not hold, there is a nogood of form

{{Thr} {Fa | a B+ o (r), A |= a} {ta | a Be(ˆr)} {Th | h H(r), A |= h}}

in ΓA Π. We now show that S contains all signed literals of this nogood, i.e., the nogood is violated by the assignment S. Since H(r) U = , Thr S (otherwise a nogood in HA r is violated). As U is not an unfounded set, Condition (ii) in Deﬁnition 5 does not hold. Consider any a B+ o (r) s.t. A |= a. Then a U, otherwise A . .U |= a and we have a contradiction with the assumption that Condition (ii) is unsatisﬁed. But then Fa S (because S is complete and would imply a U otherwise). Now consider any &g[p](c) EA(r). Then A . .U |= &g[p](c) (as (ii) is violated). If A |= &g[p](c), then Condition (i) would be satisﬁed, hence A |= &g[p](c). But then Te&g[p](c) S, otherwise A . .U |= &g[p](c) by precondition (b) of this proposition. Next consider all not &g[p](c) Be(r). Then A . .U |= &g[p](c) (as (ii) is violated). If A |= &g[p](c), then Condition (i) would be satisﬁed, hence A |= &g[p](c). But then Fe&g[p](c) S, otherwise A . .U |= &g[p](c) by precondition (a) of this proposition. Therefore, we have ta S for all a Be(ˆr). Finally, because Condition (iii) in Deﬁnition 5 does not hold, h U and therefore also Th S for all h H(r) with A |= a. This concludes the proof that S cannot be a solution to ΓA Π satisfying (a) and (b), if U is not an unfounded set. 2

Proof of Proposition 7. Let S = IΓ(U, ΓA Π, Π, A). If for an external atom &g[y](x) in Π we have Te&g[y](x) S, then by deﬁnition of IΓ(U, ΓA Π, Π, A) we have A . .U |= &g[y](x)

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

(satisfying (a)). If for an external atom &g[y](x) in Π we have Fe&g[y](x) S, then by deﬁnition of IΓ(U, ΓA Π, Π, A) we have A . .U |= &g[y](x) (satisfying (b)). 2

Proof of Proposition 8. We proceed by contraposition and show that if IΩ(U, ΩΠ, Π, A) is not a solution to ΩΠ with assumptions AA, then U cannot be an unfounded set such that AT U = . First observe that the nogoods in Hr demand Thr to be true for a rule r Π if and only if some head atom h H(r) of this rule is in U. Moreover, the nogoods in Da for each a A(Π) force a A . .U to true if and only if Ta A and a / U, which is equivalent to Ta A . .U; a A U to true if and only if Ta A and a U; and a A U to true if and only if Fa A or a U. As the truth values of hr for each r Π, and a A . .U and a A U and a A U for each a A(Π) in IΩ(U, ΩΠ, Π, A) are deﬁned exactly to these conditions, a contradiction must involve Cr for some r Π. Furthermore, the nogood {Fa | a A(Π)} is violated by IΩ(U, ΩΠ, Π, A) only if A(Π) U = , and thus AT U = ; hence, if IΩ(U, ΩΠ, Π, A) is not a solution to ΩΠ such that AT U = , since OΩ,Π is conservative, for some rule r Π the nogood in Cr must be violated. That is, we know the following:

(I) Thr IΩ(U, ΩΠ, Π, A) (and therefore H(r) U = ),

(II) Ta A IΩ(U, ΩΠ, Π, A) for all a B+(ˆr) and Fa A IΩ(U, ΩΠ, Π, A) for all a B (ˆr),

(III) Fa A U IΩ(U, ΩΠ, Π, A) for all a B+ o (r), ta IΩ(U, ΩΠ, Π, A) for all a Be(ˆr), and

(IV) Th A U IΩ(U, ΩΠ, Π, A) for all h H(r).

We now show that this implies that none of the conditions of Deﬁnition 5 holds for r wrt. U and A, which means that U is not an unfounded set (hr is true in IΩ(U, ΩΠ, Π, A), which implies H(r) U = x). Condition (i) does not hold for r because of (II), which by our assumptions AA implies A |= B(r). Condition (ii) does not hold for r. Suppose to the contrary that it holds. Then there must be some b B(r) s.t. A . .U |= b. Since Condition (i) is already known to be violated, we can assume that A |= b. We make a case distinction on the type of b:

If b is a positive default literal from A(Π) , then b U (otherwise A . .U |= b). But then we have by deﬁnition of IΩ(U, ΩΠ, Π, A) that Tb A U IΩ(U, ΩΠ, Π, A), which contradicts (III). If b is a negative default literal over A(Π) , then A |= b implies A . .U |= b. Contradiction. If b is a positive or default-negated replacement atom, then tb IΩ(U, ΩΠ, Π, A). But this implies, by deﬁnition of IΩ(U, ΩΠ, Π, A), that A . .U |= b. Contradiction. Condition (iii) does not hold for r because Th A U IΩ(U, ΩΠ, Π, A) and thus, by deﬁnition of IΩ(U, ΩΠ, Π, A), h U for all h H(r) with A |= h. Thus A |= a for all a H(r) \ U. 2

Proof of Theorem 10. Suppose U is not an unfounded set. Then some r Π exists such that H(r) U = and none of the conditions (i) (iii) in Deﬁnition 5 is satisﬁed. We show that then S, assuming that AA is satisﬁed and (a) and (b) hold, cannot be a solution to ΩΠ. Due to rule r, ΩΠ (more speciﬁcally, NΩ,Π) contains a nogood N of form N = { {Thr} {Ta A | a B+(ˆr)} {Fa A | a B (ˆr)} {Fa A U | a B+ o (r)} {ta | a Be(ˆr)} {Th A U | h H(r)} }.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

We show that S contains all signed literals of N, i.e., N is violated by S. As H(r) U = , Thr S (otherwise a nogood in Hr is violated). Furthermore, as U is not an unfounded set, Condition (i) in Deﬁnition 5 does not hold for U wrt. A, and hence A |= B(r). The assumptions AA thus enforce that Ta A S for all a B+(ˆr) and Fa A S for all a B (ˆr). Consider next an arbitrary a B+ o (r). As Condition (ii) in Deﬁnition 5 does not hold for U wrt. A, we have A |= a and a U; the latter implies by deﬁnition of U that Fa S. From the nogood {Ta A U, Fa} we conclude Fa A U S. We next show that for every a Be(ˆr), it holds that ta S. Indeed, let &g[p](c) EA(r). We have A . .U |= &g[p](c) (as Condition (ii) is violated). Furthermore, A |= &g[p](c), as A |= &g[p](c) would imply that Condition (i) is satisﬁed. Thus from Condition (b) of the hypothesis, it follows that Te&g[p](c) S. Similarly, let not &g[p](c) Be(r). Then A . .U |= &g[p](c) (as Condition (ii) is violated) and A |= &g[p](c) as A |= &g[p](c) would satisfy Condition (i). Thus from Condition (a) of the hypothesis, it follows that Fe&g[p](c) S. Thus we have ta S for all a Be(ˆr). Finally, because Condition (iii) in Deﬁnition 5 does not hold for U wrt. A, we have h U and therefore also Th S for all h H(r) with A |= a. That is, for each h H(r), either Fh A S or Th S. But by the nogoods {Fh A U, Fh A}, {Fh A U, Th} Dh, in both cases we have Th A U S. Hence, N S holds, i.e., N is violated by S, and thus S is not a solution of ΩΠ. This completes the proof of the result. 2

Proof of Proposition 11. Let S = IΩ(U, ΩΠ, Π, A). If for an external atom &g[y](x) in Π we have Te&g[y](x) S, then by deﬁnition of IΩ(U, ΩΠ, Π, A) we have A . .U |= &g[y](x) (satisfying (a)). If for an external atom &g[y](x) in Π we have Fe&g[y](x) S, then by deﬁnition of IΩ(U, ΩA Π, Π, A) we have A . .U |= &g[y](x) (satisfying (b)). 2

Proof of Proposition 12. To show that U \ {a} is an unfounded set wrt. A, consider r Π such that H(r) (U \ {a}) = . We have to show that one of the conditions (i) (iii) of Deﬁnition 5 holds for r. By hypothesis, U is an unfounded set of Π wrt. A, and H(r) (U \ {a}) = implies H(r) U = . If Condition (i) holds for U, it also holds wrt. U \{a} because this condition depends only on r and A. Also if Condition (ii) holds for U, it also holds wrt. U \ {a} because A . .U is equivalent to A . .(U \ {a}) since A |= a. Finally, if Condition (iii) holds for U, then some atom b H(r) \ U exists such that A |= b. As A |= a, it follows a = b and hence condition (iii) holds for U \ {a}. This proves the result. 2

Proof of Proposition 13. Suppose that changing the truth value of b in S turns the solution to a counterexample Sb of ΓA Π (resp. ΩΠ). That is, Sb must violate some nogood N ΓA Π resp. (N ΩΠ) containing b, i.e., either Tb N or Fb N. For the encoding ΓA Π, the nogood N corresponds to a rule with b B+(ˆr) or b B (ˆr) and A |= B(r), and N contains also the signed literals (1) Fa for all a B+ o with A |= a and (2) Ta for all a H(r) with A |= a. By hypothesis, we have either (a) Ta S for some a B+ o (r) with A |= a, or (b) Fa for some a H(r) with A |= a. But then the nogood cannot be violated, because (a) contradicts one of (1) and (b) contradicts one of (2). For the encoding ΩΠ, the nogood N corresponds to a rule r with b B+(ˆr) or b B (ˆr). The nogood contains also the signed literals (1) Ta A for all a B+(ˆr) and Fa A for all a B (ˆr), (2) Fa A U for all a B+ o , and (3) Th A U for all h H(r). Because of (1) and since A is a solution

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

to AA, we have A |= B(r). By hypothesis, we have either (a) Ta S for some a B+ o (r) with A |= a, or (b) Fa for some a H(r) with A |= a. But then the nogood N cannot be violated, because (a) contradicts part (2) by deﬁnition of AA and a A U, and (b) contradicts part (3) by deﬁnition of AA and h A U. 2

Proof of Proposition 14. If TΓ(N, A) = then the proposition trivially holds. Otherwise TΓ(N, A) = {C} and we know that Tti A for all 1 i n. Suppose C is violated by IΓ(U, ΓA Π, Π, A). Then Fti IΓ(U, ΓA Π, Π, A) and therefore ti U for all 1 i n, and Tfi IΓ(U, ΓA Π, Π, A) for all 1 i m with A |= fi, and σe&g[p](c) IΓ(U, ΓA Π, Π, A). But then A . .U |= ti for all 1 i n and A . .U |= fi for all 1 i m. Because the nogood N is a valid input-output-relationship, this implies σ&g[p](c) A . .U. By deﬁnition of IΓ(U, ΓA Π, Π, A), we then have σe&g[p](c) IΓ(U, ΓA Π, Π, A), which contradicts the assumption that TΓ(N, A) is violated. 2

Proof of Proposition 15. We know TΩ(N) = {C}. Suppose IΩ(U, ΩΠ, Π, A) violates C. Then Tti A IΩ(U, ΩΠ, Π, A) and therefore Tti A and Fti IΩ(U, ΩΠ, Π, A) for all 1 i n; Ffi A . .U IΩ(U, ΩΠ, Π, A) and therefore either Ffi A or fi U, for all 1 i m; and σe&g[p](c) I(U, ΩΠ, A). But then, by deﬁnition of IΩ(U, ΩΠ, Π, A), Tti A and ti U for all 1 i n, hence A . .U |= ti for all 1 i n. Moreover, A . .U |= fi for all 1 i m. Because nogood N is a valid input-output-relationship, this implies σ&g[p](c) A . .U. On the other hand, by deﬁnition of IΩ(U, ΩΠ, Π, A), we have σe&g[p](c) IΩ(U, ΩΠ, Π, A); this contradicts the assumption that the nogood C is violated. 2

Proof of Proposition 16. Suppose some answer set A of Π exists which is not a solution to L1(U, Π, A), i.e., it violates some nogood N = {σ0, σ1, . . . , σn} L1(U, Π, A). We show that in this case U is an unfounded set of Π wrt. A such that U A = ; this means that A is not-unfounded-free, which contradicts that A is an answer set of Π. Let r Π be a rule such that H(r) U = . We have to show that one of the conditions (i) (iii) of Deﬁnition 5 holds. If B+ o (r) U = , then Condition (ii) holds. Hence we assume in the following that B+ o (r) U = , which means that r is an external rule of Π wrt. U. But then for some σi N with 1 i n we have either (1) σi = Th for some h H(r) with h U and A |= h, or (2) σi = Fb for some b B+ o (r) with A |= b. Since A violates N by assumption, we have σi A . In Case (1) the Condition (iii) is satisﬁed, while in Case (2) then Condition (i) is satisﬁed. Moreover, by deﬁnition of L1 some a U exists such that Ta A , i.e., A intersects with U. This proves the result. 2

Proof of Proposition 17. Towards a contradiction, suppose some answer set A of Π is not a solution to L2(U, Π, A). Let N = {Ta | a A . .U} {σ0, σ1, . . . , σn} L2(U, Π, A) be a violated nogood. Because σi A for all 1 i n, we know that A falsiﬁes (at least) the bodies of rules in Π that are falsiﬁed by A; consequently, fΠA fΠA. From A |= Π and the hypothesis that U is an unfounded set it follows that A . .U |= fΠA; hence, also A . .U |= fΠA . Moreover, Ta A for all a A . .U, and therefore A T (A . .U)T. Because σ0 A , we conclude A T (A . .U)T, i.e., A is not a subset-minimal model of ΠA . Consequently, A is not an answer set of Π, which is a contradiction. 2

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

Proof of Lemma 18. If Y = , then the result holds trivially. Otherwise, let r Π with H(r) Y = . We show that one of the conditions (i) (iii) in Deﬁnition 5 holds. Observe that H(r) U = because U Y . Since U is an unfounded set of Π wrt. A, either

(i) A |= b for some b B(r); or

(ii) A . .U |= b for some b B(r); or

(iii) A |= h for some h H(r) \ U.

In Case (i), the condition also holds wrt. Y . In case (ii), let a H(r) such that a Y , and b B(r) such that A . .U |= b. We make a case distinction: either b is an ordinary literal or an external one. If b is an ordinary default-negated atom not c, then A . .U |= b implies Tc A and c U, and therefore also A . .Y |= b. So assume b is an ordinary atom. If b U then A |= b and Case (i) applies, so assume b U. Because a H(r) and b B(r), we have a b and therefore either a, b C or a, b Y (because there are no ordinary edges between C and Y ). But by assumption a Y , and therefore b Y , hence A . .Y |= b. If b is an external literal, then there is no q U with a e q and q Y . Otherwise, this would imply q C and C would have an incoming e-edge, which contradicts the assumption that C is a cut of GR Π. Hence, for all q U with a e q, also q Y , and therefore the truth value of b under A . .U and A . .Y is the same. Hence A . .Y |= b. In Case (iii), also A |= h for some h H(r) \ Y because Y U and therefore H(r) \ Y H(r) \ U. 2

Proof of Lemma 19. If U = , then the result holds trivially. Otherwise, suppose ˆr ˆΠ and a H(ˆr) U. Observe that ˆr cannot be an external atom guessing rule because U contains only ordinary atoms. We show that one of the conditions in Deﬁnition 5 holds for ˆr wrt. ˆA. Because ˆr is no external atom guessing rule, there is a corresponding rule r Π containing external atoms in place of replacement atoms. Because U is an unfounded set of Π and H(r) = H(ˆr), either:

(i) A |= b for some b B(r); or

(ii) A . .U |= b for some b B(r); or

(iii) A |= h for some h H(r) \ U

In Case (i), let b B(r) such that A |= b and ˆb the corresponding literal in B(ˆb) (which is the same if b is ordinary and the corresponding replacement literal if b is external). Then also ˆA |= ˆb because ˆA is compatible. In Case (ii), we make a case distinction: either b is ordinary or external. If b is ordinary, then b B(ˆr) and ˆA . .U |= b holds because A and ˆA are equivalent for ordinary atoms. If b is an external atom or default-negated external atom, then no atom p(c) U is input to it, i.e., p is not a predicate input parameter of b; otherwise we had a e p(c), contradicting our assumption that U has no internal e-edges. But then A . .U implies A |= b because the truth value of b under A . .U and A is the same. Therefore we can apply Case (i).

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

In Case (iii), also ˆA |= h for some h H(ˆr) \ U because H(r) = H(ˆr) contains only ordinary atoms and A is equivalent to ˆA for ordinary atoms. 2

Proof of Theorem 20. We deﬁne the reachable set R(a) from some atom a as

R(a) = {b | (a, b) { } },

i.e., the set of atoms b U reachable from a using edges from only but no e-edges. We ﬁrst assume that U contains at least one e-edge, i.e., there are x, y U such that x e y. Now we show that there is a u U with outgoing e-edge (i.e., u e v for some v U), but such that R(u) has no incoming e-edges from U (i.e., for all v R(u) and b U, b e v holds). Suppose to the contrary that for all a with outgoing e-edges, the reachable set R(a) has an incoming e-edge from U. We now construct an e-cycle under d, which contradicts our assumption. Start with an arbitrary node c0 U that has an outgoing e-edge, let p0 be the (possibly empty) path (under ) from c0 to the node d0 R(c0) such that d0 has an incoming e-edge, i.e., there is a c1 such that c1 e d0; note that c1 R(c0).4 By assumption, also some node d1 in R(c1) has an incoming e-edge (from some node c2 R(c1)). Let p1 be the path from c1 to d1, etc. By iteration we can construct the concatenation of the paths p0, (d0, c1), p1, (d1, c2), p2, . . . , pi, (di, ci+1), . . ., where the pi from ci to di are the paths within reachable sets, and the (di, ci+1) are the e-edges between reachable sets. However, as U is ﬁnite some nodes on this path must be equal, i.e., a subsequence of the constructed sequence represents an e-cycle (in reverse order). This proves that u is a node with outgoing e-edge but such that R(u) has no incoming e-edges. We next show that R(u) is a cut of GR Π. Condition (i) is immediately satisﬁed by deﬁnition of u. Condition (ii) is shown as follows. Let u R(u) and v U \R(u). We have to show that u v

and v u . Suppose, towards a contradiction, that u v . Because u R(u), there is a path from u to u under . But if u v , then there would also be a path from u to v under and v would be in R(u), a contradiction. Analogously, v u would also imply that there is a path from u to v because there is a path from u to u , again a contradiction. Therefore, R(u) U is a cut of GR Π, and by Lemma 18, it follows that U \R(u) is an unfounded set. Observe that U \ R(u) contains one e-edge less than U because u has an outgoing e-edge and that U \ R(u) = ; indeed, by assumption some w U exists such that u e w, and clearly w R(u). By iterating this argument, the number of e-edges in the unfounded set can be reduced to zero in a nonempty core. Eventually Lemma 19 applies, proving that the remaining set is an unfounded set of ˆΠ. 2

Proof of Corollary 21. Towards a contradiction, suppose an unfounded set U of Π wrt. A exists. Then U contains no e-cycle because there is no e-cycle under d. By Theorem 20 there is an unfounded set of ˆΠ wrt. ˆA, which contradicts our assumption that ˆΠ has no unfounded set wrt. A. 2

Proof of Theorem 22. If U contains no cyclic input atoms, then all cycles under d containing e-edges in the atom dependency graph of Π are broken, i.e., U does not contain an e-cycle under d. Then by Theorem 20 there exists a nonempty unfounded set of ˆΠ wrt. ˆA. 2

4. Whenever x e y for x, y U, then there is no path from x to y under , because otherwise we would have an e-cycle under d.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

Proof of Theorem 23. Let U be a nonempty unfounded set of Π wrt. A. Because C is a decomposition of A(Π) into strongly connected components, the component dependency graph

C, {(C1, C2) | C1, C2 C, a1 C1, a2 C2 : (a1, a2) e}

is acyclic. Following the hierarchical component dependency graph from the nodes without predecessor components downwards, we can ﬁnd a ﬁrst component which has a nonempty intersection with U, i.e., there exists a component C C such that C U = but C U = for all transitive predecessor components C of C. We show that U C is an unfounded set of ΠC wrt. A. Let r ΠC be a rule such that H(r) (U C) = . We have to show that one of the conditions (i)-(iii) of Deﬁnition 5 holds for r wrt. A and U C. Because U is an unfounded set of Π wrt. A we know that one of the conditions (i) (iii) holds for r wrt. A and U. In case of Condition (i), then it trivially holds also wrt. A and U C because this condition depends only on the assignment A, but not on the unfounded set U; in case of Condition (iii), it clearly holds because H(r) \ U = is included in H(r) \ (U C). In case of Condition (ii), we have that A . .U |= b for some (ordinary or external) body literal b B(r). We show next that the truth value of all literals in B(r) is the same under A . .U and A . .(U C), which proves that Condition (ii) holds also wrt. A and U C. If b = not a for some ordinary atom a, then Ta A and a U and consequently a U C, hence A . .(U C) |= b. If b is an ordinary atom, then either Fb A, which implies immediately that A . .(U C) |= b, or b U. But in the latter case b is either in a predecessor component C of C or in C itself (since h b for all h H(r)). But since U C = for all predecessor components of C, we know b C and therefore b (U C), which implies A . .(U C) |= b. If b is a positive or default-negated external atom, then all input atoms a to b are either in a predecessor component C of C or in C itself (since h e a for all h H(r)). We show with a similar argument as before that the truth value of each input atom a is the same under A . .U and A . .(U C): if A . .U |= a, then Ta A and a U, hence a (U C) and therefore A . .(U C) |= a. If A . .U |= a, then either Fa A, which immediately implies A . .(U C) |= a, or a U. But in the latter case a must be in C because U C = for all predecessor components C of C. Therefore a (U C) and consequently A . .(U C) |= a. Because all input atoms a have the same truth value under A . .U and A . .(U C), the same holds also for the positive or default-negated external atom b itself. 2

Proof of Proposition 24. If U = , then the result holds trivially. By deﬁnition of ΠC, we have H(r) C = for all r Π \ ΠC. By hypothesis we have U C. But then H(r) U = for all r Π \ ΠC and U is an unfounded set of Π wrt. A. 2

Alviano, M., Calimeri, F., Faber, W., Leone, N., & Perri, S. (2011). Unfounded Sets and Well Founded Semantics of Answer Set Programs with Aggregates. Journal of Artiﬁcial Intelligence Research, 42, 487 527.

Baader, F., & Hollunder, B. (1995). Embedding Defaults into Terminological Knowledge Representation Formalisms. Journal of Automated Reasoning, 14(1), 149 180.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

Basol, S., Erdem, O., Fink, M., & Ianni, G. (2010). HEX Programs with Action Atoms. In Hermenegildo, M., & Schaub, T. (Eds.), Technical Communications of the 26th International Conference on Logic Programming (ICLP 10), Vol. 7 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 24 33, Dagstuhl, Germany. Schloss Dagstuhl Leibniz-Zentrum fuer Informatik.

Brewka, G., & Eiter, T. (2007). Equilibria in Heterogeneous Nonmonotonic Multi-Context Systems. In Holte, R. C., & Howe, A. (Eds.), 22nd AAAI Conference on Artiﬁcial Intelligence (AAAI 07), pp. 385 390. AAAI Press.

Brewka, G., Eiter, T., & Truszczy nski, M. (2011). Answer set programming at a glance. Communications of the ACM, 54(12), 92 103.

Drescher, C., Gebser, M., Grote, T., Kaufmann, B., K onig, A., Ostrowski, M., & Schaub, T. (2008). Conﬂict-driven disjunctive answer set solving. In Brewka, G., & Lang, J. (Eds.), 11th International Conference Principles of Knowledge Representation and Reasoning (KR 2008), Sydney, Australia, September 16-19, 2008, pp. 422 432. AAAI Press.

Drescher, C., & Walsh, T. (2012). Answer set solving with lazy nogood generation. In Dovier, A., & Costa, V. S. (Eds.), Technical Communications of the 28th International Conference on Logic Programming (ICLP 2012), Vol. 17 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 188 200. Schloss Dagstuhl Leibniz-Zentrum fuer Informatik.

Dung, P. M. (1995). On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artiﬁcial Intelligence, 77(2), 321 357.

Dung, P., Mancarella, P., & Toni, F. (2007). Computing ideal sceptical argumentation. Artiﬁcial Intelligence, 171, 642 674.

Dunne, P. E. (2009). The computational complexity of ideal semantics. Artiﬁcial Intelligence, 173(18), 1559 1591.

Egly, U., Gaggl, S. A., & Woltran, S. (2010). Answer-set programming encodings for argumentation frameworks. Argument and Computation, 1(2), 147 177.

Eiter, T., Fink, M., Ianni, G., Krennwallner, T., & Sch uller, P. (2011). Pushing Efﬁcient Evaluation of HEX Programs by Modular Decomposition. In Delgrande, J., & Faber, W. (Eds.), 11th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 11), Vol. 6645 of LNAI, pp. 93 106. Springer.

Eiter, T., Fink, M., Krennwallner, T., & Redl, C. (2012a). Conﬂict-driven ASP Solving with External Sources. Theory and Practice of Logic Programming, 12(4-5), 659 679.

Eiter, T., Fink, M., Krennwallner, T., Redl, C., & Sch uller, P. (2012b). Eliminating Unfounded Set Checking for HEX-Programs. In Fink, M., & Lierler, Y. (Eds.), 5th Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2012), September 4, 2012, Budapest, Hungary, pp. 83 97.

Eiter, T., Fink, M., Krennwallner, T., Redl, C., & Sch uller, P. (2012c). Exploiting Unfounded Sets for HEX-Program Evaluation. In del Cerro, L. F., Herzig, A., & Mengin, J. (Eds.), 13th European Conference on Logics in Artiﬁcial Intelligence (JELIA 2012), September 26-28, 2012, Toulouse, France, Vol. 7519 of LNCS, pp. 160 175. Springer.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

Eiter, T., Fink, M., Sch uller, P., & Weinzierl, A. (2012b). Finding explanations of inconsistency in nonmonotonic multi-context systems. Tech. rep. INFSYS RR-1843-12-09, INFSYS RR1843-03-08, Inst. f ur Informationssysteme, TU Wien. Preliminary version in Proc. 12th International Conference on Knowledge Representation and Reasoning (KR 2010), pp. 329 339, AAAI Press, 2010.

Eiter, T., Ianni, G., Krennwallner, T., & Schindlauer, R. (2008a). Exploiting conjunctive queries in description logic programs. Annals of Mathematics and Artiﬁcial Intelligence, 53(1 4), 115 152.

Eiter, T., Ianni, G., Lukasiewicz, T., Schindlauer, R., & Tompits, H. (2008b). Combining answer set programming with description logics for the semantic web. Artiﬁcial Intelligence, 172(1213), 1495 1539.

Eiter, T., Ianni, G., Schindlauer, R., & Tompits, H. (2005). A Uniform Integration of Higher-Order Reasoning and External Evaluations in Answer-Set Programming. In Kaelbling, L. P., & Safﬁotti, A. (Eds.), 19th International Joint Conference on Artiﬁcial Intelligence (IJCAI 05), pp. 90 96. Professional Book Center.

Eiter, T., Ianni, G., Schindlauer, R., & Tompits, H. (2006a). dlvhex: A Prover for Semantic-Web Reasoning under the Answer-Set Semantics. In Proceedings of the ICLP 06 Workshop on Applications of Logic Programming in the Semantic Web and Semantic Web Services (ALPSWS2006), pp. 33 39. CEUR WS.

Eiter, T., Ianni, G., Schindlauer, R., & Tompits, H. (2006). Effective Integration of Declarative Rules with External Evaluations for Semantic-Web Reasoning. In Sure, Y., & Domingue, J. (Eds.), 3rd European Conference on Semantic Web (ESWC 06), Vol. 4011 of LNCS, pp. 273 287. Springer.

Faber, W. (2005). Unfounded sets for disjunctive logic programs with arbitrary aggregates. In Baral, C., Greco, G., Leone, N., & Terracina, G. (Eds.), 8th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 05), Vol. 3662, pp. 40 52. Springer.

Faber, W., Leone, N., & Pfeifer, G. (2011). Semantics and complexity of recursive aggregates in answer set programming. Artiﬁcial Intelligence, 175(1), 278 298.

Gebser, M., Ostrowski, M., & Schaub, T. (2009). Constraint answer set solving. In Hill, P., & Warren, D. (Eds.), Proceedings of the Twenty-ﬁfth International Conference on Logic Programming (ICLP 09), Vol. 5649 of Lecture Notes in Computer Science, pp. 235 249. Springer Verlag.

Gebser, M., Kaufmann, B., & Schaub, T. (2012). Conﬂict-driven answer set solving: From theory to practice. Artiﬁcial Intelligence, 187 188, 52 89.

Gebser, M., Kaufmann, B., & Schaub, T. (2013). Advanced conﬂict-driven disjunctive answer set solving. In Proceedings of the Twenty-Third International Joint Conference on Artiﬁcial Intelligence, IJCAI 13, pp. 912 918. AAAI Press.

Gelfond, M., & Lifschitz, V. (1991). Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9(3 4), 365 386.

Ghidini, C., & Giunchiglia, F. (2001). Local models semantics, or contextual reasoning=locality+compatibility. Artiﬁcial Intelligence, 127(2), 221 259.

EITER, FINK, KRENNWALLNER, REDL, & SCH ULLER

Goldman, R., & Boddy, M. (1996). Expressive Planning and Explicit Knowledge. In Drabble, B. (Ed.), 3rd International Conference on Artiﬁcial Intelligence Planning Systems (AIPS 96), pp. 110 117. AAAI Press.

Hoehndorf, R., Loebe, F., Kelso, J., & Herre, H. (2007). Representing default knowledge in biomedical ontologies: application to the integration of anatomy and phenotype ontologies. BMC Bioinformatics, 8, 377.

Janhunen, T., Niemel a, I., Seipel, D., Simons, P., & You, J.-H. (2006). Unfolding partiality and disjunctions in stable model semantics. ACM Trans. Comput. Log., 7(1), 1 37.

Koch, C., Leone, N., & Pfeifer, G. (2003). Enhancing disjunctive logic programming systems by SAT checkers. Artiﬁcial Intelligence, 151(1 2), 177 212.

Lee, J. (2005). A model-theoretic counterpart of loop formulas. In Kaelbling, L. P., & Safﬁotti, A. (Eds.), 19th International Joint Conference on Artiﬁcial Intelligence (IJCAI 05), pp. 503 508. Professional Book Center.

Lee, J., & Lifschitz, V. (2003). Loop Formulas for Disjunctive Logic Programs. In Palamidessi, C. (Ed.), 19th International Conference on Logic Programming (ICLP 03), Vol. 2916 of LNCS, pp. 451 465. Springer.

Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., & Scarcello, F. (2006). The DLV System for Knowledge Representation and Reasoning. ACM Transactions on Computational Logic, 7(3), 499 562.

Leone, N., Rullo, P., & Scarcello, F. (1997). Disjunctive Stable Models: Unfounded Sets, Fixpoint Semantics, and Computation. Information and Computation, 135(2), 69 112.

Lierler, Y. (2005). cmodels - SAT-Based Disjunctive Answer Set Solver. In Baral, C., Greco, G., Leone, N., & Terracina, G. (Eds.), 8th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2005), Vol. 3662 of Lecture Notes in Computer Science, pp. 447 451. Springer.

Lifschitz, V., & Turner, H. (1994). Splitting a logic program. In Hentenryck, P. V. (Ed.), 11th International Conference on Logic Programming (ICLP 94), pp. 23 37. MIT Press.

Lin, F., & Zhao, Y. (2004). ASSAT: computing answer sets of a logic program by SAT solvers. Artiﬁcial Intelligence, 157(1 2), 115 137.

Marano, M., Obermeier, P., & Polleres, A. (2010). Processing RIF and OWL2RL within DLVHEX. In Hitzler, P., & Lukasiewicz, T. (Eds.), 4th International Conference on Web Reasoning and Rule Systems (RR 10), Vol. 6333 of LNCS, pp. 244 250. Springer.

Nieuwenborgh, D. V., Cock, M. D., & Vermeir, D. (2007a). Computing fuzzy answer sets using dlvhex. In Dahl, V., & Niemel a, I. (Eds.), 23rd International Conference on Logic Programming (ICLP 07), Vol. 4670 of LNCS, pp. 449 450. Springer.

Nieuwenborgh, D. V., Eiter, T., & Vermeir, D. (2007b). Conditional planning with external functions. In Baral, C., Brewka, G., & Schlipf, J. S. (Eds.), 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 07), Vol. 4483 of LNCS, pp. 214 227. Springer.

Shen, Y.-D. (2011). Well-supported semantics for description logic programs. In Walsh, T. (Ed.), 22nd International Joint Conference on Artiﬁcial Intelligence (IJCAI 11), pp. 1081 1086. AAAI Press.

EFFICIENT HEX-PROGRAM EVALUATION BASED ON UNFOUNDED SETS

Shen, Y.-D., & Wang, K. (2011). Extending logic programs with description logic expressions for the semantic web. In Aroyo, L., Welty, C., Alani, H., Taylor, J., Bernstein, A., Kagal, L., Noy, N. F., & Blomqvist, E. (Eds.), 10th International Semantic Web Conference (ISWC 11), Vol. 7031 of LNCS, pp. 633 648. Springer.

Simons, P., Niemel a, I., & Soininen, T. (2002). Extending and implementing the stable model semantics. Artiﬁcial Intelligence, 138(1-2), 181 234.

Smith, D. E., & Weld, D. S. (1998). Conformant Graphplan. In Mostow, J., Rich, C., & Buchanan, B. (Eds.), 15th National Conference on Artiﬁcial Intelligence (AAAI 98), pp. 889 896. AAAI Press / The MIT Press.

Turner, H. (2002). Polynomial-length planning spans the polynomial hierarchy. In Flesca, S., Greco, S., Leone, N., & Ianni, G. (Eds.), European Conference on Logics in Artiﬁcial Intelligence (JELIA 02), Vol. 2424 of LNCS, pp. 111 124. Springer.

Van Gelder, A., Ross, K. A., & Schlipf, J. S. (1991). The Well-Founded Semantics for General Logic Programs. Journal of the ACM, 38(3), 619 649.

Zakraoui, J., & Zagler, W. L. (2011). A logical approach to web user interface adaptation. In Holzinger, A., & Simonic, K.-M. (Eds.), 7th Conference of the Workgroup Human-Computer Interaction and Usability Engineering of the Austrian Computer Society (USAB 11), Vol. 7058 of LNCS, pp. 645 656. Springer.

Zirtiloˇglu, H., & Yolum, P. (2008). Ranking semantic information for e-government: complaints management. In 1st International Workshop on Ontology-supported Business Intelligence (OBI 08), No. 5 in OBI 08, p. 7. ACM.