LP2SAT+MINISAT

Affiliation:

Description:

Our approach is based on the idea of 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. We use a fixed callscript to solve all problem instances by performing the following ten 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, cardinality rules, and weight rules. The outcome contains only normal rules.
• smodels (version 2.34) simplifies the instance again.
• lpcat (version 1.14) compresses the atom table again.
• lp2exp (version 1.5) 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 integer variables are represented by vectors of atomic propositions.
• lp2sat (version 1.13) forms the Clark's completion of the program as a set of clauses (DIMACS format).
• minisat (version 1.14) 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 Minisat originates from Chalmers University of Technology. Patrik Simons from Neotide Ltd revised Smodels for our purposes.

Participants:

Tomi Janhunen

Ilkka Niemelä