imply head(r) ∈ M for ea
h rule r ∈ Π. A model M of a program Π is a stable model of Π if and only if there is no model M′ ⊂ M of ΠM , where Π
M = {head(r) ← body(r)
+ | r ∈ Π and body(r)
− ∩ M = ∅}

```
is 
    alled the Gelfond-Lifs
                                  hitz redu
                                              t of Π with respe
t to M . We say that a pro-

```

gram Π is satisable if it has a stable model, and unsatisable otherwise.

The positive dependen y graph of Π, denoted by Dep+(Π), is a dire
ted graph with atom(Π) and
{hb, a**i | ∃**r ∈ Π su
h that b = head(r) and a ∈ body(r)
+}
as the sets of verti es and edges, respe tively. A non-empty set L ⊆ atom(Π) is a loop in Dep+(Π) if for any **a, b** ∈ L there is a path of non-zero length from a to b in Dep+(Π) su
h that all verti
es in the path are in L. We denote by loop(Π) the set of all loops in Dep+(Π). A NLP is tight if and only if loop(Π) = ∅. Furthermore, the external bodies of a set A of atoms in Π is eb(A) = {body(r) | r ∈ Π, head(r) ∈ A, body(r)
+ ∩ A = ∅}.

A set U ⊆ atom(Π) is unfounded if eb(U) = ∅. We denote the greatest unfounded set, that is, the union of all unfounded sets, of Π by gus(Π).

A splitting set (Lifs hitz and Turner 1994) for a NLP Π is any set U ⊆ atom(Π)
su h that for every r ∈ Π, if head(r) ∈ U , then body(r)
+ ∪ body(r)
− ⊆ U . The bottom of Π relative to U is bottom(Π, U) = {r ∈ Π | atom({r}) ⊆ U},
and the top of Π relative to U is top(Π, U) = Π \ bottom(Π, U).

The top an be partially evaluated with respe t to an interpretation X ⊆ U . The result is a program eval(top(Π, U), X) that 
ontains the rule

## Head(R) ← (Body(R) + \ U), ∼(Body(R) − \ U)

for ea h r ∈ top(Π, U) su
h that body(r)
+ ∩ U ⊆ X and (body(r)
− ∩ U) ∩ X = ∅.

Given a splitting set U for a NLP Π, a solution to Π with respe
t to U is a pair h**X, Y** i su h that X ⊆ U , Y ⊆ atom(Π) \ U , X is a stable model of bottom(Π, U), and Y
is a stable model of eval(top(Π, U), X). In this work we will apply the splitting set theorem (Lifs hitz and Turner 1994) that relates solutions with stable models.

Theorem 2.1 ((Lifs hitz and Turner 1994)) Given a normal logi program Π
and a splitting set U for Π, an interpretation M ⊆ atom(Π) is a stable model of Π
if and only if hM ∩ **U, M** \ Ui is a solution to Π with respe
t to U .

## 2.2 Propositional Satisability

Let X be a set of Boolean variables. Asso
iated with every variable x ∈ X there are two literals, the positive literal, denoted by x, and the negative literal, denoted