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.