Under consideration for publication in Theory and Practice of Logic Programming

1

A model building framework for Answer Set
Programming with external computations∗

arXiv:1507.01451v2 [] 11 Jul 2015

Thomas Eiter, Michael Fink
Institut für Informationssysteme, Technische Universität Wien
Favoritenstraße 9-11, A-1040 Vienna, Austria
(e-mail: {eiter,fink}@kr.tuwien.ac.at)

Giovambattista Ianni
Dipartimento di Matematica, Cubo 30B, Università della Calabria
87036 Rende (CS), Italy
(e-mail: ianni@mat.unical.it)

Thomas Krennwallner, Christoph Redl
Institut für Informationssysteme, Technische Universität Wien
Favoritenstraße 9-11, A-1040 Vienna, Austria
(e-mail: {tkren,redl}@kr.tuwien.ac.at)

Peter Schüller
Computer Engineering Department, Faculty of Engineering, Marmara University
Goztepe Kampusu, Kadikoy 34722, Istanbul, Turkey
(e-mail: peter.schuller@marmara.edu.tr)
submitted 27 January 2015; revised 24 June 2015; accepted 28 June 2015

Note: This article has been accepted for publication in Theory and Practice of Logic
Programming, c Cambridge University Press.
Abstract
As software systems are getting increasingly connected, there is a need for equipping nonmonotonic
logic programs with access to external sources that are possibly remote and may contain information
in heterogeneous formats. To cater for this need, HEX programs were designed as a generalization
of answer set programs with an API style interface that allows to access arbitrary external sources,
providing great flexibility. Efficient evaluation of such programs however is challenging, and it requires
to interleave external computation and model building; to decide when to switch between these tasks
is difficult, and existing approaches have limited scalability in many real-world application scenarios.
We present a new approach for the evaluation of logic programs with external source access, which is
based on a configurable framework for dividing the non-ground program into possibly overlapping
smaller parts called evaluation units. The latter will be processed by interleaving external evaluation
and model building using an evaluation graph and a model graph, respectively, and by combining
intermediate results. Experiments with our prototype implementation show a significant improvement
compared to previous approaches. While designed for HEX-programs, the new evaluation approach
may be deployed to related rule-based formalisms as well.
KEYWORDS: Answer Set Programming, Model Building, External Computation, HEX Programs

∗ This article is a significant extension of (Eiter et al. 2011) and parts of (Schüller 2012). This work has been
supported by the Austrian Science Fund (FWF) Grants P24090 and P27730, and the Scientific and Technological
Research Council of Turkey (TUBITAK) Grant 114E430.

2

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller
1 Introduction

Motivated by a need for knowledge bases to access external sources, extensions of declarative KR formalisms have been conceived that provide this capability, which is often realized
via an API-style interface. In particular, HEX programs (Eiter et al. 2005) extend nonmonotonic logic programs under the stable model semantics with the possibility to bidirectionally
access external sources of knowledge and/or computation. E.g., a rule
pointsTo(X, Y ) ← &hasHyperlink [X](Y ), url (X)
might be used for obtaining pairs of URLs (X, Y ), where X actually links Y on the Web,
and &hasHyperlink is an external predicate construct. Besides constants (i.e., values) as
above, also relational knowledge (predicate extensions) can flow from external sources to the
logic program and vice versa, and recursion involving external predicates is allowed under
safety conditions. This facilitates a variety of applications that require logic programs to
interact with external environments, such as querying RDF sources using SPARQL (Polleres
2007), default rules on ontologies (Hoehndorf et al. 2007; Dao-Tran et al. 2009), complaint
management in e-government (Zirtiloǧlu and Yolum 2008), material culture analysis (Mosca
and Bernini 2008), user interface adaptation (Zakraoui and Zagler 2012), multi-context
reasoning (Brewka and Eiter 2007), or robotics and planning (Schüller et al. 2013; Havur
et al. 2014), to mention a few.
Despite the absence of function symbols, an unrestricted use of external atoms leads to
undecidability, as new constants may be introduced from the sources; in iteration, this can
lead to an infinite Herbrand universe for the program. However, even under suitable restrictions like liberal domain-expansion safety (Eiter et al. 2014a) that avoid this problem, the
efficient evaluation of HEX-programs is challenging, due to aspects such as nonmonotonic
atoms and recursive access (e.g., in transitive closure computations).
Advanced in this regard was the work by Eiter et al. (2012), which fostered an evaluation
approach using a traditional LP system. Roughly, the values of ground external atoms
are guessed, model candidates are computed as answer sets of a rewritten program, and
then those discarded which violate the guess. Compared to previous approaches such as
the one by Eiter et al. (2006), it further exploits conflict-driven techniques which were
extended to external sources. A generalized notion of Splitting Set (Lifschitz and Turner
1994) was introduced by Eiter et al. (2006) for non-ground HEX-programs, which were
then split into subprograms with and without external access, where the former are as large
and the latter as small as possible. The subprograms are evaluated with various specific
techniques, depending on their structure (Eiter et al. 2006; Schindlauer 2006). However, for
real-world applications this approach has severe scalability limitations, as the number of
ground external atoms may be large, and their combination causes a huge number of model
candidates and memory outage without any answer set output.
To remedy this problem, we reconsider model computation and make several contributions, which are summarized as follows.
• We present a modularity property of HEX-programs based on a novel generalization of
the Global Splitting Theorem (Eiter et al. 2006), which lifted the Splitting Set Theorem (Lifschitz and Turner 1994) to HEX-programs. In contrast to previous results, the new result is
formulated on a rule splitting set comprising rules that may be non-ground, moreover it is
based on rule dependencies rather than atom dependencies. This theorem allows for defining

Model building for ASP with external atoms

3

answer sets of the overall program in terms of the answer sets of program components that
may be non-ground.
• Moreover, we present a generalized version of the new splitting theorem which allows
for sharing constraints across the split; this helps to prune irrelevant partial models and
candidates earlier than in previous approaches. As a consequence — and different from
other decomposition approaches— subprograms for evaluation may overlap and also be
non-maximal (resp. non-minimal).
• Based on the generalized splitting theorem, we present an evaluation framework that
allows for flexible evaluation of HEX-programs. It consists of an evaluation graph and a
model graph; the former captures a modular decomposition and partial evaluation order of
the program, while the latter comprises for each node collections of sets of input models
(which need to be combined) and output models to be passed on between components. This
structure allows us to realize customized divide-and-conquer evaluation strategies. As the
method works on non-ground programs, introducing new values by external calculations is
feasible, as well as applying optimization based on domain splitting (Eiter et al. 2009).
• A generic prototype of the evaluation framework has been implemented which can be
instantiated with different solvers for Answer Set Programming (ASP) (in our suite, with dlv
and clasp). It also features model streaming, i.e., enumeration of the models one by one. In
combination with early model pruning, this can considerably reduce memory consumption
and avoid termination without solution output in a larger number of settings.
Applying it to ordinary programs (without external functions) allows us to do parallel
solving with a solver software that does not have parallel computing capabilities itself
(‘parallelize from outside’).
This paper, which significantly extends work in (Eiter et al. 2011) and parts of (Schüller
2012), is organized as follows. In Section 2 we present the HEX-language and consider an
example to demonstrate it in an intuitive way; we will use it as a running example throughout
the paper. In Section 3 we then introduce necessary restrictions and preliminary concepts
that form dependency-based program evaluation. After that, we develop in Section 4 our
generalized splitting theorem, which is applied in Section 5 to build a new decomposition
framework. Details about the implementation and experimental results are given in Section 6.
After a discussion including related work in Section 7, the paper concludes in Section 8.
The proofs of all technical results are given in Appendix A.
2 Language Overview
In this section, we introduce the syntax and semantics of HEX-programs as far as this is
necessary to explain use cases and basic modeling in the language.
2.1 HEX Syntax
Let C, X , and G be mutually disjoint sets whose elements are called constant names,
variable names, and external predicate names, respectively. Unless explicitly specified,
elements from X (resp., C) are denoted with first letter in upper case (resp., lower case),
while elements from G are prefixed with ‘ & ’. Note that constant names serve both as
individual and predicate names.

4

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

Elements from C ∪ X are called terms. An atom is a tuple (Y0 , Y1 , . . . , Yn ), where
Y0 , . . . , Yn are terms; n ≥ 0 is the arity of the atom. Intuitively, Y0 is the predicate name,
and we thus also use the more familiar notation Y0 (Y1 , . . . , Yn ). The atom is ordinary (resp.
higher-order), if Y0 is a constant (resp. a variable). An atom is ground, if all its terms
are constants. Using an auxiliary predicate aux n for each arity n, we can easily eliminate
higher-order atoms by rewriting them to ordinary atoms aux n (Y0 , . . . , Yn ). We therefore
assume in the rest of this article that programs have no higher-order atoms.
An external atom is of the form
&g[Y1 , . . . , Yn ](X1 , . . . , Xm ),

(1)

where Y1 , . . . , Yn and X1 , . . . , Xm are two lists of terms (called input and output lists,
respectively), and &g ∈ G is an external predicate name. We assume that &g has fixed
lengths in(&g) = n and out(&g) = m for input and output lists, respectively.
Intuitively, an external atom provides a way for deciding the truth value of an output tuple
depending on the input tuple and a given interpretation.
Example 1
(a, b, c), a(b, c), node(X), and D(a, b) are atoms; the first three are ordinary, where the
second atom is a syntactic variant of the first, while the last atom is higher-order.
The external atom &reach[edge, a](X) may be devised for computing the nodes which
are reachable in a graph represented by atoms of form edge(u, v) from node a. We have for
the input arity in(&reach) = 2 and for the output arity out(&reach) = 1. Intuitively, given
an interpretation I, &reach[edge, a](X) will be true for all ground substitutions X 7→ b
such that b is a node in the graph given by edge list {(u, v) | edge(u, v) ∈ I}, and there is a
path from a to b in that graph.
Definition 1 (rules and HEX programs)
A rule r is of the form
α1 ∨ · · · ∨ αk ← β1 , . . . , βn , not βn+1 , . . . , not βm ,

m, k ≥ 0,

(2)

where all αi are atoms and all βj are either atoms or external atoms. We let H(r) =
{α1 , . . . , αk } and B(r) = B + (r) ∪ B − (r), where B + (r) = {β1 , . . . , βn } and B − (r) =
{βn+1 , . . . , βm }. Furthermore, a (HEX) program is a finite set P of rules.
We denote by const(P ) the set of constant symbols occurring in a program P .
A rule r is a constraint, if H(r) = ∅ and B(r) 6= ∅; a fact, if B(r) = ∅ and H(r) 6= ∅;
and nondisjunctive, if |H(r)| ≤ 1. We call r ordinary, if it contains only ordinary atoms.
We call a program P ordinary (resp., nondisjunctive), if all its rules are ordinary (resp.,
nondisjunctive). Note that facts can be disjunctive, i.e., contain multiple head atoms.
Example 2 (Swimming Example)
Imagine Alice wants to go for a swim in Vienna. She knows two indoor pools called
Margarethenbad and Amalienbad (represented by margB and amalB , respectively), and
she knows that outdoor swimming is possible in the river Danube at two locations called
Gänsehäufel and Alte Donau (denoted gansD and altD, respectively).1 She looks up on
1

To keep the example simple, we assume Alice knows no other possibilities to go swimming in Vienna.

5

Model building for ASP with external atoms
EDB
Pswim
=

IDB
Pswim



location(ind , margB ), location(ind , amalB ),
location(outd , gansD), location(outd , altD)





r1 : swim(ind ) ∨ swim(outd ) ← .








r2 :
need (inoutd , C) ← &rq[swim](C).








r
:
goto(X)
∨
ngoto(X)
←
swim(P
),
location(P,
X).


3




r4 :
go ← goto(X).
=
r5 :
need (loc, C) ← &rq[goto](C).








c
:
←
goto(X),
goto(Y
),
X
=
6
Y.


6






← not go.
 c7 :





c8 :
← need (X, money).

EDB
IDB
Fig. 1: Program Pswim = Pswim
∪ Pswim
to decide swimming location

the Web whether she needs to pay an entrance fee, and what additional equipment she will
need. Finally she has the constraint that she does not want to pay for swimming.
EDB
IDB
The HEX program Pswim = Pswim
∪ Pswim
shown in Figure 1 represents Alice’s reasonEDB
ing problem. The extensional part Pswim contains a set of facts about possible swimming
locations (where ind and outd are short for indoor and outdoor , respectively). The inIDB
tensional part Pswim
incorporates the web research of Alice in an external computation,
i.e., using an external atom of the form &rq[location-choice](required -resource), which
intuitively evaluates to true iff a given location-choice requires a certain required -resource
and represents such resources and their origin (inoutd , or loc) using predicate need . Assume Alice finds out that indoor pools in general have an admission fee, and that one also
has to pay at Gänsehäufel, but not at Alte Donau. Furthermore Alice reads some reviews
about swimming locations and finds out that she will need her Yoga mat for Alte Donau
because the ground is so hard, and she will need goggles for Amalienbad because there is
so much chlorine in the water.
We next explain the intuition behind the rules in Pswim : r1 chooses indoor vs. outdoor
swimming locations, and r2 collects requirements that are caused by this choice. Rule r3
chooses one of the indoor vs. outdoor locations, depending on the choice in r1 , and r5
collects requirements caused by this choice. By r4 and c7 we ensure that some location is
chosen, and by c6 that only a single location is chosen. Finally c8 rules out all choices that
require money. Note that there is no apparent requirement for the first argument of predicate
need , however this argument ensures, that r2 and r5 have different heads, which becomes
important in Example 13.
The external predicate &rq has input and output arity in(&rq) = out(&rq) = 1. Intuitively &rq[α](β) is true if a resource β is required when swimming in a place in the
extension of predicate α. For example, &rq[swim](money) is true if swim(ind ) is true,
because indoor swimming pool charge money for swimming. Note that this only gives an
intuitive account of the semantics of &rq which will formally be defined in Example 4.
2.2 HEX Semantics
The semantics of HEX-programs (Eiter et al. 2006; Schindlauer 2006) generalizes the
answer-set semantics (Gelfond and Lifschitz 1991). Let P be a HEX-program. Then the
Herbrand base of P , denoted HB P , is the set of all possible ground versions of atoms and
external atoms occurring in P obtained by replacing variables with constants from C. The

6

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

grounding of a rule r, grnd (r), is defined accordingly, and the grounding of P is given by
S
grnd (P ) = r∈P grnd (r). Unless specified otherwise, X and G are implicitly given by P .
Different from the ‘usual’ ASP setting, the set of constants C used for grounding a program
is only partially given by the program itself; in HEX, external computations may introduce
new constants that are relevant for semantics of the program.
Example 3 (ctd.)
In Pswim the external atom &rq can introduce constants yogamat and goggles which are
not contained in Pswim , but they are relevant for computing answer sets of Pswim .
An interpretation relative to P is any subset I ⊆ HB P containing no external atoms. We
say that I is a model of atom a ∈ HB P , denoted I |= a, if a ∈ I.
With every external predicate name &g ∈ G, we associate an (n+m+1)-ary Boolean
function (called oracle function) f&g assigning each tuple (I, y1 . . . , yn , x1 , . . . , xm ) either
0 or 1, where n = in(&g), m = out(&g), I ⊆ HB P , and xi , yj ∈ C. We say that I ⊆
HB P is a model of a ground external atom a = &g[y1 , . . . , yn ](x1 , . . . , xm ), denoted I |= a,
if f&g (I, y1 . . ., yn , x1 , . . . , xm ) = 1.2
Note that this definition of external atom semantics is very general; indeed an external
atom may depend on every part of the interpretation. Therefore we will later (Section 3.1)
formally restrict external computations such that they depend only on the extension of those
predicates in I which are given in the input list. All examples and encodings in this work
obey this restriction.
Example 4 (ctd.)
The external predicate &rq in Pswim represents Alice’s knowledge about swimming locations as follows: for any interpretation I and some predicate (i.e., constant) α,
I |= &rq[α](money) iff f&rq (I, α, money) = 1 iff α(ind ) ∈ I or α(gansD) ∈ I,
I |= &rq[α](yogamat) iff f&rq (I, α, yogamat) = 1 iff α(altD) ∈ I, and
I |= &rq[α](goggles) iff f&rq (I, α, goggles) = 1 iff α(amalB ) ∈ I.
Due to this definition of f&rq , it holds, e.g., that {swim(ind )} |= &rq[swim](money).
This matches the intuition about &rq indicated in the previous example.
Let r be a ground rule. Then we say that
(i) I satisfies the head of r, denoted I |= H(r), if I |= a for some a ∈ H(r);
(ii) I satisfies the body of r (I |= B(r)), if I |= a for all a ∈ B + (r) and I 6|= a for all
a ∈ B − (r); and
(iii) I satisfies r (I |= r), if I |=H(r) whenever I |= B(r).
We say that I is a model of a HEX-program P , denoted I |= P , if I |= r for all r ∈ grnd (P ).
We call P satisfiable, if it has some model.
Definition 2 (answer set)
Given a HEX-program P , the FLP-reduct of P with respect to I ⊆ HB P , denoted f P I , is
the set of all r ∈ grnd (P ) such that I |= B(r). Then I ⊆ HB P is an answer set of P if, I
is a minimal model of f P I . We denote by AS(P ) the set of all answer sets of P .
2

In the implementation, Boolean functions for defining external sources are realized as plugins to the reasoner
which exploit a provided interface and can be written either in Python or C++.

Model building for ASP with external atoms

7

Example 5 (ctd.)
The HEX program Pswim with external semantics as given in the previous example has a
single answer set
I = {swim(outd ), goto(altD), ngoto(gansD), go, need (loc, yogamat)}.
EDB
(Here, and in following examples, we omit Pswim
from all interpretations and answer sets.)
Under I, the external atom &rq[goto](yogamat) is true and all others (&rq[swim](money),
&rq[goto](money), &rq[swim](yogamat), . . . ) are false. Intuitively, answer set I tells
Alice to take her Yoga mat and go for a swim to Alte Donau.

HEX programs (Eiter et al. 2005) are a conservative extension of disjunctive (resp., normal)
logic programs under the answer set semantics: answer sets of ordinary nondisjunctive
HEX programs coincide with stable models of logic programs as proposed by Gelfond and
Lifschitz (1988), and answer sets of ordinary HEX programs coincide with stable models of
disjunctive logic programs (Przymusinski 1991; Gelfond and Lifschitz 1991).

2.3 Using HEX-Programs for Knowledge Representation and Reasoning
While ASP is well-suited for many problems in artificial intelligence and was successfully
applied to a range of applications (cf. e.g. (Brewka et al. 2011)), modern trends computing,
for instance in distributed systems and the World Wide Web, require accessing other sources
of computation as well. HEX-programs cater for this need by its external atoms which
provide a bidirectional interface between the logic program and other sources.
One can roughly distinguish between two main usages of external sources, which we will
call computation outsourcing, knowledge outsourcing, and combinations thereof. However,
we emphasize that this distinction concerns the usage in an application but both are based
on the same syntactic and semantic language constructs. For each of these groups we will
describe some typical use cases which serve as usage patterns for external atoms when
writing HEX-programs.

2.3.1 Computation Outsourcing
Computation outsourcing means to send the definition of a subproblem to an external
source and retrieve its result. The input to the external source uses predicate extensions and
constants to define the problem at hand and the output terms are used to retrieve the result,
which can in simple cases also be a Boolean decision.
On-demand Constraints A special case of the latter case are on-demand constraints of type
← &forbidden[p1 , . . . , pn ]() which eliminate certain extensions of predicates p1 , . . . , pn .
Note that the external evaluation of such a constraint can also return reasons for conflicts
to the reasoner in order to restrict the search space and avoid reconstruction of the same
conflict (Eiter et al. 2012). This is similar to the CEGAR approach in model checking (Clarke
et al. 2003) and can be helpful for reducing the size of the ground program: constraints do
not need to be grounded but they are outsourced into an external atom of the above form,
which then returns violated constraints as nogoods to the solver. This technique has been

8

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

