The note is organized as follows. We rst re all the useful notions of propositional logi
 (Se tion 2), formalize the problem (Se tion 3) and brie y survey previous work about the omplexity of abdu tion (Se tion 4). Then we give our algorithm (Se tion 5) and explore polynomial lasses for it (Se tion 6). Finally, we dis uss our results and perspe tives

(Se tion 7). For la k of spa e we annot detail proofs, but a longer version of this work, ontaining detailed proofs and examples, is available (Zanuttini, 2003).

## 2. Preliminaries

We assume a ountable number of propositional variables x1; x2 : : : and the standard 
onne tives :; ^; _; ;!;$. A literal is either a variable xi (positive literal) or its negation
:xi (negative literal). A propositional formula is a well-formed formula built on a nite number of variables and on the onne tives; V ar() denotes the set of variables that o

ur in the propositional formula . A 
lause is a nite disjun
tion of literals, and a propositional formula is in Conjun tive Normal Form (CNF) if it is written as a nite onjun tion of lauses. For instan e,  = (x1 _ :x2) ^ (:x1 _ x2 _ :x3) is in CNF. The dual notions of lause and CNF are the notions of term (nite onjun tion of literals) and Disjun tive Normal Form (DNF) (nite disjun tion of terms).

An assignment to a set of variables V is a set of literals m that ontains exa tly one literal per variable in V , and a model of a propositional formula  is an assignment m to V ar() that satises  in the usual way, where m assigns 1 to xi i xi 2 m; we also write m as a tuple, e.g., 0010 for f:x1; :x2; x3; :x4g. We write m[i℄ for the value assigned to xi by m, and M() for the set of all the models of a propositional formula ;  is said to be satisable if M() 6= ;. A formula  is said to imply a propositional formula 0
(written  j= 0) if M()  M(0). More generally, we identify sets of models with Boolean fun tions, and use the notations M (negation), M _ M0
(disjun tion) and so on.

The notion of proje tion is very important for the rest of the paper. For m an assignment to a set of variables V and A  V , write Sele
tA(m) for the set of literals in m that are formed upon A, e.g., Sele
tfx1;x2g(0110) = 01. Pro je
ting a set of assignments onto a subset A of its variables intuitively onsists in repla ing ea h assignment m with Sele
tA(m); for sake of simpli ity however, we dene the pro je tion of a set of models M to be built upon the same set of variables as M. This yields the following denition.

Denition 1 (pro je
tion) Let V = fx1; : : : ; xng be a set of variables, M a set of assignments to V and A  V . The pro je tion of M onto A is the set of assignments to V

MjA = fm j 9m02 M; Sele
tA(m0) = Sele
tA(m)g.

For instan e, let M = f0001; 0010; 0111; 1100; 1101g be a set of assignments to V =
fx1; x2; x3; x4g, and let A = fx1; x2g. Then it is easily seen that MjA = f0000; 0001; 0010; 0011g [ f0100; 0101; 0110; 0111g [ f1100; 1101; 1110; 1111g sin e fSele
tA(m) j m 2 Mg = f00; 01; 11g.

Remark that the pro je tion of the set of models of a formula  onto a set of variables A is the set of models of the most general onsequen e of  that is independent of all the variables not in A. Note also that the pro je tion of M() onto A is the set of models of the formula obtained from  by forgetting its variables not o

urring in A. For more details