Thus there are three **subequations for** p:
p ⇔ ¬q p ⇔ ¬r Now, q has only two subequations: q ⇔ ¬s, and ¬q. Similarly, t **has only two** subequations, t and ¬t**, but the second one automatically leads to contradiction** whenever it is chosen. Finally each of r and s **have just one defining equation,** ¬r, and ¬s**, respectively.**
First let us choose for p, the subequation ¬p, and for q, the subequation q ⇔ ¬s.

The remaining subequations are forced to t, ¬r, and ¬s**. The resulting theory has** nine clauses, when we write our program in propositional form:
S = {¬p, ¬r, ¬s, t, q ⇔ ¬s} ∪ {¬t ∨ p ∨ q, r ∨ p, s ∨ **q, t**}.

It is quite obvious that this theory is inconsistent. However, if we choose for p**, the** subequation p ⇔ ¬r and for q, the subequation q ⇔ ¬s**, then the resulting theory** written out in propositional form is S = {p ⇔ ¬r, ¬r, ¬s, t, q ⇔ ¬s} ∪ {¬t ∨ p ∨ q, r ∨ p, s ∨ **q, t**}.

In this case, {p, q, t} is a model of S and hence, {p, q, t} **is a stable model of** P. 

It should be clear that Proposition 4.1 implies an algorithm for computation of stable models. Namely, we generate candidate theories and find their propositional models.

Let us observe that the algorithm described above can be implemented as a two-tier backtracking search**, with the on-line computation of supports of guarded**
resolution proofs, and the usual backtracking scheme of DPLL. This second backtracking can be implemented using any DPLL-based SAT-solver. Proposition 4.1 implies that the algorithm we outlined is both sound and complete. Indeed, if the SAT solver returns a model M of theory T , then, by Proposition 4.1(1), M is a stable model for P**. Otherwise we generate another candidate theory and loop through**
this process until one satisfying assignment is found. Proposition 4.1(2) guarantees the completeness of our algorithm.

Our algorithm is not using loop formulas like the algorithm of Lin and Zhao
(Lin and Zhang 2002) but systematically searches for supports of **proof schemes,**
thus providing supports for atoms in the putative model. It also differs from the modified loop formulas approach of Ferraris, Lee and Lifschitz (Ferraris, Lee and Lifschitz 2006)
in that we do not consider loops of the call-graph of P at all. Instead, we compute systematically proof schemes and their supports for atoms. **While the timecomplexity of our algorithm is significant because there may be exponentially many**
supports for any given atom p, the space complexity is |P|**. This is the effect of not** looking at loop formulas at all ((Lifschitz and Razborov 2006)).