used for efficient planning in robotics where external atoms verify the feasibility of a 3D
motion (Schüller et al. 2013).
Computations which cannot (easily) be Expressed by Rules Outsourcing computations
also allows for including algorithms which cannot easily or efficiently be expressed as a
logic program, e.g., because they involve floating-point numbers. As a concrete example,
an artificial intelligence agent for the skills and tactics game AngryBirds needs to perform
physics simulations (Calimeri et al. 2013). As this requires floating point computations
which can practically not be done by rules as this would either come at the costs of very
limited precision or a blow-up of the grounding, HEX-programs with access to an external
source for physics simulations are used.
Complexity Lifting External atoms can realize computations with a complexity higher than
the complexity of ordinary ASP programs. The external atom serves than as an ‘oracle’
for deciding subprograms. While for the purpose of complexity analysis of the formalism
it is often assumed that external atoms can be evaluated in polynomial time (Faber et al.
2004)3 , as long as external sources are decidable there is no practical reason for limiting
their complexity (but of course a computation with greater complexity than polynomial
time lifts the complexity results of the overall formalism as well). In fact, external sources
can be other ASP- or HEX-programs. This allows for encoding other formalisms of higher
complexity in HEX-programs, e.g., abstract argumentation frameworks (Dung 1995).
2.3.2 Knowledge Outsourcing
In contrast, knowledge outsourcing refers to external sources which store information which
needs to be imported, while reasoning itself is done in the logic program.
A typical example can be found in Web resources which provide information for import,
e.g., RDF triple stores (Lassila and Swick 1999) or geographic data (Mosca and Bernini
2008). More advanced use cases are multi-context systems, which are systems of knowledgebases (contexts) that are abstracted to acceptable belief sets (roughly speaking, sets of atoms)
and interlinked by bridge rules that range across knowledge bases (Brewka and Eiter 2007);
access to individual contexts has been provided through external atoms (Bögl et al. 2010).
Also sensor data, as often used when planning and executing actions in an environment, is a
form of knowledge outsourcing (cf. ACTHEX (Basol et al. 2010)).
2.3.3 Combinations
It is also possible to combine the outsourcing of computations and of knowledge. A typical
example are logic programs with access to description logic knowledge bases (DL KBs),
called DL-programs (Eiter et al. 2008). A DL KB does not only store information, but also
provides a reasoning mechanism. This allows the logic program for formalizing queries
which initiate external computations based on external knowledge and importing the results.
3

Under this assumption, deciding the existence of an answer set of a propositional HEX-program is ΣP
2 -complete.

Model building for ASP with external atoms

9

3 Extensional Semantics and Atom Dependencies
We now introduce additional important notions related to HEX-programs. Some of the
following concepts are needed to make the formalism decidable, others prepare the basic
evaluation techniques presented in later sections.

3.1 Restriction to Extensional Semantics for HEX External Atoms
To make HEX programs computable in practice, it is useful to restrict external atoms, such
that their semantics depends only on extensions of predicates given in the input tuple (Eiter
et al. 2006). This restriction is relevant for all subsequent considerations.
Syntax Each &g is associated with an input type signature t1 , . . . , tn such that every ti
is the type of input Yi at position i in the input list of &g. A type is either const or a
non-negative integer.
Consider &g, its type signature t1 , . . . , tn , and a ground external atom &g[y1 , . . . ,
yn ](x1 , . . . , xm ). Then, in this setting, the signature of &g enforces certain constraints on
f&g (I, y1 , . . . , yn , x1 , . . . , xm ) such that its truth value depends only on
(a) the constant value of yi whenever ti = const, and
(b) the extension of predicate yi , of arity ti , in I whenever ti ∈ N.
Note that parameters of type const are different from parameters of type 0. In the former
case, a parameter is interpreted as a constant that is passed to the external source (essentially
as string “p”), while a parameter p with a non-negative integer as type is interpreted as
predicate whose extension is passed; in the special case of type 0, the extension reduces to
the truth value of the propositional atom p.
Example 6 (ctd.)
Continuing Example 1, for &reach[edge, a](x), we have t1 = 2 and t2 = const. Therefore
the truth value of &reach[edge, a](x) depends on the extension of binary predicate edge,
on the constant a, and on x.
Continuing Example 4, the external predicate &rq has t1 = 1, therefore the truth value of
&rq[swim](x) for various x wrt. an interpretation I depends on the extension of the unary
predicate swim in the input list.
Note that the truth value of an external atom with only constant input terms, i.e., ti =
const, 1 ≤ i ≤ n, is independent of I.
Semantic constraints enforced by signatures are formalized next.
Semantics Let a be a type, I be an interpretation and p ∈ C. The projection function
Πa (I, p) is the binary function such that Πconst (I, p) = p for a = const, and Πa (I, p) =
{(p,x1 , . . . , xa ) | p (x1 , . . . , xa ) ∈ I} for a ∈ N. Recall that atoms p(x1 , . . . , xa ) are
tuples (p, x1 , . . . , xa ). The codomain Da of Πa (I, p) is Da := C a+1 for a ∈ N, i.e., the
a+1-fold cartesian product of C, which contains all syntactically possible atoms with a
arguments; furthermore we let Dconst := C.

10

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

Definition 3 (extensional evaluation function)
Let &g be an external predicate with oracle function f&g , in(&g) = n, out(&g) = m, and
type signature t1 , . . . , tn . Then the extensional evaluation function F&g : Dt1 ×· · ·×Dtn →
m
2C of &g is defined such that for every a = (a1 , . . . , am )
a ∈ F&g (Πt1 (I, p1 ), . . . , Πtn (I, pn )) iff f&g (I, p1 , . . . , pn , a1 , . . . , am ) = 1.
Note that F&g makes the possibility of new constants in external atoms more explicit: tuples
returned by F&g may contain constants that are not contained in P . Furthermore, F&g is
well-defined only under the assertion at the beginning of this section.
Example 7 (ctd.)
For I from Example 5, we have Π1 (I, swim) = {(swim, outd )} and
Π1 (I, goto) = {(goto, altD)}. The extensional evaluation function of &rq is
F&rq (U ) = {(money) | (X, ind ) ∈ U or (X, gansD) ∈ U } ∪
{(yogamat) | (X, altD) ∈ U } ∪ {(goggles) | (X, amalB ) ∈ U }
Observe that none of the constants yogamat and goggles occurs in P (we have that
const(P ) = {swim, goto, ngoto, need , go, inoutd , loc, ind , outd , amalB , gansD, altD,
margB , money, location}). These constants are introduced by the external atom semantics.
Note that (money) is a unary tuple, as &rq has a unary output list.
3.2 Atom Dependencies
To account for dependencies between heads and bodies of rules is a common approach for
realizing semantics of ordinary logic programs, as done, e.g., by means of the notions of
stratification and its refinements like local stratification (Przymusinski 1988) or modular
stratification (Ross 1994), or by splitting sets (Lifschitz and Turner 1994). In HEX programs, head-body dependencies are not the only possible source of predicate interaction.
Therefore new types of (non-ground) dependencies were considered by Eiter et al. (2006)
and Schindlauer (2006). In the following we recall these definitions but slightly reformulate
and extend them, to prepare for the following sections where we lift atom dependencies to
rule dependencies.
In contrast to the traditional notion of dependency, which in essence hinges on propositional programs, we must consider non-ground atoms; such atoms a and b clearly depend
on each other if they unify, which we denote by a ∼ b.
For analyzing program properties it is relevant whether a dependency is positive or
negative. Whether the value of an external atom a depends on the presence of an atom b in
an interpretation I depends in turn on the oracle function f&g that is associated with the
external predicate &g of a. Depending on other atoms in I, in some cases the presence of
b might make a true, in some cases its absence. Therefore we will not speak of positive
and negative dependencies, as by Eiter et al. (2011), but more adequately of monotonic and
nonmonotonic dependencies, respectively.4
4

Note that anti-monotonicity (i.e., a larger input of an external atom can only make the external atom false, but
never true) could be a third useful distinction that was exploited in (Eiter et al. 2012). We here only distinguish
monotonic from nonmonotonic external atoms and classify antimonotonic external atoms as nonmonotonic.

Model building for ASP with external atoms

11

Definition 4
An external predicate &g is monotonic, if for all interpretations I, I 0 such that I ⊆ I 0
and all tuples X of constants, f&g (I, X) = 1 implies f&g (I 0 , X) = 1; otherwise &g is
nonmonotonic. Furthermore, a ground external atom a is monotonic, if for all interpretations
I, I 0 such that I ⊆ I 0 we have I |= a implies I 0 |= a; a non-ground external atom is
monotonic, if each of its ground instances is monotonic.
Clearly, each external atom that involves a monotonic external predicates is monotonic,
but not vice versa; thus monotonicity of external atoms is more fine-grained. In the following
formal definitions, for simplicity we only consider external predicate monotonicity and
disregard external atom monotonicity. However the extension to arbitrary monotonic external
atoms is straightforward.
Example 8 (ctd.)
Consider F&rq (U ) in Example 7: adding tuples to U cannot remove tuples from F&rq (U ),
therefore &rq is a monotonic external predicate.
Next we define relations for dependencies from external atoms to other atoms.
Definition 5 (External Atom Dependencies)
Let P be a HEX program, let a = &g[X1 , . . . , Xk ](Y) in P be an external atom with the
type signature t1 , . . . , tk and let b = p(Z) be an atom in the head of a rule in P . Then a
depends external monotonically (resp., nonmonotonically) on b, denoted a →em b (resp.,
a →en b), if &g is monotonic (resp., nonmonotonic), and for some i ∈ {1, . . . , k} we have
that Z has arity ti ∈ Nand Xi = p. We define that a →e b if a →em b or a →en b.
Example 9 (ctd.)
In our example we have the three external dependencies &rq[swim](C) →em swim(ind ),
&rq[swim](C) →em swim(outd ), and &rq[goto](C) →em goto(X).
As in ordinary ASP, atoms in HEX programs may depend on each other because of rules
in the program.
Definition 6
For a HEX-program P and atoms α, β occurring in P , we say that
(a) α depends monotonically on β (α →m β), if one of the following holds:
(i) some rule r ∈ P has α ∈ H(r) and β ∈ B + (r);
(ii) there are rules r1 , r2 ∈ P such that α ∈ B(r1 ), β ∈ H(r2 ), and α ∼ β; or
(iii) some rule r ∈ P has α ∈ H(r) and β ∈ H(r).
(b) α depends nonmonotonically on β (α →n β), if there is some rule r ∈ P such that
α ∈ H(r) and β ∈ B − (r).
Note that combinations of Definitions 5 and 6 were already introduced by Schindlauer
(2006) and Eiter et al. (2009); however these papers represent nonmonotonicity of external
atoms within rule body dependencies and use a single ‘external dependency’ relation that
does not contain information about monotonicity. In contrast, we represent nonmonotonicity
of external atoms where it really happens, namely in dependencies from external atoms to

12

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller
m

swim(ind )

swim(outd )
m
m

e
m

e
m

&rq[swim](C)
m

m

swim(P )
m

need (inoutd , C)

m

m

goto(X)

m

ngoto(X)
m

e
m

&rq[goto](C)

m

m

m
m

need (loc, C)

go

goto(Y )

m

need (X, money)

Fig. 2: Atom dependency graph of running example Pswim .
ordinary atoms. We therefore obtain a simpler dependency relation between rule bodies and
heads.
We say that atom α depends on atom β, denoted α → β, if either α →m β, α →n β, or
α →e β; that is, → is the union of the relations →m , →n , and →e .
We next define the atom dependency graph.
Definition 7
For a HEX-program P , the atom dependency graph ADG(P ) = (VA , EA ) of P has as
vertices VA the (possibly non-ground) atoms occurring in non-facts of P and as edges EA
the dependency relations →m , →n , →em , and →en between them in P .
Example 10 (ctd.)
Figure 2 shows ADG(Pswim ). Recall that c7 is ‘ ← not go’. Note that the nonmonotonic
body literal in c7 does not show up as a nonmonotonic dependency, as c7 has no head atoms.
(The rule dependency graph in Section 4 will make this negation apparent.)
Next we use the dependency notions to define safety conditions on HEX programs.
3.3 Safety Restrictions
To make reasoning tasks on HEX programs decidable (or more efficiently computable), the
following potential restrictions were formulated.
Rule safety This is a restriction well-known in logic programming, and it is required to
ensure finite grounding of a non-ground program. A rule is safe, if all its variables are safe,
and a variable is safe if it is contained in a positive body literal. Formally a rule r is safe iff
variables in H(r) ∪ B − (r) are a subset of variables in B + (r).

Model building for ASP with external atoms

13

