LP2DIFF+YICES

Affiliation:

Description:

Our approach is based on the idea of 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. We use a fixed callscript to solve all problem instances by performing the following seven steps:

• gringo (version 2.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). No search nor lookahead is performed at this point.
• lpcat (version 1.14) removes all unused atom numbers and makes the atom table contiguous.
• lp2normal (version 1.7) translates away choice rules and cardinality constraints. For the latter purpose, we use a transformation suggested by Een and Sörensson. The outcome contains only normal rules and weight rules.
• lp2diff (version 1.10) maps a normal program to a theory of difference logic using ranking constraints introduced by Niemelä. The bodies of weight rules are also transformed into special difference constraints, but otherwise they are treated very much like normal rules.
• yices (version 1.0.21) computes a model for the theory.
• The answer set is extracted using interpret (version 1.7).

Acknowledments. Almost all of our encodings originate from the Asparagus collection (authored by Gebser et al). Some of them were sligthly reformulated for better performance. The grounder Gringo has been developed at the University of Potsdam. The back-end solver Yices was provided by Stanford Research Institute. Patrik Simons from Neotide Ltd revised Smodels for our purposes.

Participants:

Tomi Janhunen

Ilkka Niemelä