A Tractable Class of Abduction Problems

1 Introduction

The abduction problem in which we are interested can be de­ fined as follows:

Definition 1 The triple <D,A,9> is an abductive problem iff n is a set of propositional Hom Clauses, A is a set of propositions and 9 is a proposition. The set of propositions il is a solution of the abductive problem <D,A,g> iff

l.il~A

2./lvn 1---9

3. ilvn is consistent

1. (aEA and Mn 1---a} ~ aEil

il is a minimal solution of <D,A,9> iff it is a solution of <D,A,g> and no subset of il is a solution of <D,A,9>.

Given the abductive proJ:>lem <0,A,9> we call n the back­ ground theory, A the abducible set, and 9 the goal. A propo­ sition is abducible if it belongs to A. (Throughout the paper, we will use e to refer to the set of non-abducible propositions in nv{9})

The purpose of condition 4 is to enable us to include clauses with abducibles at their head in the theory. It ensures that the set of assumptions adopted as the solution is closed under logical implication.

Selman and Levesque [16] show that even when only one solution is required, and the background theory n is restricted to be acyclic, finding abductive solutions is NP-hard. This has led to pessimism regarding the practical utility of abduction as formulated above.

In this paper, we present a collection of definitions, results and algorithms, which together defme a class of abduction zation of a set of proposition with respect to' the theory is tractable. This definition is new.

*This research was conducted while the author was at Hewlett Packard Labs-Stanford Science Center.

1. A test for unit-refutability of €lansal theories. This test re­ lies on the topology of the connection graph of the theory, and is polynomial time with respect to the size of the theo­ ry. Passing this test is a sufficient, but not necessary condi­ tion for unit refutability. This test is new.

As a result, we argue that the class of abduction problems which have a background theory with a unit-refutable pseu­ do-completion is tractable, and provide a sufficient, but not necessary, test for membership of this class.

Notice that the background theory can have general denials (as opposed to denials restricted to only abducible proposi­ tions), and that we allow abducibles to occur at the head of clauses.

For the case that the test fails, or we do not perform it, we will not know whether or not the pseudo-completion is unit refutable. In this situation, we can still use the algorithm, but we need to augment it with a correctness test to make sure that the set of assumptions returned is a solution. Sometimes this­ test will fail, i.e. we will not be able to generate a solution. The correctness test itself is of linear complexity, so when we do not know that the pseudo-completion is unit-refutable, we have a correct, but incomplete, tractable technique for finding solutions to abduction problems of the above form.

2 Pseudo-Completions

In order to defme the pseudo-completion of n, the first step is to assign to each clause c in n a unique proposition nc which does not occur in nu{g}uA. We call nc the name of c. No two clauses have the same name.

Definition 2 Let the clauses p+-01, p+-02····· p+-Ok, where 0 1 ,02, ... ,0k are conjunctions of propositions, be all the clauses inn which have pat their head. Let nc1· nc2, ... ,nck be the names of these clauses. Then the only-if set of p with respect tO 0 iS {-.pvnc1Vnc2V ... vnck nc1~01, nc2~02··· nck~Ok}. For a set of propositions Sand the Hom clause theory T, we use only-if(T,S) to denote the union of only-if sets of all the propositions inS with respect toT. We use only-if{T) to denote only-if(T,props(T)) where props(T) is the set of all propositions in T.

Since each Oi is a conjunction of propositions,. a sentence of the form nci~oi is equivalent to the set of clauses 'nci~qi1, nci~qi2, .. . ,nci~qin} where Oi=qi1"qi2"···"qin· Thus comput­ ing the clausal form of only-if sets is trivial.

Example: Let the clauses in T with pat their head be prq,r and p+-s,t. Let the names of these clauses be n1 and n2. Then the only-if set of p with respect to T is {-.pvn1vn2, n1~q. n 1 ~r. n2~s. n2~t}

Given the abductive problem <ll,A,g>, we defme the pseu­ do-completion of n to be nuonly-if(ll,8). (Recall the defini­ tion of 8 given on the first page). From the discussion above it is clear that we can assume the pseudo-completion to be in clausal form, which is the major reason we chose pseudo­ completions in preference to the standard notion of completiorr.

We compute solutions to the abductive problem <ll,A,g> by minimizing A with respect to nuonly-if{D,S)u{g}. In the next section we make precise the notion of minimization we are using.

3 Minimization with respect· to a theory

In order to define minimization, we need to define models.

Definition 3 Let C be a propositional clausal theory, S the set of propositions in C, and M a set of propositions. Then the truth-assignment induced by M is the assignment of true to all propositions in S which are in M, and false to those propositions inS which are not in M .. M is a model of C iff the truth assignment induced by M satisfies all the clauses in C.

Definition 4 Let C be a propositional clausal theory, and A a set of propositions. Then M is a model of C which minimizes A iff

1. M is a model of C

2. There is no other model M' of C such that M'nAcMnA

We say that!! is a minimization of A with respect to C iff there is a model M of C which minimizes A and 1!-MnA

