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.

http://www.cs.utexas.edu/users/tag/cmodels/