lp2diffz3

Association

Aalto University, Department of Information and Computer Science

Description

Our approach is based on translating an answer set program into a theory in difference logic and then computing stable models for the program indirectly by finding models for the translation. Overall, the computation takes place in the following steps:

• gringo (version 3.0.3) grounds the encoding and problem instance.
• smodels (version 2.34) simplifies the instance using the well-founded semantics and the compute statement (if any).
• lpcat (version 1.18) removes all unused atom numbers and makes the atom/symbol table contiguous.
• lp2diff (version 1.27) maps a normal program to a theory of difference logic using ranking constraints introduced by Niemelä. The bodies of cardinality and weight rules are also transformed into special difference constraints, but otherwise they are treated very much like normal rules.
• z3 (version 2.11) computes a model for the theory (if any).
• interpret (version 1.7) is used to extract an answer set.

Participants

• Tomi Janhunen
• Ilkka Niemelä

Acknowledgments

The grounder gringo has been developed at the University of Potsdam, Germany. Patrik Simons from Neotide Ltd is the author of the smodels system. The back-end solver z3 originates from Microsoft.