Proof Sketch: First we show that the states of the graphs SM−
Π
and SM(ASP)
−*Comp*(Π),Π coincide.

In view of Proposition 3 stated and proved by Lierler (Lierler 2011) it is sufficient to show that there is a non-singular edge M =⇒ M′in SMΠ justified by the transition *Unfounded*
(defined for SM) if and only if there is a non-singular edge M =⇒ M′in SM(ASP)*Comp*(Π),Π
justified by *Unfounded* (defined for SM(ASP)). We conclude by proving the last statement.

## 8.3 Proof Of Proposition 9

We first extend Lemma 8 to the "learning" version of the graph SM(ASP)F,Π.

Lemma 9 For every SM(ASP) theory [F,Π], every state M||Γ reachable from /0||/0 in SM(ASP)F,Π,
and every model N of [F,Π], if N satisfies all decision literals in M, then N satisfies M.

Proof The proof is by induction on n = |M| and proceeds similarly as that of Lemma 8. In particular, the property trivially holds for n = 0. Let us assume that the property holds for all states M||Γ, where |M| ≤ k, that are reachable from /0||/0. For the inductive step, let us consider a state M||Γ, with M = l1 ... lk, such that every model N of [F,Π] that satisfies all decision literals lj with j ≤ k satisfies M. We need to prove that applying any transition rule of SM(ASP)F,Π in the state M||Γ, leads to a state M′||Γ
′, where M′ = Mlk+1, such that if N
is a model of [F,Π] and N satisfies every decision literal lj with j ≤ k +1, then N satisfies M′.

The rules Decide, *Fail* and *Unfounded* can be dealt with as before (with only minor notational adjustments to account for extended states). Thus, we move on to the rules *Unit* Propagate Learn, *Backjump*, and Learn.

Unit Propagate Learn: We recall that Γ is a set of clauses entailed by F and Π. In other words, any model of [F,Π] is also a model of Γ. We now proceed as in the case of the rule Unit Propagate in the proof of Proposition 8 with F ∪Πcl replaced by F ∪Πcl ∪Γ.

Backjump: The argument is similar to that used in the case of the transition rule *Backtrack* in the proof of Lemma 8. Learn: This case is trivially true.

We now recall several concepts we will need in the proofs. Given a set A of atoms, we define *Bodies*(Π,A) = Sa∈A *Bodies*(Π,a). Let Π be a program and Y a set of atoms. We call the formula

a∈Y
$\bigvee_{\alpha}a\to\bigvee\{B\mid B\in\mathit{Bodies}(\Pi,Y)\text{and}B^{pos}\cap Y=0\}$
pos ∩Y = /0} (5)
the loop formula for Y (Lin and Zhao 2004). We can rewrite the loop formula (5) as the disjunction

$$B^{p o s}\cap Y=\emptyset\}.$$
$$\bigwedge\neg a)\lor\bigvee\{B\mid B\in$$

(^
a∈Y
¬a)∨_{B | B ∈ *Bodies*(Π,Y) and B
pos ∩Y = /0}. (6)