Domain-expansion safety In an ordinary logic program P , we usually assume that the set
of constants C is implicitly given by P . In a HEX program, external atoms may invent new
constant values in their output tuples. We therefore must relax this to ‘C is countable and
partially given by P ’, as shown by the following example.
Example 11
In the Swimming Example, grounding Pswim with const(Pswim ) is not sufficient. Further
constants ‘generated’ by external atoms must be considered. For example yogamat ∈
/
const(Pswim ) and I |= &rq[goto](yogamat), hence we must ground
need (loc, C) ← &rq[goto](C)
with C = yogamat to obtain the correct answer set.
Therefore grounding P with const(P ) can lead to incorrect results. Hence we want to
obtain new constants during evaluation of external atoms, and we must use these constants
to evaluate the remainder of a given HEX program. However, to ensure decidability, this
process of obtaining new constants must always terminate.
Hence, we require programs to be domain-expansion safe (Eiter et al. 2006): there must
not be a cyclic dependency between rules and external atoms such that an input predicate of
an external atom depends on a variable output of that same external atom, if the variable is
not guarded by a domain predicate.
With HEX we need the usual notion of rule safety, i.e., a syntactic restriction which
ensures that each variable in a rule only has a finite set of relevant constants for grounding.
We first recall the definition of safe variables and safe rules for HEX.
Definition 8 (Def. 5 by Eiter et al. (2006))
The safe variables of a rule r is the smallest set of variables X that occur either (i) in some
ordinary atom β ∈ B + (r), or (ii) in the output list X of an external atom &g[Y1 , . . . , Yn ](X)
in B + (r) where all Y1 , . . . , Yn are safe. A rule r is safe, if each variable in r is safe.5
However, safety alone does not guarantee finite grounding of HEX programs, because an
external atom might create new constants, i.e., constants not part of the program itself, in its
output list (see Example 7). These constants can become part of the extension of an atom in
the rule head, and by grounding and evaluation of other rules become part of the extension
of a predicate which is an input to the very same external atom.
Example 12 (adapted from Schindlauer (2006))
The following HEX program is safe according to Definition 8 and nevertheless cannot be
finitely grounded:
source(“http : //some url”) ← .
url (X) ← &rdf [source](X, “rdf :subClassOf ”, C).
source(X) ← url (X).
Suppose the &rdf [source](S, P, O) atom retrieves all triples (S, P, O) from all RDF triplestores specified in the extension of source, and suppose that each triplestore contains a
5

This is stated by Eiter et al. (2006) as ‘if each variable appearing in a negated atom and in any input list is safe,
and variables appearing in H(r) are safe’, which is equivalent.

14

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

triple with a URL S that does not show up in another triplestore. As a result, all these URLs
are collected in the extension of source which leads to even more URLs being retrieved and
a potentially infinite grounding.
However, we could change the rule with the external atom to
url (X) ← &rdf [source](X, “rdf :subClassOf ”, C), limit(X)

(3)

and add an appropriate set of limit facts. This addition of a range predicate limit(X) which
does not depend on the external atom output ensures a finite grounding.
To obtain a syntactic restriction that ensures finite grounding for HEX, so called strong
safety has been introduced for the HEX programs (Eiter et al. 2006). Intuitively, this concept
requires all output variables of cyclic external atoms (using the dependency notion from
Definition 7) to be bounded by ordinary body atoms of the same rule which are not part of
the cycle. However, this condition is unnecessarily restrictive, and therefore, the extensible
notion of liberal domain-expansion safety (lde-safety) was introduced by Eiter et al. (2014a),
which we will use in the following. For the purpose of this article, we may omit the formal
details of lde-safety (see Eiter et al. (2014a) and Appendix D for an outline); it is sufficient
to know that every lde-safe program has a finite grounding that has the same answer sets as
the original program.
4 Rule Dependencies and Generalized Rule Splitting Theorem
In this section, we first introduce a new notion of dependencies in HEX-programs, namely
between non-ground rules in a program (Section 4.1). Based on this notion, we then present a
modularity property of HEX-programs that allows us to obtain answer sets of a program from
the answer sets of its components (Section 4.2). The property is formulated as a splitting
theorem based on dependencies among rules and lifts a similar result for dependencies
among atoms, viz. the Global Splitting Theorem (Eiter et al. 2006), to this setting, and
it generalizes and improves it. This result is exploited in a more efficient HEX-program
evaluation algorithm, which we show in Section 5.
4.1 Rule Dependencies
We define rule dependencies as follows.
Definition 9 (Rule dependencies)
Let P be a program and a, b atoms occurring in distinct rules r, s ∈ P . Then r depends on
s according to the following cases:
(i) if a ∼ b, a ∈ B + (r), and b ∈ H(s), then r →m s;
(ii) if a ∼ b, a ∈ B − (r), and b ∈ H(s), then r →n s;
(iii) if a ∼ b, a ∈ H(r), and b ∈ H(s), then both r →m s and s →m r;
(iv) if a →e b, a ∈ B(r) is an external atom, and b ∈ H(s), then
• r →m s if a ∈ B + (r) and a →em b, and
• r →n s otherwise.
Intuitively, conditions (i) and (ii) reflect the fact that the applicability of a rule r depends
on the applicability of a rule s with a head that unifies with a literal in the body of rule

15

Model building for ASP with external atoms
r1 : swim(ind ) ∨ swim(outd ) ←
m

m

r2 : need (inoutd , C) ←
&rq[swim](C)

r3 : goto(X) ∨ ngoto(X) ←
swim(P ), location(P, X)
m
m

m

r5 : need (loc, C) ←
&rq[goto](C)

m

r4 : go ← goto(X)
n

m

c8 : ← need (X, money)

c6 : ← goto(X), goto(Y ), X 6= Y

c7 : ← not go

Fig. 3: Rule dependency graph of running example Pswim .
r; condition (iii) exists because r and s cannot be evaluated independently if they share
a common head atom (e.g., u ∨ v ← cannot be evaluated independently from v ∨ w ←);
and (iv) defines dependencies due to predicate inputs of external atoms.
In the sequel, we let →m,n = →m ∪ →n be the union of monotonic and nonmonotonic
rule dependencies. We next define graphs of rule dependencies.
Definition 10
Given a HEX-program P , the rule dependency graph DG(P ) = (VD , ED ) of P is the
labeled graph with vertex set VD = P and edge set ED = →m,n .
Example 13 (ctd.)
Figure 3 depicts the rule dependency graph of our running example. According to DefiniIDB
tion 9, we have the following rule dependencies in Pswim
:
• due to (i) we have r3 →m r1 , r4 →m r3 , c6 →m r3 , c8 →m r2 , and c8 →m r5 ;
• due to (ii) we have c7 →n r4 ;
• due to (iii) we have no dependencies; and
• due to (iv) we have r2 →m r1 and r5 →m r3 .
Note that if we would omit the first argument of predicate need , we would have in addition
r2 →m r5 and r5 →m r2 due to (iii). Also note that &rq is monotonic (see Example 8).

4.2 Splitting Sets and Theorems
Splitting sets are a notion that allows for describing how a program can be decomposed into
parts and how semantics of the overall program can be obtained from semantics of these
parts in a divide-and-conquer manner.
We lift the original HEX splitting theorem (Eiter et al. 2006, Theorem 2) and the according
definitions of global splitting set, global bottom, and global residual (Eiter et al. 2006,
Definitions 8 and 9) to our new definition of dependencies among rules.
A rule splitting set is a part of a (non-ground) program that does not depend on the rest
of the program. This corresponds in a sense with global splitting sets by Eiter et al. (2006).

16

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

Definition 11 (Rule Splitting Set)
A rule splitting set R for a HEX-program P is a set R ⊆ P of rules such that whenever
r ∈ R, s ∈ P , and r →m,n s, then s ∈ R holds.
Example 14 (ctd.)
The following are some rule splitting sets of Pswim : {r1 }, {r1 , r2 }, {r1 , r3 }, {r1 , r2 , r3 },
{r1 , r2 , r3 , r5 , c8 }. The set R = {r1 , r2 , c8 } is not a rule splitting set, because c8 →m r5
but r5 ∈
/ R.
Because of possible constraint duplication, we no longer partition the input program, and
the customary notion of splitting set, bottom, and residual, is not appropriate for sharing
constraints between bottom and residual. Instead, we next define a generalized bottom of
a program, which splits a non-ground program into two parts which may share certain
constraints.
Definition 12 (Generalized Bottom)
Given a rule splitting set R of a HEX-program P , a generalized bottom B of P wrt. R is
a set B with R ⊆ B ⊆ P such that all rules in B \ R are constraints that do not depend
nonmonotonically on any rule in P \ B.
Example 15 (ctd.)
A rule splitting set R of Pswim (e.g., those given in Example 14) is also a generalized
bottom of Pswim wrt. R. The set {r1 , r2 , c8 } is not a rule splitting set, but it is a generalized
bottom of Pswim wrt. the rule splitting set {r1 , r2 }, as c8 is a constraint that depends only
monotonically on rules in Pswim \ {r1 , r2 , c8 }.
Next, we describe how interpretations of a generalized bottom B of a program P lead to
interpretations of P without re-evaluating rules in B. Intuitively, this is a relaxation of the
previous non-ground HEX splitting theorem: a constraint may be put both in the bottom and
in the residual if it has no nonmonotonic dependencies to the residual. The benefit of such
constraint sharing is a smaller number of answer sets of the bottom, and hence of fewer
evaluations of the residual program.
Notation. For any set I of ground ordinary atoms, we denote by facts(I) the corresponding
set of ground facts; furthermore, for any set P of rules, we denote by gh(P ) the set of
ground head atoms occurring in grnd (P ).
Theorem 1 (Splitting Theorem)
Given a HEX-program P and a rule splitting set R of P , M ∈ AS(P ) iff M ∈ AS(P \ R ∪
facts(X)) with X ∈ AS(R).
Using the definition of generalized bottom, we generalize the above theorem.
Theorem 2 (Generalized Splitting Theorem)
Let P be a HEX-program, let R be a rule splitting set of P , and let B be a generalized
bottom of P wrt. R. Then
M ∈ AS(P ) iff M ∈ AS(P \ R ∪ facts(X)) where X ∈ AS(B).

Model building for ASP with external atoms

17

Note that B \ R contains shareable constraints that are used twice in the Generalized
Splitting Theorem, viz. in computing X and in computing M .
The Generalized Splitting Theorem is useful for early elimination of answer sets of the
bottom thanks to constraints which depend on it but also on rule heads outside the bottom.
Such constraints can be shared between the bottom and the remaining program.
Example 16 (ctd.)
We apply Theorems 1 and 2 to Pswim and compare them. Using the rule splitting set
{r1 , r2 }, we can obtain AS(Pswim ) by first computing AS({r1 , r2 }) = {I1 , I2 } where I1 =
{swim(ind ), need (inoutd , money)}, I2 = {swim(outd )}, and by then using Theorem 1:
X ∈ AS(Pswim ) iff it holds that X ∈ AS({r3 , r4 , r5 , c6 , c7 , c8 } ∪ facts(I1 )) or X ∈
AS({r3 , r4 , r5 , c6 , c7 , c8 } ∪ facts(I2 )). Note that the computation with I1 yields no answer
set, as need (inoutd , money) ∈ I1 satisfies the body of c8 and ‘kills’ any model candidate.
In
 contrast, if we use the generalized bottom {r1 , r2 , c8 }, we have AS({r1 , r2 , c8 }) =
{swim(outd )} and can use Theorem 2 to obtain AS(Pswim ) with only one further answer
set computation: X ∈ AS(Pswim ) iff X ∈ AS({r3 , r4 , r5 , c6 , c7 , c8 } ∪ {swim(outd ) ←}).
Note that we use c8 in both computations, i.e., c8 is shared between the generalized bottom
and the remaining computation.
Armed with the results of this section, we proceed to program evaluation in the next
section. A discussion of the new splitting theorems that compares them to previous related
theorems and argues for their advantage is given in Section 7.1.

5 Decomposition and Evaluation Techniques
We now introduce our new HEX evaluation framework, which is based on selections of sets
of rules of a program that we call evaluation units (or briefly units).
The traditional HEX evaluation algorithm (Eiter et al. 2006) uses a dependency graph
over (non-ground) atoms, and gradually evaluates sets of rules (the ‘bottoms’ of a program)
that are chosen based on this graph. In contrast our new evaluation algorithm exploits the
rule-based modularity results for HEX-programs in Section 4.
While previously a constraint can only kill models once all its dependencies on rules
are fulfilled, the new algorithm increases evaluation efficiency by sharing non-ground
constraints, such that they may kill models earlier; this is safe if all their nonmonotonic
dependencies are fulfilled. Moreover, units no longer must be maximal. Instead, we require
that partial models of units, i.e., atoms in heads of their rules, do not interfere with those of
other units. This allows for independence, efficient storage, and easy composition of partial
models of distinct units.
In the following, we first define a decomposition of a HEX-program into evaluation units
that are organized in an evaluation graph (Section 5.1). Then we define an interpretation
graph which contains input and output interpretations of each evaluation unit (Section 5.2).
We next extend this definition to answer set graphs which are related with answer sets of
the program (Section 5.3). Finally Section 5.4 uses these definitions in an algorithm for
enumerating answer sets of the HEX-program.

18

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller
5.1 Evaluation Graph

Using rule dependencies, we next define the notion of evaluation graph on evaluation units.
We then relate evaluation graphs to splitting sets (Lifschitz and Turner 1994) and show how
to use them to evaluate HEX-programs by evaluating units and combining the results.
We define evaluation units as follows.
Definition 13
An evaluation unit (in short ‘unit’) is any lde-safe HEX-program.
The formal definition of lde-safety (see Appendix D and Eiter et al. (2014a)) is not crucial
here, merely the property that a unit has a finite grounding with the same answer sets as
the original unit which can be effectively computed; lde-safe HEX-programs are the most
general class of HEX-programs with this property and computational support.
An important point of the notion of evaluation graph is that rule dependencies r →x s lead
to different edges, i.e., unit dependencies, depending on the dependency type x ∈ {n, m}
and whether r resp. s is a constraint; constraints cannot (directly) make atoms true, hence
they can be shared between units in certain cases, while sharing non-constraints could
violate modularity.
Given a rule r ∈ P and a set U of units, we denote by U |r = {u ∈ U | r ∈ u} the set of
units that contain rule r.
Definition 14 (Evaluation graph)
An evaluation graph E = (U, E) of a program P is a directed acyclic graph whose vertices
U are evaluation units and which fulfills the following properties:
S
(a) P = u ∈ U u, i.e., every rule r ∈ P is contained in at least one unit;
(b) every non-constraint r ∈ P is contained in exactly one unit, i.e., U |r = 1;
(c) for each nonmonotonic dependency r →n s between rules r, s ∈ P and for all
u ∈ U |r , v ∈ U |s , u 6= v, there exists an edge (u, v) ∈ E (intuitively, nonmonotonic
dependencies between rules have corresponding edges everywhere in E); and
(d) for each monotonic dependency r →m s between rules r, s ∈ P , there exists some
u ∈ U |r such that E contains all edges (u, v) with v ∈ U |s for v 6= u (intuitively, for
each rule r there is (at least) one unit in E where all monotonic dependencies from r to
other rules have corresponding outgoing edges in E).
We remark that Eiter et al. (2011) and Schüller (2012) defined evaluation units as
extended pre-groundable HEX-programs; later, Redl (2014) and Eiter et al. (2014a) defined
generalized evaluation units as lde-safe HEX-programs, which subsume extended pregroundable HEX-programs, and generalized evaluation graphs on top as in Definition 14.
As more the grounding properties of units matter than the precise fragment, we dropped
here ‘generalized’ to avoid complex terminology.
As a non-constraint can occur only in a single unit, the above definition implies that all
dependencies of non-constraints have corresponding edges in E, which is formally expressed
in the following proposition.

Model building for ASP with external atoms

19

r1 : swim(ind ) ∨ swim(outd ) ← .
r3 : goto(X) ∨ ngoto(X) ← swim(P ), location(P, X).
r : go ← goto(X).
u1 4
c6 : ← goto(X), goto(Y ), X 6= Y.
c7 : ← not go.
derives: swim(X), goto(X), ngoto(X), go
r2 : need (inoutd , C) ← &rq[swim](C).
u2 r5 : need (loc, C) ← &rq[goto](C).
derives: need (A, B)
u3

c8 : ← need (X, money).
derives nothing

Fig. 4: Evaluation graph E1 for running example HEX program Pswim .
u1

r1 : swim(ind ) ∨ swim(outd ) ←.
derives: swim(X)

r2 : need (inoutd , C) ←&rq[swim](C).
u2 c8 : ← need (X, money).
derives: need (inoutd , C)

r3 : goto(X) ∨ ngoto(X) ←
swim(P ), location(P, X).
r4 : go ← goto(X).
u3
c6 : ← goto(X), goto(Y ), X 6= Y.
c7 : ← not go.
derives: goto(X), ngoto(X), go

r5 : need (loc, C) ← &rq[goto](C).
u4 c8 : ← need (X, money).
derives: need (loc, C)

Fig. 5: Evaluation graph E2 for running example HEX program Pswim .
Proposition 1
Let E = (U, E) be an evaluation graph of a program P , and assume r →m,n s is a
dependency between a non-constraint r ∈ P and a rule s ∈ P . Then {(u, v) | u ∈ U |r , v ∈
U |s } ⊆ E holds.
Example 17 (ctd.)
Figures 4 and 5 show two possible evaluation graphs for our running example. The evaluation
graph E1 contains every rule of Pswim in exactly one unit. In contrast, E2 contains c8 both
in u2 and in u4 . Condition (d) of Definition 14 is particularly interesting for these two
graphs; it is fulfilled as follows. Graph E1 can be obtained by contracting rules in the rule
dependency graph DG(Pswim ) into units, i.e., E1 is a (graph) minor of DG(Pswim ) and
therefore all rule dependencies are realized as unit dependencies and Conditions (c) and (d)
are satisfied. In contrast, E2 is not a minor of DG(Pswim ) because dependency c8 →m r5
is not realized as a dependency from u2 to u4 . Nonetheless, all dependencies from c8 are
realized at u4 and thus E2 conforms with condition (d), which merely requires that rule

20

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

dependencies have edges corresponding to all monotonic rule dependencies at some unit of
the evaluation graph.
Evaluation graphs have the important property that partial models of evaluation units do
not intersect, i.e., evaluation units do not mutually depend on each other. This is achieved
by acyclicity and because rule dependencies are covered in the graph.
In fact, due to acyclicity, mutually dependent rules of a program are contained in the
same unit; thus each strongly connected component of the program’s dependency graph is
fully contained in a single unit. Furthermore, a unit can have in its rule heads only atoms
that do not unify with atoms in the rule heads of other units, as rules which have unifiable
heads mutually depend on one another. This ensures that under any grounding, the following
property holds.
Proposition 2 (Disjoint unit outputs)
Let E = (U, E) be an evaluation graph of a program P . Then for each distinct units
u1 , u2 ∈ U , it holds that gh(u1 ) ∩ gh(u2 ) = ∅.6
Example 18 (ctd.)
Figures 4 and 5 show for each unit which atoms can become true due to rule heads in them,
denoted as ‘derived’ atoms. Observe that both graphs have strictly non-intersecting atoms
in rule heads of distinct units.
As units of evaluation graphs can be arbitrary lde-safe programs, we clearly have the
following property.
Proposition 3
For every lde-safe HEX program P , some evaluation graph E exists.
Indeed, we can simply put P into a single unit to obtain a valid evaluation graph. Thus the
HEX evaluation approach based on evaluation graphs is applicable to all domain-expansion
safe HEX programs.

5.1.1 Evaluation Graph Splitting
We next show that units and their predecessors in an evaluation graph correspond to
generalized bottoms. We then use this property to formulate an algorithm for unit-based,
efficient evaluation of HEX-programs.
Given an evaluation graph E = (U, E), we write u < w, if a path from u to w exists in E,
and u ≤ w if either u < w or u = w.
For a unit u ∈ U , we denote by preds E (u) = {v ∈ U | (u, v) ∈ E} the set of units on
S
which u (directly) depends and by u< = w∈U,u<w w the set of rules in all units on which
u transitively depends; furthermore, we let u≤ = u< ∪ u. Note that for a leaf unit u (i.e., u
has no predecessors) we have preds E (u) = u< = ∅ and u≤ = u.

6

See page 16 for the definition of notation gh(P ).

Model building for ASP with external atoms

21

g

f
e
c

fai(b) = {e}
d

b

fai(a) = {d, e}
a

Fig. 6: First Ancestor Intersection units (FAIs) in an evaluation graph.
Theorem 3
For every evaluation graph E = (U, E) of a HEX-program Q and unit u ∈ U , it holds that
u< is a generalized bottom of u≤ wrt. R = {r ∈ u< | H(r) 6= ∅}.
Example 19 (ctd.)
≤
≤
<
In E1 , u<
2 = u1 and u2 = u1 ∪ u2 and u2 is a generalized bottom of u2 wrt. R =
≤
<
{r1 , r3 , r4 }. In E2 , we have u<
4 = u1 ∪ u2 ∪ u3 and u4 = Pswim and u4 is a generalized
bottom of Pswim wrt. R = {r1 , r2 , r3 , r4 }. We can verify this on Definition 12: we have
P = Pswim , B = u<
4 = {r1 , r2 , r3 , r4 , c6 , c7 , c8 }, and R as above. Then R ⊆ B ⊆ P ,
and furthermore B \ R = {c6 , c7 , c8 } consists of constraints none of which depends
nonmonotonically on a rule in P \ B = {r5 }.
Theorem 4
Let E = (U, E) be an evaluation graph of a HEX-program Q and u ∈ U . Then for every
unit u0 ∈ preds E (u), it holds that u0≤ is a generalized bottom of the subprogram u< wrt.
the rule splitting set R = {r ∈ u0≤ | H(r) 6= ∅}.
Example 20 (ctd.)
In E1 , we have u1 ∈ preds E1 (u2 ); hence u≤
1 = u1 is by Theorem 4 a generalized bottom of
u<
=
u
wrt.
R
=
{r
,
r
,
r
}.
Furthermore,
u2 ∈ preds E1 (u3 ) and hence u≤
1
1 3 4
2
2 = u1 ∪ u2
<
is a generalized bottom of u3 = u1 ∪ u2 wrt. R = {r1 , r2 , r3 , r4 , r5 }. The case of E2 and u4
is less clear. We have u2 ∈ preds E2 (u4 ), thus by Theorem 4 u≤
2 = u1 ∪ u2 = {r1 , r2 , c8 }
is a generalized bottom of u<
=
u
∪
u
∪
u
wrt.
R
=
{r
1
2
3
1 , r2 }. Comparing against
4
Definition 12, we have P = u1 ∪ u2 ∪ u3 and B = u1 ∪ u2 ; thus indeed R ⊆ B ⊆ P
and no constraint in B \ R = {c8 } depends nonmonotonically on any rule in P \ B =
{r3 , r4 , c6 , c7 }.
5.1.2 First Ancestor Intersection Units
We will use the evaluation graph for model building; as syntactic dependencies reflect
semantic dependencies between units, multiple paths between units require attention. Of
particular importance are first ancestor intersection units, which are units where distinct
paths starting at some unit meet first. More formally,

22

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

Definition 15
Given an evaluation graph E = (U, E) and units v 6= w ∈ U , we say that unit w is a first
ancestor intersection unit (FAI) of v, if paths p1 6= p2 from v to w exist in E that overlap
only in v and w. By fai (v) we denote the set of all FAIs of v.
Example 21
Figure 6 sketches an evaluation graph with dependencies a → b → c → e → f , a → d →
e → g, and b → d. We have that fai (a) = {d, e}, fai (b) = {e}, and fai (u) = ∅ for each
u ∈ U \ {a, b}. In particular, f and g are not FAIs of b, because all pairs of distinct paths
from b to f or g overlap in more than two units.
Note that for tree-shaped evaluation graphs, fai (v) = ∅ for each unit v as paths between
nodes in a tree are unique.
Example 22 (ctd.)
The evaluation graph E1 of Pswim is a tree (see Fig. 4), thus fai (u) = ∅ for u ∈ {u1 , u2 , u3 }.
In contrast, the evaluation graph E2 of Pswim (see Fig. 5) is not a tree; we have that
fai (u4 ) = {u1 } and no other unit in E2 has FAIs.
We can build an evaluation graph E for a program P based on the dependency graph
DG(P ). Initially, the units are set to the maximal strongly connected components of
DG(P ), and then units are iteratively merged while preserving acyclicity and the conditions
(a)-(d) of an evaluation graph; we will discuss some existing heuristics in Section 6.2, while
for details we refer to Redl (2014).
5.2 Interpretation Graph
We now define the Interpretation Graph (short i-graph), which is the foundation of our
model building algorithm. An i-graph is a labeled directed graph defined wrt. an evaluation
graph, where each vertex is associated with a specific evaluation unit, a type (input resp.
output interpretation) and a set of ground atoms.
We do not use interpretations themselves as vertices, as distinct vertices may be associated
with the same interpretation; still we call vertices of the i-graph interpretations.
Towards defining i-graphs we first define an auxiliary concept called interpretation
structure. We then define i-graphs as the subset of interpretation structures that obey certain
topological and uniqueness conditions. Finally we present an example (Example 23 and
Figure 8).
Definition 16 (Interpretation Structure)
Let E = (U, E) be an evaluation graph for a program P . An interpretation structure I
for E is a directed acyclic graph I = (M, F, unit, type, int) with nodes M ⊆ Iid from
a countable set Iid of identifiers, edges F ⊆ M × M , and total node labeling functions
unit : M → U , type : M → {I, O}, and int : M → 2HB P .
The following notation will be useful. Given unit u ∈ U in the evaluation graph associated
with an i-graph I, we denote by i -ints I (u) = {m ∈ M | unit(m) = u and type(m) = I} the

Model building for ASP with external atoms

23

input (i-)interpretations, and by o-ints I (u) = {m ∈ M | unit(m) = u and type(m) = O}
the output (o-)interpretations of I at unit u. For every vertex m ∈ M , we denote by
[
int + (m) = int(m) ∪ {int(m0 ) | m0 ∈ M and m0 is reachable from m in I}
the expanded interpretation of m.
Given an interpretation structure I = (M, F, unit, type, int) for E = (U, E) and a unit
u ∈ U , we define the following properties:
(IG-I) I-connectedness: for every m ∈ o-ints I (u), it holds that |{m0 | (m, m0 ) ∈ F }| =
|{m0 ∈ i -ints I (u) | (m, m0 ) ∈ F }| = 1;
(IG-O) O-connectedness: for every m ∈ i -ints I (u), |{mi | (m, mi ) ∈ F }| = |preds E (u)|
and for every ui ∈ preds E (u) we have |{mi ∈ o-ints I (ui ) | (m, mi ) ∈ F }| = 1;
(IG-F) FAI intersection: let E 0 be the subgraph of E on the units reachable from u7 and for
every m ∈ i -ints I (u), let I 0 be the subgraph of I reachable from m. Then I 0 contains
exactly one o-interpretation at each unit of E 0 . (Note that both I and E are acyclic,
hence I 0 does not include m and E 0 does not include u.)
(IG-U) Uniqueness: for every m1 6= m2 ∈ M such that unit(m1 ) = unit(m2 ) = u, we
have int + (m1 ) 6= int + (m2 ) (the expanded interpretations differ).
Definition 17 (Interpretation Graph)
Let E = (U, E) be an evaluation graph for a program P . then an interpretation graph
(i-graph) for E is an interpretation structure I = (M, F, unit, type, int) that fulfills for
every unit u ∈ U the conditions (IG-I), (IG-O), (IG-F), and (IG-U).
Intuitively, the conditions make every i-graph ‘live’ on its associated evaluation graph: an
i-interpretation must conform to all dependencies of the unit it belongs to, by depending
on exactly one o-interpretation at that unit’s predecessor units (IG-O); moreover an o-interpretation must depend on exactly one i-interpretation at the same unit (IG-I). Furthermore,
every i-interpretation depends directly or indirectly on exactly one o-interpretation at each
unit it can reach in the i-graph (IG-F); this ensures that no expanded interpretation int + (m)
‘mixes’ two or more i-interpretations resp. o-interpretations from the same unit. (The effect
of condition (IG-F) is visualized in Figure 7.) Finally, redundancies in an i-graph are ruled
out by the uniqueness condition (IG-U).
Example 23 (ctd.)
Figure 8 shows an interpretation graph I2 for E2 . The unit label is depicted as dashed
rectangle labeled with the respective unit. The type label is indicated after interpretation
names, i.e., m1 /I denotes that interpretation m1 is an input interpretation. For I2 the set
Iid of identifiers is {m1 , . . . , m15 }. The symbol E in a unit u pointing to an i-interpretation
m indicates that there is no o-interpretation wrt. input m of unit u. Section 5.4 describes an
algorithm for building an i-graph given an evaluation graph.
Dependencies are shown as arrows between interpretations. Observe that I-connectedness
(IG-I) is fulfilled, as every o-interpretation depends on exactly one i-interpretation at the
same unit. For example m9 and m10 depend on m7 . O-connectedness (IG-O) is similarly
7

I.e., E 0 is the subgraph of E induced by the set of units reachable from u, including u; in abuse of terminology,
we briefly say ‘the subgraph (of E) reachable from’

24

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

unit
unit dependency

OK!

Violation!

i-interpretation
o-interpretation
dependency

at unit u1

Fig. 7: Interpretation Graphs: violation of the FAI condition on the left, correct situation on
the right.

at unit unit(m)

m1 /I
Key:

∅

m2 /O
{swim(ind )}

m3 /O

m / type(m)
int(m)

{swim(outd )}
at unit u3

at unit u2
m4 /I

m5 /I

int(m2 )

int(m3 )
m6 /O

E

∅

m7 /I

m8 /I

int(m2 )

int(m3 )

m9 /O

{go,
{go,
ngoto(margB ),
ngoto(amalB ),
goto(amalB )}
goto(margB )}

m13 /I
at unit u4

m10 /O

{go, goto(altD), ngoto(gansD)}

m11 /O
{go,
ngoto(gansD),
goto(altD)}

m12 /O
{go,
ngoto(altD),
goto(gansD)}

m14 /I
{go, goto(gansD), ngoto(altD)}

m15 /O
{need (loc, yogamat)}

E

Fig. 8: Interpretation graph I2 for E2 : dashed areas group interpretations according to their
unit(·) value.

fulfilled, in particular consider i-interpretations of u4 in I2 : u4 has two predecessor units
(u2 and u3 ) and every i-interpretation at u4 depends on exactly one o-interpretation at u2
and exactly one o-interpretation at u3 . The condition on FAI intersection (IG-F) could
only be violated by i-interpretations at u4 , concretely it would be violated if two different
o-interpretations are reachable at u1 from one i-interpretation at u4 . We can verify that
from both m13 and m14 we can reach exactly one o-interpretation at each unit; hence the
condition is fulfilled. An example for a violation would be an i-interpretation at u4 that
depends on m6 and m9 : in this case we could reach two distinct o-interpretations m2 and

Model building for ASP with external atoms

25

m3 at u1 , thereby violating (IG-F). Uniqueness (IG-U) is satisfied, as in both graphs no unit
has two output models with the same content.
Note that the empty graph is an i-graph. This is by intent, as our model building algorithm
will progress from an empty i-graph to one with interpretations at every unit, precisely if
the program has an answer set.

5.2.1 Join
We will build i-graphs by adding one vertex at a time, always preserving the i-graph
conditions. Adding an o-interpretation requires to add a dependency to one i-interpretation
at the same unit. Adding an i-interpretation similarly requires addition of dependencies.
However this is more involved because condition (IG-F) could be violated. Therefore, we
next define an operation that captures all necessary conditions.
We call the combination of o-interpretations which yields an i-interpretation a ‘join’.
Formally, the join operation ‘ ./ ’ is defined as follows.
Definition 18
Let I = (M, F, unit, type, int) be an i-graph for an evaluation graph E = (V, E) of a
program P . Let u ∈ V be a unit, let preds E (u) = {u1 , . . . , uk } be the predecessor units
of u, and let mi ∈ o-ints I (ui ), 1 ≤ i ≤ k, be an o-interpretation at ui . Then the join
S
m1 ./ · · · ./ mk = 1≤i≤k int(mi ) at u is defined iff for each u0 ∈ fai (u) the set of
o-interpretations at u0 that are reachable (in F ) from some o-interpretation mi , 1 ≤ i ≤ k,
contains exactly one o-interpretation m0 ∈ o-ints I (u0 ).
Intuitively, a set of interpretations can only be joined if all interpretations depend on the
same (and on a single) interpretation at every unit.
Example 24 (ctd.)
In I2 , i-interpretations m1 , m4 , m5 , m7 , and m8 are created by trivial join operations with
none or one predecessor unit. For m13 and m14 , we have a nontrivial join: int(m13 ) =
int(m6 ) ∪ int(m11 ) and the join is defined because fai (u4 ) = {u1 }, and from m6 and
m11 we can reach in I2 exactly one o-interpretation at u1 . Observe that the join m6 ./ m9
is not defined, as we can reach in I2 from {m6 , m9 } the o-interpretations m2 and m3 at
u1 , and thus more than exactly one o-interpretation at some FAI of u4 . Similarly, the join
m6 ./ m10 is undefined, as we can reach m2 and m3 at u1 .
The result of a join is the union of predecessor interpretations; this is important for answer
set graphs and join operations on them, which comes next. Note that each leaf unit (i.e.,
without predecessors) has exactly one well-defined join result, viz. ∅.
If we add a new i-interpretation from the result of a join operation to an i-graph and
dependencies to all participating o-interpretations, the resulting graph is again an i-graph;
thus the join is sound wrt. to the i-graph properties. Moreover, each i-interpretation that can
be added to an i-graph while preserving the i-graph conditions can be synthesized by a join;
that is, the join is complete for such additions. This is a consequence of the following result.

26

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

Proposition 4
Let I = (M, F, unit, type, int) be an i-graph for an evaluation graph E = (V, E) and u ∈ V
with preds E (u) = {u1 , . . . , uk }. Furthermore, let mi ∈ o-ints I (ui ), 1 ≤ i ≤ k, such that
no vertex m ∈ i -ints I (u) exists such that {(m, m1 ), . . . , (m, mk )} ⊆ F . Then the
join J = m1 ./ · · · ./ mk is defined at u iff I 0 = (M 0 , F 0 , unit 0 , type 0 , int 0 ) is an igraph for E where (a) M 0 = M ∪ {m0 } for some new vertex m0 ∈ Iid \ M , (b) F 0 =
F ∪ {(m0 , mi ) | 1 ≤ i ≤ k}, (c) unit 0 = unit ∪ {(m0 , u)}, (d) type 0 = type ∪ {(m0 , I)},
and (e) int 0 = int ∪ {(m0 , J)}.
Note that the i-graph definition specifies topological properties of an i-graph wrt. an evaluation graph. In the following we extend this specification to the contents of interpretations.
5.3 Answer Set Graph
We next restrict i-graphs to answer set graphs such that interpretations correspond with
answer sets of certain HEX programs that are induced by the evaluation graph.
Definition 19 (Answer Set Graph)
An answer set graph A = (M, F, unit, type, int) for an evaluation graph E = (U, E) is an
i-graph for E such that for each unit u ∈ U , it holds that
(a) {int + (m) | m ∈ i -ints I (u)} ⊆ AS(u< ), i.e., every expanded i-interpretation at u is
an answer set of u< ;
(b) {int + (m) | m ∈ o-ints I (u)} ⊆ AS(u≤ ), i.e., every expanded o-interpretation at u is
an answer set of u≤ ; and
S
(c) for each m ∈ i -ints I (u), it holds that int(m) = (m,mi )∈F int(mi ).
Note that each leaf unit u, has u< = ∅, and thus ∅ is the only i-interpretation possible.
Moreover, condition (c) is necessary to ensure that an i-interpretation at unit u contains all
atoms of answer sets of predecessor units that are relevant for evaluating u. Furthermore,
note that the empty graph is an answer set graph.
Example 25 (ctd.)
The example i-graph I2 is in fact an answer set graph. First, int + (m1 ) = ∅ and u<
1 = ∅
and indeed ∅ ∈ AS(∅) which satisfies condition (a). Less obvious is the case of o-interpretation m6 in I2 : int + (m6 ) = {swim(outd )} and u≤
2 = {r1 , r2 , c8 }; as c8 kills all answer
sets where money is required, AS({r1 , r2 , c8 }) = {{swim(outd )}}; hence int + (m6 ) is
the only expanded interpretation of an o-interpretation possible at u2 . Furthermore, the
condition (IG-U) on i-graphs implies that m6 is the only possible o-interpretation at u2 .
Consider next m13 :
u<
4 = {r1 , r2 , r3 , r4 , c6 , c7 , c8 } and
int + (m13 ) = {go, goto(altD), ngoto(gansD), swim(outd )}.
The two answer sets of u<
4 are {go, goto(altD), ngoto(gansD), swim(outd )}, and {go,
goto(gansD), ngoto(altD), swim(outd )}, and int + (m13 ) is one of them; the other one is
int + (m14 ). Finally
int + (m15 ) = {swim(outd ), goto(altD), go, ngoto(gansD), need (loc, yogamat)},
which is the single answer set of u≤
4 = Pswim .

Model building for ASP with external atoms

27

Similarly as for i-graphs, the join is a sound and complete operation to add i-interpretations to an answer set graph.
Proposition 5
Let A = (M, F, unit, type, int) be an answer set graph for an evaluation graph E = (V, E)
and let u ∈ V with preds E (u) = {u1 , . . . , uk }. Furthermore, let mi ∈ o-ints A (ui ),
1 ≤ i ≤ k, such that no m ∈ i -ints A (u) with {(m, m1 ), . . . , (m, mk )} ⊆ F exists. Then
the join J = m1 ./ · · · ./ mk is defined at u iff A0 = (M 0 , F 0 , unit 0 , type 0 , int 0 ) is an
answer set graph for E where (a) M 0 = M ∪ {m0 } for some new vertex m0 ∈ Iid \ M ,
(b) F 0 = F ∪ {(m0 , mi ) | 1 ≤ i ≤ k}, (c) unit 0 = unit ∪ {(m0 , u)}, (d) type 0 = type ∪
{(m0 , I)}, and (e) int 0 = int ∪ {(m0 , J)}.
Example 26 (ctd.)
Imagine that I2 has no interpretations at u4 . The following candidate pairs of o-interpretations exist for creating i-interpretations at u4 : m6 ./ m9 , m6 ./ m10 , m6 ./ m11 ,
and m6 ./ m12 . A seen in Example 24, m13 = m6 ./ m11 and m14 = m6 ./ m12 are
the only joins at u4 that are defined. In Example 25 we have seen that AS(u<
4) =
{int + (m13 ), int + (m14 )}, and due to (IG-U), we cannot have additional i-interpretations
with the same content.

5.3.1 Complete Answer Set Graphs
We next introduce a notion of completeness for answer set graphs.
Definition 20
Let A = (M, F, unit, type, int) be an answer set graph for an evaluation graph E = (U, E)
and let u ∈ U . Then
• A is input-complete for u, if {int + (m) | m ∈ i -ints A (u)} = AS(u< ), and
• A is output-complete for u, if {int + (m) | m ∈ o-ints A (u)} = AS(u≤ ).
If an answer set graph is complete for all units of its corresponding evaluation graph,
answer sets of the associated program can be obtained as follows.
Theorem 5
Let E = (U, E), where U = {u1 , . . . , un }, be an evaluation graph of a program P , and let
A = (M, F, unit, type, int) be an answer set graph that is output-complete for every unit
u ∈ U . Then
nS
o
n
0
AS(P ) =
i=1 int(mi ) | mi ∈ o-ints A (ui ), 1 ≤ i ≤ n, |o-ints A (ui )| = 1 , (4)
where A0 is the subgraph of A consisting of all interpretations that are reachable in A from
some interpretation m1 , . . . , mn .
Example 27 (ctd.)
In I2 we first choose m15 ∈ o-ints(u4 ), which is the only o-interpretation at u4 . The

28

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

subgraph reachable from m15 must contain exactly one o-interpretation at each unit; we
thus must choose every o-interpretations m such that m15 →+ m. Hence we obtain

int(m3 ) ∪ int(m6 ) ∪ int(m11 ) ∪ int(m15 )

= {swim(outd )} ∪ ∅ ∪ {goto(altD), ngoto(gansD), go} ∪ {need (loc, yogamat)}

= {swim(outd ), goto(altD), ngoto(gansD), go, need (loc, yogamat)}
which is indeed the set of answer sets of Pswim .
The rather involved set construction in (4) establishes a relationship between answer sets
of a program and complete answer set graphs that resembles condition (IG-F) of i-graphs.
To obtain a more convenient way to enumerate answer sets, we can extend an evaluation
graph always with a single void unit ufinal that depends on all other units in the graph (i.e.,
(ufinal , u) ∈ E for each u ∈ U \ {ufinal }), which we call a final unit; the answer sets of P
correspond then directly to i-interpretations at ufinal . Formally,
Proposition 6
Let A = (M, F, unit, type, int) be an answer set graph for an evaluation graph E = (U, E)
of a program P , where E contains a final unit ufinal , and assume that A is input-complete
for U and output-complete for U \ {ufinal }. Then
AS(P ) = {int(m) | m ∈ i -ints A (ufinal )}.

(5)

Expanding i-interpretations at ufinal is not necessary, as ufinal depends on all other units;
thus for every m ∈ i -ints A (ufinal ) it holds that int + (m) = int(m).
We will use the technique with ufinal for our model enumeration algorithm; as the join
condition must be checked anyways, this technique is an efficient and simple method for
obtaining all answer sets of a program using an answer set graph without requesting an
implementation of the conditions in Theorem 5.
5.4 Answer Set Building
Thanks to the results above, we can obtain the answer sets of a HEX-program from any
answer set graph for it. To build an answer set graph, we proceed as follows. We start with
an empty graph, obtain o-interpretations by evaluating a unit on an i-interpretation, and then
gradually generate i-interpretations by joining o-interpretations of predecessor units in an
evaluation graph at hand.
Towards an algorithm for evaluating a HEX-program based on an evaluation graph, we
use a generic grounding algorithm G ROUND HEX for lde-safe programs, and a solving
algorithm E VALUATE G ROUND HEX which returns for a ground HEX-program P its answer
sets AS(P ). We assume that they satisfy the following properties.
Property 1
Given an lde-safe program P , G ROUND HEX(P ) returns a finite ground program such that
AS(P ) = AS(G ROUND HEX(P )).
Property 2
Given a finite ground HEX-program P , E VALUATE G ROUND HEX(P ) = AS(P ).

Model building for ASP with external atoms

29

Algorithm 1: E VALUATE LDES AFE
Input: A liberally de-safe HEX-program P , an input interpretation I
Output: All answer sets of P ∪ facts(I) without I
// add input facts and ground, cf. (Eiter et al. 2014a)
P 0 ← G ROUND HEX(P ∪ facts(I))
// evaluate the ground program, cf. (Eiter et al. 2014b),
// and
 perform output projection
return I 0 \ I | I 0 ∈ E VALUATE G ROUND HEX(P 0 )

Concrete such algorithms are given in (Eiter et al. 2014a) and (Eiter et al. 2014b), respectively. Since the details of these algorithms are not relevant for the further understanding of
this paper, we give here only an informal description and refer the interested reader to the
respective papers. The idea of the grounding algorithm is to iteratively extend the grounding
by expanding the set of constants until it is large enough to ensure that it has the same
answer sets as the original program. To this end, the algorithm starts with the constants in
the input program only, and in each iteration of the algorithm it evaluates external atoms a
(finite) number of relevant inputs in order to determine additional relevant constants. Under
the syntactic restrictions recapitulated in the preliminaries, this iteration will reach a fixpoint
after finitely many steps. The solving algorithm is based on conflict-driven clause learning
(CDCL) and lifts the work of Gebser et al. (2012) from ordinary to HEX programs. The main
idea is to learn not only conflict clauses, but also (parts of) the behavior of external sources
while the search space is traversed. The behavior is described in terms of input-output
relations, i.e., certain input atoms and constants lead to a certain output of the external atom.
This information is added to the internal representation of the program such that guesses for
external atoms that violate the known behavior are eliminated in advance.
By composing the two algorithms, we obtain Algorithm 1 for evaluating a single unit.
Formally, it has the following property.
Proposition 7
Given an lde-safe HEX-program P and an input interpretation I, Algorithm 1 returns the set
{I 0 \ I | I 0 ∈ AS(P ∪ facts(I))}, i.e., the answer sets of P augmented with facts for the
input I, projected to the non-input.
We are now ready to formulate an algorithm for evaluating HEX programs that have been
decomposed into an evaluation graph.
To this end, we build first an evaluation graph E and then compute gradually an answer
set graph A = (M, F, unit, type, int) based on E, proceeding along already evaluated units
towards the unit ufinal . Algorithm 2 shows the model building algorithm in pseudo-code,
in which the positive integers N = {1, 2, . . .} are used as identifiers Iid and max(M ) is
maximum in any set M ⊆ N where, by convention, max(∅) = 0. Intuitively, the algorithm
works as follows. The set U contains units for which A is not yet output-complete (see
Definition 20); we start with an empty answer set graph A, thus initially U = V . In each
iteration of the while loop (a), a unit u that is not output-complete and depends only on
output-complete units is selected. The first for loop (c) makes u input-complete; if u is the
final unit, the answer sets are returned in (d), otherwise the second for loop (e) makes u

30

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

Algorithm 2: B UILD A NSWER S ETS
Input: E = (V, E): evaluation graph for HEX program P , which contains a unit ufinal
that depends on all other units in V
Output: a set of all answer sets of P
M := ∅, F := ∅, unit := ∅, type := ∅, int := ∅, U := V
(a)

(b)

(c)

(d)

(e)

(f)

while U 6= ∅ do
choose u ∈ U s.t. preds E (u) ∩ U = ∅
let {u1 , . . . , uk } = preds E (u)
if k = 0 then
m := max (M ) + 1
M := M ∪ {m}
unit(m) := u, type(m) := I, int(m) := ∅
else
for m1 ∈ o-ints(u1 ), . . . , mk ∈ o-ints(uk ) do
if J = m1 ./ · · · ./ mk is defined then
m := max (M ) + 1
M := M ∪ {m}, F := F ∪ {(m, mi ) | 1 ≤ i ≤ k}
unit(m) := u, type(m) := I, int(m) := J
if u = ufinal then
return i -ints(ufinal )
for m0 ∈ i -ints(u) do
O := E VALUATE LDES AFE(u, int(m0 ))
for o ∈ O do
m := max (M ) + 1
M := M ∪ {m}, F := F ∪ {(m, m0 )}
unit(m) := u, type(m) := O, int(m) := o
U := U \ {u}

output-complete, and then u is removed from U . Each iteration makes one unit input- and
output-complete; hence when the algorithm reaches ufinal and makes it input-complete, all
answer sets can directly be returned in (d). Formally, we have
Theorem 6
Given an evaluation graph E = (V, E) of a HEX program P , B UILD A NSWER S ETS(E)
returns AS(P ).
A run of the algorithm on our running example using the evaluation graph E2 extended
with a final unit is given in Appendix B.
5.4.1 Model Streaming
Algorithm B UILD A NSWER S ETS as described above keeps all answer sets in memory, and
it evaluates each unit only once wrt. every possible i-interpretation. This may lead to a

Model building for ASP with external atoms

31

resource bound excess, as in general an exponential number of answer sets respectively
interpretations at evaluation units are possible. However, keeping the whole answer set
graph in memory is not necessary for computing all answer sets.
We have realized a variant of Algorithm B UILD A NSWER S ETS that uses the same principle of constructing an answer set graph, interpretations are created at a unit on demand when
they are requested by units that depend on it; furthermore, the algorithm keeps basically
only one interpretation at each evaluation unit in memory at a time, which means that
interpretations are provided in a streaming fashion one by one, and likewise the answer
sets of the program at the unit ufinal , where the model building starts. Such answer set
streaming is particularly attractive for applications, as one can terminate the computation
after obtaining sufficiently many answer sets. On the other hand, it comes at the cost of
potential re-evaluation of units wrt. the same i-interpretation, as we need to trade space
for time. However, in practice this algorithm works well and is the one used in the dlvhex
prototype. We describe this algorithm in Appendix C.
6 Implementation
In this section we give some details on the implementation of the techniques. Our prototype
system is called dlvhex; it is written in C++ and online available as open-source software.8
The current version 2.4.0 was released in September 2014.
We first describe the general architecture, the major components, and their interplay
(Section 6.1). Then we give an overview about the existing heuristics for building evaluation
graphs (Section 6.2). Experimental results are presented and discussed in Section 6.3. For
details on the usage of the system, we refer to the website; an exhaustive description of the
supported command-line parameters is output when the system is called without parameters.
6.1 System Architecture
The dlvhex system architecture is shown in Figure 9. The arcs model both control and data
flow within the system. The evaluation of a HEX-program works as follows.
First, the input program is passed to the evaluation framework 1 , which creates an
evaluation graph depending on the chosen evaluation heuristics. This results in a number
of interconnected evaluation units. While the interplay of the units is managed by the
evaluation framework, the individual units are handled by model generators of different
kinds.
Each instance of a model generator realizes E VALUATE LDES AFE (Algorithm 1) for a
single evaluation unit, receives input interpretations from the framework (which are either
output by predecessor units or come from the input facts for leaf units), and sends output
interpretations back to the framework 2 , which manages the integration of the latter to
final answer sets and realizes B UILD A NSWER S ETS (Algorithm 2).
Internally, the model generators make use of a grounder and a solver for ordinary ASP
programs. The architecture of our system is flexible and supports multiple concrete backends
that can be plugged in. Currently it supports dlv, gringo 4.4.0 and clasp 3.1.0, as well as an
8

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

32

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

internal grounder and a solver that were built from scratch (mainly for testing purposes); they
use basically the same core algorithms as gringo and clasp, but without optimizations. The
reasoner backends gringo and clasp are statically linked to our system; thus no interprocess
communication is necessary. The model generator within the dlvhex core sends a non-ground
evaluation unit to the HEX-grounder which returns a ground evaluation unit 3 . The HEXgrounder in turn uses one of the above mentioned ordinary ASP grounders as backend 4
and accesses external sources to handle newly introduced constants that are not part of the
input program (called value invention) 5 . The ground evaluation unit is then sent to the
ASP solver and answer sets of the ground unit are returned 6 .
Intuitively, model generators evaluate evaluation units by replacing external atoms by
ordinary ‘replacement’ atoms, guessing their truth value, and making sure that the guesses
are correct with respect to the external oracle functions. To achieve that, the solver backend
needs to make callbacks to the Post Propagator in the dlvhex core during model building.
The Post Propagator checks guesses for external atoms against the actual semantics and
checks the minimality of the answer set. It processes a complete or partial model candidate,
and returns learned nogoods to the external solver 7 as formalized in (Eiter et al. 2012).
The dlv backend calls the Post Propagator only for complete model candidates, the internal
solver and the clasp backend also call it for partial model candidates of evaluation units.
For the clasp backend, we exploit its SMT interface, which was previously used for the
special case of constraint answer set solving (Gebser et al. 2009b). Verifying guesses of
replacement atoms requires calling plugins that implement the external sources (i.e., the
oracle functions F&g from Definition 3) 8 . Moreover, the Post Propagator also ensures
answer set minimality by eliminating unfounded sets that are caused by external sources
and therefore can not be detected by the ordinary ASP solver backend (as shown by Eiter
et al. (2014b)). Finally, as soon as the evaluation framework obtains an i-interpretation of
the final evaluation unit ufinal , this i-interpretation (which is an answer set according to
Proposition 6) is returned to the user 9 .
6.2 Heuristics
As for creating evaluation graphs, several heuristics have been implemented. A heuristics
starts with the rule dependency graph as by Definition 10 and then acyclically combines
nodes into units.
Some heuristics are described in the following.
H0 is a ‘trivial’ heuristics that makes units as small as possible. This is useful for debugging,
however it generates the largest possible number of evaluation units and therefore incurs a
large overhead. As a consequence H0 performs clearly worse than other heuristics and we
do not report its performance in experimental results.
H1 is the evaluation heuristics of the dlvhex prototype version 1. H1 makes units as large
as possible and has several drawbacks as discussed above.
H2 is a simple evaluation heuristics which has the goal of finding a compromise between
the H0 and H1 . It places rules into units as follows:
(i) it puts rules r1 , r2 into the same unit whenever r1 →m,n s and r2 →m,n s for some
rule s and there is no rule t such that exactly one of r1 , r2 depends on t;

33

Model building for ASP with external atoms
dlvhex core
HEX Program

Evaluation
Framework

1

9

Answer
Sets

6

ASP Solver

2

Model
Generators
3

ASP Grounder

4

HEX -Grounder
5

Post
Propagator

7

8

Plugins
Fig. 9: Architecture of dlvhex
(ii) it puts rules r1 , r2 into the same unit whenever s →m,n r1 and s →m,n r2 for some
rule s and there is no rule t such that t depends on exactly one of r1 , r2 ; but
(iii) it never puts rules r, s into the same unit if r contains external atoms and r →m,n s.
Intuitively, H2 builds an evaluation graph that puts all rules with external atoms and their
successors into one unit, while separating rules creating input for distinct external atoms.
This avoids redundant computation and joining unrelated interpretations.
H3 is a heuristics for finding a compromise between (1) minimizing the number of units,
and (2) splitting the program whenever a de-relevant nonmonotonic external atom would
receive input from the same unit. We mention this heuristics only as an example, but
disregard it in the experiments since it was developed in connection with novel ‘liberal’
safety criteria (Eiter et al. 2013) that are beyond the scope of this paper. H3 greedily gives
preference to (1) and is motivated by the following considerations. The grounding algorithm
by Eiter et al. (2014a) evaluates the external sources under all interpretations such that the
set of observed constants is maximized. While monotonic and antimonotonic input atoms
are not problematic (the algorithm can simply set all to true resp. false), nonmonotonic
parameters require an exponential number of evaluations in general. Thus, although program
decomposition is not strictly necessary for evaluating liberally safe HEX-programs, it is still
useful in such cases as it restricts grounding to those interpretations that are actually relevant
in some answer set. However, on the other hand it can be disadvantageous for propositional
solving algorithms such as those in (Eiter et al. 2012).
Program decomposition can be seen as a hybrid between traditional and lazy grounding

34

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

(cf. e.g. Palù et al. (2009)), as program parts are instantiated that are larger than single rules
but smaller than the whole program.
6.3 Experimental Results
In this section, we evaluate the model-building framework empirically. To this end, we
compare the following configurations. In the H1 column, we use the previous state-of-the-art
evaluation method (Schindlauer 2006) before the framework in Section 5 was developed.
This previous method also makes use of program decomposition. However, in contrast to
our new framework, the decomposition is based on atom dependencies rather than rule
dependencies, and the decomposition strategy is hard-coded and not customizable. This
evaluation method corresponds to heuristics H1 in our new framework.
In the w/o framework column, we present the results without application of the framework
using the HEX-program evaluation algorithm by Eiter et al. (2014a) which allows to first
instantiate and then solve the instantiated HEX-program. Note that before this algorithm was
developed, such a ‘two-phase’ evaluation was not possible since program decomposition was
necessary for grounding purposes. With the algorithm in (Eiter et al. 2014a), decomposition
is not necessary anymore, but can still be useful as the results in the H2 column shows,
which correspond to the results when applying the heuristics H2 described above.
The configuration of the grounding algorithm and the solving algorithm (e.g., conflictdriven learning strategies) also influence the results. Moreover, in addition to the default
heuristics of framework, other heuristics have been developed as well and the best selection
of the heuristics often depends on the configuration of the grounding and the solving
algorithm. Since they were used as black boxes in Algorithm 1, an exhaustive experimental
analysis of the system is beyond the scope of this paper and would require an in-depth
description of these algorithms. Thus, we confine the discussion to the default settings, which
suffices to show that the new framework can speed up the evaluation significantly. The only
configuration difference between the result columns H1 and H2 is the evaluation heuristics,
all other parameters are equal. Evaluating the w/o framework column requires the grounding
algorithm from (Eiter et al. 2014a) instead of evaluation via decomposition, therefore w/o
framework does not use any heuristics. The solver backend (clasp) configuration is the same
in H1, H2, and w/o framework. We use the streaming algorithm (see Appendix C) in all
experiments. For an in depth discussion, we refer to Eiter et al. (2014b; 2014a) and Redl
(2014), where the efficiency was evaluated using a variety of applications including planning
tasks (e.g., robots searching an unknown area for an object, tour planning), computing
extensions of abstract argumentation frameworks, inconsistency analysis in multi-context
systems, and reasoning over description logic knowledge bases.
We discuss here two benchmark problems, which we evaluated on a Linux server with
two 12-core AMD 6176 SE CPUs with 128GB RAM running dlvhex version 2.4.0. and an
HTCondor load distribution system9 that ensures robust runtimes. The HTCondor system
ensures that multiple runs of the same instance have negligible deviations in the order of
fractions of a second, thus we can restrict the experiments to one run. The grounder and
solver backends for all benchmarks are gringo 4.4.0 and clasp 3.1.1. For each instance, we
9

http://research.cs.wisc.edu/htcondor

35

Model building for ASP with external atoms
Topology and
Instance Size

H1

d-7-7-3-3 (10)
d-7-7-4-4 (10)
d-7-7-5-5 (10)
h-9-9-3-3 (10)
h-9-9-4-4 (10)
r-7-7-4-4 (10)
r-7-7-5-5 (10)
r-7-8-5-5 (10)
r-7-9-5-5 (10)
r-8-7-5-5 (10)
r-8-8-5-5 (10)
z-7-7-3-3 (10)
z-7-7-4-4 (10)
z-7-7-5-5 (10)

1.23 (0)
18.43 (0)
94.18 (1)
83.17 (1)
389.74 (6)
39.27 (0)
389.88 (6)
226.04 (3)
355.37 (5)
502.64 (8)
390.81 (6)
2.34 (0)
33.32 (0)
164.33 (2)

First Answer Set
w/o framework
0.29 (0)
1.09 (0)
3.60 (0)
3.77 (0)
30.56 (0)
2.82 (0)
105.80 (1)
25.11 (0)
145.99 (2)
329.47 (5)
201.08 (3)
0.32 (0)
1.58 (0)
12.69 (0)

H2

H1

0.38 (0)
0.76 (0)
1.52 (0)
0.70 (0)
2.14 (0)
0.33 (0)
0.93 (0)
0.57 (0)
0.87 (0)
1.21 (0)
1.00 (0)
0.44 (0)
1.07 (0)
3.52 (0)

4.93 (0)
50.78 (0)
289.35 (4)
300.96 (4)
555.94 (9)
366.17 (5)
600.00 (10)
541.80 (9)
600.00 (10)
555.26 (9)
600.00 (10)
9.17 (0)
182.44 (2)
502.49 (8)

All Answer Sets
w/o framework
0.76 (0)
3.39 (0)
20.21 (0)
28.67 (0)
335.11 (5)
57.26 (0)
377.37 (5)
317.64 (5)
458.14 (7)
443.15 (7)
495.41 (8)
1.13 (0)
9.00 (0)
89.01 (1)

H2
0.79 (0)
1.80 (0)
4.97 (0)
2.11 (0)
12.56 (0)
2.06 (0)
4.39 (0)
3.99 (0)
5.42 (0)
5.84 (0)
5.38 (0)
1.00 (0)
2.67 (0)
6.90 (0)

Table 1: MCS experiments: variable topology (d, h, r, z) and instance size.

limited the CPU usage to two cores and 8GB RAM. The timeout for each instance was 600
seconds. Each line shows the average runtimes over all instances of a certain size, where
each timeout counts as 600 seconds. While instances usually become harder with larger
size, there might be some exceptions due to the randomly generated instances; however, the
overall trend shows that runtimes increase with the instance size. Numbers in parentheses
are the numbers of instances of respective size in the leftmost column and the numbers of
timeout instances elsewhere. The generators, instances and external sources are available at
http://www.kr.tuwien.ac.at/research/projects/hexhex/hexframework.

6.3.1 Multi-Context Systems (MCS)
The MCS benchmarks originate in the application scenario of enumerating output-projected
equilibria (i.e., global models) of a given multi-context system (MCS) (cf. Section 2.3.2).
Each instance comprises 7–9 contexts (propositional knowledge bases) whose local semantics is modeled by external atoms; roughly speaking, they single out assignments to the
atoms of a context occurring in bridge rules such that local models exist. For each context,
5–10 such atoms are guessed and bridge rules, which are modeled by ordinary rules, are
randomly constructed on top. The MCS instances were generated using the DMCS (Bairakdar et al. 2010) instance generator, with 10 randomized instances for different link structure
between contexts (diamond (d), house (h), ring (r), zig-zag (z)) and system size; they have
between 4 and about 20,000 answer sets, with an average of 400. We refer to (Bairakdar
et al. 2010) and (Schüller 2012) for more details on the benchmarks and the HEX-programs.
Table 1 shows the experimental results: computation with the old method H1 often
exceeds the time limit, while the new method H2 manages to enumerate all solutions of all
instances. Monolithic evaluation without decomposition shows a performance between the
old and new method. These results show that our new evaluation method is essential for
using HEX to computationally realize the MCS application.

36

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller
Instance Size
H1
1 (1)
2 (1)
3 (1)
4 (1)
5 (1)
6 (1)
7 (1)
8 (1)
9 (1)
10 (1)
11 (1)
12 (1)
13 (1)
14 (1)
15 (1)
16 (1)
17 (1)
18 (1)
19 (1)
20 (1)
21 (1)

2.84 (0)
6.13 (0)
10.18 (0)
15.92 (0)
26.06 (0)
47.06 (0)
92.76 (0)
198.59 (0)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)

First Answer Set
w/o framework
3.14 (0)
7.18 (0)
12.30 (0)
18.66 (0)
28.47 (0)
45.71 (0)
79.41 (0)
155.10 (0)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)

