of correctness to every SM(ASP) solver in this class and a proof of termination under the assumption that basic transition rules periodically appear in a path constructed from /0||/0.

Nieuwenhuis et al. (2006) proposed the transition rules to model such techniques as forgetting and restarts. The graph SML(ASP)F,Π can easily be extended with such rules.

## 5 Abstract Cmodels, Clasp And Minisat(Id)

We can view a path in the graph SML(ASP)F,Π as a description of a process of search for a model of an SM(ASP) theory [F,Π] by applying transition rules. Therefore, we can characterize the algorithm of a solver that utilizes the transition rules of SML(ASP)F,Π
by describing a strategy for choosing a path in this graph. A strategy can be based, in particular, on assigning priorities to transition rules of SML(ASP)F,Π, so that a solver never applies a rule in a state if a rule with higher priority is applicable to the same state.

We use this approach to describe and compare the algorithms implemented in the solvers CMODELS, CLASP and MINISAT(ID). We stress that we talk here about characterizing and comparing algorithms and not their specific implementations in the solvers. We refer to these algorithms as abstract CMODELS, CLASP and MINISAT(ID), respectively. Furthermore, we only discuss the abstract MINISAT(ID) for the case of the total PC(ID) theories whereas the MINISAT(ID) system implements additional totality check propagation rule to deal with the non-total theories. Given a program Π, abstract CMODELS and abstract CLASP
construct first *ED-Comp*(Π). Afterwards, they search the graph SML(ASP)*ED-Comp*(Π),Π for a path to a semi-terminal state. In other words, both algorithms, while in a node of the graph SML(ASP)*ED-Comp*(Π),Π, progress by selecting one of the outgoing edges. By Proposition 9 and Corollary 1, each algorithm is indeed a method to compute answer sets of programs.

However, abstract CMODELS selects edges according to the priorities on the transition rules of the graph that are set as follows:
Backjump,Fail ≫ Unit Propagate ≫ Decide ≫ *Unfounded*,
while abstract CLASP uses a different prioritization:

## Backjump,Fail ≫ Unit Propagate ≫ Unfounded ≫ Decide.

The difference between the algorithms boils down to when the rule *Unfounded* is used.

We now describe the algorithm behind the PC(ID) solver MINISAT(ID) (Mari¨en et al.

2008) for total PC(ID) theories - the abstract MINISAT(ID). Speaking precisely, MINI-SAT(ID) assumes that the program Π of the input PC(ID) theory (F,Π) is in the definitional normal form (Mari¨en 2009). Therefore, in practice MINISAT(ID) is always used with a simple preprocessor that converts programs into the definitional normal form. We will assume here that this preprocessor is a part of MINISAT(ID). Under this assumption, given a PC(ID) theory (F,Π), MINISAT(ID) can be described as constructing the completion ED-Comp(Πo) (the new atoms are introduced by the preprocessor when it converts Π into the definitional normal form, the completion part is performed by the MINISAT(ID) proper),
and then uses the transitions of the graph SML(ASP)*ED-Comp*(Πo)∪F,Πo to search for a path to a semi-terminal state. In other words, the graph SML(ASP)*ED-Comp*(Πo)∪F,Πo represents the abstract MINISAT(ID). The strategy used by the algorithm follows the prioritization:
Backjump,Fail ≫ Unit Propagate ≫ Unfounded ≫ Decide.