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.


Compute Systems Invocation Version(s)
Red Hat Linux (64-bit) % /util/bin/lparse 1.1.2 (default)
Red Hat Linux (64-bit) % /util/bin/smodels 2.34 (default)


  1. Example:
    % puzzle1.lp  -- Knights and Knaves
    % author: Tommi Syrjnen 
    % Raymond Smullyan presents the following puzzle in his book `Forever
    % Undecided'.
    % The Island of Knights and Knaves has two types of inhabitants:
    % knights, who always tell the truth, and knaves, who always lie.
    % One day, three inhabitants (A, B, and C) of the island met a foreign
    % tourist and gave the following information about themselves:
    % 1. A said that B and C are both knights.
    % 2. B said that A is a knave and C is a knight.
    % What types are A, B, and C?
    % lparse /util/lparse/examples/puzzle/puzzle1.lp | smodels
    smodels version 2.34. Reading...done
    Answer: 1
    Stable Model: knave(a) knave(b) knave(c) person(c) person(b) person(a) 
    Duration: 0.000
    Number of choice points: 0
    Number of wrong choices: 0
    Number of atoms: 20
    Number of rules: 28
    Number of picked atoms: 1
    Number of forced atoms: 1
    Number of truth assignments: 23
    Size of searchspace (removed): 0 (0)


  1. Stuart Shapiro, researcher.


  1. http://www.tcs.hut.fi/Software/smodels/