Description

Current version of system SUP is 0.4.

SUP [1] is a native Answer Set Programming (ASP) solver that can be seen as a combination of computational ideas behind two ASP solvers: Cmodels and Smodels.

Answer set solver Cmodels operates by computing a supported model M of the given logic program P, and then continuing this process, if necessary, in the presence of additional constraints expressed by loop formulas. Computing M is accomplished by forming the completion of P, clausifying it (at this step additional atoms can be introduced) and then invoking a SAT solver.

Solver SUP operates in a similar way, by computing a sequence of supported models of P, but it does not form the completion of P. Instead, SUP applies Minisat (v1.12b) to P itself (with each rule written as a clause), and the "nonclausal constraint" mechanism [2] of Minisat is employed for expressing the supportedness restriction. The new solver can be described as "Cmodels without completion."

Computing a supported model of P without forming the completion formula can be also accomplished by running the Atleast algorithm of Smodels (this idea was suggested by Miroslaw Truszczynski). Computing supported models using Minisat with nonclausal constraints can be thought of as an alternative implementation of Atleast (enhanced by learning). In this sense, SUP combines Smodels and Cmodels algorithms.

• the interface of SAT-solver Minisat (v1.12b) that supports nonclausal constraints [2] in order to (1) implement inferences analogous to Atleast procedure of Smodels and (2) implement learning;
• parts of Cmodels code that supports model verification and backtracking in case if a model of a program is not an answer set.

SUP was implemented by Yulia Lierler: The program modifies the code of Minisat (v1.12b) by Niklas Eén and Niklas Soerensson, and the code of Cmodels.

General Information about SUP

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

The input of SUP may contain choice rules and weight constraints, but optimize statements are not allowed. The representation of weight constraints by propositional formulas used in SUP is analogous to the one used in Cmodels [3].

Installing SUP

• Download SUP and untar the package:
  % gunzip sup.tar.gz
  % tar xf sup.tar
   

• cd to the sup directory and compile the program:
  % cd sup
  % make
  

Invoking SUP

SUP is typically invoked as follows:

% lparse (options) program | sup (options)

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

Both lparse and sup can be followed by options. Options of Lparse are described in Section 3 of the Lparse user manual.

The options of Sup

Usage:

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

-temp
learns and forgets loop formulas (default keeps LF permanently)

-atomreason
learns only an implicant of a loop formula rather than a loop formula (when a model is not an answer set).

Questions?

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

Related Publications

[1] Yuliya Lierler Abstract Answer Set Solvers, In Proc. ICLP, 2008.

[2] Niklas Een and Niklas Soerensson, An Extensible SAT-solver, SAT, 2003.

[3] P. Ferraris and V. Lifschitz, Weight constraints as nested expressions, Theory and Practice of Logic Programming, Vol. 5, 2005.

This material is based upon work supported by the National Science Foundation under Grant IIS-0712113.