[an error occurred while processing this directive]
These tools translate a normal program into a set of clauses such
that any SAT solver can be used to calculate its answer sets. The
software is compatible with the intermediate file format of
and can be used with a modern grounder such as
(see the Potassco
lp2lp2[JN10]. The first tool removes positive conditions from the rules while the second does not.
lp2satmust be called to form the completion of the program in DIMACS format.
The computation of answer sets for
using, e.g., the SAT solver
minisat as the back-end:
$ gringo program.lp | lp2atomic | lp2sat > program.cnf
$ gringo program.lp | lp2lp2 | lp2sat > program.cnf
$ minisat program.cnf model.out
$ cat model.out | interpret -p -d program.cnf
The first two lines illustrate the use of
lp2lp2 for the
translation into CNF. After that the SAT solver can be called and any
satisfying assignments can be mapped back to answer sets using the
interpret. To enable this
contains the required symbolic information as comments. Please refer
to the documentation of your SAT solver to see what command line
arguments/options are needed for printing the satisfying
Tomi Janhunen. Some (In)translatability Results for Normal Logic Programs and Propositional Theories. Journal of Applied Non-Classical Logics, 16(1-2), 35-86, 2006. Special issue on implementing logics.
Tomi Janhunen. Representing Normal Programs with Clauses. In R. L. de Mántaras and L. Saitta, editors, the Proceedings of the 16th European Conference on Artificial Intelligence, pages 358-362, Valencia, Spain, August 2004.
Tomi Janhunen. A Counter-Based Approach to Translating Logic Programs into Set of Clauses. In M. de Vos and A. Provetti, editors, the Proceedings of the 2nd International Workshop on Answer Set Programming, pages 166-180, Messina, Sicily, September 2003. Sun SITE Central Europe (CEUR), vol. 78.
Tomi Janhunen. Translatability and Intranslatability Results for Certain Classes of Logic Programs. In the Report Series of the Laboratory for Theoretical Computer Science, Series A, Research Reports, number A82.
T. Janhunen and I. Niemelä. Compact Translations of Non-Disjunctive Answer Set Programs to Propositional Clauses. In Michael Gelfond's Festschrift, 2010, 111—130. Springer LNCS 6565.[an error occurred while processing this directive]