Cmodels

• 1) simplifies the given program,
• 2) verifies that the simplified program is tight,
• 3) verifies that the simplified program is head-cycle-free,
• 4) forms its completion,
• 5) converts the completion to clausal form,
• 6) calls a SAT solver to find the models of the completion,
• 7) if there is no such a model, returns with no answer sets, otherwise
• 8)
  a) if program is tight, returns a model as an answer set. [2, 5, 10]
  b) if program is not tight verifies if the model is indeed an answer set (if program is not head-cycle-free SAT solver zChaff is invoked for this verification).
• 9) if the model is an answer set, returns an answer set. When more than one answer sets needed:
  a) in case of Relsat Cmodels adds negation of a current model to the completion and goes back to step 5.
  b) in case of Simo or zChaff Cmodels adds negation of a current model to the set of clauses and makes the solver to proceed with its computation. Once the SAT solver returns a model Cmodels goes back to step 6.
• 10) if the model is not an answer set, Cmodels finds loop formulas unsatisfied by the current model and
  a) in case of Relsat Cmodels adds the loop formula to the completion and goes back to step 5
  b) in case of Simo or zChaff Cmodels finds one unsatisfied clause inferred from one of the loop formulas. Note that this clause may also be the loop formula itself. It passes this clause back to the SAT solver and makes SAT solver to proceed with the computation. SAT solver continues the computation and returns a new model to Cmodels. Cmodels goes back to step 6.

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

• Download Cmodels and untar the package:
  % gunzip cmodels-3.tar.gz
  % tar xf cmodels-3.tar
   
• cd to the cmodels directory and compile the program (gcc version 4.6.3 was used last to compile):
  % cd cmodels
  % make
   
• Create the alias
  alias cmodels   path_to_cmodels/cmodels   path_to_cmodels/CONFIG

(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.

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.