Testing the Equivalence of Disjunctive Logic Programs

Reference:

Emilia Oikarinen. Testing the equivalence of disjunctive logic programs. Research Report A85, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2003.

Abstract:

To solve a problem in answer set programming (ASP), one constructs a logic program so that its answer sets correspond to the solutions of the problem and computes the answer sets of the program using a special purpose search engine. The encodings are not unique, i.e. several versions of a program can be used e.g. in optimizing the execution time or space. Since the solutions to the problem correspond to answer sets of the program, it is necessary to ensure that the different encodings yield the same output. In ASP this means that one has to check whether given two logic programs have the same answer sets, i.e., whether they are semantically equivalent. We consider in this work the class of disjunctive logic programs, that form a proper generalization of normal logic programs.

The equivalence of logic programs and can naturally be verified using an explicit cross-check of all the answer sets of both programs. Our aim is, however, to develop a systematic method for testing the equivalence so that a naive cross-check of answer sets is not needed.

The idea is to translate logic programs and into a single logic program that has an answer set if and only if has an answer set that is not an answer set of . Thus answer sets of the translation (if found), act as a counter-examples for the equivalence of and . The counter-examples for equivalence divide naturally in two types. Thus the search for counter-examples can be performed separately for both types using a two-phased translation.

We have implemented the translation functions. Experiments with the implementation show that in several cases the translation-based approach is superior to the naive cross-checking approach, especially, if the programs to be tested have several answer sets and are likely to be nonequivalent. If the number of answer sets is low, then the naive cross-checking approach is likely to be faster. Furthermore, in general it is faster to use the two-phased translation.

Keywords:

disjunctive logic programs, equivalence testing, stable model semantics, answer set programming, non-monotonic reasoning, computational complexity

Suggested BibTeX entry:

@techreport{HUT-TCS-A85,
    address = {Espoo, Finland},
    author = {Emilia Oikarinen},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {December},
    number = {A85},
    pages = {61},
    title = {Testing the Equivalence of Disjunctive Logic Programs},
    type = {Research Report},
    year = {2003},
}