H2

H1

2.78 (0)
4.90 (0)
8.32 (0)
12.12 (0)
17.17 (0)
23.39 (0)
31.19 (0)
37.85 (0)
46.61 (0)
57.48 (0)
68.98 (0)
84.41 (0)
99.55 (0)
117.39 (0)
138.45 (0)
163.12 (0)
184.99 (0)
208.83 (0)
236.98 (0)
267.54 (0)
600.00 (1)

2.73 (0)
6.05 (0)
10.25 (0)
15.86 (0)
26.23 (0)
46.84 (0)
96.56 (0)
199.74 (0)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)

All Answer Sets
w/o framework
3.14 (0)
7.17 (0)
12.35 (0)
18.85 (0)
28.35 (0)
45.62 (0)
79.82 (0)
155.26 (0)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)
600.00 (1)

H2
2.79 (0)
4.88 (0)
8.37 (0)
12.16 (0)
17.06 (0)
23.26 (0)
31.04 (0)
38.06 (0)
46.75 (0)
57.40 (0)
69.45 (0)
84.11 (0)
99.52 (0)
117.15 (0)
137.51 (0)
158.43 (0)
181.94 (0)
210.82 (0)
237.45 (0)
268.60 (0)
600.00 (1)

Table 2: RST RACK experiments: variable number of conference tracks, single answer set.
6.3.2 Reviewer Selection (RS)
Our second benchmark is Reviewer Selection (RS): we represent c conference tracks, r
reviewers and p papers. Papers and reviewers are assigned to conference tracks, and there
are conflicts between reviewers and papers, some of which are given by external atoms. We
consider two scenarios: RST RACK and RSPAPER. They are designed to measure the effect
of external atoms on the elimination of a large number of answer set candidates; in contrast
to the MCS experiments we can control this aspect in the RS experiments.
In RST RACK we vary the number c of conference tracks, where each track has 20 papers
and 20 reviewers. Each paper must get two reviews, and no reviewer must get more than
two papers. Conflicts are dense such that only one valid assignment exists per track, hence
each instance has exactly one answer set, and in each track two conflicts are external. For
each number c there is only one instance because RST RACK instances are not randomized.
The results of RST RACK are shown in Table 2: runtimes of the old evaluation heuristics
(H1 ) grow fastest with size, without using decomposition grows slightly slower but also
reaches timeout at size 9. Only the new decomposition (H2 heuristics) can deal with size 20
without timeout. Finding the first answer set and enumerating all answer sets show very
similar times, as RST RACK instances have a single answer set and finding it seems hard.
In RSPAPER we fix the number of tracks to c = 5; we vary the number p of papers in each
track and set the number of reviewers to r = p. Each paper must get three reviews and each
reviewer must not get more than three papers assigned. Conflicts are randomized and less
dense than in RST RACK: the number of answer sets is greater than one and does not grow
with the instance size. Over all tracks and papers, 2p randomly chosen conflicts are external,
and we generate 10 random instances per size and report results averaged per instance size
in Table 3. As clearly seen, our new method is always faster than the other methods, and

