program P , we write At(P) for its signature, that is, the set of atoms o

urring in P ,
and **Body(**P) and **Head(**P) for the respe
tive subsets of At(P) having body o

ur-

```
ren
  es and head o
            
             urren
                  es in the rules of P . Furthermore, Choices(P) ⊆ Head(P)

denotes the set of atoms having a head o
                                       
                                        urren
                                              e in a 
                                                    hoi
                                                        e rule of P .

```

Given a program P , an interpretation M of P is a subset of At(P) dening whi
h atoms a ∈ At(P) are true (a ∈ M ) and whi
h are false (a 6∈ M ). A weight rule (1)
is satised in M if and only if a ∈ M whenever the sum of weights

$$\sum_{b\in B\cap M}w_{b}+\sum_{c\in C\setminus M}w_{c}$$

is at least w. A 
hoi
e rule {A} ← B, ∼C is always satised in M . An interpretation M ⊆ At(P) is a (
lassi
al) model of P , denoted by M |= P , if and only if M satises all the rules in P .

The generalization of the Gelfond-Lifs hitz redu t (Gelfond and Lifs hitz 1988)

for smodels programs is dened as follows.

Denition 3.2 For an smodels program P and an interpretation M ⊆ At(P),
the redu t P M 
ontains

1. a rule a ← B if and only if there is a 
hoi
e rule {A} ← B, ∼C in P su
h that a ∈ A ∩ M , and M ∩ C = ∅;
2. a rule a ← w
′ ≤ {B = WB} if and only if there is a weight rule a ← w ≤
{B = WB, ∼C = WC } in P su
h that w
′ = max(0, w −Pc∈C\M wc).
We say that an smodels program P is positive if ea
h rule in P is a weight rule restri ted to the ase C = ∅. Re
alling that the basi rules are just a spe
ial 
ase of weight rules, we note that the redu t P M is always positive. An interpretation M ⊆ At(P) is the least model of a positive smodels program P , denoted by LM(P),
if and only if M |= P and there is no M′|= P su
h that M′ ⊂ M . Given the least model semanti s for positive programs (Janhunen and Oikarinen 2007), the

```
stable model semanti
                      s (Gelfond and Lifs
                                           hitz 1988) straightforwardly generalizes
                                                                                    

```

for smodels programs (Simons et al. 2002).

Denition 3.3 An interpretation M ⊆ At(P) is a stable model of an smodels program P if and only if M **= LM(**P M ).

Given an smodels program P and a, b ∈ At(P), we say that a depends dire
tly on b, denoted by b ≤1 a, if and only if P 
ontains a rule r su
h that a ∈ **Head(**r)
and b ∈ **Body**+(r). The positive dependen
y graph of P , denoted by Dep+(P), is the graph hAt(P), ≤1i. The reexive and transitive 
losure of ≤1 gives rise to the dependen y relation ≤ over At(P). A strongly 
onne
ted 
omponent (SCC) S of Dep+(P) is a maximal set S ⊆ At(P) su
h that b ≤ a holds for every **a, b** ∈ S .

## 3.2 Splitting Sets And Loop Formulas

```
In this se
          tion we 
                   onsider only the 
                                     lass of normal logi
                                                          programs. We formu-

```

late the splitting-set theorem (Lifs hitz and Turner 1994) in the ase of normal