Proposition 7 For any SM(ASP) theory [F,Π],
(a) graph SM(ASP)F,Π is finite and acyclic,
(b) for any terminal state M of SM(ASP)F,Π other than *FailState,* M is a model of [F,Π],
(c) *FailState* is reachable from /0 in SM(ASP)F,Π if and only if [F,Π] has no models.

Proposition 7 shows that algorithms that correctly find a path in the graph SM(ASP)F,Π
from /0 to a terminal node can be regarded as SM(ASP) solvers. It also provides a proof of correctness for every SM(ASP) solver that can be shown to work in this way.

One of the ways in which SM(ASP) encompasses ASP (specifically, Corollary 1(c)) is closely related to the way the answer-set solver SMODELS works. We recall that to represent SMODELS Lierler (2011) proposed a graph SMΠ. We note that the rule *Unfounded* above is closely related to the transition rule with the same name used in the definition of SMΠ (Lierler 2011). In fact, if Π = Πothen these rules are identical.

Lierler (2011) observed that SMODELS as it is implemented never follows certain edges in the graph SMΠ, and called such edges singular. Lierler (2011) denoted by SM−
Π
the graph obtained by removing from SMΠ all its singular edges and showed that SM−
Π
is still sufficient to serve as an abstract model of a class of ASP solvers including SMODELS. The concept of a singular edge extends literally to the case of the graph SM(ASP)F,Π. An edge M =⇒ M′in the graph SM(ASP)F,Π is singular if:
1. the only transition rule justifying this edge is *Unfounded*, and 2. some edge M =⇒ M′′ can be justified by a transition rule other than *Unfounded* or Decide.

We define SM(ASP)
−
F,Π
as the graph obtained by removing all singular edges from SM(ASP)F,Π.

Proposition 8 below can be seen as an extension of Proposition 4 in (Lierler 2011) to nontight programs.

Proposition 8 For every program Π, the graphs SM−
Π
and SM(ASP)
−
Comp(Π),Π
are equal.

It follows that the graph SM(ASP)
−
Comp(Π),Π
provides an abstract model of SMODELS.

We recall though that *Comp*(Π) can be exponentially larger than the completion formula before clausification. Using ASP specific propagation rules such as *Backchain True* and All Rules Cancelled (Lierler 2011) allows SMODELS to avoid explicit representation of the clausified completion and infer all the necessary transitions directly on the basis of the program Π.

A similar relationship, in terms of pseudocode representations of SMODELS and DPLL,
is established in (Giunchiglia and Maratea 2005) for tight programs.

The answer-set solvers CMODELS, CLASP and the PC(ID) solver MINISAT(ID) cannot be described in terms of the graph SM(ASP) nor its subgraphs. These solvers implement such advanced features of SAT and SMT solvers as learning (forgetting), backjumping and restarts (Nieuwenhuis et al. (2006) give a good overview of these techniques). In the next section we extend the graph SM(ASP)F,Π with propagation rules that capture these techniques. In the subsequent section, we discus how this new graph models solvers CMODELS,
CLASP, and MINISAT(ID). Then we provide insights into how they are related.