welcome: please sign in
location: Diff for "Participants\LP2BV-2"
Differences between revisions 2 and 3
⇤ ← Revision 2 as of 2013-05-23 22:14:16 →
Size: 1170
Editor: FrancescoCalimeri
Comment:
← Revision 3 as of 2013-05-23 22:15:12 → ⇥
Size: 1172
Editor: FrancescoCalimeri
Comment:
Deletions are marked like this. Additions are marked like this.
Line 26: Line 26:
 * Mai Nguyen, Tomi Janhunen, and Ilkka Niemelä. ''Translating Answer-Set Programs into Bit-Vector Logic. In the Proceedings of the 19th International Conference on Applications of Declarative Programming and Knowledge Management, 105—116. Vienna, Austria, September 2011  * Mai Nguyen, Tomi Janhunen, and Ilkka Niemelä. ''Translating Answer-Set Programs into Bit-Vector Logic''. In the Proceedings of the 19th International Conference on Applications of Declarative Programming and Knowledge Management, 105—116. Vienna, Austria, September 2011

LP2BV-2

Team

  • Tomi Janhunen (Aalto University)
  • Guohua Liu (Aalto University)
  • Jori Bomanson (Aalto University)
  • Ilkka Niemelä (Aalto University)

Description

A given ASP program is grounded by GRINGO and the ground program is simplified by SMODELS, then the simplified program is normalized using LP2NORMAL2 and translated to bit vectors using LP2BV, and finally, the bit vectors are solved by Z3.

System Settings

The main modules and option flags are as below:

  • GRINGO 3.0.4 --shift
  • SMODELS 2.34 -internal -nolookahead
  • LP2NORMAL2 1.1 -wp -wt -wh -wn -wy -cs
  • LP2BV 1.10 -f
  • Z3 4.3.1 --smt2

The input language is Gringo 3.

References

  • Participant URL.

  • Mai Nguyen, Tomi Janhunen, and Ilkka Niemelä. Translating Answer-Set Programs into Bit-Vector Logic. In the Proceedings of the 19th International Conference on Applications of Declarative Programming and Knowledge Management, 105—116. Vienna, Austria, September 2011

  • A paper on LP2NORMAL2 has been submitted.

ASP Competition 2013: Participants\LP2BV-2 (last edited 2013-05-23 22:15:12 by FrancescoCalimeri)