LP2ACYC

Implementing answer set programming via SAT modulo acyclicity.

Main Components of the Implementation

• The acyclicity transformation is implemented by a translator called lp2acyc.
• The final translation into back-end formats can be achieved either by lp2sat (for SAT solvers like lingeling below) or acyc2solver (for other kinds of solvers like boolector, z3, cplex, or opbdp).

The respective binaries are available for download. For further command line options of the tools, please check lists provided by the --help option of each individual tool.

Using the Software

The typical use cases are illustrated by the following command lines. The file program.lp is assumed to contain the ASP encoding as well as instance data (if appropriate).

gringo program.lp | lpstrip | lp2normal2 | lpcat | lp2acyc | lp2sat -g | acycminisat

gringo program.lp | lpstrip | lp2normal2 | lpcat | lp2acyc | lp2sat | lingeling

gringo program.lp | lpstrip | lp2normal2 | lpcat | clasp

gringo program.lp | lpstrip | lpcat | lp2acyc | acyc2solver --bv | boolector --smt2 -m

gringo program.lp | lpstrip | lpcat | lp2acyc | acyc2solver --diff | z3 -smt2 -m /dev/stdin

gringo program.lp | lpstrip | lpcat | lp2acyc | acyc2solver --mip > program.mip

gringo program.lp | lpstrip | lpcat | lp2acyc | acyc2solver --pb | opbdp -s

gringo program.lp | lpstrip | lpcat | clasp

To ensure clean and contiguous input for the translators after grounding, we use lpstrip to remove unnecessary hidden atoms and lpcat to remove unused atom numbers in the examples above.

Related Publications

M. Gebser, T. Janhunen, and J. Rintanen. SAT Modulo Graphs: Acyclicity. In the Proceedings of JELIA'14, 137—151. Springer LNCS 8761.

M. Gebser, T. Janhunen, and J. Rintanen. Answer Set Programming as SAT modulo Acyclicity. In the Proceedings of ECAI'14, 351—356. IOS Press.

J. Bomanson, M. Gebser, and T. Janhunen. Improving the Normalization of Weight Rules in Answer Set Programs. In the Proceedings of JELIA'14, 166—180. Springer LNCS 8761.