37

Model building for ASP with external atoms
Instance Size
H1
5 (10)
8 (10)
11 (10)
14 (10)
17 (10)
20 (10)
23 (10)
26 (10)
29 (10)
32 (10)
35 (10)
38 (10)
41 (10)
44 (10)
47 (10)
50 (10)

1.06 (0)
8.76 (0)
108.70 (1)
180.99 (2)
418.92 (6)
485.35 (8)
542.03 (9)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)

First Answer Set
w/o framework
0.28 (0)
2.73 (0)
83.26 (1)
125.83 (1)
364.95 (5)
453.39 (7)
508.75 (8)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)

H2

H1

0.21 (0)
0.38 (0)
0.98 (0)
2.08 (0)
5.15 (0)
7.32 (0)
13.91 (0)
33.20 (0)
60.78 (0)
129.95 (0)
136.84 (0)
308.92 (3)
421.69 (6)
470.61 (7)
485.60 (7)
485.07 (7)

2.25 (0)
14.73 (0)
171.01 (2)
299.22 (4)
549.01 (9)
507.66 (8)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)

All Answer Sets
w/o framework

H2

0.43 (0)
4.54 (0)
104.84 (1)
245.62 (3)
513.21 (8)
501.74 (8)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)
600.00 (10)

0.23
0.44
1.28
2.67
8.14
14.45
23.16
154.51
108.03
315.56
302.90
441.06
529.80
553.19
529.00
526.66

(0)
(0)
(0)
(0)
(0)
(0)
(0)
(2)
(0)
(4)
(3)
(6)
(8)
(9)
(8)
(8)

Table 3: RSPAPER experiments: variable number of papers/reviewers, multiple answer sets,
randomized.

evaluation without a decomposition framework performs slightly better than the old method.
Different from RST RACK, we can see a clear difference between finding the first answer
set and enumerating all answer sets as RSPAPER instances have more than one answer set.
To confirm that the new method is geared towards handling many external atoms, we
conducted also experiments with instances that had few external atoms for eliminating
answer set candidates but many local constraints. For such highly constrained instances, the
new decomposition framework is not beneficial as it incurs an overhead compared to the
monolithic evaluation that increases runtimes.

6.3.3 Summary
The results demonstrate a clear improvement using the new framework; they can often be
further improved by fine-tuning the grounding and solving algorithm, and by customizing
the default heuristics of the framework, as discussed by Eiter et al. (2014b; 2014a), and
Redl (2014). However, already the default settings yield results that are significantly better
than using the previous evaluation method or using no framework at all; note that the latter
requires an advanced grounding algorithm as by Eiter et al. (2014a), which was not available
at the time the initial evaluation approach as by Schindlauer (2006) was developed.
In conclusion, the evaluation framework in Section 5 pushes HEX-programs towards
scalability for realistic instance sizes, which previous evaluation techniques missed.

7 Related Work and Discussion
We now discuss our results in the context of related work, and will address possible
optimizations.

38

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller
7.1 Related Work

We first discuss related approaches for integrating external reasoning into ASP formalisms,
then we discuss work related to the notion of rule dependencies that we introduced in
Section 4.1, we discuss related notions of modularity and program decomposition. Finally
we relate our splitting theorems to other splitting theorems in the literature.

