Department of ICS / Software / lp2diff

LP2DIFF: Translating Normal/Smodels Programs for SMT (difference logic) solvers

This software has been designed to be used between

  1. the front-end lparse of the smodels system or any compatible grounder such as gringo and
  2. any SMT solver supporting the QF_IDL dialect (difference logic over integers) of the SMT library.

Related Publications

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.


Using the Software

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.


Disclaimer

The software below is provided on "as is" basis, without warranties of any kind or fitness for a particular purpose.

Copyright

The copyright for the binaries is held by Tomi Janhunen.
You may freely use this software for academic and research purposes but not redistribute it.

Download

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.

Benchmarking

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.


[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 21 May 2013. Tomi Janhunen