Proposition 1 Let  = (; ; A) be an abdu
tion problem, and F a ful l hypothesis of .

Then F is an explanation for  if and only if there exists an assignment m to V ar() with F = Sele
tA(m) and m 2 M() ^ (M( ^ ))jA.

Proof Assume rst F is an explanation for . Then (i) there exists an assignment m to V ar() with m j=  ^ F , thus F = Sele
tA(m) and m 2 M(), and (ii)  ^ F j= , i.e.,
 ^ F ^  is unsatisable, thus F 2= fSele
tA(m) j m 2 M( ^ )g, thus m 2= (M( ^ ))jA,
thus m 2 (M( ^ ))jA. Conversely, if m 2 M() ^ (M( ^ ))jA let F = Sele
tA(m).

Then we have (i) sin e m 2 M(),  ^ F is satisable, and (ii) sin e m 2= (M( ^ ))jA,
there is no m0 2 M( ^ ) with Sele
tA(m0) = F , thus  ^ F ^  is unsatisable, thus
 ^ F j= . 

Thus we have hara terized the full explanations for a given abdu tion problem. Now minimizing su h an explanation F is not a problem, sin e the following greedy pro edure, given by Selman and Levesque (1990) redu es F into a best explanation for :

For every literal ` 2 F do If  ^ F nf`g j=  then F F nf`g endif;

## Endfor;

Note that depending on the order in whi h the literals ` 2 F are onsidered the result may be dierent, but that in all ases it will be a best explanation for .

Finally, we an give our general algorithm for omputing a best explanation for a given abdu tion problem  = (; ; A); its 
orre
tness follows dire
tly from Proposition 1:
0 a propositional formula with M(0
) = M() ^ (M( ^ ))jA;
If 0 is unsatisable then return \No explanation";

Else m a model of 0
;

F Sele
tA(m);
minimize F ;

return F ;

Endif;

## 6. Polynomial Classes

We now explore the new polynomial lasses of abdu tion problems that our algorithm allows to exhibit. Throughout the se tion, n denotes the number of variables in V ar().

## 6.1 Aæne Formulas

A propositional formula is said to be aÆne (or in XOR-CNF ) (S
haefer, 1978; Kavvadias &

Sideri, 1998; Zanuttini, 2002) if it is written as a nite onjun tion of linear equations over the two-element eld, e.g.,  = (x1 x3 = 1) ^ (x1 x2 x4 = 0). As 
an be seen, equations play the same role in aÆne formulas as lauses do in CNFs; roughly, aÆne formulas represent onjun tions of parity or equivalen e onstraints. This lass proves interesting for knowledge representation, sin e on one hand it is tra table for most of the ommon reasoning tasks, and
