clasp

Answer Set Programming (ASP) provides users with a modeling language designed to solve combinational problems. The clasp utility is an answer set solver for (extended) normal and disjunctive logic programs. It takes advantage of the modeling capacities for ASP while also relying on Boolean constraint solving techniques.

The main clasp algorithm uses conflict-driven nogood learning, and it does not rely on legacy software, such as SAT solvers or other ASP solvers. It has been created to perform answer set solving based on conflict-driven nogood learning.

clasp can be used as an ASP solver (on the aspif or smodels format, as output by gringo), as an SAT solver (on a simpler version of the dimacs/CNF format) or as a PB solver (on the OPB format). It can be used as a C++ library in another program.

The software provides you with multiple reasoning modes and features from Boolean constraint solving, including: enumeration of (projected) solutions, optimization of solutions, cautions and brave reasoning, conflict-driven (or multithreaded) search, dedicated propagation of extended rules or equivalence reasoning and resolution-based preprocessing.

If you are just getting started, you can check the detailed documentation available on the project’s official website, which can help you get everything up and running.