  An algorithm for computing the stable model semantics of logic programs is
developed. It is shown that one can extend the semantics and the algorithm to
handle new and more expressive types of rules. Emphasis is placed on the use of
efficient implementation techniques. In particular, an implementation of
lookahead that safely avoids testing every literal for failure and that makes
the use of lookahead feasible is presented. In addition, a good heuristic is
derived from the principle that the search space should be minimized.
  Due to the lack of competitive algorithms and implementations for the
computation of stable models, the system is compared with three satisfiability
solvers. This shows that the heuristic can be improved by breaking ties, but
leaves open the question of how to break them. It also demonstrates that the
more expressive rules of the stable model semantics make the semantics clearly
preferable over propositional logic when a problem has a more compact logic
program representation. Conjunctive normal form representations are never more
compact than logic program ones.
