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**;

**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**;