On computing all abductive explanations
On Computing all Abductive Explanations
Thomas Eiter
Institut f¨u r Informationssysteme,
Technische Universit¨a t Wien Favoritenstra?e9–11,A-1040Wien,Austria e-mail:eiter@kr.tuwien.ac.at
Kazuhisa Makino
Division of Systems Science, Graduate School of Engineering Science, Osaka University,Toyonaka,Osaka560-8531 makino@sys.es.osaka-u.ac.jp
Abstract
We consider the computation of all respectively a polynomial subset of the explanations of an abductive query from a Horn theory,and pay particular attention to whether the query is
a positive or negative letter,the explanation is based on lit-
erals from an assumption set,and the Horn theory is rep-resented in terms of formulas or characteristic models.We derive tractability results,one of which refutes a conjecture by Selman and Levesque,as well as intractability results,and furthermore also semi-tractability results in terms of solvabil-ity in quasi-polynomial time.Our results complement previ-ous results in the literature,and elucidate the computational complexity of generating the set of explanations.
Introduction
Abduction is a fundamental mode of reasoning,which has
been recognized as an important principle of common-sense
reasoning(see e.g.(Brewka,Dix,&Konolige1997)).It has
applications in many areas of AI including diagnosis,plan-
ning,learning,natural language understanding and many
others(see e.g.references in(Eiter&Gottlob1995)).In
a logic-based setting,abduction can be de?ned as the task,
given a set of formulasΣ(the background theory)and a for-
mulaχ(the query),to?nd a smallest set of formulas E(an
explanation)from a set of hypotheses such thatΣplus E is
satis?able and logically entailsχ.For use in practice,the
computation of abductive explanations is an important prob-
lem,for which well-known early systems such as Theorist
(Poole1989)or ATMS solvers have been devised.Since
then,there has been a vastly growing literature on this sub-
ject,indicating the need for ef?cient abductive procedures. Main problems considered.In this paper,we consider
computing a set of explanations for queries from Horn theo-
ries.More precisely,we address the following problems:?Computing all explanations of a queryχgiven by a letter q,with and without a set of assumption literals A from which explanations E must be formed,similar as in(Poole1989;
Selman&Levesque1996).Note that the logical disjunc-
tion of all explanations is a weakest disjunctive form over
the hypotheses explainingχ.It is easy to see that in general,
there might be exponentially many explanations,and com-
puting all explanations is inevitably exponential.However, Copyright c 2002,American Association for Arti?cial Intelli-gence(https://www.wendangku.net/doc/7a2385685.html,).All rights reserved.it is in this case of interest whether the computation is pos-sible in polynomial total time(or output-polynomial time), i.e.,in time polynomial in the combined size of the input and the output.Furthermore,if exponential space is pro-hibitive,it is of interest to know whether a few explanations (e.g.,polynomially many)can be generated in polynomial time,as studied by Selman and Levesque(1996).
?We contrast formula-based(syntactic)with model-based (semantic)representation of Horn theories.The latter form of representation,where a Horn theory is represented by the characteristic models,was advocated by Kautz et al.(1993). As they showed,important inference problems are tractable in the model-based https://www.wendangku.net/doc/7a2385685.html,ly,whether a Horn theory Σimplies a CNF?,and whether a query q has an explana-tion w.r.t.an assumption set A;the latter is intractable under formula-based representation.Similar results were shown for other theories by Khardon and Roth(1996).
?We investigate the role of syntax for computing abductive queries.In the framework of(Selman&Levesque1996; Kautz,Kearns,&Selman1993),the query is a positive let-ter q.However,it is of equal interest to consider negative queries as well,i.e.,to explain the complement q of an atom q.Since the Horn property imposes semantic restrictions on theories,it is not straightforward to express such negative queries in terms of positive queries.
?Finally,we consider as a meaningful generalization the computation of joint explanations.That is,given a back-ground theoryΣand observations o1,o2,...,o l,where l≥2,compute a single explanation E which is good for each o i.Joint explanations are relevant,e.g.,in diagnostic reasoning.We may want to know whether different observa-tions allow to come up with the same diagnosis,given by an abductive explanation,about a system malfunctioning.Such a diagnosis is particularly strong,as it is backed up by sev-eral cases.
Main results.Our main results are summarized as follows.?We refute Selman and Leveque’s belief(1996,p.266),that given a Horn theoryΣand a query letter q,it is hard to list all explanations of q fromΣeven if we are guaranteed that there are only few explanations.More precisely,we disprove their conjecture that generating O(n)many explanations of q is NP-hard,where n is the number of propositional letters in the language.This is a consequence of our result that
generating all nontrivial explanations of q is possible in total polynomial time(Theorem1).
?We give a detailed characterization of computing all ex-planations of a query from Horn theory in the formula-vs model-based setting,for both general explanations and ex-planations w.r.t.a set of assumption literals.In a nutshell, we obtain three kinds of results:
(1)A procedure which enumerates all nontrivial explana-tions of a query letter q from a Horn theoryΣwith incremen-tal polynomial delay.This is a positive result and trivially implies that all explanations can be found in polynomial to-tal time.Moreover,it means that any polynomial number of explanations can be generated in polynomial time in the size of the input(Corollary1).
(2)Intractability results for generating all explanations for
a negative query q from a Horn theoryΣcontained in a set of assumption literals A;this complements a similar result for positive queries in(Selman&Levesque1996).Both results emerge from the fact that the associated problems of recog-nizing the correct output are co-NP-complete.Since some hard instances have only small(polynomial-size)output, they also imply that computing few(polynomially many) explanations is intractable.
(3)Under model-based representation,generating all ex-planations is polynomial-time equivalent to the well-known problem of dualizing a positive CNF(D UALIZATION),i.e., given a CNF?in which no negative literal occurs,com-pute the(unique)prime DNF of?.D UALIZATION is a well-known open problem in NP-completeness,cf.(Bioch &Ibaraki1995;Fredman&Khachiyan1996);it is known to be solvable in quasi-polynomial total time,i.e.,in time N o(log N)where N denotes the combined size of the in-put and output(Fredman&Khachiyan1996);furthermore, polynomial total time algorithms are known for many spe-cial cases,and as recently shown,the decisional variant of recognizing the prime DNF of?is solvable with limited nondeterminism,i.e.,in polynomial time with O(log2N) many guesses(Eiter,Gottlob,&Makino2002).Since D U-ALIZATION is strongly believed not to be co-NP-hard,our result thus provides strong evidence that under model-based representation,computing all explanations is not co-NP-hard.Interestingly,the equivalence result holds for both positive and negative queries,and whether arbitrary or ex-planations over a set of assumption literals A are admitted. This means that,in a sense,model-based representation,in contrast to formula-based representation,is not sensitive to these aspects.Furthermore,by resorting to respective algo-rithms for dualization,the result provides us with algorithms for enumerating all or polynomially many explanations with quasi-polynomial time delay between outputs.
?We show that deciding the existence of a joint explanation is intractable,for both formula-and model-based represen-tation.Thus,the positive results for ordinary explanations do not extend to joint explanations.
Proofs of all results are given in(Eiter&Makino2002).
Preliminaries
We assume a standard propositional language with letters x1,x2,...,x n from a set P,where each x i takes either value 1(true)or0(false).Negated atoms are denoted by x i,and the opposite of a literal by .Furthermore,we use A= { | ∈A}for any set of literals A and set Lit=P∪P.
A clause is a disjunction c= p∈P(c)p∨ p∈N(c)p of literals,where P(c)and N(c)are the sets of atoms occurring positive and negated in c and P(c)∩N(c)=?.Dually,a term is conjunction t= p∈P(t)p∧ p∈N(t)p of literals, where P(t)and N(t)are similarly de?ned.We also view clauses and terms as sets of literals P(c)∪N(c)and P(t)∪N(t),respectively.A clause c is Horn,if|P(c)|≤1,and a CNF is Horn,if it contains only Horn clauses.A theoryΣis any set of formulas;it is Horn,if it is a set of Horn clauses. As usual,we identifyΣwith?= c∈Σc,and write c∈?etc.
De?nition1Given a(Horn)theoryΣ,called the back-ground theory,a letter q(called query),and a set of literals A?Lit,an explanation of q w.r.t.A is a minimal set of literals E over A such that
(i)Σ∪E|=q,and
(ii)Σ∪E is satis?able.
If A=Lit,then we call E simply an explanation of q. Observe that the above de?nition is slightly more gen-eral than the assumption-based explanations of(Selman& Levesque1996),which emerge as A=P ∪P where P ?P(i.e.,A contains all literals over a subset P of the letters).Furthermore,in some texts explanations must be sets of positive literals.As for Horn theories,the following is known,cf.(Khardon&Roth1996):
Proposition1Let E be any explanation of q w.r.t.A?Lit. Then E?P,i.e.,E contains only positive literals. Example1Consider a theoryΣ={x1∨x4,x4∨x3, x1∨x2,x4∨x5∨x1}.Suppose we want to explain q=x2 from A={x1,x4}.Then,we?nd that E={x1}is an ex-planation.Indeed,Σ∪{x1}|=x2,andΣ∪{x1}is satis?-able;moreover,E is minimal.On the other hand,E ={x1, x4}satis?es(i)and(ii)for q=x2,but is not minimal.2 Horn theories have a well-known semantic characteriza-tion.A model is a vector v∈{0,1}n,whose i-th component is denoted by v i.For B?{1,...,n},we let x B be the model v such that v i=1,if i∈B and v i=0,if i/∈B,for i∈{1,...,n}.The set of models of formula?(resp.theory Σ),denoted by m od(?)(resp.m od(Σ)),is de?ned as usual. For models v,w,we denote by v≤w the usual com-ponentwise ordering,i.e.,v i≤w i for all i=1,2,...,n, where0≤1;v As discussed by Kautz et al.(1993),a Horn theoryΣis semantically represented by its characteristic models,where v∈m od(Σ)is called characteristic(or extreme(Dechter& Pearl1992)),if v∈Cl∧(m od(Σ)\{v}).The set of all such models,the characteristic set ofΣ,is denoted by c har(Σ). Note that c har(Σ)is unique. E.g.,(0101)∈c har(Σ2), while(0000)/∈c har(Σ2);we have c har(Σ2)=M1. Generating Explanations In this section,we consider the generation of all explana-tions for an atom q.We exclude in our considerations the trivial explanation E={q},which always exists if q be-longs to the assumption literals A,Σ∪{q}is satis?able and Σ|=q.These conditions can be ef?ciently checked under both formula-and model-based representations. Recall that a prime implicate(res.,prime implicant)of a theoryΣis a smallest(w.r.t.inclusion)clause c(resp.,term t)such thatΣ|=c(resp.,t|=Σ).As well-known,explana-tions can be characterized by prime implicates as follows. Proposition2For a theoryΣ,E is a nontrivial explanation of q w.r.t.A?Lit if and only if the clause c= p∈E p∨q is a prime implicate ofΣsuch that E?A. We start with the generation of all nontrivial explanations under formula-based representation.For this problem,we present the following algorithm. Algorithm E XPLANATIONS Input:A Horn CNF?and a positive letter q. Output:All nontrivial explanations of q from?. Step1.? :=?,S:=?,and O:=?; Step2.for each c∈?do add any prime implicate c ?c of?to? ; for each c ∈? with P(c )={q}and N(c )/∈S do begin output N(c );S:=S∪{N(c )}; O:=O∪{(c,c )|c∈? } end; Step3.while some(c1,c2)∈O exists do begin O:=O\{(c1,c2)}; if(1)q/∈N(c1),(2)P(c1)={r}?N(c2)and (3)? ∪N(c1)∪N(c2)\P(c1)is satis?able then begin c:=resolvent of c1and c2; compute any prime implicate c ?c of?; if N(c )/∈S then begin output N(c );S:=S∪{N(c )}; O:=O∪{(c,c )|c∈? } end end end.2 Example3We consider algorithm E XPLANATION on input of?=(x1∨x4)(x4∨x3)(x1∨x2)(x3∨x5∨x1),and q=x2. As easily seen,each clause in?is a prime implicate,and thus after Step2,? =?and S={{x1}}.Furthermore, the explanation E1={x1}was output. In Step3,(c1,c2),where c1=x3∨x5∨x1and c2= x1∨x2,is the only pair in O satisfying(2)P(c2)={x1}?N(c2)(={x1});moreover,(1)q/∈N(c1)(={x3,x5}) holds and(3)? ∪{x3,x5}is satis?able.Thus,in the body of the while-loop,its resolvent c=x3∨x5∨x2is computed.Clause c is a prime implicate of?,and thus E2={x3,x5} is output and added to S.Furthermore,O is updated. In the next iterations,no pair(c1,c2)∈O is found which satis?es condition(2),and thus the algorithm halts.Note that E1and E2are the nontrivial explanations of q=x2.2 The following result states that our algorithm works as desired.For any formula?,denote by ? its length,i.e., the number of literal occurrences in it. Theorem1Algorithm E XPLANATIONS incrementally out-puts,without duplicates,all nontrivial explanations of q from?.Moreover,the next output resp.termination occurs within O(e·m·n· ? )time,where m is the number of clauses in?,n the number of atoms,and e the number of explanations output so far. Proof.(Sketch)Only pairs(c,c )are added to O such that c is a prime implicate of?.Furthermore,by condition(3) in Step3,each such c must have P(c )={q}.Thus,by Props.1and2,algorithm E XPLANATIONS outputs only non-trivial(clearly different)explanations E1,E2,...,E k for q. To show that it outputs all nontrivial explanations E for q,assume that such an E is not output,i.e.,E=E i,i= 1,...,k.Let?N be the CNF of all negative prime impli-cates of?,and let? =?N∪{ p∈E i p∨q|i∈{1,...,k}}. Since c= p∈E p∨q is a prime implicate of?and c/∈? , there exists a model v∈m od(? )such that c(v)=0.Let w be a maximal such model,i.e.,no model u(>w)exists such that u∈m od(? )and c(u)=0.Since c(w)=0implies w∈m od(?),there exists a prime implicate c1in? (when Step2is?nished)such that c1(w)=0.Clearly c1∈? , i.e.,c1is of form c1= p∈N(c1)p∨x i such that x i=q. Moreover,we have q∈N(c1)by c(w)=c1(w)=0.Con-sider now the model w de?ned by w i=1and w j=w j, for all j=i.Note that c(w )=0,and by the maximality of w,there is a prime implicate c2∈? such that c2(w )=0. Since c2(w)=1and c2(w )=0,we have x i∈N(c2). Since q∈N(c1),a resolvent c of c1and c2thus exists.It can be shown(Eiter&Makino2002)that c creates a new prime implicate c = p∈N(c )p∨q?c of?in Step3,i.e., N(c )=E i,i=1,...,k.This contradicts our assumption. Thus,E XPLANATION is correct,and it remains to verify the time https://www.wendangku.net/doc/7a2385685.html,puting a prime implicate c ?c of?in Steps2and3is feasible in time O(n· ? ),and thus the outputs in Step2occur with O(m·n· ? )delay.As for Step3,note the O contains only pairs(c1,c2)where c1∈? and c2=N(c2)∪{q}such that N(c2)was output, and each such pairs is added to O only once.Thus,the next output or termination follows within e·m runs of the while-loop,where e is the number of solutions output so far.The body of the loop can be done,using proper data structures, in O(n· ? )time(for checking N(c1)/∈S ef?ciently,we may store S in a pre?x tree).Thus,the time until the next output resp.termination is bounded by O(e·m·n· ? ).2 From this result,we obtain the following corollary. Corollary1Given a Horn CNF?and a query q,comput-ing O(n k)many explanations of q,where k is a constant,is possible in polynomial time. This corollary implies that Selman and Leveque’s con-jecture(1996,p.266)that generating O(n)many expla-nations of q is NP-hard,where n is the number of propo-sitional letters in the language,is not true(unless P=NP). Note,however,that by the results of(Selman&Levesque 1996),computing O(n)many or all assumption-based ex-planations from a HornΣis not possible in total polynomial time unless P=NP. Let us now consider computing all explanations in the model-based setting. Theorem2Given the characteristic set M=c har(Σ)?{0,1}n of a Horn theoryΣ,a query q,and A?Lit,com-puting the set of all explanations for q fromΣw.r.t.A is polynomial-time equivalent to dualizing a positive CNF. Here,polynomial-time equivalence means mutual poly-nomial-time transformability between deterministic func-tions,i.e.,A reduces to B,if there a polynomial functions f,g s.t.for any input I of A,f(I)is an input of B,and if O is the output for f(I),then g(O)is the output of I,cf. (Papadimitriou1994);we also request that O has size poly-nomial in the size of the output for I(if not,trivial reduc-tions may exist).In our reduction,explanations correspond to clauses of the dual prime CNF and vice versa. Proof.(Sketch)By Props.1and2,we need only compute all nontrivial explanations E?A corresponding to prime implicates c ofΣs.t.P(c)={q}and N(c)=E?A∩P. We describe how the problem can be transformed to dual-ization of polynomially many positive CNFs?1,...,?k,such that the clauses of the dual prime CNFsψi for?i correspond to the explanations of q w.r.t.A∩P(equivalently,w.r.t.A). Thus,the problem is polynomially reducible to dualizing(in parallel)several positive CNFs?i.By simple methods,we can combine?1,...,?k into a single CNF?(using further variables)such that the clauses of the dual prime CNF for?correspond to the explanations of q w.r.t.A.(This step is of less interest in practice,since dualization of the individual ?i is at the core of the computation.) To construct the?i,we proceed as follows.Let q=x j. (1)De?ne M i={v∈M|v j=i},i∈{0,1}. (2)For every model v∈max(M1),let F v=max({v∧x A∧w|w∈max(M0)}). We associate with F v a monotone Boolean function f v on the variables P v=A∩{x i|v i=1}such that f v(w)= 0?w≤s for some vector s in the projection of F v on P v.That is,F v describes the maximal false points of f v. (3)Finally,de?ne for every v∈max(M1) ?v={c|N(c)=?,P(c)=P v\S,x S∈F v}. Note that?v is a prime CNF for f v. It can be shown(Eiter&Makino2002)that the nontrivial explanations of q w.r.t.A are given by the clauses in all dual prime CNFsψv for?v where v∈max(M1)(equivalently, by all prime implicants t,i.e.,a prime DNF representation of f v,v∈max(M1)).This proves one direction of the result. For the converse,we show that,given a positive CNF?on atoms P,computing an equivalent prime DNFψis reducible to computing all explanations as follows.Let q be a fresh letter(for component n+1),and de?ne M={(v,0)|v∈max({w|?(w)=0})}∪{(11···1)}and A=P;note that max({w|?(w)=0})is easily computed from?.2 Example4Let M={(11011),(11010),(10101),(01010), (00001)},and suppose we want all explanations of q=x1 w.r.t.A={x3,x4,x5}.According to above,we obtain: (1)M0={(01010),(00001)}and M1={(11011), (11010),(10101)},thus max(M1)={(11011),(10101)}. (2)We have two vectors v(1)=(11011)and v(2)=(10101): F v(1)=max (11011)∧(00111)∧(01010), (11011)∧(00111)∧(00001) ={(00010),(00001)}, F v(2)=max (10101)∧(00111)∧(01010), (10101)∧(00111)∧(00001) ={(00001)}. Thus,P v(1)={x4,x5}and f v(1)(w)=0iff w∈{(10), (01),(00)},and P v(2)={x3,x5}and f v(2)(w)=0iff w∈{(01),(00)}. (3)We obtain?(1)=x4∧x5and?(2)=x3.The respective prime dual CNFs areψ(1)=x4∨x5andψ(2)=x3. Thus,the explanations of q w.r.t.A are E1={x4,x5} and E2={x3}.It can be seen that this is the correct result. Negative Queries So far,we considered Horn theoriesΣand queries given by a letter q.In a general setting,we might allow that the formulas inΣand the query are any propositional formulas. As for computation,we can introduce for a query,given by any formulaχ,a fresh letter q,add implications q→χ,χ→q inΣ,and then ask for a nontrivial explanation of q. Thus,positive letter queries do not constrain the expressivity of the framework.However,this technique does not work for Horn theories,if one of the implications q→χ,χ→q is not Horn.In the simplest case,χis a negative literal q. The next result tells us that already in this case,abduction from a Horn CNF is intractable.Recall that a Horn CNF?is acyclic,if the graph on P with arcs from x i∈N(c)to x i∈P(c),c∈?,has no directed cycle. Theorem3Given a Horn CNF?,a general queryχin CNF,and A?Lit,deciding ifχhas a nontrivial explana-tion w.r.t.A is NP-complete.Hardness holds even ifχ=q,?is acyclic,and either(i)A=P or(ii)A=P ∪P for some P ?P. Proof.(Sketch)The problem is in NP,since clearly an ex-planation E exists if some set E?A exists such thatΣ∪E is satis?able andΣ∪E|=χ;such an E can be guessed and the conditions can be checked in polynomial time. Hardness is shown by a reduction from3SAT.Letγ= c1∧···∧c m be a3CNF over atoms x1,...,x n,where c i= i,1∨ i,2∨ i,3.We introduce for each clause c i a new atom y i,for each x j a new atom x j,and a special atom z.The Horn CNF?contains the following clauses: ?x i∨ i for all i=1,...,n; ?z∨y1 ?y i∨ i,j∨y i+1if i,j is positive and y i∨ i,j∨y i+1if i,j is negative,for all i=1,...,m?1and j=1,2,3; ?y m∨ m,j if m,j is positive and y m∨ m,j if i,j is neg-ative,for j=1,2,3. As easily seen,?is acyclic Horn.It can be shown(Eiter &Makino2002)that the query q=?z has a nontrivial ex-planation E consisting of positive literals iffγis satis?able, which proves NP-hardness under restriction(i).For(ii),we use a similar construction.2 Note that this result contrasts the tractability result that a nontrivial explanation E?P for a positive query q can be computed in polynomial time(Selman&Levesque1996). Thus,the framework of Horn abduction is sensitive with re-spect to query representation.We also remark that we can ?nd an arbitrary explanation E for a query q(which may contain negative literals),in polynomial time. In the model-based setting,we obtain for computing all explanations for a negative query a similar result as for a positive query. Theorem4Given the characteristic set M=c har(Σ)?{0,1}n of a Horn theoryΣ,a negative query q,and A?Lit,computing all explanations for q fromΣw.r.t.A is polynomial-time equivalent to dualizing a positive CNF. Proof.(Sketch)Observe that since the query is not positive, explanations of q may involve negative literals. Proposition2implies that the nontrivial explanations for q w.r.t.A correspond to the prime implicates c ofΣsuch that q∈N(c)and P(c)∪N(c)?A∪{q}.Let q=x j,and de?ne sets M0and M1for M as in the proof of Theorem2. Denote by A+(resp.,A?)the set of positive(resp.,negative) literals in A.We consider the following two cases: (1)Positive explanations for q.I.e.,all prime implicates c of Σs.t.{q}?N(c)?A+∪{q}and P(c)=?. Similarly as in the proof of Theorem2,we construct du-alization problems for functions f v,but for v∈max(M0): (1.1)For every v∈max(M0),let F v=max({v∧x A+∧w|w∈max(M1)}). The associated monotone Boolean function f v on P v= A∩{x i|v i=1}is de?ned by f v(w)=0?w≤s holds for some vector s in the projection of F v on P v. (1.2)We de?ne,for v∈max(M0), ?v={c|N(c)=?,P(c)=P v\S,x S∈F v}. Similarly as in Theorem2,we can show that the clauses in the dual prime CNFs for all?v,v∈max(M0),correspond to the positive explanations of q(Eiter&Makino2002). (2)Non-positive explanations for q.These are all prime implicates c ofΣs.t.{q}?N(c)?A+∪{q}and P(c)={r},where r∈A?. For each r=x j (where j =j),we proceed as follows. (2.1)For every v∈max(M0)and i∈{0,1},de?ne M r i={v∈M i|v r=i}. (2.2)For each v(0)∈max(M r0)and v(1)∈max(M r1),let F v(0),v(1)=max({v(0)∧v(1)∧x A+∧w| w∈max({u∈M1|u j =0)}). We associate with it a monotone Boolean function f v(0),v(1) on P v(0),v(1)=A∩{x i|v(0)i=v(1)i=1}such that f v(0),v(1)(w)=0?w≤s for some s in the projection of F v(0),v(1)on P v(0),v(1). (2.3)We de?ne the CNFs ? v(0),v(1) ={c|N(c)=?,P(c)=P v\S,x S∈F v(0),v(1)}. Then,it can be shown(Eiter&Makino2002)that the clauses in the dual prime CNFsψv(0),v(1)for all?v(0),v(1), where v(0)∈max(M r0)and v(1)∈max(M r1)and r∈A?, correspond to the non-positive explanations of q. In total,computing all explanations of q is polynomial-time reducible to dualizing(in parallel)polynomially many positive CNFs.As mentioned in the proof of Theorem2, this is polynomially reducible to dualizing a single CNF. The converse is shown by a reduction similar to the one in the proof of Theorem2;we just invert the polarity of q.2 Joint Explanations We call any set of E?A of literals a joint explanation of observations o1,o2,...,o l from a background theoryΣw.r.t.a set of assumptions A?Lit,if E is an explanation of each o i fromΣw.r.t.A.The observations o i may be letters, or in a generalized setting propositional formulas. Note that any such E is also an explanation for the con-junctionα=o1∧o2∧···∧o l of all observations,while the converse is not true in general:an explanation E ofαmay not satisfy minimality for o1,say,i.e.,some E ?E may explain o1.Thus,joint explanations are stronger than ordinary explanations.In case of multiple explanations,this may be used to single out those which match with each of the(possibly independently made)observations. For example,the malfunctioning of a car may be ex-plained by two car mechanics,based on observations o1and o2,respectively.A match of their(individual)diagnoses E1 and E2(i.e.,E1=E2)may be taken in favor of believ-ing in their correctness.In fact,the diagnoses are robust in the sense that adding the other observation does not require a change;from another perspective,the same diagnosis is good for explaning different observations.If E1and E2are different,then we might want to know whether alternative diagnoses E 1and E 2do exist which coincide,i.e.,whether a joint explanation is possible. As it turns out,recognizing joint explanations for CNFs, i.e.,deciding whether E is a joint explanation for observa-tions o1,...,o l described by CNFs,fromΣw.r.t.assump-tions A is tractable,for both formula-and model based rep-resentation.However,deciding existence is harder. Theorem5Given a Horn CNF?,query CNFsχ1,χ2,...,χl,where l≥2,and A?Lit,deciding if a joint explanation exists fromΣw.r.t.A is NP-complete.Hardness holds even if l=2,eachχi is a letter,?is acyclic,and A=Lit. Theorem6Given the characteristic set M=c har(Σ)of a Horn theoryΣ,query CNFsχ1,χ2,...,χl,l≥2,and A?Lit,deciding if a joint explanation exists fromΣw.r.t. A is NP-complete.Hardness holds even if l=2,eachχi is a letter,and A=Lit. Thus,the tractability results in(Selman&Levesque1996; Kautz,Kearns,&Selman1993)do not generalize to joint explanations for positive queries.Similar intractability re-sults hold for negative queries and combined positive and negative queries. Related Works Selman and Levesque(1990;1996)were among the?rst to study the complexity of computing general and assumption-based explanations;Corollary1closes an open problem of them.The underlying algorithm E XPLANATIONS is a rela-tive of a similar procedure by Boros et al.(1990)for comput-ing all prime implicates of a Horn CNF in output-polynomial time.In fact,Theorem1can be seen as a strengthening of their result.For negative queries,a similar algorithm is not evident.del Val(2000)presented generation of implicates and prime implicates of certain clausal theories in a target language,which is formed on a subset of the atoms,using a procedure based on kernel resolution and derived expo-nential bounds on its running time.Furthermore,del Val described the use of this procedure for generating jointly all explanations of all literals not on a set of atoms V.However, neither is this method incremental in nature,nor is it clear whether it is total polynomial time.Moreover,it considers a letter q and its negation q at once. Inoue(1992)considered,in the propositional and the?rst-order context,generating explanations and prime implicates using SOL-resolution.He proposed a strategy which pro-cesses,starting from the empty set,clauses from a theory incrementally.However,due to possible large intermediate results,this method is not total polynomial time in general. Khardon et al.(1999)show how computing all keys of a re-lational database schema,which is constrained by a Boolean formula?,can be polynomially transformed into computing all explanations of a query q from?∧ψ,whereψis Horn. Thus,our algorithm E XPLANATIONS can be used for ef?-ciently generating all keys of a database scheme where?is a Horn CNF.This generalizes the result for?consisting of non-negative Horn clauses,i.e.,a set of functional depen-dencies(Lucchesi&Osborn1978).1Note that Khardon et al.also show how to compute a single explanation of a query q from a theory?polynomially,using repeatedly an oracle for computing a key of a database schema constrained by ?∧ψ,whereψis Horn;however,this method is not us-able for generating explanations from general Horn theories (cf.Footnote1).Less related to our work is(Eiter&Gottlob 1995),which considered abduction from Horn and general propositional theories,but focused on existence of explana-tions and reasoning tasks about explanations. Conclusion We have presented a number of positive and negative results about generating all and some abductive explanations,re-1In fact,Khardon et al.’s transformation works only if?has no negative prime implicate;otherwise,keys introduce inconsistency.spectively,which complement previous work in the litera-ture.In particular,we analyzed the role of positive vs nega-tive abductive queries,under both formula-and model-based representation,and we considered the novel notion of joint explanation.Our positive results may be readily applied for ef?ciently computing(a subset of)all explanations.The re-sults draw a complete picture for the model-based setting, and almost so for the formula-based setting;the complexity of generating all explanations for a negative query in it is currently open. Acknowledgments We thank the reviewers for helpful comments.This work was partly supported by the Austrian Science Fund(FWF) project Z29-INF,by TU Wien through a scienti?c collabora-tion grant,and by the Scienti?c Grant in Aid of the Ministry of Education,Science,Sports and Culture of Japan. References Bioch,C.,and Ibaraki,https://www.wendangku.net/doc/7a2385685.html,plexity of identi?cation and dualization of positive Boolean https://www.wendangku.net/doc/7a2385685.html,rmation and Computation123:50–63. Boros,E.;Crama,Y.;and Hammer,P.L.1990.Polynomial-time inference of all valid implications for Horn and related formulae. Annals of Mathematics&Arti?cial Intelligence1:21–32. Brewka,G.;Dix,J.;and Konolige,K.1997.Nonmonotonic Reasoning–An Overview.Number73in CSLI Lecture Notes. CSLI Publications,Stanford University. Dechter,R.,and Pearl,J.1992.Structure identi?cation in rela-tional data.Arti?cial Intelligence58:237–270. del Val,A.2000.The complexity of restricted consequence?nd-ing and abduction.In Proc.AAAI-00,337–342. Eiter,T.,and Gottlob,G.1995.The complexity of logic-based abduction.J.ACM42(1):3–42. Eiter,T.,and Makino,K.2002.On computing all abductive explanations(preliminary report).Technical Report INFSYS RR-1843-02-04,Institut f¨u r Informationssysteme,TU Wien,Austria. Eiter,T.;Gottlob,G.;and Makino,K.2002.New results on monotone dualization and generating hypergraph transversals.In Proc.34th ACM Symp.on Theory of Computing(STOC2002). Fredman,M.,and Khachiyan,L.1996.On the complexity of dualization of monotone disjunctive normal forms.Journal of Algorithms21:618–628. Inoue,K.1992.Linear resolution for consequence?nding.Arti-?cial Intelligence56(2-3):301–354. Kautz,H.;Kearns,M.;and Selman,B.1993.Reasoning with characteristic models.In Proc.AAAI-93,34–39. Khardon,R.,and Roth,D.1996.Reasoning with models.Arti?-cial Intelligence87(1/2):187–213. Khardon,R.;Mannila,H.;and Roth,D.1999.Reasoning with ex-amples:Propositional formulae and database dependencies.Acta Informatica36(4):267–286. Lucchesi,C.L.,and Osborn,S.1978.Candidate keys for https://www.wendangku.net/doc/7a2385685.html,puter and System Sciences17:270–279. Papadimitriou,https://www.wendangku.net/doc/7a2385685.html,putational Complexity. Poole,D.1989.Explanation and prediction:An architecture for default and abductive https://www.wendangku.net/doc/7a2385685.html,p.Intelligence5(1):97–110. Selman,B.,and Levesque,H.J.1990.Abductive and default reasoning:A computational core.In Proc.AAAI-90,343–348. Selman,B.,and Levesque,H.J.1996.Support set selection for abductive and default reasoning.Artif.Intell.82:259–272.