7.1.1 External Sources
The dlv-ex system (Calimeri et al. 2007) was a pioneering work on value invention through
external atoms in ASP. It supported VI-restricted programs, which amount to HEX-programs
under extensional semantics without higher-order atoms and a strong safety condition that
is subsumed by lde-safety. Answer set computation followed the traditional approach on top
of dlv, but used a special progressive grounding method (thus an experimental comparison
to solving, i.e., model building as in the focus of this paper, is inappropriate).
With respect to constraint theories and ASP, several works exist. The ACsolver system
(Mellarkod et al. 2008), the Ezcsp system (Balduccini 2009), and the clingcon system (Ostrowski and Schaub 2012) divide the program into ASP-literals and constraint-literals, which
can be seen as a special case of HEX-programs that focuses on a particular external source.
As for evaluation, an important difference to general external sources is that constraint atoms
do not use value invention. The modularity techniques from above are less relevant for this
setting as grounding the overall program in one shot is possible. However, this also fits
into our framework as disabling decomposition in fact corresponds to a dedicated (trivial)
heuristics which keeps the whole program as a single unit. For a detailed comparison
between ACsolver, Ezcsp, and clingcon see (Lierler 2014).
Balduccini and Lierler (2013) also experimentally compared Ezcsp and clingcon while
varying the degree of integration between the constraint solver and the ASP solver backend.
Their ‘black-box integration’ corresponds with dlvhex’s integration of the dlv backend:
external atom semantics are verified by plugins callbacks only when a full answer set
candidates has been found in the backend; moreover their ‘clear-box integration’ corresponds
with dlvhex’s integration of the clasp solver backend: plugin callbacks are part of the CDCL
propagation and can operate on partial answer set candidates. Note that constraint answer
set programs can be realized as a dlvhex-plugin (such an effort is currently ongoing).10
We also remark that gringo and clasp use a concept called ‘external atoms’ for realizing
various applications such as constraint ASP solving as in clingcon and incremental solving (Gebser et al. 2014). However, despite their name they are different from external atoms
in HEX-programs. In the former case, external atoms are excluded from grounding-time
optimization such that these atoms are not eliminated even if their truth value is deterministically false during grounding. This allows to add rules that found truth of such atoms in
later incremental grounding steps. In case of HEX the truth value is determined by external
sources. Moreover gringo contains an interface for Lua and Python functions that can perform computations during grounding. HEX external atoms are more expressive: they cannot

10

http://github.com/hexhex/caspplugin

Model building for ASP with external atoms

39

always be evaluated during grounding because their semantics is defined with respect to the
answer set.
7.1.2 Rule Dependencies
In the context of answer set programming, dependency graphs over rules have been used
earlier, e.g., by Linke (2001) and Linke and Sarsakov (2004). However, these works consider
only ordinary ground programs, and furthermore the graphs are used for characterizing
and computing the answer sets of a program from these graphs. In contrast, we consider
nonground programs with and external atoms, and we use the graph to split the program
into evaluation units with the goal of modularly computing answer sets.
7.1.3 Modularity
Our work is naturally related to work on program modularity under stable model semantics,
as targeted by splitting sets (Lifschitz and Turner 1994) and descendants, with the work
by Oikarinen and Janhunen (2008) and Janhunen et al. (2009) a prominent representative
that lifted them to modular programs with choice rules and disjunctive rules, by considering
‘symmetric splitting’. Other works, e.g., by Lierler and Truszczynski (2013) go further
to define semantics of systems of program modules, departing from a mere semanticspreserving decomposition of a larger program into smaller parts, or consider multi-language
systems that combine modules in possibly different formalisms on equal terms (cf. e.g.
Järvisalo et al. (2009) and Tasharrofi and Ternovska (2011)).
Comparing the works by Oikarinen and Janhunen (2008) and Janhunen et al. (2009) as,
from a semantic decomposition perspective, the closest in this group to ours, an important
difference is that our approach works for non-ground programs and explicitly considers
possible overlaps of modules. It is tailored to efficient evaluation of arbitrary programs,
rather than to facilitate module-style logic programming with declarative specifications,
or to provide compositional semantics for modules beyond uni-lateral evaluation, as done
by Järvisalo et al. (2009) and Tasharrofi and Ternovska (2011); for them, introducing values
outside the module domain (known as value invention) does not play a visible role. In
this regard, it is in line with previous HEX-program evaluation (Eiter et al. 2006) and
decomposition techniques to ground ordinary programs efficiently (Calimeri et al. 2008).
7.1.4 Splitting Theorems
Our new splitting theorems compare to related splitting theorems as follows.
Theorem 1 is similar to Theorem 4.6.2 by Schindlauer (2006); however, we do not use
splitting sets on atoms, but splitting sets on rules. Furthermore, Schindlauer (2006) has no
analog to Theorem 2.
The seminal Splitting Set Theorem by Lifschitz and Turner (1994) divides the interpretation of P into disjoint sets X and Y , where X is an answer set of the ‘bottom’ gb A (P ) ⊆ P
and Y is an answer set of a ‘residual’ program obtained from P \ gb A (P ) and X. In the
residual program, all references to atoms in X are removed, in a way that it semantically
behaves as if facts X were added to P \ gb A (P ), while the answer sets of the residual do

40

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

not contain any atom in X. This works nicely for answer set programs, but it is problematic
when applied to HEX programs, because external atoms may depend on the bottom and
on atoms in heads of the residual program; hence, they cannot be eliminated from rule
bodies. The only way to eliminate bottom facts from the residual program would be to
‘split’ external atoms semantically into a part depending on the bottom and the program
remainder, and by replacing external atoms in rules with external atoms that have been
partially evaluated wrt. a bottom answer set. Technically, this requires to introduce new
external atoms, and formulating a splitting theorem for HEX programs with two disjoint
interpretations X and Y is not straightforward. Furthermore, such external atom splitting
and partial evaluation might not be possible in a concrete application scenario.
Different from the two splitting theorems recalled above, the Global Splitting Theorem
by Eiter et al. (2006) does not split an interpretation of the program P into disjoint interpretations X and Y , and thus should be compared to our Theorem 2. However, the Global
Splitting Theorem does not allow constraint sharing, and it involves a residual program
which specifies how external atoms are evaluated via ‘replacement atoms’, which lead to
extra facts D in the residual program that must be removed from its answer sets. Both the
specification of replacement atoms and the extra facts make the Global Splitting Theorem
cumbersome to work with when proving correctness of HEX encodings. Moreover, the
replacement atoms are geared towards a certain implementation technique which however
is not mandatory and can be avoided.
Lemma 5.1 by Eiter et al. (1997) is structurally similar to our Theorem 2: answer sets
of the bottom program are evaluated together with the program depending on the bottom
(here called the residual), hence answer sets of the residual are answer sets of the original
program. However, the result was based on atom dependencies and did neither consider
negation nor external atoms.
In sumary our new Generalized Splitting Theorem has the following advantages.
• By moving from atom to rule splitting sets, no separate definition of the bottom is
needed, which just becomes the (rule) splitting set.
• As regards HEX-programs, splitting is simple (and not troubled) if all atoms that are
true in an answer set of the bottom also appear in the residual program. Typically, this
is not the case in results from the literature.
• Finally, also the residual program itself is simpler (and easier to construct), by just
dropping rules and adding facts. No rule rewriting needs to be done, and no extra
facts need to be introduced in the residual program nor in the bottom.
The only (negligible) disadvantage of the new theorems is that the answer sets of the bottom
and the residual program may no longer be disjoint; however, each residual answer set
includes some (unique) bottom answer set.
7.2 Possible Optimizations
Evaluation graphs naturally encode parallel evaluation plans. We have not yet investigated
the potential benefits of this feature in practice, but this property allows us to do parallel
solving based on solver software that does not have parallel computing capabilities itself
(‘parallelize from outside’). This applies both to programs with external atoms, as well as to

Model building for ASP with external atoms

41

ordinary ASP programs (i.w., without external atoms). Improving reasoning performance
by decomposition has been investigated by Amir and McIlraith (2005), however, only wrt.
monotonic logics.
Improving HEX evaluation efficiency by using knowledge about domain restrictions of
external atoms has been discussed by Eiter et al. (2009). These rewriting methods yield
partially grounded sets of rules which can easily be distributed into distinct evaluation units
by an optimizer. This directly provides efficiency gains as described in the above work.
As a last remark on possible optimizations, we observe that the data flow between
evaluation units can be optimized using proper notions of model projection, such as in
(Gebser et al. 2009a). Model projections would tailor input data of evaluation units to
necessary parts of intermediate answer sets; however, given that different units might need
different parts of the same intermediate input answer set, a space-saving efficient projection
technique is not straightforward.
8 Conclusion
HEX -programs extend answer set programs with access to external sources through an
API-style interface, which has been fruitfully deployed to various applications. Providing
efficient evaluation methods for such programs is a challenging but important endeavor, in
order to enhance the practicality of the approach and to make it eligible for a broader range
of applications. In this direction, we have presented in this article a novel evaluation method
for HEX-programs based on modular decomposition. We have presented new results for the
latter using special splitting sets, which are more general than previous results and use rule
sets as a basis for splitting rather than sets of atoms as in previous approaches. Furthermore,
we have presented an evaluation framework which employs besides a traditional evaluation
graph that consists of program components and reflects syntactic dependencies among
them, also a model graph whose nodes collect answer sets that are combined and passed on
between components. Using decomposition techniques, evaluation units can be dynamically
formed and evaluated in the framework using different heuristics, Moreover, the answer sets
of the overall program can be produced in a streaming fashion. The new approach leads in
combination with other techniques to significant improvements for a variety of applications,
as demonstrated by Eiter et al. (2014a; 2014b) and Redl (2014). Notably, while our results
target HEX-programs, the underlying concepts and techniques are not limited to them (e.g.,
to separate the evaluation and the model graph) and may be fruitfully transferred to other
rule-based formalisms.

8.1 Outlook
The work we presented can be continued in different directions. As for the prototype
reasoner, a rather straightforward extension is to support brave and cautious reasoning
on top of HEX programs, while incorporating constructs like aggregates or preference
constraints requires more care and efforts. Regarding program evaluation, our general
evaluation framework provides a basis for further optimizations and evaluation strategies.
Indeed, the generic notions of evaluation unit, evaluation graph and model graph allow to
specialize and improve our framework in different respects. First, evaluation units (which

42

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

may contain duplicated constraints), can be chosen according to a proper estimate of the
number of answer sets (the fewer, the better); second, evaluation plans can be chosen by
ad-hoc optimization modules, which may give preference to (a combination of) time, space,
or parallelization conditions. Third, the framework is amenable to a form of coarse-grained
distributed computation at the level of evaluation units (in the style of Perri et al. (2010)).
While modular evaluation is advantageous in many applications, it can also be counterproductive, as currently the propagation of knowledge learned by conflict-driven techniques
into different evaluation units is not possible. In such cases, evaluating the program as a
single evaluation unit is often also infeasible due to the properties of the grounding algorithm, as observed by Eiter et al. (2014a). Thus, another starting point for future work is a
tighter integration of the solver instances used to evaluate different units, e.g., by exchanging
learned knowledge. In this context, also the interplay of the grounder and the solver is an
important topic.
Acknowledgements
We would like to thank the anonymous reviewers and Michael Gelfond for their constructive
feedback.
References
A MIR , E. AND M C I LRAITH , S. A. 2005. Partition-based logical reasoning for first-order and
propositional theories. Artificial Intelligence 162, 1-2, 49–88.
BAIRAKDAR , S. E.-D., DAO -T RAN , M., E ITER , T., F INK , M., AND K RENNWALLNER , T. 2010.
The DMCS solver for distributed nonmonotonic multi-context systems. In European Conference
on Logics in Artificial Intelligence (JELIA). Springer, 352–355.
BALDUCCINI , M. 2009. Representing Constraint Satisfaction Problems in Answer Set Programming.
In Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP).
BALDUCCINI , M. AND L IERLER , Y. 2013. Hybrid Automated Reasoning Tools: from Black-box to
Clear-box Integration. In Answer Set Programming and Other Computing Paradigms (ASPOCP).
17–31.
BASOL , S., E RDEM , O., F INK , M., AND I ANNI , G. 2010. HEX programs with action atoms. In
Technical Communications of the International Conference on Logic Programming (ICLP). 24–33.
B ÖGL , M., E ITER , T., F INK , M., AND S CH ÜLLER , P. 2010. The MCS-IE system for explaining
inconsistency in multi-context systems. In European Conference on Logics in Artificial Intelligence
(JELIA). 356–359.
B REWKA , G. AND E ITER , T. 2007. Equilibria in heterogeneous nonmonotonic multi-context systems.
In AAAI Conference on Artificial Intelligence. AAAI Press, 385–390.
B REWKA , G., E ITER , T., AND T RUSZCZYNSKI , M. 2011. Answer set programming at a glance.
Commun. ACM 54, 12, 92–103.
C ALIMERI , F., C OZZA , S., AND I ANNI , G. 2007. External sources of knowledge and value invention
in logic programming. Annals of Mathematics and Artificial Intelligence 50, 3–4, 333–361.
C ALIMERI , F., C OZZA , S., I ANNI , G., AND L EONE , N. 2008. Computable functions in ASP: Theory
and implementation. In ICLP. LNCS. Springer, 407–424.
C ALIMERI , F., F INK , M., G ERMANO , S., I ANNI , G., R EDL , C., AND W IMMER , A. 2013. AngryHEX: an artificial player for angry birds based on declarative knowledge bases. In National
Workshop and Prize on Popularize Artificial Intelligence. 29–35.

Model building for ASP with external atoms

43

C LARKE , E., G RUMBERG , O., J HA , S., L U , Y., AND V EITH , H. 2003. Counterexample-guided
abstraction refinement for symbolic model checking. J. ACM 50, 5, 752–794.
DAO -T RAN , M., E ITER , T., AND K RENNWALLNER , T. 2009. Realizing default logic over description
logic knowledge bases. In Symbolic and Quantitative Approaches to Reasoning with Uncertainty.
Springer, 602–613.
D UNG , P. M. 1995. On the acceptability of arguments and its fundamental role in nonmonotonic
reasoning, logic programming and n-person games. Artificial Intelligence 77, 2, 321–357.
E ITER , T., F INK , M., I ANNI , G., K RENNWALLNER , T., AND S CH ÜLLER , P. 2011. Pushing efficient
evaluation of HEX programs by modular decomposition. In International Conference on Logic
Programming and Nonmonotonic Reasoning (LPNMR). 93–106.
E ITER , T., F INK , M., AND K RENNWALLNER , T. 2009. Decomposition of Declarative Knowledge
Bases with External Functions. In International Joint Conference on Artificial Intelligence (IJCAI).
AAAI Press, 752–758.
E ITER , T., F INK , M., K RENNWALLNER , T., AND R EDL , C. 2012. Conflict-driven ASP solving with
external sources. Theory and Practice of Logic Programming 12, 4-5, 659–679.
E ITER , T., F INK , M., K RENNWALLNER , T., AND R EDL , C. 2013. Liberal Safety Criteria for
HEX-Programs. In Twenty-Seventh AAAI Conference (AAAI 2013), July 14–18, 2013, Bellevue,
Washington, USA (July 14–18, 2013), M. desJardins and M. Littman, Eds. AAAI Press. To appear.
E ITER , T., F INK , M., K RENNWALLNER , T., AND R EDL , C. 2014a. Domain expansion for ASPprograms with external sources. Tech. Rep. INFSYS RR-1843-14-02, Institut für Informationssysteme, Technische Universität Wien, A-1040 Vienna, Austria.
E ITER , T., F INK , M., K RENNWALLNER , T., R EDL , C., AND S CH ÜLLER , P. 2014b. Efficient
HEX-program evaluation based on unfounded sets. Journal of Artificial Intelligence Research 49,
269–321.
E ITER , T., G OTTLOB , G., AND M ANNILA , H. 1997. Disjunctive datalog. ACM Transactions on
Database Systems 22, 3, 364–418.
E ITER , T., I ANNI , G., L UKASIEWICZ , T., S CHINDLAUER , R., AND T OMPITS , H. 2008. Combining
answer set programming with description logics for the semantic web. Artificial Intelligence 172, 1213, 1495–1539.
E ITER , T., I ANNI , G., S CHINDLAUER , R., AND T OMPITS , H. 2005. A Uniform Integration of
Higher-Order Reasoning and External Evaluations in Answer-Set Programming. In International
Joint Conference on Artificial Intelligence (IJCAI). Professional Book Center, 90–96.
E ITER , T., I ANNI , G., S CHINDLAUER , R., AND T OMPITS , H. 2006. Effective integration of
declarative rules with external evaluations for semantic-web reasoning. In European Semantic Web
Conference (ESWC). Springer, 273–287.
FABER , W., L EONE , N., AND P FEIFER , G. 2004. Recursive aggregates in disjunctive logic programs:
Semantics and complexity. In European Conference on Logics in Artificial Intelligence (JELIA).
Springer, 200–212.
G EBSER , M., K AMINSKI , R., K AUFMANN , B., AND S CHAUB , T. 2014. Clingo = ASP + control:
Preliminary report. CoRR abs/1405.3694.
G EBSER , M., K AUFMANN , B., AND S CHAUB , T. 2009a. Solution enumeration for projected
boolean search problems. In Integration of AI and OR Techniques in Constraint Programming for
Combinatorial Optimization Problems (CPAIOR). Springer, 71–86.
G EBSER , M., K AUFMANN , B., AND S CHAUB , T. 2012. Conflict-driven answer set solving: From
theory to practice. Artificial Intelligence 187–188, 52–89.
G EBSER , M., O STROWSKI , M., AND S CHAUB , T. 2009b. Constraint answer set solving. In
International Conference on Logic Programming (ICLP). Springer, 235–249.
G ELFOND , M. AND L IFSCHITZ , V. 1988. The Stable Model Semantics for Logic Programming. In
Logic Programming: Proceedings of the 5th International Conference and Symposium, R. Kowalski
and K. Bowen, Eds. MIT Press, 1070–1080.

44

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

G ELFOND , M. AND L IFSCHITZ , V. 1991. Classical negation in logic programs and disjunctive
databases. New Generation Computing 9, 3/4, 365–386.
H AVUR , G., O ZBILGIN , G., E RDEM , E., AND PATOGLU , V. 2014. Geometric Rearrangement of
Multiple Movable Objects on Cluttered Surfaces: A Hybrid Reasoning Approach. In International
Conference on Robotics and Automation (ICRA). 445–452.
H OEHNDORF, R., L OEBE , F., K ELSO , J., AND H ERRE , H. 2007. Representing default knowledge in
biomedical ontologies: Application to the integration of anatomy and phenotype ontologies. BMC
Bioinformatics 8, 1, 377.
JANHUNEN , T., O IKARINEN , E., T OMPITS , H., AND W OLTRAN , S. 2009. Modularity Aspects of
Disjunctive Stable Models. Journal of Artificial Intelligence Research 35, 813–857.
J ÄRVISALO , M., O IKARINEN , E., JANHUNEN , T., AND N IEMEL Ä , I. 2009. A module-based
framework for multi-language constraint modeling. In Logic Programming and Nonmonotonic
Reasoning (LPNMR). 155–168.
L ASSILA , O. AND S WICK , R. 1999. Resource description framework (RDF) model and syntax
specification. http://www.w3.org/TR/1999/REC-rdf-syntax-19990222.
L IERLER , Y. 2014. Relating constraint answer set programming languages and algorithms. Artificial
Intelligence 207, 1–22.
L IERLER , Y. AND T RUSZCZYNSKI , M. 2013. Modular answer set solving. In Late-Breaking
Developments in the Field of Artificial Intelligence, Bellevue, Washington, USA, July 14-18, 2013.
AAAI Workshops, vol. WS-13-17. AAAI.
L IFSCHITZ , V. AND T URNER , H. 1994. Splitting a Logic Program. In Proceedings ICLP-94.
MIT-Press, Santa Margherita Ligure, Italy, 23–38.
L INKE , T. 2001. Graph Theoretical Characterization and Computation of Answer Sets. In International Joint Conference on Artificial Intelligence (IJCAI). 641–645.
L INKE , T. AND S ARSAKOV, V. 2004. Suitable graphs for answer set programming. In LPAR,
F. Baader and A. Voronkov, Eds. Lecture Notes in Computer Science, vol. 3452. Springer, 154–168.
M ELLARKOD , V. S., G ELFOND , M., AND Z HANG , Y. 2008. Integrating Answer Set Programming
and Constraint Logic Programming. Annals of Mathematics and Artificial Intelligenc 53, 1-4,
251–287.
M OSCA , A. AND B ERNINI , D. 2008. Ontology-driven geographic information system and dlvhex
reasoning for material culture analysis. In Italian Workshop RiCeRcA at ICLP.
N IEMEL Ä , I. 1999. Logic programming with stable model semantics as constraint programming
paradigm. Annals of Mathematics and Artificial Intelligenc 25, 3–4, 241–273.
O IKARINEN , E. AND JANHUNEN , T. 2008. Achieving compositionality of the stable model semantics
for smodels programs. TPLP 8, 5-6, 717–761.
O STROWSKI , M. AND S CHAUB , T. 2012. ASP modulo CSP: the clingcon system. Theory and
Practice of Logic Programming (TPLP) 12, 4-5, 485–503.
PAL Ù , A. D., D OVIER , A., P ONTELLI , E., AND ROSSI , G. 2009. Gasp: Answer set programming
with lazy grounding. Fundamenta Informaticae 96, 3, 297–322.
P ERRI , S., R ICCA , F., AND S IRIANNI , M. 2010. A parallel ASP instantiator based on DLV. In
Declarative Aspects of Multicore Programming (DAMP’10). LNCS. Springer, 73–82.
P OLLERES , A. 2007. From SPARQL to rules (and back). In International Conference on World Wide
Web (WWW). ACM, 787–796.
P RZYMUSINSKI , T. C. 1988. On the Declarative Semantics of Deductive Databases and Logic
Programs. In Foundations of Deductive Databases and Logic Programming, J. Minker, Ed. Morgan
Kaufman, 193–216.
P RZYMUSINSKI , T. C. 1991. Stable semantics for disjunctive programs. New Generation Computing 9, 401–424.
R EDL , C. 2014. Answer set programming with external sources: Algorithms and efficient evaluation.
Ph.D. thesis, Vienna University of Technology.

Model building for ASP with external atoms

45

ROSS , K. 1994. Modular Stratification and Magic Sets for Datalog Programs with Negation. Journal
of the ACM 41, 6, 1216–1267.
S CHINDLAUER , R. 2006. Answer set programming for the semantic web. Ph.D. thesis, Vienna
University of Technology, Vienna, Austria.
S CH ÜLLER , P. 2012. Inconsistency in multi-context systems: Analysis and efficient evaluation. Ph.D.
thesis, Vienna University of Technology, Vienna, Austria.
S CH ÜLLER , P., PATOGLU , V., AND E RDEM , E. 2013. A Systematic Analysis of Levels of Integration
between Low-Level Reasoning and Task Planning. In Workshop on Combining Task and Motion
Planning at IEEE International Conference on Robotics and Automation (ICRA).
S HEN , Y., WANG , K., E ITER , T., F INK , M., R EDL , C., K RENNWALLNER , T., AND D ENG , J. 2014.
FLP answer set semantics without circular justifications for general logic programs. Artificial
Intelligence 213, 1–41.
TASHARROFI , S. AND T ERNOVSKA , E. 2011. A semantic account for modularity in multi-language
modelling of search problems. In International Symposium on Frontiers of Combining Systems
(FroCoS). 259–274.
WANG , Y., YOU , J., Y UAN , L., S HEN , Y., AND Z HANG , M. 2012. The loop formula based semantics
of description logic programs. Theor. Comput. Sci. 415, 60–85.
Z AKRAOUI , J. AND Z AGLER , W. L. 2012. A method for generating CSS to improve web accessibility
for old users. In Int. Conf. on Computers Helping People with Special Needs (ICCHP). 329–336.
Z IRTILO ǦLU , H. AND YOLUM , P. 2008. Ranking semantic information for e-government: complaints
management. In International Workshop on Ontology-supported business intelligence (OBI). ACM.

Appendix A Proofs
Proof of Theorem 1 (Splitting Theorem)
Given a set of ground atoms M and a set of rules R, we denote by M |R = M ∩ gh(R) the
projection of M to ground heads of rules in R.
(⇒) Let M ∈ AS(P ). We show that (1) M |R ∈ AS(R) and that (2) M ∈ AS(P \ R ∪
facts(M |R )).
As for (1), we first show that M |R satisfies the reduct f RM |R , and then that M |R is indeed
a minimal model of f RM |R . M satisfies f P M and R ⊆ P . Observe that, by definition of
FLP reduct, f RM ⊆ f P M . By definition of rule splitting set, satisfiability of rules in R does
not depend on heads of rules in P \ R (due to the restriction of external atoms to extensional
semantics, this is in particular true for external atoms in R). Therefore f RM |R = f RM ,
M satisfies f RM |R , and M |R satisfies f RM |R . For showing M |R ∈ AS(R), it remains to
show that M |R is a minimal model of f RM |R .
Assume towards a contradiction that some S ⊂ M |R is a model of f RM |R . Then there
is a nonempty set A = M |R \ S of atoms with A ⊆ gh(R). Let M ? = M \ A. We
next show that M ? is a model of f P M , which implies that M ∈
/ AS(P ). Assume on the
contrary that M ? is not a model of f P M . Hence there exists some rule r ∈ f P M such that
H(r) ∩ M ? = ∅, B + (r) ⊆ M ? , B − (r) ∩ M ? = ∅ and external atoms in B + (r) (resp.,
B − (r)) evaluate to true (resp., false) wrt. M ? . S agrees with M ? on atoms from gh(R), and
S satisfies f RM |R . The truth values of external atoms in bodies of rules in R depends only
on atoms from gh(R), therefore external atoms in R evaluate to the same truth value wrt. S
and M ? . Therefore r ∈
/ f RM |R and r ∈ f (P \ R)M . Since r ∈ P \ R, H(r) ⊆ gh(P \ R),
and because M and M ? agree on atoms from gh(P \ R), H(r) ∩ M ? = ∅ from above
implies that H(r)∩M = ∅. Because r ∈ f P M , its body is satisfied in M , and since its head

46

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

has no intersection with M , we get that f P M is not satisfied by M , which is a contradiction.
Therefore M ? is a model of f P M . As M ? ⊂ M , this contradicts our assumption that
M ∈ AS(P ). Therefore S = M |R = X is a minimal model of f RM .
We next show that M satisfies the reduct f (P \ R ∪ facts(M |R ))M , and then that
it is indeed a minimal model of the reduct. By the definition of reduct, f (P \ R ∪
facts(M |R ))M = f (P \ R)M ∪ facts(M |R ). M satisfies facts(M |R ) because M |R ⊆ M .
Furthermore f (P \ R)M ⊆ f P M , hence M satisfies f (P \ R)M . Therefore M satisfies
f (P \ R ∪ facts(M |R ))M .
To show that M is a minimal model of f (P \ R ∪ facts(M |R ))M , assume towards a
contradiction that some S ⊂ M is a model of f (P \ R ∪ facts(M |R ))M . Since facts(M |R )
is part of the reduct, M |R ⊆ S, therefore S|gh(R) = M |R . By definition of rule splitting
set, satisfiability of rules in R does not depend on heads of rules in P \ R, hence S satisfies
f RM . Because S satisfies f (P \ R ∪ facts(M |R ))M = f (P \ R)M ∪ facts(M |R ), it also
satisfies f (P \ R)M . Since S satisfies both f RM , S satisfies f P M = f (P \ R)M ∪ f RM .
This is a contradiction to M ∈ AS(P ). Therefore S = M is a minimal model of f (P \ R ∪
facts(M |R ))M .
(⇐) Let M ∈ AS(P \ R ∪ facts(X)) and let X ∈ AS(R). We first show that M satisfies
f P M , and then that it is a minimal model of f P M .
As facts X are part of the program P \R∪facts(X), and by definition of rule splitting set,
P \ R contains no rule heads unifying with gh(R), hence we have X = M |R . Furthermore
f (P \ R ∪ facts(X))M \ facts(X) ∪ f RM = f P M , and as M satisfies the left side, it
satisfies the right side. To show that M is a minimal model of f P M , assume S ⊂ M is
a smaller model of f P M . By definition of reduct, S also satisfies f (P \ R)M and f RM .
Since R is a splitting set, satisfiability of rules in R does not depend on heads of rules in
P \ R, therefore f RM = f RM |R = f RX and S|gh(R) satisfies f RX . Since S ⊂ M , we
have S|gh(R) ⊆ X. Because X is a minimal model of f RX , S|gh(R) ⊂ X is impossible
and S|gh(R) = X. Therefore S|gh(P \R) ⊂ M |gh(P \R) . Because S satisfies f (P \ R)M
and S|gh(R) = X, S also satisfies f (P \ R ∪ facts(X))M . Since S ⊂ M , this contradicts
the fact that M is a minimal model of P \ R ∪ facts(X). Therefore S = M is a minimal
model of f P M .

Proof of Theorem 2 (Generalized Splitting Theorem)
By definition of generalized bottom, the set C = B \ R contains only constraints, therefore
gh(B) = gh(R) and M |gh(B) = M |gh(R) . As R ⊆ B and B \ R contains only constraints,
AS(B) ⊆ AS(R). The only difference between Theorem 1 and Theorem 2 is, that for
obtaining X, the latter takes additional constraints into account.
(⇒) It is sufficient to show that M |gh(B) does not satisfy the body of any constraint in
C ⊆ P if M does not satisfy the body of any constraint in P . Since B is a generalized
bottom, no negative dependencies of constraints C to rules in P \ B exist; therefore if the
body of a constraint c ∈ C is not satisfied by M , the body of c is not satisfied by M |gh(B) .
As M satisfies P , it does not satisfy any constraint body in P , hence the projection M |gh(B)
does not satisfy any constraint body in B \ R.
(⇐) It is sufficient to show that an answer set of R that satisfies a constraint body in
C also satisfies that constraint body in P , which raises a contradiction. As constraints in

Model building for ASP with external atoms

47

C have no negative dependencies to rules in P \ B, a constraint with a satisfied body in
M |gh(R) also has a satisfied body in M , therefore the result follows.
Proof of Proposition 1
Assume towards a contradiction that there exist a non-constraint r ∈ P , a rule s ∈ P with
r →m,n s, and u0 ∈ U |r , v 0 ∈ U |s such that (u0 , v 0 ) ∈
/ E. Due to Definition 9, r →m,n s
implies that s has H(s) 6= ∅ and therefore that s is a non-constraint. Definition 14 (b) then
implies that U |r = {u0 } and U |s = {v 0 } (non-constraints are present in exactly one unit).
Case (i): for r →n s, Definition 14 (c) specifies that for all u ∈ U |r and v ∈ U |s there
exists an edge (u, v) ∈ E, therefore also (u0 , v 0 ) ∈ E, which is a contradiction.
Case (ii): for r →m s, Definition 14 (d) specifies that some u ∈ U |r exists such that for
every v ∈ U |s there exists an edge (u, v) ∈ E; since U |r = {u0 } and U |s = {v 0 }, it must
hold that (u0 , v 0 ) ∈ E, which is a contradiction.
Proof of Proposition 2
Given two distinct units u1 , u2 ∈ U , assume towards a contradiction that some γ ∈
gh(u1 ) ∩ gh(u2 ) exists. Then there exists some r ∈ u1 with α ∈ H(r) and α ∼ γ, and
there exists some s ∈ u2 with β ∈ H(s) and β ∼ γ. As α ∼ γ and β ∼ γ and γ is ground,
we obtain α ∼ β; hence, by Definition 9 (iii) we have r →m s and s →m r. As r and s
have nonempty heads, they are non-constraints. Thus by Proposition 1, there exist edges
(u1 , u2 ), (u2 , u1 ) ∈ E. As an evaluation graph is acyclic, it follows u1 = u2 ; this is a
contradiction.
Proof of Proposition 3
For an lde-safe program P , the graph E = ({P }, ∅) is a valid evaluation graph.
Proof of Theorem 3
For any set of rules, let constr (S) = {r ∈ S | H(r) = ∅} denote the set of constraints in
S. We say that the dependencies of r ∈ Q are covered at unit u ∈ U , if for every rule s ∈ Q
such that r →m,n s and s ∈
/ u, it holds that (u, u0 ) ∈ E for all u0 ∈ U |s , i.e., u has an edge
to all units containing s.
To prove that B = u< is a generalized bottom of P = u≤ wrt. the rule splitting set
R = u< \ constr (u< ) as by Definition 12, we prove that (a) R ⊆ B ⊆ P , (b) B \ R
contains only constraints, (c) no constraint in B \ R has nonmonotonic dependencies to
rules in P \ B, and (d) R is a rule splitting set of P .
Statement (a) corresponds to u< \ constr (u< ) ⊆ u< ⊆ u≤ and u≤ is defined as
≤
u = u< ∪ u, therefore the relations all hold. For (b), B \ R = u< \ (u< \ constr (u< )),
and as A \ (A \ B) = A ∩ B, it is easy to see that B \ R = u< ∩ constr (u< ) and thus
B \ R only contains constraints. For (c), we show a stronger property, namely that no
rule (constraint or non-constraint) in B has nonmonotonic dependencies to rules in P \ B.
B = u< is the union of evaluation units V = {v ∈ U | v < u}. By Definition 14 (c) all
nonmonotonic dependencies r →n s are covered at every unit w such that w ∈ Ur . Hence
if r ∈ w and w ∈ V , then either s ∈ w or s ∈ w< holds, and hence s ∈ w≤ ⊆ u< . As
P \B = u≤ \u< , no nonmonotonic dependencies from B = u< to P \B exist and (c) holds.
For (d) we know that R = u< \ constr (u< ) contains no constraints, and by Proposition 1

48

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

all dependencies of non-constraints in R are covered by E. Therefore r ∈ R, r →m,n s,
and s ∈ P implies that s ∈ R. Consequently, (d) holds which proves the theorem.
Proof of Theorem 4
Similar to the proof of Theorem 3, we show this in four steps; given P = u< , R =
u0≤ \ constr (u0≤ ), and B = u0≤ = u0 ∪ u0< , we show that (a) R ⊆ B ⊆ P , (b) B \ R
contains only constraints, (c) no constraint in B \ R has nonmonotonic dependencies to
rules in P \ B, and (d) R is a rule splitting set of P . Let preds E (u) = {u1 , . . . , uk } and
Let V = {v ∈ U | v < u0 } be the set of units on which u0 transitively depends. (Note that
V ⊂ preds E (u) and u ∈
/ V .) As u0< contains all units u0 transitively depends on, we have
S
0
B = u ∪ w∈V w.
For (a), R ⊆ B holds trivially, and B ⊆ P holds by definition of u< and u0≤ and
because u0 ∈ preds E (u). Statement (b) holds, because B \ R removes R from B, i.e., it
removes everything that is not a constraint in B from B, therefore only constraints remain.
For (c) we show that no rule in B has a nonmonotonic dependency to rules in P \ B. By
Definition 14 (c), all nonmonotonic dependencies are covered at all units. Therefore a rule
r ∈ w, w ∈ {u0 } ∪ V with r →n s, s ∈ U implies that either s ∈ w, or that s is contained
in a predecessor unit of w and therefore in u0 or in V . Hence there are no nonmonotonic
dependencies from rules in B to any rules not in B, and hence also not to rules in P \ B
and (c) holds. For (d) we know that R contains no constraints and by Proposition 1 all
dependencies of non-constraints in R are covered by E. Therefore r ∈ R, r →m,n s, s ∈ P
implies that s ∈ R and the theorem holds.
Proof of Proposition 4
(⇒) The added vertex m0 is assigned to one unit and gets assigned a type. Furthermore, the
graph stays acyclic as only outgoing edges from m0 are added. I-connectedness is satisfied,
as it is satisfied in I and we add no o-interpretation. O-connectedness is satisfied, as m0 gets
appropriate edges to o-interpretations at its predecessor units, and for other i-interpretations
it is already satisfied in I.
For FAI intersection, observe that if we add an edge (m0 , mi ) to I and it holds that
mi ∈ o-ints I (ui ), then m0 reaches in I only one o-interpretation at ui , and due to Oconnectedness that o-interpretation is connected to exactly one i-interpretation at ui , which
is part of the original graph I and therefore satisfies FAI intersection. Therefore it remains
to show that the union of subgraphs of I reachable in I from m1 ,. . . ,mk , contains one
o-interpretation at each unit in the subgraph of E reachable from u1 ,. . . ,uk . We make a case
distinction.
Case (I): two o-interpretations mi ∈ o-ints I (ui ), mj ∈ o-ints I (uj ) in the join, with
1 ≤ i < j ≤ k, have no common unit that is reachable in E from ui and from uj : then
the condition is trivially satisfied, as the subgraphs of I reachable in I from mi and mj ,
respectively, do not intersect at any unit.
Case (II): two o-interpretations mi ∈ o-ints I (ui ), mj ∈ o-ints I (uj ) in the join, with
1 ≤ i < j ≤ k, have at least one common unit that is reachable from ui and from uj in E.
Let uf be a unit reachable in E from both ui and uj on two paths that do not intersect before
reaching uf . From ui to uf , and from uj to uf , exactly one o-interpretation is reachable in
I from mi and mj , respectively, as these paths do not intersect. uf is a FAI of u, and as the

Model building for ASP with external atoms

49

join is defined, we reach in E exactly one o-interpretation at unit uf from mi and mj . Due
to O-connectedness, we also reach in I exactly one i-interpretation m00 at uf from mi and
mj . Now m00 is common to subgraphs of I that are reachable in I from mi and mj , and
m00 satisfies FAI intersection in I.
Consequently, FAI intersection is satisfied in I 0 for all pairs of predecessors of m0 and
therefore in all cases. As no vertex m with {(m, m1 ), . . . , (m, mk )} ⊆ F exists and and as
I satisfies Uniqueness, also I 0 satisfies Uniqueness.
(⇐) Assume towards a contradiction that I 0 is an i-graph but that the join is not defined.
Then there exists some FAI u0 ∈ fai (u) such that either no or more than one o-interpretation
from o-ints I (u) is reachable in I from some mi , 1 ≤ i ≤ k. As I is an i-graph, due to
I-connectedness and O-connectedness, if a unit u0 is a FAI and therefore u0 is reachable in
E from ui , then at least one i-interpretation and one o-interpretation at u0 is reachable in
I from mi . If more than one o-interpretation is reachable in I from some mi , 1 ≤ i ≤ k,
this means that more than one o-interpretation at u0 is reachable in I 0 from the newly added
i-interpretation m. However, this violates FAI intersection in I 0 , which is a contradiction.
Hence the result follows.
Proof of Proposition 5
(⇒) Whenever the join is defined, A0 is an i-graph by Proposition 4. It remains to show
that int(m0 )+ ∈ AS(u< ), and that A0 fulfills items (a) and (c) of an answer set graph.
<
By Theorem 4 we know that for each ui , u≤
i is a generalized bottom of u wrt. the set
≤
Ri = {r ∈ ui | B(r) 6= ∅}. For each ui , therefore Y ∈ AS(u< ) iff Y ∈ AS(u< \ Ri ∪
facts(X)) for some X ∈ AS(u≤
i ). As A is an answer set graph, for each mi we know that
int(mi )+ ∈ AS(u≤
);
hence
Y
∈ AS(u< ) if Y ∈ AS(u< \ Ri ∪ int(mi )+ ). Now from the
i
≤
evaluation graph properties we know that u< = u≤
1 ∪ · · · ∪ uk , and from the construction of
0
0
0 +
int(m ) and its dependencies in A we obtain that int(m ) = int(m1 )+ ∪· · ·∪int(mk )+ .
It follows that int(m0 )+ ∈ AS(u< ), which satisfies condition (a). Due to the definition of
join, condition (c) is also satisfied and A0 is indeed an answer set graph.
(⇐) As A0 is an answer set graph, it is an i-graph, and hence by Proposition 4 m =
m1 ./ · · · ./ mk is defined.
Proof of Theorem 5
We prove this theorem using Proposition 6. We construct E 00 = (U 00 , E 00 ) with U 00 = U ∪
{ufinal }, ufinal = ∅, and E 00 = E ∪{(ufinal , u) | u ∈ U }. As ufinal contains no rules and as
E 00 is acyclic, no evaluation graph property of gets violated and E 00 is also an evaluation graph.
As A contains no interpretations at ufinal and dependencies from units in U are the same in E
and E 00 , A is in fact an answer set graph for E 00 . We now modify A to obtain A00 as follows.
We add the set Mnew = {m | m = m1 ./ · · · ./ mn is defined at ufinal (wrt. A)} as iinterpretations of ufinal and dependencies from each m ∈ Mnew to the respective o-interpretations mi , 1 ≤ i ≤ n. By Proposition 5, A00 is an answer set graph for E 00 , and moreover A00
gets input-complete for ufinal by construction. As A00 is input-complete for U ∪{ufinal } and
output-complete for U , by Proposition 6 we have that AS(P ) = i -ints A (ufinal ) = Mnew .
As for every join m = m1 ./ · · · ./ mn , we have int(m) = int(m1 )∪ · · · ∪int(mn ), to
complete the proof of the theorem, it remains to show that the join m between m1 ,. . . ,mn
is defined at ufinal iff the subgraph A0 of A reachable from the o-interpretations mi in

50

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