Our definition of minimization corresponds to the notion of minimal model used in circumscription, when the proposi­ tions in A are circumscribed relative to C, and all other prop­ ositions are allowed to vary [10] . It also corresponds to the notion· of minimal diagnosis used in [14] , where the assump­ tions A will be the abnormality assumptions associated with the components of the system.

4 Abductive solutions and minimization

Theorem 1 is the basis of our technique for fmding minimal solutions of abductive problems. (Proof in Appendix 1)

Theorem 1 Let F .. <ll,A,g;:. be an abduction problem, where n is acyclic. Let 8 be the set of all propositions in nu{g} which do not occur in A. Then !! is a minimal solution of <ll,A,g> iff it is a minimization of A with respect to nuonly-if{D,8)u{g}.

Corollary: When n is a acyclic, nuonly-if(n,e)u{g} is in­ consistent iff <ll,A,g> has no solution.

In order to use this result for finding a solution to the abuc­ tion problem <ll,A,g> we proceed as follows: first we com­ pute only-if(ll,8) (the pseudo-completion of n). Then we check nuonly-if{H,8)u{g} for consistency. If inconsistent, the abduction problem has no solution. If consistent, we use the algorithm in the next section to find a minimization of A with respect to nuonly-if(D,8)u{g}. The set of assumptions re­ turned is a minimal solution to the abduction problem.

5 Finding a minimizatitm of A

The following algorithm (reported, for e~ample, in [6] ) can be used for finding a minimization of A with respect to C. This algorithm assumes that C is consistent. (M halds a set of literals, N and S hold a set of propositions, a holds a proposi­ tion):

