Welcome to CMODELS Home Page

Description

Current version of system Cmodels is 3.85.

Starting version 3.81 of Cmodels, the system supports incremental answer set solving. (One may add constraints to a program on the fly.) The interface for incremental answer ser solving is provided and documented in ctable.h source file.

Description of Cmodels

Cmodels is a system that computes answer sets for either disjunctive logic programs or logic programs containing choice rules. Answer set solver Cmodels uses SAT solvers as a search engine for enumerating models of the logic program -- possible solutions, in case of disjunctive programs SAT solver zChaff is also used for verifying the minimality of found models. The system Cmodels is based on the relation between two semantics: the answer set and the completion semantics for logic programs. For big class of programs called tight, the answer set semantics is equivalent to the completion semantics, so that the answer sets for such a program can be enumerated by a SAT solver. On the other hand for nontight programs [6], and [7] introduced the concept of the loop formulas, and showed that models of completion extended by all the loop formulas of the program are equivalent to the answer sets of the program. Unfortunetly number of loop formulas might be large, therefore computing all of them may become computationally expensive. This led to the adoption of the algorithm that computes loop formulas ''as needed'' for finding answer sets of a program.

Algorithm of Cmodels

Cmodels

General Information about Cmodels

In some cases, this method produces answer sets faster than the algorithms used in the general-purpose answer set solvers such as Smodels (see benchmarks.tar and comparison.ps).

Cmodels is similar to Smodels or GnT in that its input is a grounded logic program that can be generated by the front-end called Lparse, (Lparse --dlp-choice or Lparse --dlp) or Gringo. You can find information on the input language of Lparse in the Lparse user manual.

The input of Cmodels may contain weight constraints, but optimize statements are not allowed. The representation of weight constraints by propositional formulas used in Cmodels is based on [3].

Cmodels was written by Yulia Lierler with the help of other members of Texas Action Group at Austin and Marco Maratea. The program includes some parts of the code written by Patrik Simons for system Smodels. Cmodels also includes the code of SAT solvers Simo, Minisat, and zChaff. Marcello Balduccini adapted the Cmodels code for Windows.

Installing Cmodels

Cmodels Code for Sun/Linux/Windows.

Instructions for Sun/Linux

(path_to_cmodels is the full path to the cmodels directory). You may find more information about the CONFIG file in README. Executing Cmodels with Relsat requires placing the executables of the SAT solvers in the same directory as executable of Cmodels.

Invoking Cmodels

Cmodels is typically invoked as follows:

% lparse (options) program | cmodels (options)

or

% gringo (options) program | cmodels (options)

(program is the name of the file containing the input program).

Both lparse and cmodels can be followed by options. To specify that the input program is disjunctive lparse should be followed by option --dlp-choice or --dlp. In case when option --dlp-choice is used disjunctive and choice rules are allowed in the input of Lparse. When option --dlp is used by Lparse, Cmodels shall be followed by the same option --dlp. Other options of Lparse are described in Section 3 of the Lparse user manual.

The options of Cmodels

   Usage: cmodels [-solver] [number] [--dlp] [-verify <0 or 1>][-numlf ]

-solver
   Use solver to find the solutions. The possible values are -zc (default) for zChaff, -ms for Minisat, -si for Simo, -rs for Relsat.

--dlp
   Specifies to cmodels that input program is disjunctive without choice rules, i.e. Lparse --dlp is used to parse the input program.

number
   Find the given number of models of completion (0 means "compute all models"; 1 is the default).

-verify <0 or 1>
   This flag specify the method for verifying the models of completion, when program is not head cycle free: -verify 0 takes into account structure of the program and splits the verification into verifying the model on subprograms (default); -verify 1 performs verification on the whole program at once using method similar to the one employed in GnT. More information on the last method can be found at [11].

-numlf
in case when program is disjunctive by default only 1 clause unsatisfied by a model from loop formula is added. With this flag you can specify how many clauses you would like to be added.

 

Notes

The official websites for m(z)Chaff, Minisat, Simo, Relsat, Lparse may contain information about newer versions of the systems.

On the linux machines of the CS Department at UT Austin the cmodels directory is /projects/tag/cmodels3/linux . The alias that you need to run Cmodels on these machines is

   alias cmodels /projects/tag/cmodels3/linux/cmodels

If you liked Cmodels then you may be also interested in systems

ASSAT, blackbox, CCalc, DLV, Smodels, and VITAL.

Questions?

Send an e-mail to cmodels-help@cs.utexas.edu.

Related Publications

[1] Yu. Babovich, E. Erdem and V. Lifschitz, Fages' theorem and answer set programming. In Proceedings of the 8th International Workshop on Non-Monotonic Reasoning, 2000.

[2] E. Erdem and V. Lifschitz, Tight logic programs. Submitted for publication.

[3] P. Ferraris and V. Lifschitz, Weight constraints as nested expressions, unpublished draft.

[4] V. Lifschitz, Answer set programming and plan generation. Artificial Intelligence, Vol. 138, 2002.

[5] Yu. Babovich and V. Lifschitz, Computing Answer Sets Using Program Completion, unpublished draft, 2003.

[6] F. Lin and Yu. Zhao, ASSAT: Computing Answer Sets of A Logic Program By SAT Solvers, In Proc. of AAAI-02 .

[7] J. Lee and V. Lifschitz, Loop Formulas for Disjunctive Logic Programs, In Proc. ICLP, 2003.

[8] Yu. Lierler and M. Maratea, Cmodels-2: SAT-based Answer Set Solver Enhanced to Non-tight Programs, In Proc. of LPNMR-7, 2004.

[9] E. Giunchiglia, Yu. Lierler and M. Maratea, Cmodels-2: SAT-Based Answer Set Programming, In Proc. of AAAI , 2004.

[10] Yu. Lierler, Cmodels for Tight Disjunctive Logic Programs, In Proc. of WCLP, 2005.

[11] Yu. Lierler, Disjunctive Answer Set Programming via Satisfiability , In Proc. of Workshop on ASP, 2005.

[12] E. Giunchiglia, Yu. Lierler, M. Maratea Answer Set Programming based on Propositional Satisfiability ,to appear in Journal of Automated Reasoning, 2006.