Smodels: A System for Answer Set Programming

TL;DR

Smodels is a system that implements stable model semantics for normal logic programs, supporting extensions like built-in functions and constraints, enabling applications in planning, model checking, and more.

Contribution

It provides a flexible core engine for answer set programming with extensions, facilitating various complex applications.

Findings

Successfully applied to planning and model checking

Supports extensions like cardinality and weight constraints

Enables building more involved systems on top of the core engine

Abstract

The Smodels system implements the stable model semantics for normal logic programs. It handles a subclass of programs which contain no function symbols and are domain-restricted but supports extensions including built-in functions as well as cardinality and weight constraints. On top of this core engine more involved systems can be built. As an example, we have implemented total and partial stable model computation for disjunctive logic programs. An interesting application method is based on answer set programming, i.e., encoding an application problem as a set of rules so that its solutions are captured by the stable models of the rules. Smodels has been applied to a number of areas including planning, model checking, reachability analysis, product configuration, dynamic constraint satisfaction, and feature interaction.