Minicsp is a clause learning CSP solver.


Minicsp is a clause learning CSP solver. Briefly, it combines clause learning, as it is used in SAT solvers, with the ability to use global constraints. In terms of modeling, it contains implementations of several constraints, either by providing a propagator or a decomposition. A full list of supported constraints is in the files core/cons.hpp and core/setcons.hpp in the source distribution.

Minicsp can be used as a library or as a black box solver. It can read instances in flatzinc or XCSP.

Its implementation is based on MiniSat.


The minicsp source is hosted in a mercurial repository at bitbucket. You can download the tarball of version 1.0. Note that it requires boost, and relatively recent versions of flex and bison (for the flatzinc frontend) and libxml (for the XCSP frontend) to compile. If you do not have access to these, you can download a complete tarball that includes the subset of boost and necessary to compile minicsp and the files produced by flex and bison (but not libxml).


George Katsirelos