lp2sat
This software has been designed to be used with the front-end
lparse of the smodels system.
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.
lp2sat is used as follows in order to compute
stable models for program.lp using, e.g.,
minisat as the back-end:
lparse program.lp > program.smlp2atomic program.sm | lp2sat > program.cnf minisat program.cnf model.out
The first translator called lp2atomic removes
positive body atoms from the program by introducing new atoms.
The second translator effectively produces the Clark's completion
for a normal program.
Linux binaries: lp2atomic (version 1.12), lp2sat (version 1.11)
Benchmark instances: