Modular Answer Set Programming

Reference:

Emilia Oikarinen. Modular answer set programming. Research Report A106, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2006.

Abstract:

Answer set programming (ASP) is a declarative rule-based constraint programming paradigm. In ASP the problem at hand is solved declaratively by writing down a logic program the answer sets of which correspond to the solutions of the problem, and then computing the answer sets of the program using a special purpose search engine. The growing interest towards ASP is mostly due to efficient search engines available today. Consequently, a variety of interesting applications of ASP has emerged, for example, in planning, product configuration, computer aided verification, and wire routing in VLSI design.

Despite the declarative nature of ASP the development of programs resembles that of programs in conventional programming: a programmer often develops a series of gradually improving programs for a particular problem, for example, when optimizing execution time and space. However, currently ASP programs are considered as integral entities. This becomes problematic as programs become more complex, and the sizes of program instances grow. In ASP there is a lack of mechanisms, available in other modern programming languages, that ease program development by allowing re-use of code or breaking programs into smaller pieces, modules. Even though modularity has been studied extensively in conventional logic programming, there are only few approaches how to incorporate modularity into ASP.

In this report we propose a simple and intuitive notion of a logic program module that interacts through an input/output interface. The module system is fully compatible with the stable model semantics. This is achieved by restricting the composition of modules in a way that module-level stability implies program-level stability, and vice versa. Furthermore, we introduce a notion of modular equivalence that is a proper congruence relation for the composition of modules and analyze the computational complexity of deciding modular equivalence. We extend an earlier translation-based method for verifying equivalence of ASP programs to cover the verification of modular equivalence of SMODELS program modules, and evaluate experimentally the efficiency of the translation-based method in the verification of modular equivalence. We also study questions related to finding a suitable module structure for a program when there is no explicit a priori knowledge on the underlying structure.

Keywords:

modular answer set programming, modular congruence, equivalence verification, stable model semantics, nonmonotonic reasoning

Suggested BibTeX entry:

@techreport{HUT-TCS-A106,
    address = {Espoo, Finland},
    author = {Emilia Oikarinen},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {December},
    number = {A106},
    pages = {x+81},
    title = {Modular Answer Set Programming},
    type = {Research Report},
    year = {2006},
}