
SmodelsThe 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 standalone program together with a suitable frontend. The main frontend is lparse. The current version is smodels2.34. It extends the normal logic programs by adding new special rule types:
Smodels is implemented by Patrik Simons. LparseSmodels works with variablefree programs that are quite cumbersome to generate by hand. Lparse is a frontend that adds variables (and a lot of other stuff) to the accepted language and generates a variablefree 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 lparse1.1.2. Lparse has been implemented by Tommi Syrjänen. DocumentationThe 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. DownloadsBoth smodels and lparse are distributed under the GNU Public Licence.
UsageAssume that the file program contains a logic program. A stable model would typically be computed as follows:
$ lparse  smodels The command smodels help will display the available smodels options and lparse help the lparse options. Other programsPsmodels: 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 1safe Petri nets and employs smodels as its computational engine. Related PublicationsK. 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 1719, 2001. [ps.gz] [pdf]Tommi Syrjänen: Omegarestricted 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. ©SpringerVerlag. 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 3756, 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, LogicBased Artificial Intelligence, pages 491521. 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 NonMonotonic 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 NonMonotonic Reasoning (cs.AI/0003073)}, Breckenridge, Colorado, USA, April 2000. (CoRR: arXiv:cs.AI/0003033) Tomi Janhunen, Ilkka Niemelä, Patrik Simons, and JiaHuai 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 411419, 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 7984, 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 719. 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 475486, Lecture Notes in Computer Science 1853, Geneva, Switzerland, July 2000. © Springer. Heljanko, K.: Model Checking with Finite Complete Prefixes is PSPACEcomplete. In Proceedings of the 11th International Conference on Concurrency Theory (Concur'2000), pages 108122, 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 1Safe Petri Nets. Fundamenta Informaticae, 37(3):247268, 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 24, 1999. SpringerVerlag. 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 1216, 1999. SpringerVerlag. See LNCS Series Homepage. K. Heljanko. Minimizing Finite Complete Prefixes. In Proceedings of the Workshop Concurrency, Specification & Programming 1999 (CS&P' 99), pages 8395, 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. SpringerVerlag. See LNCS Series Homepage. K. Heljanko. Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1Safe Petri Nets. In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), pages 240254, Lecture Notes in Computer Science 1579, SpringerVerlag, 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)
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 30June 1, 1998.
T. Soininen and I. Niemelä. Formalizing Configuration Knowledge Using Rules with Choices . Technical Report TKOB142, 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 wellfounded 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 420429, Dagstuhl, Germany, July 1997. (Test programs) I. Niemelä and P. Simons. Efficient implementation of the wellfounded and stable model semantics. Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming, pages 289303, Bonn, Germany, September 1996. (Long version) (Test programs) I. Niemelä and P. Simons. Efficient implementation of the wellfounded and stable model semantics. Fachbericht 796, Universität KoblenzLandau, 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 6672, Montreal, Canada, August 1995. 