|
⇤ ← Revision 1 as of 2013-05-23 22:23:24
Size: 1124
Comment:
|
← Revision 2 as of 2013-05-23 22:24:29 ⇥
Size: 1134
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 3: | Line 3: |
| = LP2SAT = | = LP2SAT-mt = |
| Line 12: | Line 12: |
| 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. | 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 PLINGELING. |
| Line 16: | Line 16: |
| * GRINGO 3.0.4 --shift, | * GRINGO 3.0.4 --shift |
| Line 21: | Line 21: |
| * PRECOSAT 570 | * PLINGELING al6 -t 6 |
| Line 28: | Line 28: |
| * A paper on LP2NORMAL2 has been submitted. |
* A paper on LP2NORMAL2 has been submitted. |
LP2SAT-mt
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 PLINGELING.
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
- PLINGELING al6 -t 6
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.