=Paper=
{{Paper
|id=Vol-1451/paper7
|storemode=property
|title=Modeling Abduction over Acyclic First-Order Logic Horn Theories in Answer Set Programming: Preliminary Experiments
|pdfUrl=https://ceur-ws.org/Vol-1451/paper7.pdf
|volume=Vol-1451
|dblpUrl=https://dblp.org/rec/conf/aiia/Schuller15
}}
==Modeling Abduction over Acyclic First-Order Logic Horn Theories in Answer Set Programming: Preliminary Experiments==
https://ceur-ws.org/Vol-1451/paper7.pdf
Modeling Abduction over Acyclic First-Order
Logic Horn Theories in Answer Set
Programming: Preliminary Experiments⋆
Peter Schüller
Computer Engineering Department, Faculty of Engineering
Marmara University, Turkey
peter.schuller@marmara.edu.tr
Abstract. We describe encodings in Answer Set Programming for ab-
ductive reasoning in First Order Logic in acyclic Horn theories in the
presence of value invention and in the absence of Unique Names Assump-
tion. We perform experiments using the Accel benchmark for abductive
plan recognition in natural language processing. Results show, that our
encodings cannot compete with state-of-the-art realizations of First Or-
der Logic abduction, mainly due to large groundings. We analyze reasons
for this bad performance and outline potential future improvements.
1 Introduction
Abduction [29] is reasoning to the best explanation, which is an important topic
in diverse areas such as diagnosis, planning, and natural language processing.
We experiment with the Accel benchmark [27] for abduction in acyclic First
Order Logic (FOL) Horn theories and model this problem in Answer Set Pro-
gramming (ASP) [25]. Existing methods for solving Accel use backward-chaining
search [28], Markov Logic [22, 2], or Integer Linear Programming (ILP) [19].
In this work we realize abduction for Accel in the declarative mechanism of
Answer Set Programming. Our motivated is twofold: (a) it will allow for adding
complex constraints and optimization criteria more flexibly than in search-based
realizations of abduction, moreover (b) it can provide insights for managing other
problems with prohibitively large groundings in ASP.
Tackling this problem in ASP seems possible, because a recent solution for
Accel is based on first creating an ILP theory (in Java) and then solving it [19].
Yet there are two major challenges when realizing FOL abduction in ASP.
– The Unique Names Assumption (UNA) is not applicable in FOL in general.
In particular the Accel benchmark requires a partial UNA that holds only
for sort names. In ASP, on the contrary, UNA holds for all ground terms.
– Backward-chaining requires instantiation of body variables with new con-
stant terms. In ASP this is equivalent to existential variables in rule heads,
⋆
This work has been supported by Scientific and Technological Research Council of
Turkey (TUBITAK) Grant 114E777.
76
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
i.e., variables that are absent in the rule body which makes the rule unsafe.
In ASP rules must be safe, therefore we need to encode value invention.
Note that value invention makes FOL abduction undecidable in general. The
Accel knowledge base is an acyclic theory,1 therefore undecidability is not an
issue and we can realize value invention in ASP using Skolemization.
Partial UNA has the effect that we must encode equivalence classes between
terms and effects of these equivalences in ASP. Sort names make the problem
of finding the smallest set of abducibles that explains a goal nontrivial (without
sort names the smallest explanation is those where all terms are equivalent).
Both value invention and partial UNA make an ASP solution tricky, in par-
ticular the size of the instantiated program can become problematic easily.
In this study we approach these challenges and analyze problems that become
apparent. We describe three encodings which use different rewritings of the Accel
knowledge base and an observation that should be explained into ASP:
– BackCh models a backward-chaining algorithm and the notion of ‘factoring’
(to deal with equivalence) similar to the algorithm proposed by Ng [28],
– BwFw defines potential domains of predicates (as in Magic Sets [33]), gues-
ses all potential atoms as abducibles, infers truth of atoms using the original
axioms from the knowledge base, and checks if this explains the observation,
– Simpl realizes a simplified abduction with closed domain and UNA.
BackCh and BwFw realizing existential quantification using uninterpreted
functions to build Skolem terms. Simpl serves as a performance baseline.
Our experiments with Accel show, that only small instances can be solved
within reasonable resource limits, and that memory as well as proving optimality
of solutions are problematic issues. We analyze the main reasons for these ob-
servations using solver statistics, and we outline possibilities for achieving better
results in future work.
Section 2 gives preliminaries of abduction and ASP, Section 3 describes
rewritings and ASP encodings, Section 4 reports on experiments, and Section 5
concludes with related work and an outlook on future work.
2 Preliminaries
We give a brief introduction of Abduction in general and First Order Horn
abduction in specific, moreover we give brief preliminaries of ASP.
Notation: variables start with capital letters and constants with small letters.
2.1 Abduction
Abduction, originally described in [29], can be defined logically as follows. Given
a set T of background knowledge axioms and an observation O, find a set H
1
This should be true according to [28]. Actually we had to deactivate one cyclic axiom
in the knowledge base to make this property true.
77
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
of hypothesis atoms such that T and H are consistent, and reproduce the ob-
servation, i.e., T ∪ H ⊧
/ and T ∪ H ⊧ O. In this work we formalize axioms and
observations in First Order Logic (FOL) as done by Ng [28]: the observation (in
the following called ‘goal’) O is an existentially quantified conjunction of atoms
∃V1 , . . . , Vk ∶ o1 (V1 , . . . , Vk ) ∧ ⋯ ∧ om (V1 , . . . , Vk ) (1)
and an axiom in T is a universally quantified Horn clause of form
c(V1 , . . . , Vk ) ⇐ p1 (V1 , . . . , Vk ) ∧ ⋯ ∧ pr (V1 , . . . , Vk ). (2)
or an integrity constraints (like (2) but without a head).
The set H of hypotheses can contain any predicate from the theory T and
the goal O, hence existence of a solution is trivial. Explanations with minimum
cardinality are considered optimal. A subset of constants is declared as sort
names that cannot be abduced as equivalent with other constants.
Example 1 (Running Example). Consider the following text
‘Mary lost her father. She is depressed.’
which can be encoded as the following FOL goal, to be explained by abduction.
name(m, mary)∧lost(m, f )∧fatherof (f, m)∧inst(s, female)∧is(s, depressed )
Given the set of axioms
inst(X, male) ⇐ fatherof (X, Y ) (3)
inst(X, female) ⇐ name(X, mary) (4)
importantfor (Y, X) ⇐ fatherof (Y, X) (5)
inst(X, person) ⇐ inst(X, male) (6)
is(X, depressed ) ⇐ inst(X, pessimist) (7)
is(X, depressed ) ⇐ is(Y, dead ) ∧ importantfor (Y, X) (8)
lost(X, Y ) ⇐ is(Y, dead ) ∧ importantfor (Y, X) ∧ inst(Y, person) (9)
and sort names
person male female dead depressed (10)
we can use abduction to infer the following: (a) loss of a person here should be
interpreted as death, (b) ‘she’ refers to Mary, and (c) her depression is because
of her father’s death because her father was important for her.
This is reached by abducing the following atoms and equivalences.
name(m, mary) fatherof (f, m) is(f, dead ) m = s (11)
78
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
The first two atoms directly explain goal atoms. We can explain the remaining
goal atoms by showing inferring truth of the following atoms.
inst(f, male) [infered via (3) using (11)] (12)
inst(m, female) [infered via (4) using (11)] (13)
inst(s, female) [goal, factored from (13) using (11)]
importantfor (f, m) [infered via (5) using (11)] (14)
inst(f, person) [infered via (6) using (12)] (15)
is(m, depressed ) [infered via (8) using (11) and (14)] (16)
is(s, depressed ) [goal, factored from (16) using (11)]
lost(m, f ) [goal, infered via (9) using (11), (14), and (15)]
Note that there are additional possible inferences but they are not necessary
to explain the goal atoms. Moreover note that another abductive explanations
(with higher number of abduced atoms and therefore higher cost) would be to
abduce all goal atoms, or to abduce inst(m, pessimist) and lost(m, f ) instead of
abducing is(f, dead ). ◻
Complexity-wise we think that deciding optimality of a solution is harder than
for cardinality minimal abduction on (non-ground) logic programs under well-
founded semantics [11, Sec. 4.1.3] because value invention provides a ground
term inventory of polynomial size in the number of constants in the goal. The
propositional case has been analyzed in [3, 10]. See also Section 5.1.
2.2 Answer Set Programming
We assume familiarity with ASP [16, 25, 12, 14] and give only brief preliminaries
of those part of the ASP-Core-2 standard [5] that we will use: logic programs with
(uninterpreted) function symbols, aggregates, choices, and weak constraints. A
logic program consists of rules of the form
α ← β1 , . . . , βn , not βn+1 , . . . , not βm .
where α and βi are head and body atoms, respectively, and not denotes negation
as failure. We say that a rule is a fact if m = 0, and it is a constraint if there
is no head α. Atoms can contain constants, variables, and function terms, and
programs must obey safety restrictions (see [5]) to ensure a finite instantiation.
Anonymous variables of form ‘_’ are replaced by new variable symbols.
An aggregate literal in the body of a rule accumulates truth values from a
set of atoms, e.g., 2 = #count{X ∶ p(X)} is true iff the extension of p (in the
answer set candidate) contains exactly 2 elements.
Choice constructions can occur instead of rule heads, they generate a solution
space if the rule body is satisfied; e.g., 1 ≤ {p(a); p(b); p(c)} ≤ 2 in the rule head
generates all solution candidates where at least 1 and at most 2 atoms of the
set are true. The bounds can be omitted. The colon symbol ‘:’ can be used
to define conditions for including atoms in a choice, for example the choice
79
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
{p(X) ∶ q(X), not r(X)} encodes a guess over all p(X) such that q(X) is true
and r(X) is not true.
A weak constraint of form
↜ p(X). [1@1, X]
denotes that an answer set I has cost equivalent to the size of the extension of p
in I. Answer sets of the lowest cost are considered optimal. Note that the syntax
[A@B, X] denotes that cost A is incurred on level B, and costs are summed over
all distinct X (i.e., X ensures each atom p(X) ∈ I is counted once).
Semantics of an answer set program P are defined using its Herbrand uni-
verse, ground instantiation, and the GL-reduct [16] which intuitively reduces the
program using assumptions in an answer set candidate.
3 Modeling Abduction in ASP
We next describe two encodings for modeling abduction with partial UNA and
with value invention in ASP (Sections 3.1 and 3.2) and one simpler encoding
with UNA for all constants and without value invention (Section 3.3).
All atoms in Accel have arity 2. For practical reasons we represent an atom
of the form pred(arg1, arg2) as c(pred, arg1, arg2).
Goals in Accel have no variables, hence we can represent them as facts. For
our example we represent the goal as the following set of ASP facts.
goal (c(name, m, mary)). goal (c(lost, m, f )). goal (c(fatherof , f, m)).
goal (c(inst, s, female)). goal (c(is, s, depressed )).
Sorts are encoded as facts as follows.
sortname(person). sortname(male). sortname(female).
sortname(dead ). sortname(depressed ).
3.1 Modeling Backward-Chaining (BackCh)
Our first encoding represents the abduction algorithm by Ng [28] in the ASP
grounder: (i) backward-chain from the goal and invent new constants on the
way, (ii) factor atoms with other atoms in the goal or with atoms discovered in (i)
and abduce equivalences between constant terms, (iii) mark atoms that have not
been inferred or factored as abduced, and (iv) search for the solution with the
minimum number of abduced atoms while obeying integrity constraints. Note
that this is the most straightforward modeling idea, although we consider it the
least declarative one because it is oriented towards realizing an algorithm and
does not realize abduction as usually done in ASP (for that see next section).
First, everything that is a goal is defined to be true, and everything true
must either be abduced, inferred, or factored.
true(P ) ← goal(P ).
1 ≤ {abduce(P ); inf er(P ); f actor(P )} ≤ 1 ← true(P ). (17)
80
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
We prefer solutions with a minimum number of abduced terms.
↜ abduce(P ). [1@1, P ] (18)
Backward chaining is realized by rewriting each axiom of form (2) into two
parts: a guess whether the head is inferred via this rule, and for each body atom
that it must be inferred, abduced, or factored, if the head was inferred.
For example axiom (8) is translated into
0 ≤ {inferVia(r1 , c(is, X, depressed ))} ≤ 1 ←
infer (c(is, X, depressed )). (19)
inferenceNeeds(c(is, X, depressed ), r1 , c(importantfor , s1 (X), X)) ←
inferVia(r1 , c(is, X, depressed )). (20)
inferenceNeeds(c(is, X, depressed ), r1 , c(is, s1 (X), dead )) ←
inferVia(r1 , c(is, X, depressed )). (21)
where r1 is a unique identifier for axiom (8); rule (19) guesses if inferring
is(X, depressed ) happens via r1 ; and rules (20) and (21) define that this in-
ference requires to justify atoms importantfor (s1 (X), X) and is(s1 (X), dead ).
Note that s1 (⋅) is a Skolem function unique to axiom (8).
For each atom that is inferred, we add a constraint that it must be inferred
via at least one rule. Moreover each atom required by such inference is defined
as true and hence must be justified according to (17).
← inf er(P ), 0 ≤ #count{A, P ∶ inf erV ia(A, P )} ≤ 0.
true(Body) ← inf erenceN eeds(Head, Axiom, Body).
For factoring we need to handle absence of the UNA, so we obtain the Herbrand
Universe (HU) and obtain the ‘User Herbrand Universe’ (UHU) of constants
that are not sort names and can be equivalent to other constants.
hu(C) ← true(c(_, C, _)).
hu(C) ← true(c(_, _, C)).
uhu(C) ← hu(C), not sortname(C).
We guess if a member of UHU is represented by another member of UHU.
0 ≤ {rep(X, Y ) ∶ uhu(X), X < Y } ≤ 1 ← uhu(Y ). (22)
This guesses at most one representative for each member of UHU. Note that
operator ‘<’ in (22) realizes lexicographic comparison of ground terms; this means
the representative of an equivalence class of UHU terms is always the smallest
term in that class (this reduces symmetries in the search space).
The following rules ensure that no ground term is both represented and
representing another one using rep.
representative(X) ← rep(X, Y ). (23)
represented(Y ) ← rep(X, Y ). (24)
← representative(X), represented(X). (25)
81
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
Rules (22)–(25) generate all possible equivalence relations over UHU terms, en-
coded as mappings to representative terms. If a term has neither a representative
nor is representing another term, it is a singleton equivalence class.
Given rep, we define a mapping map for all HU terms to their representative,
where singletons and sort names are their own representatives.
map(X, Y ) ← rep(X, Y ). (26)
map(X, X) ← hu(X), not represented(X). (27)
Now that we generate and represent equivalence classes, we can perform
factoring. We experiment with three formulations: all of them define a predicate
f actorOk(P ) if factoring is allowed, and they share the following three rules:
(28) requires f actorOk to be true for factored atoms, while (29) and (30) define
the factoring base which is the set of inferred or abduced atoms, i.e., the set of
atoms that other atoms can be factored with.
← factor (P ), not factorOk (P ). (28)
factoringbase(A) ← infer (A). (29)
factoringbase(A) ← abduce(A). (30)
The three factoring variations are as follows.
● Factoring (a) uses the map predicate to match factored atoms to the factoring
base and is realized as follows.
factorOk (c(P, A1 , B1 )) ← factor (c(P, A1 , B1 )), factoringbase(c(P, A2 , B2 )),
map(A, A1 ), map(A, A2 ), map(B, B1 ), map(B, B2 ).
● Factoring (b) defines a canonical factoring base using the map predicate and
matches factored elements with that canonical base using the following rules.
cfactoringbase(c(P, A, B)) ← factoringbase(c(P, A1 , B1 )),
map(A, A1 ), map(B, B1 ).
factorOk (c(P, A1 , B1 )) ← cfactoringbase(c(P, A, B)),
factor (c(P, A1 , B1 )), map(A, A1 ), map(B, B1 ).
● Factoring (c) defines a relation for canonicalizing atoms using the map predi-
cate and defines factorOk using that relation.
noncanonical (P ) ← factor (P ).
noncanonical (Q) ← factoringbase(Q).
canonical (c(P, A, B), c(P, A1 , B1 )) ← noncanonical (c(P, A1 , B1 )),
map(A, A1 ), map(B, B1 ).
factorOk (P1 ) ← factor (P1 ), factoringbase(P2 ),
canonical (P, P1 ), canonical (P, P2 ).
82
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
3.2 Skolemized Domain and Standard ASP Abduction (BwFw)
This encoding follows an idea similar to Magic Sets [33]: starting from the goal
(in Magic Sets the query) we represent the domain of each argument of each
predicate. Subsequently we define domains of predicates in the body of an axiom
based on the domain of the predicate in heads of that axiom, deterministically
expanding the domain with Skolem terms whenever there are variables in the
axiom body that are not in the axiom head. Once we have the domains, we
can follow the usual ASP approach for abduction: (i) guess (using the domain)
which atoms are our abduction hypothesis, (ii) use axioms to infer what becomes
true due to the abduction hypothesis; and (iii) require that the observation is
reproduced. In BackCh, equivalence was used for factoring (which reduces the
number of abducibles required to derive the goal). In BwFw, we instantiate the
whole potential proof tree, so we do not need factoring between atoms in rules,
it is sufficient to factor abducibles with one another. Hence in this encoding we
handle equivalences by defining an atom to be true if its terms are equivalent
with the terms of an abduced atom.
We next give the encoding in detail.
Predicates in Accel have arity 2, so we represent the domain as dom(P, S, O),
i.e., predicate P has ⟨S, O⟩ as potential extension. We seed dom from the goal.
dom(P, S, O) ← goal(c(P, S, O)).
Domains are propagated by rewriting axioms of form (2) as indicated above. For
example (8) is translated into the following rules.
dom(importantfor , s1 (X), X) ← dom(is, X, depressed ). (31)
dom(is, s1 (X), dead ) ← dom(is, X, depressed ). (32)
Additionally we rewrite each axiom into an equivalent rule in the ASP rep-
resentation, for example we rewrite (8) into the following rule.
true(c(is, X, depressed )) ← true(c(importantfor , Y, X)),
true(c(is, Y, dead )). (33)
For guessing representatives we first define UHU for first and second argu-
ments of each predicate and we define HU over all arguments.
dom 1 (P, X) ← dom(P, X, _).
dom 2 (P, Y ) ← dom(P, _, Y ).
uhu1 (P, X) ← dom 1 (P, X), not sortname(X).
uhu2 (P, Y ) ← dom 2 (P, Y ), not sortname(Y ).
hu(X) ← dom 1 (_, X).
hu(Y ) ← dom 2 (_, Y ).
We guess representatives, i.e., equivalence classes, only among those UHU ele-
ments that can potentially be unified because they are arguments of the same
83
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
predicate at the same argument position.2
0 ≤ {rep(X1 , X2 ) ∶ uhu1 (P, X2 ), X1 < X2 } ≤ 1 ← uhu1 (P, X1 ).
0 ≤ {rep(Y1 , Y2 ) ∶ uhu2 (P, Y2 ), Y1 < Y2 } ≤ 1 ← uhu2 (P, Y1 ).
We reuse (23)–(27) from the BackCh encoding to ensure that rep encodes an
equivalence relation and to define map. (Note also that hu is used in (27).)
We abduce atoms using the domain under the condition that the domain
elements are representatives of their equivalence class (symmetry breaking).
{abduce(c(P, S, O)) ∶ dom(P, S, O), not represented (S), not represented (O)}.
We define that abduced atoms are true, and we use map to define that atoms
equivalent with abduced atoms are true.
true(A) ← abduce(A).
true(c(P, A, B)) ← abduce(c(P, RA, RB)), map(RA, A), map(RB, B). (34)
This makes all consequences of the abduction hypothesis in the axiom theory
true while taking into account equivalences.
Finally we again require that the observation is reproduced, and we again
minimize the number of abduced atoms. (Note that term equivalence has been
taken care of in (34) hence we can ignore it for checking the goal.)
← goal (A), not true(A). (35)
↜ abduce(P ). [1@1, P ] (36)
3.3 Closed Domain and UNA (Simpl)
This encoding propagates domains differently from the previous one: it does
not introduce Skolem terms but always the same null term for variables in
axiom bodies that are not contained in the axiom head. Abduction substitutes
all possible constants for these null terms, hence this encoding does not realize
an open domain. Moreover, this encoding uses the UNA for all terms.
This encoding is less expressive than the previous ones, it is incomplete but
sound: Simpl finds a subset of solutions that other encodings find, and for this
subset each solution has same cost as in other encodings. We use Simpl pri-
marily for comparing memory and time usage with other encodings and other
approaches. For readability we repeat some rules from previous encodings.
As in BwFw, the domain is seeded from the goal.
dom(P, S, O) ← goal (c(P, S, O)).
The rewriting is different, however: instead of rewriting the example axiom (8)
into (31) and (32) we create the following rules.
dom(importantfor , null , X) ← dom(is, X, depressed ).
dom(is, null , dead ) ← dom(is, X, depressed ).
2
A more naive encoding showed significantly higher memory requirements.
84
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
Status Resources
Encoding OPT SAT OOT OOM Space (osp) Time (otm/grd/slv)
sum sum sum sum MB/avg s/avg
BackCh (a) 40 0 0 460 4636 (1375) 148 (152/142/ 6)
BackCh (b) 238 2 0 260 3537 (2339) 175 (147/135/ 41)
BackCh (c) 36 4 0 460 4612 (1146) 126 (152/117/ 9)
BwFw 10 0 0 490 4884 ( 524) 212 ( 12/211/ 0)
Simpl 132 258 10 100 1875 ( 208) 380 (107/ 52/323)
Table 1. Experimental Results, accumulated over 10 runs of each of the 50 instances of
Accel: OPT, SAT, OOT, and OOM denote that the solver found the optimal solution,
found a solution without proving optimality, exceeded the time limit (10 min), and
exceeded the memory (5 GB), respectively. Numbers in brackets are the space and
time usage of runs that found the optimum (osp/otm), the time spent in grounding
(grd), and the time spent in solving (slv). Averages are computed over all runs, except
for (osp) and (otm) that are averaged over runs where the optimum was found.
Here, null is used instead of Skolem terms.
We define the HU as all domain elements except null .
hu(X) ← dom(_, X, _), X ≠ null .
hu(Y ) ← dom(_, _, Y ), Y ≠ null .
Now we define a mapping that maps null to each element of (implicit) UHU and
contains the identity mapping for HU.
nullrepl (X, X) ← hu(X).
nullrepl (null , X) ← hu(X), not sortname(X). (37)
We abduce atoms using this mapping and define that abduced atoms are true.
{abduce(c(P, S ′ , O′ ))} ← dom(P, S, O), nullrepl (S, S ′ ), nullrepl (O, O′ ).
true(c(P, A, B)) ← abduce(c(P, A, B)).
We propagate truth as in BwFw using the rewriting exemplified in (33).
We again require goals to be true and minimize the number of abduced atoms.
← goal (A), not true(A).
↜ abduce(P ). [1@1, P ]
Note that, although this encoding solves an easier problem than the other
encodings, we will see that it does not necessarily perform better.
4 Experimental Results
To test the above encodings, we performed experiments using the Accel bench-
mark3 [28]. This benchmark consists of 50 instances (i.e., goals) with between 5
3
ftp://ftp.cs.utexas.edu/pub/mooney/accel
85
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
and 26 atoms in a goal (12.6 atoms on average), and a knowledge base consisting
of 190 first order Horn rules with bodies of size between 1 and 11 atoms (2.2 on
average). Our encodings and instances used in experiments are available online.4
The benchmarks were performed on a computer with 48 GB RAM and two
Intel E5-2630 CPUs (total 16 cores) using Ubuntu 14.04 and Clingo 4.5.0 [15].
Each run was limited to 10 minutes and 5 GB RAM, HTCondor was used as a job
scheduling system, each run was repeated 10 times and no more than 8 jobs were
running simultaneously. For Clingo we used the setting --configuration=handy.
Table 1 shows results of the experiments.
Exceeding the memory of 5 GB turns out to be a significant problem in
all encodings, even for Simpl where (only) 10 instances exceeding the memory.
Memory was always exceeded during grounding, never during solving.
Our encodings perform much worse than the state-of-the-art for solving Accel
which is less than 10 s per instance on average [19].
Encoding Simpl is able to ground more instances than the other encodings,
however it only finds the optimal solution for 132 runs while BackCh (b) finds
optimal solutions for 238 runs, although Simpl encodes a sound approximation
of the problem encoded in BackCh and BwFw.
Encoding BwFw, which is most similar to classical abduction encodings in
ASP, performs worst due to memory exhaustion: only one instance can be solved.
In BwFw the high space complexity comes from the full forward-instantiation
of the whole knowledge base after guessing representatives for the domain of
each abduced atom. Although BwFw first backward-chains the domain using
a deterministic set of rules, it seems to instantiate a much larger part of the
rules necessary for solving the problem, in particular in comparison with the
BackCh encoding. Observe that we split the representation for UHU which
might seem unintuitive as we do not do this in other encodings. However, when
we experimented with a more naive encoding for BwFw (replacing uhu1 and
uhu2 by a single uhu) this encoding could not even solve a single instance within
the 5 GB memory limit.
The BackCh encodings perform best and show big differences among the
factoring variations. Factoring (b) is clearly superior to (a) and (c): it uses sig-
nificantly less memory (only 260 out-of-memory runs) and once grounding is
successful it solves many instances (238) within the timeout. The reason for this
can be found in the rules defining factorOk : factoring (a) contains 4 atoms of
map with six joining 6 variables, hence its instantiation contains (in worst case)
O(n6 ) rules, where n is the size of HU; moreover (c) defines canonical from map
with by defining O(n3 ) distinct atoms and joins these atoms to define factorOk ,
again resulting in O(n6 ) rules. Encoding (b) on the other hand defines O(n3 )
distinct atoms with predicate cfactoringbase and joins them to 2 instances of
map, resulting in O(n5 ) rules defining factorOk .
Single Instance Analysis. To analyze performance differences between en-
codings, we looked at instance # 8 which is the smallest instance and the single
instance where all encodings found an optimal solution.
4
https://bitbucket.org/knowlp/supplement-rcra2015-asp-fo-abduction/
86
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
Encodings BackCh (a) and BackCh (c) require 117 s and 244 s grounding
time, respectively, and both groundings contain ∼150 k ASP rules. Although
BackCh (b), BwFw, and Simpl stay below 10 s grounding time, BwFw pro-
duces an amazing 803 k ASP rules. The reason is, that (34) creates many po-
tentially true atoms, which instantiates many axioms. As a consequence BwFw
grounds comparatively fast but at the same time produces the biggest grounding.
The smallest grounding is produced by Simpl, which also has fewest OOM
results. Yet Simpl finds the optimal solution for fewer instances than BackCh
(b). Solver statistics show that Simpl requires 463 k choice points in the solver
and creates 4 k conflict lemmas for instance 8, while BackCh (b) proves opti-
mality using 737 choice points and 150 lemmas. We conjecture that these choice
points originate in the naive substitution of null with UHU elements in (37),
which produces a big grounding and a big hypothesis space with many symmet-
ric solutions of equal cost. Such symmetries makes it difficult to prove optimality.
Additional Observations. As suggested by a reviewer we ran our encodings
with and without projection to abduce atoms. This did not change run times
significantly, however it greatly reduced log file size.
5 Discussion and Conclusion
We presented encodings for realizing abduction with an open domain in the
absence of the UNA and performed experiments using the Accel benchmark.
Experiments show clear differences between our encodings, and they all per-
form much worse than the state-of-the-art for Accel [19]. Hence we consider this
work a negative result. Nevertheless we observed huge performance variation
between our encodings, and we think there is still potential for finding better
encodings (and solver parameters).
5.1 Related Work
The idea of abduction goes back to Peirce [29] and was later formalized in logic.
Abductive Logic Programming (ALP) is an extension of logic programs with
abduction and integrity constraints. Kakas et al. [20] discuss ALP and applica-
tions, in particular they relate Answer Set Programming and abduction. Fung
et al. describe the IFF proof procedure [13] which is a FOL rewriting that is
sound and complete for performing abduction in a fragment of ALP with only
classical negation and specific safety constraints. Denecker et al. [8] describe
SLDNFA-resolution which is an extension of SLDNF resolution for performing
abduction in ALP in the presence of negation as failure. They also describe a
way to ‘avoid Skolemization by variable renaming’ which is a strategy that can
be mimicked in ASP by using HEX for value invention (instead of uninterpreted
function terms). Kakas et al. describe the A-System for evaluating ALP using
an algorithm that interleaves instantiation of variables and constraint solving
[21]. The CIFF framework [26] is conceptually similar to the A-System but it
87
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
allows a more relaxed use of negation. The SCIFF framework [1] relaxes some
restrictions of CIFF and provides facilities for modeling agent interactions.
Implementations of ALP have in common that they are based on evaluation
strategies similar to Prolog [26]. CIFF is compare with ASP on the example
of n-queens and the authors emphasize that CIFF has more power due to its
partial non-ground evaluation [26]. However they also show a different CIFF
encoding that performs much worse than ASP. Different from CIFF and earlier
ALP implementations, our ASP encodings are first instantiated and then solved.
Weighted abduction (called cost-based abduction by some authors) [18] is
FOL abduction with costs that are propagated along axioms in a proof tree.
The purpose of costs is to find the most suitable abductive explanations for
interpretation of natural language. The solver Henry-n700 [19] realizes weighted
abduction by first instantiating an ILP instance with Java and then finding
optimal solutions for the ILP instance. Our approach is similar and therefore
our work is related more to weighted abduction than to ALP.
Probabilistic abduction was realized in Markov Logic [30] in the Alchemy
system [23] although without an open domain [2, 32], which makes it similar to
the Simpl encoding. (Alchemy naively instantiates existential variables in rule
heads with all known ground terms just as Simpl does.)
5.2 Future Work
As the Accel benchmark problems can be solved much faster (i.e., within a few
seconds on average) with a classical backward chaining implementation in Java
and an ILP solver [19], we conjecture that a solution in ASP has the potential
to be similarly fast. In the future we want to develop encodings that perform
nearer to the state-of-the-art. We believe that we can gain increased flexibility if
we model this problem in ASP as opposed to creating an ILP theory using Java.
Our experiments show that small changes in encodings can lead to big per-
formance changes regarding grounding size, grounding speed, finding an initial
solution, and proving optimality. We are currently investigating alternative en-
codings, in particular to replace guessing of representatives by a more direct
guessing of the equivalence relation.
As large groundings are a major issue in our work, interesting future work
includes using dlv [24] which is known to be strong in grounding, or solvers that
perform lazy grounding such as idp [7] or OMiGA [6]. Another possible improve-
ment of grounding is to replace grounding-intensive constraints by sound approx-
imations with lower space complexity, and create missing constraints on demand
when they are violated. An equivalent strategy is used in Henry-n700 where and
it is called Cutting Plane Inference and described as essential for the performance
of the ILP solution for weighted abduction [19]. In ASP such strategies are used
by state-of-the-art solvers for on-demand generation of loop-formula nogoods.
User-defined on-demand constraints can be realized using a custom propagator
in Clingo [15] or on-demand constraints in HEX [9, Sec. 2.3.1].
Potentially beneficial for future improvements of this work are Open Answer
Set Programming (OASP) [17] which inherently supports open domains, and
88
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
Datalog± [4] which supports existential constructions in rule heads. Both for-
malisms have been used for representing Description Logics in ASP and could
provide insights for future work about modeling FOL abduction in ASP.
So far we prefer the least number of abduced atoms to find optimal solu-
tions. In the future we want to consider more sophisticated preferences based on
Coherence [27] and based on Relevance Theory [31].
Acknowledgements
We thank the anonymous reviewers for their constructive and useful feedback.
References
1. M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello, and P. Torroni. Ver-
ifiable agent interaction in abductive logic programming: The SCIFF framework.
ACM Transactions on Computational Logic, 9(4):Article No. 29, 2008.
2. J. Blythe, J. R. Hobbs, P. Domingos, R. J. Kate, and R. J. Mooney. Implementing
Weighted Abduction in Markov Logic. In International Conference on Computa-
tional Semantics (IWCS), pages 55–64, 2011.
3. T. Bylander, D. Allemang, M. C. Tanner, and J. R. Josephson. The computational
complexity of abduction. Artificial Intelligence, 49(1-3):25–60, 1991.
4. A. Calì, G. Gottlob, and T. Lukasiewicz. Datalog+/-: A Unified Approach to
Ontologies and Integrity Constraints. In International Conference on Database
Theory, pages 14–30, 2009.
5. F. Calimeri, W. Faber, M. Gebser, G. Ianni, R. Kaminski, T. Krennwallner,
N. Leone, F. Ricca, and T. Schaub. ASP-Core-2 Input language format. Tech-
nical report, ASP Standardization Working Group, 2012.
6. M. Dao-tran, T. Eiter, M. Fink, G. Weidinger, and A. Weinzierl. OMiGA : An
Open Minded Grounding On-The-Fly Answer Set Solver. In Logics in Artificial
Intelligence (JELIA), pages 480–483, 2012.
7. B. De Cat, M. Denecker, P. Stuckey, and M. Bruynooghe. Lazy model expansion:
Interleaving grounding with search. Journal of Artificial Intelligence Research,
52:235–286, 2015.
8. M. Denecker and D. de Schreye. SLDNFA: An abductive procedure for abductive
logic programs. The Journal of Logic Programming, 34(2):111–167, 1998.
9. T. Eiter, M. Fink, G. Ianni, T. Krennwallner, C. Redl, and P. Schüller. A model
building framework for answer set programming with external computations. The-
ory and Practice of Logic Programming, 2015. arXiv:1507.01451 [cs.AI], to appear.
10. T. Eiter and G. Gottlob. The Complexity of Logic-Based Abduction. Journal of
the ACM, 42(1):3–42, 1995.
11. T. Eiter, G. Gottlob, and N. Leone. Abduction from logic programs: Semantics
and complexity. Theoretical Computer Science, 189(1-2):129–177, 1997.
12. T. Eiter, G. Ianni, and T. Krennwallner. Answer Set Programming: A Primer. In
Reasoning Web Summer School, Lecture Notes in Computer Science, 2009.
13. T. H. Fung and R. Kowalski. The IFF proof procedure for abductive logic pro-
gramming. The Journal of Logic Programming, 33(2):151–165, 1997.
14. M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub. Answer Set Solving in
Practice. Morgan Claypool, 2012.
89
P.Schüller Modeling Abduction over Acyclic First-Order Logic Horn Theories in ASP
15. M. Gebser, B. Kaufmann, R. Kaminski, M. Ostrowski, T. Schaub, and M. Schnei-
der. Potassco: The Potsdam Answer Set Solving Collection. AI Communications,
24(2):107–124, 2011.
16. M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming.
In International Conference and Symposium on Logic Programming (ICLP/SLP),
pages 1070–1080, 1988.
17. S. Heymans, D. Van Nieuwenborgh, and D. Vermeir. Open Answer Set Pro-
gramming with Guarded Programs. ACM Transactions on Computational Logic,
9(4):26, 2008.
18. J. R. Hobbs, M. Stickel, P. Martin, and D. Edwards. Interpretation as abduction.
Artificial Intelligence, 63(1-2):69–142, 1993.
19. N. Inoue and K. Inui. ILP-based Inference for Cost-based Abduction on First-order
Predicate Logic. Information and Media Technologies, 9:83–110, 2014.
20. A. C. Kakas, R. A. Kowalski, and F. Toni. Abductive Logic Programming. Journal
of Logic and Computation, 2(6):719–770, 1992.
21. A. C. Kakas, B. Van Nuffelen, and M. Denecker. A-System: Problem solving
through abduction. In International Joint Conference on Artificial Intelligence
(IJCAI), pages 591–596, 2001.
22. R. J. Kate and R. J. Mooney. Probabilistic Abduction using Markov Logic Net-
works. In IJCAI Workshop on Plan, Activity, and Intent Recognition, 2009.
23. S. Kok, M. Sumner, M. Richardson, P. Singla, H. Poon, L. D, J. Wang, A. Nath, and
P. Domingos. The Alchemy system for statistical relational AI. Technical report,
Department of Computer Science and Engineering, University of Washington, 2010.
24. N. Leone, G. Pfeifer, W. Faber, and T. Eiter. The DLV system for knowledge
representation and reasoning. ACM Transactions on Computational Logic, 7(3):1–
58, 2006.
25. V. Lifschitz. What Is Answer Set Programming ? In AAAI Conference on Artificial
Intelligence, pages 1594–1597, 2008.
26. P. Mancarella, G. Terreni, F. Sadri, F. Toni, and U. Endriss. The CIFF proof pro-
cedure for abductive logic programming with constraints: Theory, implementation
and experiments. Theory and Practice of Logic Programming, 9(6):691–750, 2009.
27. H. Ng and R. Mooney. Abductive Plan Recognition and Diagnosis: A Compre-
hensive Empirical Evaluation. In Knowledge Representation and Reasoning (KR),
pages 499–508, 1992.
28. H. T. Ng. A General Abductive System with Applications to Plan Recognition and
Diagnosis. Phd thesis, University of Texas at Austin, 1992.
29. C. S. Peirce. Abduction and Induction. In Philosophical Writings of Peirce, chap-
ter 11, pages 150–156. Dover Publications, 1955.
30. M. Richardson and P. Domingos. Markov logic networks. Machine Learning, 62(1-
2):107–136, Jan. 2006.
31. P. Schüller. Tackling Winograd Schemas by Formalizing Relevance Theory in
Knowledge Graphs. In International Conference on Principles of Knowledge Rep-
resentation and Reasoning (KR). AAAI Press, 2014.
32. P. Singla and R. J. Mooney. Abductive Markov Logic for Plan Recognition. In
AAAI Conference on Artificial Intelligence, pages 1069–1075, 2011.
33. J. D. Ullman. Principles of Database and Knowledge Base Systems. Computer
Science Press, 1989.
90