ECAI 2004 Conference Paper

[full paper]

Representing Normal Programs with Clauses

Tomi Janhunen

We present a new method for transforming normal logic programs into sets of clauses. This transformation is based on a novel characterization of stable models in terms of level numberings and it uses atomic normal programs, which are free of positive body atoms, as an intermediary representation. The corresponding translation function has a unique combination of properties: (i) a bijective relationship is established between stable models and classical models, (ii) the models coincide up to the set of atoms At(P) appearing in a program P, and (iii) the length of the translation as well as the translation time are of order len(P)xlog2|At(P)| where len(P) is the length of the program P. Our preliminary experiments with an implementation of the transformation, translators called lp2atomic and lp2sat, and SAT solvers such as chaff and relsat suggest that our approach is competitive when the task is to compute not just one but all stable models for a normal program given as input.

Keywords: normal logic program, translation, SAT solver

Citation: Tomi Janhunen: Representing Normal Programs with Clauses. In R.López de Mántaras and L.Saitta (eds.): ECAI2004, Proceedings of the 16th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2004, pp.358-362.