SAT-based Answer Set Programming: System Cmodels
Answer set solver Cmodels is a system that computes answer sets for
disjunctive logic programs. Cmodels uses a SAT solver as a search engine for
enumerating models of the logic program -- possible solutions, in case of
disjunctive programs SAT solver zChaff is also used for verifying the
minimality of found models. The system Cmodels is based on the relation
between two semantics: the answer set and the completion semantics for
logic programs. Cmodels operates by computing a model of completion of the
given logic program, and then continuing this process, if necessary, in the
presence of additional constraints expressed by loop formulas.