## 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.