We describe encodings in Answer Set Programming for abductive reasoning in First Order Logic in acyclic Horn theories in the presence of value invention and in the absence of Unique Names Assumption. 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 Order Logic abduction, mainly due to large groundings. We analyze reasons for this bad performance and outline potential future improvements.
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 particular 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]), guesses 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 observations 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
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, 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.
of hypothesis atoms such that T and H are consistent, and reproduce the
observation, 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)
and an axiom in T is a universally quantified Horn clause of form
c(V1, . . . , Vk) ⇐ p1(V1, . . . , Vk) ∧ ⋯ ∧ pr(V1, . . . , Vk).
or an integrity constraints (like (
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.
(
This is reached by abducing the following atoms and equivalences.
is(X, depressed ) ⇐ is(Y, dead ) ∧ importantfor (Y, X)
lost (X, Y ) ⇐ is(Y, dead ) ∧ importantfor (Y, X) ∧ inst (Y, person) (
m = s 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 ) inst (X, female) ⇐ name(X, mary ) importantfor (Y, X) ⇐ fatherof (Y, X) inst (X, person) ⇐ inst (X, male) is(X, depressed ) ⇐ inst (X, pessimist ) 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) inst (m, female) inst (s, female) importantfor (f, m)
inst (f, person)
is(m, depressed )
is(s, depressed )
lost (m, f )
[infered via (
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 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). 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 universe, ground instantiation, and the GL-reduct [16] which intuitively reduces the program using assumptions in an answer set candidate. 3
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 ). 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 ).
(
↜ abduce(P ). [1@1, P ]
Backward chaining is realized by rewriting each axiom of form (
For example axiom (
infer (c(is, X, depressed )).
inferenceNeeds (c(is, X, depressed ), r1, c(importantfor , s1(X), X)) ←
inferenceNeeds (c(is, X, depressed ), r1, c(is, s1(X), dead )) ←
inferVia(r1, c(is, X, depressed )). (
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 (
← 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)).
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 ).
(
The following rules ensure that no ground term is both represented and representing another one using rep.
representative(X) ← rep(X, Y ).
(
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 ).
map(X, X) ← hu(X), not represented(X).
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:
(
← factor (P ), not factorOk (P ).
factoringbase(A) ← infer (A).
factoringbase(A) ← abduce(A).
(
factor (c(P, A1, B1)), map(A, A1), map(B, B1). ● Factoring (c) defines a relation for canonicalizing atoms using the map predicate 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)), factorOk (P1) ← factor (P1), factoringbase(P2), map(A, A1), map(B, B1).
canonical (P, P1), canonical (P, P2). 3.2
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 (
dom(importantfor , s1(X), X) ← dom(is, X, depressed ).
dom(is, s1(X), dead ) ← dom(is, X, depressed ).
Additionally we rewrite each axiom into an equivalent rule in the ASP
representation, for example we rewrite (
true(c(is, X, depressed )) ← true(c(importantfor , Y, X)),
(
For guessing representatives we first define UHU for first and second arguments of each predicate and we define HU over all arguments.
dom1(P, X) ← dom(P, X, _). dom2(P, Y ) ← dom(P, _, Y ). uhu1(P, X) ← dom1(P, X), not sortname(X). uhu2(P, Y ) ← dom2(P, Y ), not sortname(Y ).
hu(X) ← dom1(_, X).
hu(Y ) ← dom2(_, Y ).
We guess representatives, i.e., equivalence classes, only among those UHU elements that can potentially be unified because they are arguments of the same 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 (
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). 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 primarily 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 (
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. Status
Resources Encoding
OPT SAT OOT OOM sum sum sum sum
Space (osp) Time (otm/grd/slv)
MB/avg s/avg
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) true(c(P, A, B)) ← abduce(c(P, A, B)).
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′).
We propagate truth as in BwFw using the rewriting exemplified in (
We again require goals to be true and minimize the number of abduced atoms. ← goal (A), not true(A).
Note that, although this encoding solves an easier problem than the other encodings, we will see that it does not necessarily perform better. 4
To test the above encodings, we performed experiments using the Accel benchmark3 [28]. This benchmark consists of 50 instances (i.e., goals) with between 5 3 ftp://ftp.cs.utexas.edu/pub/mooney/accel 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 significantly 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 encodings, 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/
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 produces an amazing 803 k ASP rules. The reason is, that (34) creates many potentially 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 optimality 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 symmetric 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
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 perform 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
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 applications, 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 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
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 performance changes regarding grounding size, grounding speed, finding an initial solution, and proving optimality. We are currently investigating alternative encodings, 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 improvement of grounding is to replace grounding-intensive constraints by sound approximations 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 Datalog± [4] which supports existential constructions in rule heads. Both formalisms 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 solutions. In the future we want to consider more sophisticated preferences based on Coherence [27] and based on Relevance Theory [31].
We thank the anonymous reviewers for their constructive and useful feedback.