M:={};N: .. {};S:=A; whileS*{} { choose a from S; S: ... s- a; if {-.a} uCuM is consistent M:=Mu{-,a} else N: .. Nu{a};

Notice that the selection of a from S in the frrst step of the loop is non-detenninistic, but this is a don't care type of non­ detenninism, i.e. no matter which proposition is chosen, the algorithm will succeed and there is no need for backtracking.

It is easy to prove that, for propositional C and A, this algo­ rithm always tenninates, and when it does, N holds a minimi­ zation of A with respect to C. Let k be the size of A. Then it is clear that the cost of computing a minimization of A with re­ spect to C using this algorithm is k times the cost of checking the consistency of CuM, where M is a set of unit clauses whose size is bounded by the size of A.

In general, checking the consistency of CuM is an NP-com­ plete problem. But there is a class of theories for which the cost of consistency checking, using unit resolution, is linear with respect to the size of the theory. We investigate this class, and the repercussions for fmding solutions to abduction problems, next.

6 Unit Resolution

Unit resolution is a restriction of the resolution rule where one of the resolvent must be a unit clause. Unit resolution, es­ pecially for propositional clauses, can be implemented very efficiently. But unit resolution is not a complete rule of infer­ ence, i.e. for some clausal theories, there are theorems which can not be proved using unit resolution. For a clausal theory C and a clause s, we say that s is unit-derivable. from C iff there is a derivation of s from C in which every step is a unit resolution.

Definition 5 A propositional clausal theory C is unit refutable iff, for every set of unit clauses U, if CuU is inconsistent, then the empty clause is unit-derivable from CuU.

Notation: For a clause c, size( c) denotes the number of liter­ als in c. For a set of clauses C, size(C) denotes the sum of the sizes of all the clauses in C.

Lemma 1 Let C be a unit-refutable propositional theory, and U a set of. unit clauses .. Then the cost of checking the consistency of CuU islinear with-respect to size(Cul:.l) (proof omitted).

Thus, if Cis unit refutable. the cost of minimizing A with re­ spectto C using the abo:ve algorithm is bounded by O((k+n)k), where k is the size of A, and. A is the· size of c.

I.emma 2 Let <il,A,g> fle all' abduction problem. Then size(nuonly-if{ll,8})<4(si:z:e(n)) (proof omitted)

The following lemma states; the consequences of these facts for· finding solutions to abduction probl~ms:

Lemma 3, Let <H.A,g> be an abduction problem, where n is acyclic, and nuonly-if(ll,8) is unit refutable. Then the cost of fmding a minimal solution to this problem is bounded by 0( (k+n+ 1 )(k+ 1) }, where k is the size of A, and n is the size of n.

This lemma relies on using unit resolution to check the con­ sistency of nuonly-if(ll,8)u{g}, and using the algorithm above for minimizing A with respect to nuonly-if(ll,8)u{g}.

At this point, two questions need to be asked: how can we say whether nuonly-if(ll,8} is unit refutable, and what hap­ pens if it isn't?

In the next section we introduce a test for unit refutability based on the topology of the connection graph of the theory.

7 When is a set of clauses unit refutable?

Our test for unit refutability is based on the topology of the connection graph of the set of clauses. We show that if the connection graph of a propositional clausal theory lacks cer­ tain topological features, which we have called tied chains, it is unit refutable. Notice that this is a sufficient, but not neces­ sary condition. But frrst, we need some preliminaries.

7.1 Connection Graphs

Connection graphs were introduced in [9] to help construct more efficient resolution theorem provers.

Definition 6 Given a set of clauses C, the connection graph of C is the graph obtained by drawing a link between each complimentary pair of literals in the set.

Example: Let C be the set {avb, -,ave, -,cv-,a, -,bv-, d, -,bvd}. Then the connection graph of C is:

We say that the clause c1 is linked to the clause c2 if there is a link between a literal in c1 and a literal in c2, i.e. c1 has a literal such as p where c2 has -,p.

The next concept we need to introduce is that of a chain. Inruitively, a chain corresponds to a subgraph comprised of a sequence of clauses each linked to the next, with the links connecting tile clause c to the previous and next clauses land­ ing on different literals in c. For example, the following cor­ responds to a chain:

-,avc----------------,cv-,a

To defme chains fonnally, we need the notion of a c-triple. A c-triple is a triple (x,e,y) where e is a clause and x and y are different literals in e.

Definition 7 Given the set of clauses e, the sequence [(x'F,e1 ,y1 Mx2,e2,Y2) ... (Jen,en,Yn>l,of c-triples is a chain inC iff for alt k, ek is a clause in C and Yk=-,xk+ 1.

DefinitiOn. 8 [(x1,e1,Y1 ),(x2;e2,Y2) ... (X0 ,9n·YnH is. a tied dwin in C iff it is a chain in C and x1-y 0 ·

Example: (--,a,-,avc,e)(-.c,-.cv-,a,-.a) is a tied chain.

Theorem 2 Every propositional clausal theory whose connection gmph has no tied chains is unit refutable. (Proof in Appendix 2)

Notice that the reverse is not necessarily true, i.e. there are unit refutable sets of clauses which have tied chains.

7.2 The cost of checking for tied chains

To estimate the cost of checking for tied chains, for the set of clauses C we define the binary relations chain between liter­ als as follows:

chain(l1 ,-.12) iff l1 and l2 are literals in a clause inC and l1*'2· Let chain* be the tmnsitive closure of chain. Then it is easy to show that there is a tied chain in C iff for some literal I, chain*(l,-.1) holds. Thus the cost of checking for existence of tied chains is bounded by the cost of computing the relation chain*, which is polynomial.

8 What if we don't know if nuonly-it(n,e) is unit-refutable

We might not want to do the test for tied chains in nuonly­ if(ll,El), or we might test and fmd a tied chain. In both cases, we do not know whether or not nuonly-if(ll,El) is unit-refut­ able. So what happens?

It is important to emphasize that while lack of tied chains in nuonly-if(ll,El) is a sufficient condition for the correctness and completeness of the algorithm, it is not a necessary con­ dition. In other words, even ifnuonly-if(ll,El} has tied chains, in many instances the algorithm returns a correct solution. Thus, when we do not know that nuonly-if(ll,El} is unit refut­ able, the best strategy to adopt is to use the algorithm to find a potential solution 6 anyway. But, in order to make sure that we have a solution, we can test the conditions 2 to 4 in Defi­ nition 1 in linear time (since n is Hom). If the conditions are satisfied, then we have a solution. In other words, without any consideration as to the unit-refutability of nuonly-lf(ll,El), the combination of the algorithm in section 5 and the further test of correctness can be considered a tractable algorithm for finding solutions to abduction problems which is correct, but incomplete.

In fact, pmctical experience has shown that, without any checking of nuonly-if(ll,El}, the algorithm rarely fails to re­ turn a correct answer. More substantial practical evidence supporting this claim will be presented when enough data is gathered.

9 Comparison with related work and conclusion

The A TMS [3] essentially computes all the minimal solutions for the abductive problems <ll,A,g1>, <ll,A,g2>, .. where 91 ,g2, .. are the propositions in n. But the performance of A TMS can be exponential with the number of propositions in n [12] .

The use of predicate completion to characterize abduction as deduction has been proposed by a number of researchers [2] [13] [8] . In this regard, the relationship established by Theorem 1 is closest to the work of Console et. al. in [2] .

They, too, consider acyclic Hom background theories, but they restrict them so that a) all defmite clauses have non-ab­ ducibles at the head and b) all the denials only have abduci­ bles atoms. Also, they do not establish a relationship between minimal solutions and the minimization of the abducible set with respect to the completion.

As far as the test for unit-refutability is concerned, to our knowledge the work reported here is new. DeKleer in [4] ad­ vocates the use of unit resolution (which he calls clausal bi­ nary constraint propagation) and gives some pragmatic techniques for making unit resolution complete for consisten­ cy checking.

A top-down algorithm for abduction using negation as fail­ ure type reasoning was reported in [5] . There are a number of published algorithms for finding generalized stable models of logic programs [7] , such as the algorithms reported in [15] . Computing general stable models is a generalised version of the abduction problem, thus all the algorithms developed for that purpose can be used for computing solutions to the ab­ ductive problems of the type considered in this paper. No tmctability results have been published concerning these al­ gorithms.

The techniques presented here (without the test for unit-re­ futability) have recently been implemented in the context of a general purpose abduction/reason-maintenance system. So far, the system has given promising performance, though de­ finitive judgement has to await further experiments.

Acknowledgment: I would like to thank Bruno Bertolino, Chris Preist, Ajay Gupta and Alex Loopik for many useful discussions on the subject of this paper.