Logic programs with the stable model semantics can be thought of as a newparadigm for constraint satisfaction, where the rules of a program are seen as constraints on the stable models. In this work the paradigm is realized by developing an efficient procedure for computing the stable models of ground logic programs. A strong pruning technique based on two deductive closures is introduced. The technique is further strengthened by the introduction of backjumping, which is an improvement over chronological backtracking, and lookahead, a new pruning method. Moreover, a strong heuristic is derived. The two deductive closures are given linear-time implementations that provide a linear-space implementation method for the decision procedure. A high lower bound on the least upper bound on the complexity of the procedure is found. In order to generalize the procedure such that it can handle programs with variables, an algorithm for grounding a function-free range restricted logic program that avoids generating the whole ground instantiation is presented.
展开▼