F fulfills |o-ints A (ui )| = 1, for each ui ∈ U . As the join involves all units in U , and
since A00 is an answer set graph and thus an i-graph, it follows from the conditions for
an i-graph that at each ui ∈ U exactly one o-interpretation is reachable from m, and thus
also from each mi ; thus the condition for A0 holds. Conversely, if the subgraph A0 fulfills
|o-ints A (ui )| = 1 for each ui ∈ U , then clearly the FAI condition for the join m being
defined is fulfilled.
Proof of Proposition 6
As ufinal depends on all units in U \ {ufinal }, due to O-connectedness every i-interpretation
m ∈ i -ints A (ufinal ) depends on one o-interpretation at every unit in U \ {ufinal }. Let
U \ {ufinal } = {u1 , . . . , uk } and let MM = {m1 , . . . , mk } be the set of o-interpretations
such that (m, mi ) ∈ F and mi ∈ o-ints A (ui ), 1 ≤ i ≤ k. Then, due to FAI intersection,
Mm contains each o-interpretation that is reachable from m in A, and Mm contains only
interpretations with this property. Hence int(m)+ = int(m1 ) ∪ · · · ∪ int(mk ), and due to
condition (c) in Definition 19, we have int(m) = int(m)+ . By the dependencies of ufinal ,
<
we have u<
final = P , and as ufinal is input-complete, we have that AS(P ) = AS(ufinal ) =
+
+
{int(m) | m ∈ i -ints A (ufinal )}. As int(m) = int(m) for every i-interpretation m at
ufinal , we obtain the result.
Proof of Proposition 7
The proposition follows from Property 1, which asserts that the grounding P 0 has the same
answer sets as P , and from the soundness and completeness of the evaluation algorithm for
ground HEX-programs as asserted by Property 2.
Proof of Theorem 6
We show by induction on its construction that I = (M, F, unit, type, int) is an answer set
graph for E, and that at the beginning of the while-loop I is input- and output-complete for
V \ U.
(Base) Initially, I is initially and V = U , hence the base case trivially holds.
(Step) Suppose that I is an answer set graph for E at the beginning of the while-loop,
and that it is input- and output-complete for V \ U . As the chosen u only depends on
units in V \ U , it depends only on output-complete units. For a leaf unit u, (b) creates an
empty i-interpretation and therefore makes u input-complete. For a non-leaf unit u, the first
for-loop (c) builds all possible joins of interpretations at predecessors of u and adds them
as i-interpretations to I. As all predecessors of u are output-complete by the hypothesis,
this makes u input-complete. Now suppose that Condition (d) is false, i.e., u 6= ufinal . Then
the second for-loop (e) evaluates u wrt. every i-interpretation at u and adds the result to
u as an o-interpretation. Due to Proposition 7, E VALUATE LDES AFE(u, int(m0 )) returns
all interpretations o such that o ∈ {X \ int(m0 ) | X ∈ AS(u ∪ facts(int(m0 ))}. As u
depends on all units on which its rules depend, and as i-interpretations contain all atoms
from o-interpretations of predecessor units (due to condition (c) of Definition 19), we have
E VALUATE LDES AFE(u, int(m0 )) = E VALUATE LDES AFE(u, int(m0 )+ ). By Theorem 3,
u< is a generalized bottom of u≤ , and by the induction hypothesis int(m0 )+ ∈ AS(u< );
hence by Theorem 2, we have that int(m0 )+ ∪ o ∈ AS(u≤ ). Consequently, adding a new
o-interpretation m with interpretation int(m) = o and dependency to m0 to the graph I

Model building for ASP with external atoms

51

results in int(m)+ ∈ AS(u≤ ), and adding all of them makes I output-complete for u.
Finally, in (f) u is removed from U ; hence at the end of the while-loop I is an answer set
graph and again input- and output-complete for V \ U .
It remains to consider the case where Condition (d) is true. Then ufinal was made
input-complete, which means that all predecessors of ufinal are output-complete. As ufinal
depends on all other units, we have U = {ufinal } and the algorithm returns i -ints A (u); by
Proposition 6, it thus returns AS(P ), which will happen in the |V |-th iteration of the while
loop.

Appendix B Example Run of Algorithm 2
We provide here an example run of Algorithm 2 for our running example.
Example 28 (ctd.)
Consider an evaluation graph E20 which is E2 plus ufinal = ∅, which depends on all other
units. Following Algorithm 2 we first choose u = u1 , and as u1 has no predecessor
units, step (b) creates the i-interpretation m1 withint(m1 ) = ∅. As u1 6= ufinal , we
continue and in loop (e) obtain O = AS(u1 ) = {swim(ind )}, {swim(outd )} . We
add both answer sets as o-interpretations m2 and m3 and then finish the outer loop with
U = {u2 , u3 , u4 , ufinal }. In the next iteration, we could choose u = u2 or u = u3 ; assume
we choose u2 . Then preds E (u2 ) = {u1 } and k = 1, and we enter the loop (c) and build all
joins that are possible with o-interpretations at u1 (all joins are trivial and all are possible),
i.e., we copy the interpretations and store them at u2 as new i-interpretations m4 and
m5 . In the loop (e), we obtain O = E VALUATE LDES AFE(u2 , {swim(ind )}) = ∅, as
indoor swimming requires money which is excluded by c8 ∈ u2 . Therefore i-interpretation {swim(ind )} yields no o-interpretation, indicated by E. However, we obtain O =
E VALUATE LDES AFE(u2 , {swim(outd )}) = {∅}: as outdoor swimming neither requires
money nor anything else, i-interpretation {swim(outd )} derives no additional atoms and
yields the empty answer set, which we store as o-interpretation m6 at u2 ; the iteration ends
with U = {u3 , u4 , ufinal }. In the next iteration we choose u = u3 , we add in loop (c) i-interpretations m7 and m8 to u3 , and in loop (e) o-interpretations m9 , . . . , m12 to u3 ; the iteration
ends with U = {u4 , ufinal }. In the next iteration we choose u = u4 ; this time we have
multiple predecessors, and in loop (c) we check join candidates m6 ./ m9 and m6 ./ m10 ,
which are both not defined. The other join candidates are m6 ./ m11 and m6 ./ m12 , which
are both defined; we thus add their results as i-interpretations m13 and m14 , respectively, to
u4 . The loop (e) computes then one o-interpretation m15 for i-interpretation m13 and no
o-interpretation for m14 . The iteration ends with U = {ufinal }. In the next iteration, we
have preds E (ufinal ) = {u1 , u2 , u3 , u4 } and the loop (c) checks all combinations of one
o-interpretation at each unit in preds E (ufinal ). Only one such join candidate is defined,
namely m = m3 ./ m6 ./ m11 ./ m15 , whose result is stored as a new i-interpretation
at ufinal . The check
 (d) now succeeds, and we return all i-interpretations at ufinal ; i.e.,
we return {m} = {swim(outd ), goto(altD), ngoto(gansD), go, need (loc, yogamat)} .
This is indeed the set of answer sets of Pswim .

52

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

Algorithm 3: A NSWER S ETS O N D EMAND
Input: evaluation graph E for program P , with final unit ufinal = ∅
Output: the answer sets of P
initialize global storage S
repeat
mout := G ET N EXT O UTPUT M ODEL (ufinal )
if mout 6= UNDEF then output mout
until mout = UNDEF

Appendix C On Demand Model Streaming Algorithm
Algorithm 2 fully evaluates all other units before computing results at the final evaluation
unit ufinal , and it keeps the intermediate results in memory. If we are only interested in one
or a few answer sets, many unused results may be calculated.
Using the same evaluation graph, we can compute the answer sets with a different,
more involved algorithm A NSWER S ETS O N D EMAND (shown in Algorithm 3) that operates
demand-driven from units, starting with ufinal , rather than data-driven from completed units.
It uses in turn several building blocks that are shown in Algorithms 4–6
A NSWER S ETS O N D EMAND calls Algorithm G ET N EXT O UTPUT M ODEL for ufinal and
outputs its output models, i.e., the answer sets of the input program P given by the evaluation
graph E, one by one until it gets back UNDEF. Like Algorithm 2, G ET N EXT O UTPUTM ODEL builds in combination with the other algorithms an answer set graph A for E that is
input-complete at all units, if all statements marked with ’(+)’ are included; omitting them,
it builds A virtually and has at any time at most one input and one output model of each
unit in memory.
Roughly speaking, the models at units are determined in the same order in which a rightto-left depth-first-traversal of the evaluation graph E would backtrack from edges. This is
because first all models of the subgraph reachable from a unit u are determined, then models
at the unit u, and then the algorithm backtracks. The models of the subgraph are retrieved
with G ET N EXT I NPUT M ODEL one by one, and using NextAnswerSet the output models
are generated and returned. The latter function is assumed to return, given a HEX-program
P and the i-th element in an arbitrary but fixed enumeration I1 , I2 , . . . , Im of the answer
sets of P (without duplicates), the next answer set Ii+1 , where by convention I0 = UNDEF
and the return value for Im is UNDEF. This is easy to provide on top of current solvers, and
the incremental usage of NextAnswerSet allows for an efficient stateful realization (e.g.
answer set computation is suspended).
The trickiest part of this approach is G ET N EXT I NPUT M ODEL, which has to create locally
and in an incremental fashion all joins that are globally defined, i.e., all combinations of
incrementally available output models of predecessors which share a common predecessor
model at all FAIs. To generate all combinations of output models in the right order, it uses
the algorithm E NSURE M ODEL I NCREMENT.
The algorithms operate on a global data structure S = (E, A, cur I, cur O, refs O) called
storage, where
• E = (U, E) is the evaluation graph containing ufinal ∈ U ,

Model building for ASP with external atoms

53

Algorithm 4: G ET N EXT O UTPUT M ODEL(u)
Input: u: unit
Output: mout : next omodel at u or UNDEF

(+)

if refs O(u) > 0 then return UNDEF
if cur I(u) = UNDEF then cur I(u) := G ET N EXT I NPUT M ODEL(u)
while cur I(u) 6= UNDEF do
cur O(u) := NextAnswerSet(u ∪ facts(cur I(u)), cur O(u))
if cur O(u) 6= UNDEF then
add omodel cur O(u) to A with dependency to cur I(u)
return cur O(u)
cur I(u) := G ET N EXT I NPUT M ODEL(u)
return UNDEF

Algorithm 5: E NSURE M ODEL I NCREMENT(u, at)
Input: u: unit with {u1 , . . . , uk } = preds E (u), at: index 1 ≤ at ≤ k
Output: at0 : index at ≤ at0 ≤ k or UNDEF
repeat
refs O(uat ) := refs O(uat ) − 1
m := G ET N EXT O UTPUT M ODEL(uat )
if m = UNDEF then at := at + 1
else
refs O(uat ) := refs O(uat ) + 1
return at
until at = k + 1
return UNDEF

• A = (M, F, unit, type, int) is the (virtually built) answer set graph,
• cur I : U → M ∪ {UNDEF} and cur O : U → M ∪ {UNDEF}, are functions
that informally associate with a unit u the current input respectively output model
considered, and
• refs O : U → N ∪ {0} is a function that keeps track of how many current input models
point to the current output model of u; this is used to ensure correct joins, by checking
in G ET N EXT O UTPUT M ODEL that the condition (IG-F) for sharing models in the
interpretation graph is not violated (for details see Section 5.1.2 and Definition 17).
Initially, the storage S is empty, i.e., it contains the input evaluation graph E, an empty
answer set graph A, and the functions are set to cur I(u) = UNDEF, cur O(u) = UNDEF,
and refs O(u) = 0 for all u ∈ U . The call of G ET N EXT O UTPUT M ODEL for ufinal triggers
the right-to-left depth-first traversal of the evaluation graph.
We omit tracing Algorithm A NSWER S ETS O N D EMAND on our running example, as this
would take quite some space; however, one can check that given the evaluation graph E2 , it

54

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

Algorithm 6: G ET N EXT I NPUT M ODEL(u)
Input: u: unit
Output: mout : imodel at u or UNDEF
(a)

(+)

(b)

(+)

if preds E (u) = ∅ then
if cur I(u) = UNDEF then
add imodel ∅ at u to A
return ∅
else return UNDEF
let {u1 , . . . , uk } = preds E (u)
/* assume this order is fixed for each unit u */
if cur I(u) 6= UNDEF then
at := E NSURE M ODEL I NCREMENT(u, 1)
if at = UNDEF then return UNDEF
at := at − 1
else at := k
while at 6= 0 do
if cur O(uat ) 6= UNDEF then
refs O(uat ) := refs O(uat ) + 1
at := at − 1
else
m := G ET N EXT O UTPUT M ODEL(uat )
if m = UNDEF then
if at = k then return UNDEF
at := E NSURE M ODEL I NCREMENT(u, at + 1)
if at = UNDEF then return UNDEF
else
refs O(uat ) := refs O(uat ) + 1
at := at − 1
let m = cur O(u1 ) ./ · · · ./ cur O(uk )
add imodel m to A with dependencies to cur O(u1 ), . . . , cur O(uk )
return m

correctly outputs the single answer set
I = {swim(outd ), goto(altD), ngoto(gansD), go, need (loc, yogamat)}.
Formally, it can be shown that given an evaluation graph E = (U, E) of a program P such
that E contains a final unit ufinal = ∅, Algorithm A NSWER S ETS O N D EMAND outputs one
by one all answer sets of P , without duplicates, and that in the version without (+)-lines, it
stores at most one input and one output model per unit (hence the size of the used storage is
linear in the size of the ground program grnd (P )).

Model building for ASP with external atoms

55

Appendix D Overview of Liberal Domain-Expansion Safety
Strong domain-expansion safety is overly restrictive, as it also excludes programs that
clearly are finitely restrictable. In this section we give an overview about the notion and
refer to (Eiter et al. 2014a) for details.
Example 29
Consider the following program:
(
)
r1 : p(a). r3 : s(Y ) ← p(X), &concat[X, a](Y ).
P=
r2 : q(aa). r4 : p(X) ← s(X), q(X).
It is not strongly safe because Y in the cyclic external atom &concat[X, a](Y ) in r3 does
not occur in an ordinary body atom that does not depend on &concat[X, a](Y ). However,
P is finitely restrictable as the cycle is “broken” by dom(X) in r4 .
To overcome unnecessary restrictions of strong safety in (Eiter et al. 2006), liberal domainexpansion safety (lde-safety) has been introduced (Eiter et al. 2014a), which incorporates
both syntactic and semantic properties of a program. The details of the notion are not
necessary for this paper, except that all lde-safe programs have finite groundings with the
same answer sets; we give here a brief overview.
Unlike strong safety, liberal de-safety is not a property of entire atoms but of attributes,
i.e., pairs of predicates and argument positions. Intuitively, an attribute is lde-safe, if the
number of different terms in an answer-set preserving grounding (i.e. a grounding which
has the same answer sets if restricted to the positive atoms as the original program) is finite.
A program is lde-safe, if all its attributes are lde-safe.
The notion of lde-safety is designed in an extensible fashion, i.e., such that several safety
criteria can be easily integrated. For this we parametrize our definition of lde-safety by a
term bounding function (TBF), which identifies variables in a rule that are ensured to have
only finitely many instantiations in the answer set preserving grounding. Finiteness of the
overall grounding follows then from the properties of TBFs.
For an ordinary predicate p ∈ P, let pi be the i-th attribute of p for all 1 ≤ i ≤ ar (p).
For an external predicate &g ∈ X with input list X in rule r, let &g[X]r T i with T ∈ {I, O}
be the i-th input resp. output attribute of &g[X] in r for all 1 ≤ i ≤ ar T (&g). For a ground
program P , the range of an attribute is, intuitively, the set of ground terms which occur in
the position of the attribute. Formally, for an attribute pi we have range(pi, P ) = {ti |
p(t1 , . . . , tar (p) ) ∈ A(P )}; for an attribute &g[X]r T i we have range(&g[X]r T i, P ) =
{xTi | &g[xI ](xO ) ∈ EA(P )}, where xs = xs1 , . . . , xsar s (&g) .
We use the following monotone operator to compute by fixpoint iteration a finite subset
of grnd (P ) for a program P :
[
GP (P 0 ) =
{rθ | ∃I ⊆ A(P 0 ), I 6|= ⊥, I |= B + (rθ)},
r∈P

where A(P ) = {Ta, Fa | a ∈ A(P 0 )} \ {Fa | a ← . ∈ P } and rθ is the ground instance
of r under variable substitution θ : V → C. Note that in this definition, I might be partial,
but by convention we assume that all atoms which are not explicitly assigned to true are
false. That is, GP takes a ground program P 0 as input and returns all rules from grnd (P )
whose positive body is satisfied under some assignment over the atoms of Π0 . Intuitively, the
0

56

Eiter, Fink, Ianni, Krennwallner, Redl, and Schüller

operator iteratively extends the grounding by new rules if they are possibly relevant for the
evaluation, where relevance is in terms of satisfaction of the positive rule body under some
assignment constructable over the atoms which are possibly derivable so far. Obviously, the
least fixpoint G∞
P (∅) of this operator is a subset of grnd (P ); we will show that it is finite
if P is lde-safe according to our new notion. Moreover, we will show that this grounding
preserves all answer sets as all omitted rule instances have unsatisfied bodies anyway.
Example 30
Consider the following program P :
r1 : s(a). r2 : dom(ax ). r3 : dom(axx ).
r4 : s(Y ) ← s(X), &concat[X, x](Y ), dom(Y ).
The least fixpoint of GP is the following ground program:
r10 : s(a). r20 : dom(ax ). r30 : dom(axx ).
r40 : s(ax ) ← s(a), &concat[a, x](ax), dom(ax).
r50 : s(axx ) ← s(ax), &concat[ax, x](axx), dom(axx).
Rule r40 is added in the first iteration and rule r50 in the second.
Towards a definition of lde-safety, we say that a term in a rule is bounded, if the number
of substitutions in G∞
P (∅) for this term is finite. This is abstractly formalized using term
bounding functions.
Definition 21 (Term Bounding Function (TBF))
A term bounding function, denoted b(P, r, S, B), maps a program P , a rule r ∈ P , a set S
of (already safe) attributes, and a set B of (already bounded) terms in r to an enlarged set
of (bounded) terms b(P, r, S, B) ⊇ B, such that every t ∈ b(P, r, S, B) has finitely many
∞
substitutions in G∞
P (∅) if (i) the attributes S have a finite range in GP (∅) and (ii) each term
in terms(r) ∩ B has finitely many substitutions in G∞
P (∅).
Intuitively, a TBF receives a set of already bounded terms and a set of attributes that are
already known to be lde-safe. Taking the program into account, the TBF then identifies and
returns further terms which are also bounded.
The concept yields lde-safety of attributes and programs from the boundedness of variables according to a TBF. We provide a mutually inductive definition that takes the empty
set of lde-safe attributes S0 (P ) as its basis. Then, each iteration step n ≥ 1 defines first
the set of bounded terms Bn (r, P, b) for all rules r, and then an enlarged set of lde-safe
attributes Sn (P ). The set of lde-safe attributes in step n + 1 thus depends on the TBF, which
in turn depends on the domain-expansion safe attributes from step n.
Definition 22 (Liberal Domain-Expansion Safety)
Let b be a term bounding function. The set Bn (r, P, b) of bounded terms in a rule r ∈ P in
S
step n ≥ 1 is Bn (r, P, b) = j≥0 Bn,j (r, P, b) where Bn,0 (r, P, b) = ∅ and for all j ≥ 0,
Bn,j+1 (r, P, b) = b(P, r, Sn−1 (P ), Bn,j ).
S
The set of domain-expansion safe attributes S∞ (P ) = i≥0 Si (P ) of a program P is
iteratively constructed with S0 (P ) = ∅ and for n ≥ 0:
• pi ∈ Sn+1 (P ) if for each r ∈ P and atom p(t1 , . . . , tar (p) ) ∈ H(r), we have that term
ti ∈ Bn+1 (r, P, b), i.e., ti is bounded;

Model building for ASP with external atoms

57

• &g[X]r I i ∈ Sn+1 (P ) if each Xi is a bounded variable, or Xi is a predicate input
parameter p and p1, . . . , par (p) ∈ Sn (P );
• &g[X]r O i ∈ Sn+1 (P ) if and only if r contains an external atom &g[X](Y) such that
Yi is bounded, or &g[X]r I 1, . . . , &g[X]r I ar I (&g) ∈ Sn (P ).
A program P is liberally domain-expansion (lde) safe, if it is safe and all its attributes
are domain-expansion safe.
A detailed description of liberal safety is beyond the scope of this paper. However, it is
crucial that each liberally domain-expansion safe HEX-program P is finitely restrictable, i.e.,
there is a finite subset Pg of grndC (P ) s.t. AS(Pg ) = AS(grnd C (P )). A concrete grounding algorithm G ROUND HEX is given in (Eiter et al. 2014a); we use G ROUND HEX(P ) in
this article to refer to a finite grounding of P that has the same answer sets.

