#acl EditorsGroup:read,write,delete,revert,admin All:read

= LP2SOLRED-mt =

== Team ==
 * Tomi Janhunen (Aalto University) 
 * Guohua Liu (Aalto University)
 * Jori Bomanson (Aalto University) 
 * Siert Wieringa (Aalto University)
 * Keijo Heljanko (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 GLUCORED.

== 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
 * GLUCORED 2.1 

The input language is Gringo 3.
  
== References ==
 * Participant [[http://users.ics.aalto.fi/swiering/solver_reducer|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.
 * Siert Wieringa and Keijo Heljanko, ''Concurrent Clause Strengthening'', 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), accepted for publication.
 * A paper on LP2NORMAL2 has been submitted.