
## 7 Related Work And Discussion

Lierler (2011) introduced the graphs SML and GTL that extended the graphs SM and GT (Lierler 2011), respectively, with transition rules *Backjump* and *Learn*. The graph SML was used to characterize the computation of such answer set solvers implementing learning as SMODELScc 8(Ward and Schlipf 2004) and SUP9(Lierler 2011) whereas the graph GTL was used to characterize CMODELS. These graphs are strongly related to our graph SML(ASP)
but they are not appropriate for describing the computation behind answer set solver CLASP
or PC(ID) solver MINISAT(ID). The graph SML reflects only propagation steps based on a program whereas CLASP and MINISAT(ID) proceed by considering both the program and a propositional theory. The graph GTL, on the other hand, does not seem to provide a way to imitate the behavior of the *Unfounded* rule in the SML(ASP) graph.

Giunchiglia and Maratea (2005) studied the relation between the answer set solver SMODELS and the DPLL procedure for the case of tight programs by means of pseudocode analysis. Giunchiglia et al (2008) continued this work by comparing answer set solvers SMODELS, DLV10 (Eiter et al. 1997), and CMODELS via pseudocode. In this paper we use a different approach to relate solvers that was proposed by Lierler (2011). That is, we use graphs to represent the algorithms implemented by solvers, and study the structure of these graphs to find how the corresponding solvers are related. We use this method to state the relation between the answer set solvers CMODELS, CLASP, and the PC(ID) solver MINI-SAT(ID) designed for different knowledge representation formalisms. Gebser and Schaub (2006) introduced a deductive system for describing inferences involved in computing answer sets by tableaux methods. The abstract framework presented in this paper can be viewed as a deductive system also, but a very different one. For instance, we describe backtracking and backjumping by inference rule, while the GebserSchaub system does not. Also the Gebser-Schaub system does not take learning into account. Accordingly, the derivations considered in this paper describe a search process, while derivations in the Gebser-Schaub system do not. Further, the abstract framework discussed here does not have any inference rule similar to Cut; this is why its derivations are paths rather than trees.

Mari¨en (2009) (Section 5.7) described a MINISAT(ID) transition system to model a computation behind the PC(ID) solver MINISAT(ID). We recall that we modeled the abstract MINISAT(ID) with the graph SML(ASP). The graphs SML(ASP) and MINISAT(ID)
are defined using different sets of nodes and transition rules. For instance, SML(ASP) allows states containing inconsistent sets of literals whereas the MINISAT(ID) graph considers consistent states only. Due to this difference the MINISAT(ID) graph requires multiple versions of "backjump" and "fail" transition rules.

We used transition systems to characterize algorithms for computing answer sets of logic programs and models of PC(ID) theories. These transition systems are also suitable for formal comparison of the strength or power of reasoning methods given rules that specify them. An approach to do so was proposed by Mari¨en (2009) (Section 5.7), who introduced