lp2sat2minisat
Association
Aalto University, Department of Information and Computer Science
Description
Our approach is based on translating an answer set program into a set of propositional clauses and then computing stable models for the program indirectly by finding models for the translation. The second version of the translator (a.k.a lp2sat2) incorporates an improved translation based on ranking constraints that were used to translate answer set programs into difference logic. 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.
- lp2normal (version 1.11) translates away choice rules, cardinality rules, and weight rules. The outcome contains only normal rules.
- igen (version 1.7) is needed for backward compatibility.
- smodels (version 2.34) simplifies the instance again.
- lpcat (version 1.18) compresses the symbol/atom table again.
- lp2lp2 (version 1.17) transforms a normal program so that all supported models are also stable. The translation is analogous to that produced by lp2diff for SMT solvers but integers are encoded as vectors of atoms.
- lp2sat (version 1.15) forms the Clark's completion of the program as a set of clauses in the DIMACS format.
- minisat (version 1.14) computes a model for the theory (if any).
- interpret (version 1.7) is used to extract an answer set.
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 Minisat originates from Chalmers University of Technology.
Participants
- Tomi Janhunen
- Ilkka Niemelä