Smodels

The program smodels is an implementation of the stable model semantics for logic programs. Smodels can be used either as a C++-library that can be called from user programs or as a stand-alone program together with a suitable front-end. The main front-end is lparse.

The current version is smodels-2.32. It extends the normal logic programs by adding new special rule types:

constraint rules
choice rules
weight rules

Smodels is implemented by Patrik Simons.

Lparse

Smodels works with variable-free programs that are quite cumbersome to generate by hand. Lparse is a front-end that adds variables (and a lot of other stuff) to the accepted language and generates a variable-free simple logic program that can be given to smodels. Lparse also implements several other semantics (classical negation, partial stable models) by translating them into normal logic programs.

The current lparse version is lparse-1.0.17 . Lparse is implemented by Tommi Syrjänen

Documentation

The most comprehensive documentation for the smodels system is currently the lparse user's manual (uncompressed) that details the lparse input language and gives also a brief overview on the smodels library API.

The smodels implementation details are discussed in Patrik's Ph.D. thesis Extending and Implementing the Stable Model Semantics.

Downloads

Both smodels and lparse are distributed under the GNU Public Licence.

smodels-2.32 source package
a pre-compiled smodels-2.26 Windows 98 binary
lparse-1.0.17. source package
a pre-compiled lparse-1.0.5 Windows 98 binary
Lparse user's manual (uncompressed ps)

Usage

Assume that the file program contains a logic program. A stable model would typically be computed as follows:

$ lparse | smodels smodels version 2.6. Reading...done Answer: 1 Stable Model: v0 v7 v41 v26 v51 v52 v29 v46 true True Duration: 0.030 Number of choice points: 17 Number of wrong choices: 14 Number of atoms: 65 Number of rules: 66 Number of picked atoms: 796 Number of forced atoms: 47 Number of truth assignments: 4981 Size of searchspace (removed): 42 (0)

The command smodels -help will display the available smodels options and lparse --help the lparse options.

Other programs

Psmodels: a modification of smodels that can be used to compute preferred answer sets under the ordered disjunction semantics.

GnT: an implementation of disjunctive stable models on top of Smodels.

Mcsmodels is a deadlock and reachability checker developed by Keijo Heljanko. It uses finite complete prefixes generated by the PEP tool from 1-safe Petri nets and employs smodels as its computational engine.

Related Publications

K. Heljanko and I. Niemelä. Bounded LTL Model Checking with Stable Models. Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning, Vienna, Austria, September 17-19, 2001. [ps.gz] [pdf]

Tommi Syrjänen: Omega-restricted Logic Programs In Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning LPNMR 2001, Vienna, Austria, Volume 2173 of Lecture Notes in Artificial Intelligence, Springer, Berlin. ©Springer-Verlag.

K. Heljanko and I. Niemelä. Answer Set Programming and Bounded Model Checking. Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge. Stanford, USA, March 2001. [ps.gz]

T. Soininen, I. Niemelä, J. Tiihonen, and R. Sulonen. Representing Configuration Knowledge With Weight Constraint Rules. Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge. Stanford, USA, March 2001. [ps.gz]

Esparza, J. and Heljanko, K.: Implementing LTL Model Checking with Net Unfoldings. Research Report A68, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland, March 2001, 29p.

Esparza, J. and Heljanko, K.: Implementing LTL Model Checking with Net Unfoldings. In Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN'2001), pages 37-56, Lecture Notes in Computer Science 2057, Toronto, Canada, May 2001. © Springer.

Ilkka Niemelä and Patrik Simons. Extending the Smodels System with Cardinality and Weight Constraints. This is an introduction to the extended rule language of Smodels 2.x. To appear in Jack Minker, editor, Logic-Based Artificial Intelligence, pages 491-521. Kluwer Academic Publishers, 2000.

Hietalahti, M., Massacci, F., and Niemelä, I. DES: a challenge problem for nonmonotonic reasoning systems. In Proceedings of the 8th International Workshop on Non-Monotonic Reasoning, Breckenridge, Colorado, USA. (CoRR: arXiv:cs.AI/0003039) (Test cases)

I. Niemelä, P. Simons, and T. Syrjänen. Smodels: a system for answer set programming. In Proceedings of the 8th International Workshop on Non-Monotonic Reasoning (cs.AI/0003073)}, Breckenridge, Colorado, USA, April 2000. (CoRR: arXiv:cs.AI/0003033)

Tomi Janhunen, Ilkka Niemelä, Patrik Simons, and Jia-Huai You. Unfolding partiality and disjunctions in stable model semantics. In A.G. Cohn, F. Guinchiglia, and B. Selman, editors, Proceedings of the Seventh International Conference on Principles of Knowledge Representation and Reasoning, pages 411-419, Breckenridge, Colorado, USA, April 2000. Morgan Kaufmann Publishers.

T. Soininen, I. Niemelä, J. Tiihonen, and R. Sulonen. Unified configuration knowledge representation using weight constraint rules. In Workshop Notes of the ECAI'2000 Configuration Workshop, pages 79--84, Berlin, Germany, August 2000. [ps.gz]

