Towards Constraint Satisfaction through Logic Programs and the Stable Model Semantics

Reference:

Patrik Simons. Towards constraint satisfaction through logic programs and the stable model semantics. Research Report A47, Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory, Espoo, Finland, August 1997.

Abstract:

Logic programs with the stable model semantics can be thought of as a new paradigm 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 decision procedure for the stable model semantics that computes the stable models of a ground logic program. 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 rule. 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. Finally, an implementation of the decision procedure is compared with a state-of-the-art satisfiability checker using hard satisfiability problems as a test domain.

Keywords:

stable model semantics, logic programming, nonmonotonic reasoning, automatic theorem proving

Suggested BibTeX entry:

@techreport{HUT-TCS-A47,
    address = {Espoo, Finland},
    author = {Patrik Simons},
    institution = {Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory},
    month = {August},
    number = {A47},
    pages = {49},
    title = {Towards Constraint Satisfaction through Logic Programs and the Stable Model Semantics},
    type = {Research Report},
    year = {1997},
}