Cmodels for Tight Disjunctive Logic Programs

Disjunctive logic programming under the stable model semantics [GL91] is a new answer set programming (ASP) methodology for solving combinatorial search problems. It is a form of declarative programming related to logic programming languages, such as Prolog, where the solutions to a problem are represented by answer sets, and not by answer substitutions produced in response to a query as in convential logic programming. Instead of Prolog systems, this programming method uses answer set solvers, such as smodels1, smodelscc2, cmodels3, dlv4, and gnt1. These systems made it possible for ASP to be successfully applied in such areas as planning, bounded model checking, and space shuttle control. dlv and gnt are more general as they work with the class of disjunctive logic programs, while other systems cover nondisjunctive programs. System cmodels uses SAT solvers as search engines, which allows it to take advantage of rapid progress in the area of SAT. cmodels proved to be an efficient system in providing the solution to the wire-routing problem [EW04], and to the problem of reconstructing probable phylogenies in the area of historical linguistics [BEMR05]. In this work we extend cmodels [GLM04] to tight disjunctive programs. Complexity of finding a solution for such programs is NP, as in the case of nondisjunctive programs. Extending the syntax of the input language of cmodels to tight disjunctive programs permits the knowledge engineer to be more flexible with the encoding of the problems in the NP complexity class. Experimental analyses demonstrate that the approach is computationally promising and may advance applications of disjunctive logic programming