Smodels_cc ("Smodels with conflict clauses") is a modified version of the Answer Set Programming tool Smodels. Smodels_cc uses "conflict clauses" (an idea taken from the area of Boolean satisfiability search) to prune the search space, thereby obtaining improved runtime performance.

Smodels_cc is described in the paper "Answer Set Programming with Clause Learning", by Jeffrey Ward and John S. Schlipf, which appeared in Logic Programming and Nonmonotonic Reasoning, 7th International Conference (LPNMR 2004), Vladimir Lifschitz and Ilkka Niemela, editors. A more detailed treatment is given by my PhD dissertation:

The test data that was used in the dissertation is available on request.

The latest version of Smodels_cc is provided here as a gzipped tar file:

Version 1.08 supports computing multiple models of a single logic program. It also removes "deprecated" headers from the source code and instead uses C++ namespaces, so it should be compatible with current compilers.

Smodels_cc does not accept Smodels' "weight rules" or "optimize rules" as input.

Like Smodels, Smodels_cc uses Lparse as a front-end to parse a logic program.

Smodels_cc usually performs better if lookaheads are turned off, in which case it uses a search heuristic that is based on the conflict clauses. So, if you want to run Smodels_cc on a logic program called foo.lp, you might type

./lparse foo.lp | ./smodels -nolookahead