lp2diff
This software has been designed to be used between
lparse of the smodels
system or any compatible grounder
such as
gringo and
Tomi Janhunen, Ilkka Niemelä, and Mark Sevalnev: Computing Stable Models via Reductions to Difference Logic. In E. Erdem, F. Lin, and T. Schaub, editors, the Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning, pages 142—154, Potsdam, Germany, September 2009. Springer, LNAI 5753.
Ilkka Niemelä: Stable Models and Difference Logic. Annals of Mathematics and Artificial Intelligence, 53 (1—4), 313—329, 2008.
Tomi Janhunen, Ilkka Niemelä, and Mark Sevalnev: Computing Stable Models via Reductions to Boolean Circuits and Difference Logic. In M. Denecker, editor, the Working Notes of the 2nd International Workshop on Logic and Search, pages 16—30, Leuven, Belgium, November 2008.
The following example demonstrates how a stable model is computed using our translator:
$ lparse program.lp > program.sm$ lp2diff program.sm > program.idl$ bclt program.idl -model model.out
First, the source code program.lp is grounded using
lparse. Then, the resulting ground program is translated
into QF_IDL format. Last, an SMT-solver (such as BarceLogic)
is invoked to compute a stable model. The given example is merely
about checking the existence of a stable model because the
transformation implemented by lp2diff does not preserve
symbolic names of atoms since they would be interpreted differently
under QF_IDL anyway.
The actual answer set can be recovered using two additional tools,
lpcat and interpret, from the
asptools collection.
When used with lp2diff, they are invoked roughly as follows.
$ lparse program.lp | lpcat -s=symbols.sm | lp2diff > program.idl
$ bclt program.idl -model model.out
$ cat model.out | tr -d '\000' | fgrep var_
| fgrep true | interpret symbols.sm
The last command line is specific to bclt and, for
simplicity, all pretty printing aspects have been omitted. To this
end, you might want to use sed or write a perl script of
your own. For futher hints, feel free to consult a sample callscript which uses
gringo as a grounder. It also shows how
smodels can be used as a preprocessor to
lp2diff in order to reduce the input program.
Linux binaries: lp2diff (version 1.27 / 64 bit, 1.27, 1.10 / 32 bit).
The version 1.10 was used in the second
ASP competition.
However, it requires preprocessing by lp2normal from asptools
collection in order to support choice rules.
Benchmark instances based on ASP 2009 competition instances are available
here
(a big 480MB file, SMT-LIB 1.2 format). This
a gzip-compressed tar-archive of
gzip-compressed formulas in QF_IDL format which can
be used as direct input for SMT-solvers when uncompressed.