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 $x\in A$ occurs (either negated or unnegated); let us call them full hypotheses. Note indeed that every explanation $E$ for an abduction problem is a subconjunction of a full explanation $F$; indeed, since $E$ is by definition such that $\Sigma\wedge E$ is satisfiable and implies $\alpha$, it suffices to let $F$ be $Select_A(m)$ for a model $m$ of $\Sigma\wedge E\wedge\alpha$. Minimization of $F$ will be discussed later on.

Proposition 1   Let $\Pi=(\Sigma,\alpha,A)$ be an abduction problem, and $F$ a full hypothesis of $\Pi$. Then $F$ is an explanation for $\Pi$ if and only if there exists an assignment $m$ to $Var(\Sigma)$ with $F=Select_A(m)$ and $m\in {\mathcal M}(\Sigma)\wedge \overline{({\mathcal M}(\Sigma\wedge\overline{\alpha}))_{\vert A}}$.

Proof Assume first $F$ is an explanation for $\Pi$. Then (i) there exists an assignment $m$ to $Var(\Sigma)$ with $m\models\Sigma\wedge F$, thus $F=Select_A(m)$ and $m\in{\mathcal M}(\Sigma)$, and (ii)  $\Sigma\wedge F\models\alpha$, i.e., $\Sigma\wedge F\wedge\overline{\alpha}$ is unsatisfiable, thus $F\notin \{Select_A(m)\ \vert\ m\in{\mathcal M}(\Sigma\wedge\overline{\alpha})\}$, thus $m\notin({\mathcal M}(\Sigma\wedge\overline{\alpha}))_{\vert A}$, thus $m\in\overline{({\mathcal M}(\Sigma\wedge\overline{\alpha}))_{\vert A}}$. Conversely, if $m\in {\mathcal M}(\Sigma)\wedge \overline{({\mathcal M}(\Sigma\wedge\overline{\alpha}))_{\vert A}}$ let $F=Select_A(m)$. Then we have (i) since $m\in{\mathcal M}(\Sigma)$, $\Sigma\wedge F$ is satisfiable, and (ii) since $m\notin({\mathcal M}(\Sigma\wedge\overline{\alpha}))_{\vert A}$, there is no $m'\in{\mathcal M}(\Sigma\wedge\overline{\alpha})$ with $Select_A(m')=F$, thus $\Sigma\wedge F\wedge\overline{\alpha}$ is unsatisfiable, thus $\Sigma\wedge F\models\alpha$. $\square$

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

 
For every literal $\ell\in F$ do
......If $\Sigma\wedge F\backslash\{\ell\}\models\alpha$ then $F\leftarrow F\backslash\{\ell\}$ endif;
Endfor;

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

Finally, we can give our general algorithm for computing a best explanation for a given abduction problem $\Pi=(\Sigma,\alpha,A)$; its correctness follows directly from Proposition 1:

 
$\Sigma'\leftarrow$ a propositional formula with ${\mathcal M}(\Sigma')= {\mathcal M}(\Sigma)\wedge \overline{({\mathcal M}(\Sigma\wedge\overline{\alpha}))_{\vert A}}$;
If $\Sigma'$ is unsatisfiable then return ``No explanation'';
Else
......$m\leftarrow$ a model of $\Sigma'$;
...... $F\leftarrow Select_A(m)$;
......minimize $F$;
......return $F$;
Endif;