CMODELS [1, 2] is an answer set programming [3] system that uses the same frontend LPARSE as answer set solver SMODELS (http://www.tcs.hut.fi/Software/smodels/). CMODELS main computational characteristics is that it computes answer sets using a SAT solver for search.

The use of SAT solvers for generating answer sets is based on the fact that for logic programs satisfying syntactic condition, tightness, the answer set semantics is equivalent to the Clark’s completion semantics. In addition, [4] introduced concept of a loop formula, and demonstrated that the answer sets of a logic program are exactly the models of its completion that satisfy the loop formulas of all loops. These findings allowed to extend the applicability of SAT-based answer set solving to the case of nontight programs.