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.
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;
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'';
...... a model of ;