welcome: please sign in
location: Diff for "Participants\LP2SAT"
Differences between revisions 1 and 2
⇤ ← Revision 1 as of 2013-05-23 22:24:08 →
Size: 1656
Editor: FrancescoCalimeri
Comment:
← Revision 2 as of 2013-05-23 22:24:19 → ⇥
Size: 1124
Editor: FrancescoCalimeri
Comment:
Deletions are marked like this. Additions are marked like this.
Line 30: Line 30:
== bibtex entry ==
@inproceedings{JN11:scmcs,
    author = {Tomi Janhunen and Ilkka Niemel{\"a}},
    booktitle = {Proceedings of the Symposium on Constructive Mathematics and
                 Computer Science in Honour of Michael Gelfonds 65th Anniversary},
    pages = {111--130},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Compact Translations of Non-Disjunctive Answer Set Programs to
             Propositional Clauses},
    volume = {6565},
    year = {2011},
}

LP2SAT

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 SAT clauses using LP2LP2 and LP2SAT, and finally, the SAT clauses are solved by PRECOSAT.

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
  • LP2LP2 1.18
  • LP2SAT 1.15 -n
  • PRECOSAT 570

The input language is Gringo 3.

References

  • Participant URL.

  • Tomi Janhunen and Ilkka Niemelä, Compact Translations of Non-Disjunctive Answer Set Programs to Propositional Clauses, In Gelfond Festschrift, 111—130, 2010. Springer LNCS 6565.

  • A paper on LP2NORMAL2 has been submitted.

ASP Competition 2013: Participants\LP2SAT (last edited 2013-05-23 22:24:19 by FrancescoCalimeri)