|
⇤ ← Revision 1 as of 2013-05-23 22:11:39
Size: 1504
Comment:
|
Size: 1509
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 16: | Line 16: |
| * GRINGO 3.0.4 --shift * SMODELS 2.34 -internal -nolookahead * LP2NORMAL2 1.1 -wp -wt -wh -wn -wy -cs * LP2BV 1.10 -f * BOOLECTOR 1.5.118 --smt2 -m |
* GRINGO 3.0.4 --shift * SMODELS 2.34 -internal -nolookahead * LP2NORMAL2 1.1 -wp -wt -wh -wn -wy -cs * LP2BV 1.10 -f * BOOLECTOR 1.5.118 --smt2 -m |
LP2BV-1
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 BOOLECTOR.
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
- BOOLECTOR 1.5.118 --smt2 -m
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.
bibtex entry
@inproceedings{DBLP:journals/corr/abs-1108-5837,
- author = {Mai Nguyen and
- Tomi Janhunen and Ilkka Niemel{\"a}},
}