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.
If we look in a broader context, then finding a stable model is a combinatorial search problem. Other forms of combinatorial search problems are propositional satisfiability, constraint satisfaction, constraint logic programming and integer linear programming problems, and some other logic programming problems such as those expressible in @cite_28 . The difference between these problem formalisms and the stable model semantics is that they do not include default negation. In addition, all but the last one are not nonmonotonic.
@cite_28
2051790368
In this paper a logic-based specification language, called NP-SPEC, is presented. The language is obtained by extending DATALOG through allowing a limited use of some second-order predicates of predefined form. NP-SPEC programs specify solutions to problems in a very abstract and concise way, and are executable. In the present prototype they are compiled to PROLOG code, which is run to construct outputs. Second-order predicates of suitable form allow to limit the size of search spaces in order to obtain reasonably efficient construction of problem solutions. NP-SPEC expressive power is precisely characterized as to express exactly the problems in the class NP. The specification of several combinatorial problems in NP-SPEC is shown, and the efficiency of the generated programs is evaluated.