ASP(DL)

This is an extension of answer set programming (ASP) where rules and difference constraints are used together for modelling.

Prototype Implementation

• DINGO (v. 2011-09-23) uses gringo (v. 3.0.3) to ground the logic program, lp2diff (v. 1.33) to translate it into difference logic formulae, and an appropriate SMT solver (such as z3, v. 2.11) to compute answer sets.
• Scripts for downloading third-party software are provided.
• The distribution contains also two benchmark problems, viz. Newspaper and Sorting, and their instances as reporeted in our GTTV'11 paper.

Simple Example

• A special predicate int/1 is reserved for declaring the required integer variables.
• Predicates dl_lt/3, dl_le/3, dl_gt/3, dl_ge/3, dl_eq/3, and dl_ne/3 are used to denote difference constraints having the respective operator <,<=,>,>=,=, and =/=.
• The predicates above can be renamed in the implementation if appropriate.
• The famous n-queens problem is encoded as follows:

  queen(1..n).

  int(row(X)) :- queen(X).

  int(zero).

  :- dl_le(row(X),zero,0), queen(X).

  :- dl_gt(row(X),zero,n), queen(X).

  :- dl_eq(row(X),row(Y),0), queen(X;Y), X

  :- dl_eq(row(X),row(Y),#abs(X-Y)), queen(X;Y), X!=Y.

• The example above, stored as queens.lp, is run as follows (the parameter n is also set):
  $ dingo.sh -cn=7 queen.lp
SATISFIABLE
queen(1) queen(2) queen(3) queen(4) queen(5) queen(6) queen(7)
Theory:
Vars: row(7)=7 zero=0 row(6)=2 row(5)=4 row(4)=6 row(3)=1 row(2)=3 row(1)=5
• For more details, please consult the slides of the workshop presentation or the paper below.

Related Publications

T. Janhunen, G. Liu, and I. Niemelä: Tight Integration of Non-Ground Answer Set Programming and Satisfiability Modulo Theories. In P. Cabalar, D. Mitchell, D. Pearce, and E. Ternovska, editors, the Proceedings of the 1st Workshop on Grounding and Transformations for Theories with Variables (GTTV'11), 1—13. Vancouver, British Columbia, Canada, May 2011.