Cmodels-2: SAT-based Answer Set Solver Enhanced to Non-tight Programs

Answer set programming is a new programming paradigm proposed in [1] and [2], and based on the answer set semantics of Prolog [3]. It is well known that an answer set for a logic program is also a model of the program’s completion [4]. The converse is true when the logic program is “tight” [6, 5]. Lin and Zhao [7] 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 ASSAT1 has some disadvantages: it can work only with basic rules, and it can compute only one answer set. Answer set solver CMODELS-12 [12] 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-21, that is able to fix ASSAT’s 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. In the rest of the paper we omit number 2 in the name of the system