Characterizing and computing stable models of logic programs: The non-stratified case

TL;DR

This paper explores the conditions under which logic programs have stable models, introduces the Extended Dependency Graph for better analysis, and reformulates the existence problem as a graph coloring task.

Contribution

It characterizes cyclic negative dependencies in logic programs, introduces the Extended Dependency Graph, and links stable model existence to graph coloring.

Findings

Extended Dependency Graph effectively captures program features affecting stable models

Stable model existence can be determined through graph coloring of EDG

Provides new syntactic criteria for program consistency

Abstract

Stable Logic Programming (SLP) is an emergent, alternative style of logic programming: each solution to a problem is represented by a stable model of a deductive database/function-free logic program encoding the problem itself. Several implementations now exist for stable logic programming, and their performance is rapidly improving. To make SLP generally applicable, it should be possible to check for consistency (i.e., existence of stable models) of the input program before attempting to answer queries. In the literature, only rather strong sufficient conditions have been proposed for consistency, e.g., stratification. This paper extends these results in several directions. First, the syntactic features of programs, viz. cyclic negative dependencies, affecting the existence of stable models are characterized, and their relevance is discussed. Next, a new graph representation of logic programs, the Extended Dependency Graph (EDG), is introduced, which conveys enough information for reasoning about stable models (while the traditional Dependency Graph does not). Finally, we show that the problem of the existence of stable models can be reformulated in terms of coloring of the EDG.