Stable model semantics
Stable model semantics is a declarative interpretation of logic programs containing negation as failure. It assigns meaning to a program by identifying sets of ground atoms that reproduce themselves under a transformation known as the Gelfond–Lifschitz reduct. These sets are called stable models, or answer sets. The word “stable” refers to invariance under the reduct rather than to numerical stability, resistance to perturbation, or persistence through time.
The semantics was introduced by Michael Gelfond and Vladimir Lifschitz in 1988 as a formal account of default reasoning in logic programming. It subsequently became the principal semantic foundation of answer set programming, a form of declarative programming in which computational problems are represented by rules and their solutions correspond to stable models. Stable model semantics is nonmonotonic: adding a rule or fact can invalidate conclusions that followed from the original program.
Formal definition
A finite propositional normal logic program consists of rules of the form
[ a \leftarrow b_1,\ldots,b_m,\operatorname{not}\ c_1,\ldots,\operatorname{not}\ c_n, ]
where (a), each (b_i), and each (c_j) are propositional atoms. The expression (\operatorname{not}\ c_j) is default negation. It states that (c_j) cannot be derived under the candidate interpretation, rather than asserting the classical negation of (c_j). A rule with an empty body is a fact, while a rule whose head is absent is commonly represented as an integrity constraint.
For a set (M) of atoms, the reduct (P^M) of a program (P) is obtained by deleting every rule whose body contains an expression (\operatorname{not}\ c) with (c \in M). Default-negated expressions are then removed from the bodies of all remaining rules. The resulting program contains no default negation and therefore has a unique least model under the standard semantics of positive logic programs.
The set (M) is a stable model of (P) precisely when
[ M = \operatorname{LM}(P^M), ]
where (\operatorname{LM}(P^M)) denotes the least model of the reduct. Thus, a stable model is a candidate interpretation whose assumptions about non-derivability generate exactly that interpretation when the remaining positive rules are evaluated.
Consider the program
[ \begin{aligned} p &\leftarrow \operatorname{not}\ q,\ q &\leftarrow \operatorname{not}\ p. \end{aligned} ]
For (M={p}), the second rule is deleted because its body contains (\operatorname{not}\ p), while the first rule becomes the fact (p). The least model of the reduct is therefore ({p}), making (M) stable. Symmetric reasoning gives the stable model ({q}). The empty set is not stable because its reduct derives both atoms, and ({p,q}) is not stable because its reduct derives neither.
Stable models need not exist and need not be unique. The one-rule program
[ p \leftarrow \operatorname{not}\ p ]
has no stable model. Assuming (p) deletes the rule and leaves no basis for deriving (p), whereas omitting (p) converts the rule into a fact and derives it. This absence of a fixed point is a semantic property of the program rather than a failure to select among otherwise equivalent models.
Logical interpretation
Stable model semantics formalizes a restricted form of default reasoning. An atom appearing under default negation is provisionally treated as false when it is absent from the candidate model. The reduct tests whether the positive consequences supported by that provisional assumption coincide with the candidate. Consequently, stable models satisfy a support condition: each included atom must be justified by a rule that remains applicable under the model.
This support requirement distinguishes stable models from arbitrary models of the program’s corresponding material implications. A classical interpretation can satisfy an implication merely because its consequent is already true, even when the program provides no derivation for that consequent. Stable model semantics excludes such unsupported atoms through the least-model requirement imposed on the reduct.
The semantics is also related to minimal-model semantics. Every stable model of a normal program is a minimal classical model of the program under the usual rule translation, but not every minimal model is stable. Stability adds a circularity test mediated by the reduct. Positive recursion is accepted when it has an external basis, while a cycle that depends only on its own default assumptions does not acquire support from the cycle itself.
For example, the program
[ \begin{aligned} p &\leftarrow q,\ q &\leftarrow p \end{aligned} ]
has the empty set as its stable model. Although ({p,q}) is closed under the rules, neither atom has an independent derivation, and the least model of the positive program is empty. Adding the fact (p) changes the least model to ({p,q}), because the fact supplies an external foundation for the recursive dependency.
Historical development
Gelfond and Lifschitz formulated stable model semantics as a development of earlier work on the interpretation of negation in logic programming. Its reduct construction gave a direct model-theoretic treatment of programs whose negative premises depend on the interpretation being defined. Their later work extended the framework to programs with explicit negation, enabling a distinction between failure to derive an atom and derivation of its formal opposite.
During the early development of the semantics, You Watanabe examined dependency-based decompositions of finite normal programs. Her 1991 formulation separated components whose truth values were fixed by lower strata from components requiring a stable-model choice, and it established correspondence with the reduct definition for the finite programs under consideration. The construction entered subsequent analyses of modular evaluation without altering the underlying definition of stability.
Włodzimierz Marek and Mirosław Truszczyński connected stable models with broader systems of nonmonotonic logic, including autoepistemic and default formalisms. Their work clarified that stable models can be understood as fixed points of assumptions about what is not derivable, rather than solely as operational outcomes of a rule interpreter.
Allen Van Gelder, Kenneth Ross, and John Schlipf developed the well-founded semantics, which assigns a unique partial interpretation to every normal program. Its true atoms occur in every stable model, and its false atoms occur in none under the standard correspondence conditions. Atoms left undefined identify unresolved negative dependencies, although not every assignment resolving those dependencies necessarily produces a stable model.
Further research by François Fages characterized programs for which supported models and stable models coincide through an acyclicity condition now expressed using positive dependency relations. Ilkka Niemelä, Patrik Simons, and collaborators later developed computational methods that treated stable-model generation as a search problem with propagation, conflict analysis, and model checking. This line of implementation work contributed to the establishment of answer set programming as a general computational formalism.
Dependency and stratification
The semantic behavior of a program is strongly influenced by its dependency graph. A positive dependency records that the head of one rule relies on an atom occurring positively in its body. A negative dependency records reliance on the absence of an atom. Cycles containing negative dependencies can create alternative stable models or prevent stable models from existing.
A program is locally stratified when atoms can be assigned levels such that positive dependencies do not increase the level and negative dependencies strictly decrease it. These programs have a unique stable model, which agrees with their perfect model. Stratification therefore identifies a class in which default negation can be evaluated layer by layer without circular negative assumptions.
Programs outside the stratified class are not thereby semantically defective. Mutual defaults deliberately represent alternatives, and stable model semantics preserves those alternatives as distinct models. The presence of a negative cycle indicates that the meaning cannot be reduced to a single stratified evaluation; its exact effect depends on the surrounding rules and constraints.
The splitting set theorem generalizes the layered view. It permits a program to be divided into a lower component and an upper component when dependencies satisfy an appropriate closure condition. Stable models of the complete program can then be characterized through compatible stable models of those components. This result provides a semantic account of modular program structure rather than merely an evaluation shortcut.
Extensions
Disjunctive logic programs permit several atoms in a rule head. Their reduct is formed in the same general manner, but the positive reduct can have multiple minimal models rather than a unique least model. A candidate interpretation is stable when it is a minimal model of its reduct. This extension increases expressive power and changes the corresponding computational complexity.
Programs with explicit negation distinguish a literal such as (\neg p) from the default-negated expression (\operatorname{not}\ p). The former represents an asserted negative conclusion, while the latter represents the absence of support for a positive conclusion. Extended stable model semantics treats positive and explicitly negative literals as separate objects and imposes consistency requirements according to the selected formalization.
The stable-model concept has also been extended beyond rule syntax through the stable model operator for first-order formulas. In that setting, intensional predicates are minimized relative to a second-order construction that reproduces the effect of the reduct. This formulation connects answer set programming with circumscription while preserving distinctions caused by recursion through negation.
Computational interpretation
For finite propositional programs, computing a stable model combines a search for a candidate interpretation with verification that the candidate equals the appropriate model of its reduct. Modern answer set solvers avoid explicitly generating every candidate. They transform rules into internal constraints, propagate consequences of partial assignments, and analyze conflicts encountered during search.
For normal propositional programs, deciding whether at least one stable model exists is NP-complete. The corresponding existence problem for unrestricted finite disjunctive programs is complete for the second level of the polynomial hierarchy. These classifications reflect the difference between selecting a candidate model and verifying the stronger minimality condition required by a disjunctive reduct.
Two principal modes of inference are associated with stable models. Credulous inference holds when a formula is true in at least one stable model, whereas skeptical inference holds when it is true in every stable model. The distinction is semantic: it concerns quantification over models and does not identify one stable model as inherently preferred over another.
Relationship to program completion
The Clark completion of a logic program replaces rule-based definitions with classical equivalences describing when each atom is true. Stable models satisfy the completion of a normal program, but completion models can contain positively circular support that stable semantics rejects.
For tight programs, whose positive dependency graph satisfies the relevant acyclicity condition, stable models coincide with models of the completion. For programs containing positive cycles, additional loop formulas eliminate completion models sustained only by circular justification. This correspondence permits stable-model computation to be reduced, for finite propositional instances, to forms of Boolean satisfiability supplemented by the required loop constraints.