On Tight Logic Programs and yet Another Translation from Normal Logic Programs to Propositional Logic

Abstract

Fages showed that if a program is tight, then every propositional model of its completion is also its stable model. Recently, Babovich, Erdem, and Lifschitz generalized Fages' result, and showed that this is also true if the program is tight on the given model of the completion. As it turned out, this is quite a general result. Among the commonly known benchmark domains, only Niemelii's normal logic program encoding of the Hamiltonian Circuit (HC) problem does not have this property. In this paper, we propose a new normal logic program for solving the HC problem, and show that the program is tight on every model of its completion. Experimental results showed that for many graphs, this new encoding improves the performance of both SMODELS and ASSAT(Chaff2), especially of the latter system which is based on the SAT solver Chaff2. We also propose a notion of inherently tight logic programs and show that for any program, it is inherently tight iff all its completion models are stable models. We then propose a polynomial transformation from a logic programs to one that is inherently tight, thus providing a reduction of stable model semantics to program completion semantics and SAT.