K. Heljanko and I. Niemelä. Petri net analysis and nonmonotonic reasoning. In Leksa Notes in Computer Science, Festschrift in Honour of Professor Leo Ojala, pages 7-19. Helsinki University of Technology, Laboratory for Theoretical Computer Science, 2000. [ps.gz]

Esparza, J. and Heljanko, K.: A New Unfolding Approach to LTL Model Checking. Research Report A60, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland, April 2000, 32p.

Esparza, J. and Heljanko, K.: A New Unfolding Approach to LTL Model Checking. In Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP'2000), pages 475-486, Lecture Notes in Computer Science 1853, Geneva, Switzerland, July 2000. © Springer.

Heljanko, K.: Model Checking with Finite Complete Prefixes is PSPACE-complete. In Proceedings of the 11th International Conference on Concurrency Theory (Concur'2000), pages 108-122, Lecture Notes in Computer Science 1877, State College, Pennsylvania, USA, August 2000. © Springer.

P. Simons. Extending and Implementing the Stable Model Semantics. Doctoral dissertation. Research Report 58, Helsinki University of Technology, Helsinki, Finland, April 2000.

Heljanko, K.: Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets. Fundamenta Informaticae, 37(3):247-268, IOS Press, 1999.

Heljanko, K.: Deadlock and Reachability Checking with Finite Complete Prefixes. Research Report A56, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland, December 1999, 70p. (See also experiments).

I. Niemelä, P. Simons and T. Soininen. Stable Model Semantics of Weight Constraint Rules. In Proceedings of the Fifth International Conference on Logic Programming and Nonmonotonic Reasoning, El Paso, Texas, USA, December 2-4, 1999. Springer-Verlag. See LNCS Series Homepage.

T. Soininen, E. Gelle and I. Niemelä. A Fixpoint Definition of Dynamic Constraint Satisfaction. In Proceedings of the Fifth International Conference on Principles and Practice of Constraint Programming, Alexandria, Virginia, USA, October 12-16, 1999. Springer-Verlag. See LNCS Series Homepage.

K. Heljanko. Minimizing Finite Complete Prefixes. In Proceedings of the Workshop Concurrency, Specification & Programming 1999 (CS&P;' 99), pages 83-95, Warsaw, Poland, September 1999. Full version.

P. Simons. Extending the Stable Model Semantics with More Expressive Rules. This is an extended version of a paper that will appear in the Proceedings of the 5th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR'99, El Paso, Texas, USA, 1999. cs.LO/9908004

T. Soininen and I. Niemelä. Developing a declarative rule language for applications in product configuration. In Proceedings of the First International Workshop on Practical Aspects of Declarative Languages, San Antonio, Texas, May 1999. Springer-Verlag. See LNCS Series Homepage.

K. Heljanko. Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets. In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), pages 240-254, Lecture Notes in Computer Science 1579, Springer-Verlag, Berlin, March 1999. See LNCS Series Homepage. (See also experiments).

T. Syrjänen, Implementation of local grounding for logic programs with stable model semantics Technical Report B18, Digital Systems Laboratory, Helsinki University of Technology, October 1998.

I. Niemelä. Logic Programs with Stable Model Semantics as a Constraint Programming Paradigm. (Test cases)
This is an extended version of the paper presented at the Workshop on Computational Aspects of Nonmonotonic Reasoning, Trento, Italy, May 30-June 1, 1998.

I. Niemelä. Logic Programs with Stable Model Semantics as a Constraint Programming Paradigm. In Proceedings of the Workshop on Computational Aspects of Nonmonotonic Reasoning, Trento, Italy, May 30-June 1, 1998.
Research Report A52, Digital Systems Laboratory, Helsinki University of Technology. (Test cases)

T. Soininen and I. Niemelä. Formalizing Configuration Knowledge Using Rules with Choices . Technical Report TKO-B142, Laboratory of Information Processing Science, Helsinki University of Technology, 1998. Presented at the Workshop on Formal Aspects and Applications of Nonmonotonic Reasoning, Trento, Italy, May 31, 1998.

P. Simons. Towards constraint satisfaction through logic programs and the stable model semantics. Research Report 47, Helsinki University of Technology, Helsinki, Finland, August 1997.

I. Niemelä and P. Simons. Smodels - an implementation of the stable model and well-founded semantics for normal logic programs. In Proceedings of the 4th International Conference on Logic Programming and Nonmonotonic Reasoning, volume 1265 of Lecture Notes in Artificial Intelligence, pages 420-429, Dagstuhl, Germany, July 1997. (Test programs)

I. Niemelä and P. Simons. Efficient implementation of the well-founded and stable model semantics. Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming, pages 289-303, Bonn, Germany, September 1996. (Long version) (Test programs)

I. Niemelä and P. Simons. Efficient implementation of the well-founded and stable model semantics. Fachbericht 7-96, Universität Koblenz-Landau, 1996.

P. Simons. Efficient implementation of the stable model semantics for normal logic programs. Research Report 35, Helsinki University of Technology, September 1995.

I. Niemelä and P. Simons. Evaluating an algorithm for default reasoning. Working Notes of the IJCAI'95 Workshop on Applications and Implementations of Nonmonotonic Reasoning Systems, pages 66-72, Montreal, Canada, August 1995.

Patrik Simons

Last modified: Mon Sep 11 10:08:03 EEST 2000