Next: Polynomial Classes Up: Research Note: New Polynomial Previous: Previous Work

A General Algorithm

We now give the principle of our algorithm. Let us stress first that, as well as, e.g., Marquis' construction [Mar00, Section 4.2], its outline matches point by point the definition of a best explanation; our ideas and Marquis' are anyway rather close.

We are first interested in the hypotheses in which every abducible occurs (either negated or unnegated); let us call them full hypotheses. Note indeed that every explanation for an abduction problem is a subconjunction of a full explanation ; indeed, since is by definition such that is satisfiable and implies , it suffices to let be for a model of . Minimization of will be discussed later on.

Proposition 1   Let be an abduction problem, and a full hypothesis of . Then is an explanation for if and only if there exists an assignment to with and .

Proof Assume first is an explanation for . Then (i) there exists an assignment to with , thus and , and (ii)  , i.e., is unsatisfiable, thus , thus , thus . Conversely, if let . Then we have (i) since , is satisfiable, and (ii) since , there is no with , thus is unsatisfiable, thus .

Thus we have characterized the full explanations for a given abduction problem. Now minimizing such an explanation is not a problem, since the following greedy procedure, given by Selman and Levesque [SL90] reduces into a best explanation for :

For every literal do
......If then endif;
Endfor;

Note that depending on the order in which the literals are considered the result may be different, but that in all cases it will be a best explanation for .

Finally, we can give our general algorithm for computing a best explanation for a given abduction problem ; its correctness follows directly from Proposition 1:

a propositional formula with ;
If is unsatisfiable then return No explanation'';
Else
...... a model of ;
...... ;
......minimize ;
......return ;
Endif;

Next: Polynomial Classes Up: Research Note: New Polynomial Previous: Previous Work
Bruno Zanuttini 2003-06-30