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 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 disadvantages. Another attractive feature of the new system is that it organizes the search process more efficiently than ASSAT, because it does not explore the same part of the search tree more than once.

PS

In Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), pp. 346-350 2004.

@INPROCEEDINGS{bab03, title={Cmodels-2: SAT-based Answer Set Solver Enhanced to Non-tight Programs}, author={ Yuliya Lierler and Marco Maratea}, booktitle={Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR)}, pages={346-350}, url="http://www.cs.utexas.edu/users/ai-lab?bab03", year={2004} }