For an SM(ASP) theory [F,Π] and a node M||Γ in SM(ASP)F,Π, a resolution derivation C1,...,Cn is trivial on M with respect to [F,Π]
11 if
(1) {C1,...,Ci} = RM
(2) Ci+1 is a conflicting clause on M with respect to [F,Π]
(3) Cj, j > i + 1, is derived from Cj−1 and a clause Ck, where k ≤ i (that is, Ck ∈ RM),
by resolving on some non-decision literal of *consistent*(M).

For a record M0 l1M1 ... lkMk, where li are all the decision literals of the record, we say that the literals of liMi belong to a decision level i. For a state MlM′l
′M′′, we say that l is older than l
′. We say that a state is a backjump state if it is inconsistent, contains a decision literal, and is reachable from /0||/0 in SML(ASP)F,Π.

## Lemma 13

For every SM(ASP) theory [F,Π], the transition rule *Backjump* is applicable in every backjump state in SM(ASP)F,Π.

## Proof

Let M||Γ be a backjump state in SM(ASP)F,Π. We will show that M has the form Pl∆Q and that there is a literal l
′that has a reason to be in Pl′ with respect to [F,Π].

Since M||Γ is a backjump state, it follows that M has the form consistent(M)l N. It is clear that l is not a decision literal (otherwise *consistent*(M)l would be consistent). By Lemma 11, there is a reason, say R for l to be in M. We denote this reason by R. Since consistent(M)l is inconsistent, l ∈ *consistent*(M). This observation and the definition of a reason imply that *consistent*(M) |= ¬R. Moreover, since F,Πo|= R (as R is a reason), R is a conflicting clause.

Let dec be the largest of the decision levels of the complements of the literals in R
(each of them occurs in *consistent*(M)). Let D be the set of all non-decision literals in consistent(M). By D
dec we denote a subset of D that contains all the literals that belong to decision level dec.

It is clear that C1,...,Ci,Ci+1, where {C1,...Ci} = RM and Ci+1 = R, is a trivial resolution derivation with respect to M and *consistent*(M) |= ¬Ci+1. Let us consider a trivial resolution derivation with respect to M of the form C1,...,Ci,Ci+1,...,Cn, where n ≥ i+1 and *consistent*(M) |= ¬Cn. Let us assume that there is a literal l ∈ D such that l in Cn. It follows that Cn = l∨C
′n
, for some clause C
′n
.

Since l ∈ D (is a non-decision literal in *consistent*(M)), the set RM contains the clause rM(l), which is a reason for l to be in M. The clause rM(l) is of the form l∨l1 ∨... ∨lm, where literals l1,...,lm are older than l and *consistent*(M) |= ¬(l1 ∨ ... ∨lm). Resolving Cn and rM(l) yields the clause Cn+1 = C
′n ∨l1 ∨... ∨lm. Clearly, C1,...,Cn+1 is a trivial resolution derivation with respect to M and *conistent*(M) |= ¬Cn+1.

If we apply this construction selecting at each step a non-decision literal l ∈ D
dec such that l ∈ R, then at some point we obtain a clause Cn that contains exactly one literal whose complement belongs to decision level dec (the reason is that in each step of the construction, the literal with respect we perform the resolution is replaced by older ones).