Remark 1 Corollary 1 specifies three ways to describe answer sets of a program in terms of models of SM(ASP) theories. This offers an interesting view into answer-set generation. The CNF
formulas appearing in the SM(ASP) theories in the conditions (b) - (d) make explicit some of the "propositional satisfiability inferences" that may be used when computing answer sets. The condition (b) shows that when computing answer sets of a program, atoms not occurring as heads can be inferred as false. The theory in (c) makes it clear that a much broader class of inferences can be used, namely those that are based on the clauses of the completion. The theory in (d) describes still additional inferences, as now, thanks to new atoms, we can explicitly infer whether bodies of rules must evaluate to true or false. In each case, some inferences needed for generating answer sets are still not captured by the respective CNF theory and require a reference to the program Π. We note that it is possible to express these "answer-set specific" inferences in terms of clauses corresponding to loop formulas (Lin and Zhao 2004; Lee 2005). We do not consider this possibility in this paper.

Next, we show that SM(ASP) encompasses the logic PC(ID). The well-founded model M
of a program Π is total if it assigns all atoms occurring in Π. For a PC(ID) theory (F,Π), a program Π is total on a model M of F if W
fix Πo (MO
Π) is total. A program Π is total if Π is total on every model M of F. The PC(ID) theories (F,Π) where Π is total form an important class of total PC(ID) theories.

There is a tight relation between models of a total PC(ID) theory (F,Π) and models of an SM(ASP) theory [F,Π].

Proposition 6 For a total PC(ID) theory (F,Π) and a set M of literals over the set At(F∪Π) of atoms, the following conditions are equivalent:
(a) M is a model of (F,Π),
(b) M is a model of the SM(ASP) theory [F,Π],
(c) M is a model of the SM(ASP) theory [*Comp*(ΠAt(Π))∪F,Π],
(d) for some model M′ of the SM(ASP) theory [*ED-Comp*(ΠAt(Π))∪F,Π], M = M′ ∩
At(F ∩Π).

The conditions (b), (c), (d) state that the logic PC(ID) restricted to total theories can be regarded as a fragment of the SM(ASP) formalism. The comments made in Remark 1 pertain also to generation of models in the logic PC(ID).

We now characterize models of SM(ASP) theories, and computations that lead to them, in terms of transition systems. Later we discuss implications this characterization has for ASP and PC(ID) solvers.

We define the transition graph SM(ASP)F,Π for an SM(ASP) theory [F,Π] as follows.

The set of nodes of the graph SM(ASP)F,Π consists of the states relative to At(F ∪ Π).

There are five transition rules that characterize the edges of SM(ASP)F,Π. The transition rules Unit Propagate, Decide, Fail, *Backtrack* of the graph DPF∪Πcl , and the transition rule Unfounded: M =⇒ M¬a if a ∈ U for a set U unfounded on M w.r.t. Πo.

The graph SM(ASP)F,Π can be used for deciding whether an SM(ASP) theory [F,Π] has a model.