w ∈ N and the respe
tive weights wbj ∈ N and wck ∈ N asso
iated with ea
h positive literal bj and negative literal ∼ck . We use a shorthand ∼A = {∼a | a ∈ A} for any set of atoms A. Ea
h basi 
onstraint rule r 
onsists of two parts: a or {a1**, . . . , a**h} is the head of the rule, denoted by **Head(**r), whereas the rest is 
alled its body. The set of atoms appearing in a body of a rule an be further divided into the set of positive body atoms, dened as Body+(r) = {b1**, . . . , b**n}, and the set of negative body atoms, dened as Body−(r) = {c1**, . . . , c**m}. We denote by Body(r) = Body+(r)∪**Body**−(r)
the set of atoms appearing in the body of a rule r. Roughly speaking, the body

```
gives the 
          onditions on whi
                             h the head of the rule must be satised. For example,
                                                                                    

```

in ase of a hoi e rule (2), this means that any head atom ai 
an be inferred to be true if b1**, . . . ,b**n hold true by some other rules but none of the atoms c1**, . . . ,c**m .

Weight rules of the form (1) 
over many other kinds of rules of interest as their

```
spe
   ial 
     ases:
         

```

$$a\gets l\leq\{b_{1},\ldots,b_{n},\sim\!c_{1},\ldots,\sim\!c_{m}\}\tag{3}$$ $$a\gets b_{1},\ldots,b_{n},\sim\!c_{1},\ldots,\sim\!c_{m}$$ (4) $$\gets b_{1},\ldots,b_{n},\sim\!c_{1},\ldots,\sim\!c_{m}$$ (5) $$\mbox{compute}\{b_{1},\ldots,b_{n},\sim\!c_{1},\ldots,\sim\!c_{m}\}\tag{6}$$

Cardinality rules of the form (3) are essentially weight rules (1) where w = l and all weights asso iated with literals equal to 1. A normal rule, or alternatively a basi rule (4) is a spe ial ase of a ardinality rule (3) with l = n + m. The in-

```
tuitive meaning of an integrity 
                                    onstraint (5) is that the 
                                                                onditions given in the
                                                                                        

body are never simultaneously satised. The same 
                                         an be stated in terms of a basi
                                                                 

```

rule f ← b1, . . . ,bn, ∼c1**, . . . ,**∼cm, ∼f where f is a new atom dedi
ated to integrity onstraints. Finally, ompute statements (6) of the smodels system ee tively orrespond to sets of integrity onstraints ← ∼b1, . . . ,← ∼bn and ← c1**, . . . ,**← cm .

Be ause the order of literals in (1) and (2) is onsidered irrelevant, we introdu e shorthands A = {a1, . . . , ah}, B = {b1**, . . . , b**n}, and C = {c1**, . . . , c**m} for the sets of atoms involved in rules, and WB = {wb1
, . . . , wbn } and WC = {wc1
, . . . , wcm}
for the respe tive sets of weights in (1). Using these notations (1) and (2) are abbreviated by a ← w ≤ {B = WB, ∼C = WC }
2 and {A} ← B, ∼C .

In the smodels system, the internal representation of programs is based on rules of the forms (1)(4) and (6) and one may on lude that basi
 
onstraint rules, as introdu ed above, provide a reasonable overage of smodels programs. Thus we on entrate on rules of the forms (1) and (2) and view others as synta ti sugar in the sequel.

Denition 3.1 An smodels program P is a nite set of basi 
onstraint rules.

```
An smodels program 
                onsisting only of basi
                                rules is 
                                      alled a normal logi
                                                     pro-

```

gram (NLP), and a basi rule with an empty body is alled a fa t. Given an smodels 2 Stri tly speaking B = WB and ∼C = WC are to be understood as sets of pairs of the form
(**b, w**b) and (∼**c, w**c), respe
tively. For 
onvenien
e the exa
t mat
hing between literals and weights is left impli it in the shorthand.