Answer set programming is a new programming paradigm proposed based on the answer set semantics of Prolog. It is well known that an answer set for a logic program is also a model of the program's completion. The converse is true when the logic program is "tight". Lin and Zhao showed that for non-tight programs the models of completion which do not correspond to answer sets can be eliminated by adding to the completion what they called "loop formulas". Nevertheless, their solver ASSAT 1 has some disadvantages: it can work only with basic rules, and it can compute only one answer set. Answer set solver CMODELS-1 is a system that computes answer sets for logic programs that are tight or can be transformed into tight programs, and does not suffer from these limitations. We are going to present a new system CMODELS-2 , that is able to fix ASSAT's disadvantages. Another attractive feature of the new system is that it organizes the search process more efficiently then ASSAT, because it does not explore the same part of the search tree more than once. In the rest of the paper we will omit number 2 in the name of the system.

PDF

In 2nd International Workshop on Answer Set Programming 2003.

@inproceedings{lierler:asp2003, title={Computing Answer Sets of a Logic Program via Enumeration of SAT Certificates}, author={Yuliya Lierler and Marco Maratea}, booktitle={2nd International Workshop on Answer Set Programming}, url="http://www.cs.utexas.edu/users/ai-lab?lierler:asp2003", year={2003} }