Stable Models

Stable models are one of the most popular semantics for non-stratified programs. The intuition behind the stable model semantics for a ground program $P$ can be seen as follows. Each negative literal $not L$ in $P$ is treated as a special kind of atom called an assumption. To compute the stable model, a guess is made about whether each assumption is true or false, creating an assumption set, $A$. Once an assumption set is given, negative literals do not need to be evaluated as in the well-founded semantics; rather an evaluation treats a negative literal as an atom that succeeds or fails depending on whether it is true or false in $A$.

Example 5.3.1   Consider the simple, non-stratified program

writes_manual(terry)-$\neg$writes_manual(kostis),has_time(terry).

writes_manual(kostis)-$\neg$writes_manual(terry),has_time(kostis).

has_time(terry).

has_time(kostis).

there are two stable models of this program: in one writes_manual(terry) is true, and in another writes_manual(kostis) is true. In the Well-Founded model, neither of these literals is true. The residual program for the above program is

writes_manual(terry)-$\neg$writes_manual(kostis).

writes_manual(kostis)-$\neg$writes_manual(terry).

has_time(terry).

has_time(kostis).

Computing stable models is an intractable problem, meaning that any algorithm to evaluate stable models may have to fall back on generating possible assumption sets, in pathological cases. For a ground program, if it is ensured that residual clauses are produced for all atoms, using the residual program may bring a performance gain since the search space of algorithms to compute stable models will be correspondingly reduced. In fact, by using XSB in conjunction with a Stable Model generator, Smodels [30], an efficient system has been devised for model checking of concurrent systems that is 10-20 times faster than competing systems [28].