minicsp

Minicsp is a clause learning CSP solver.

Features

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.

Downloads

The minicsp source is hosted in a git repository at github. 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).

References

Generalized Nogoods in CSPs. George Katsirelos and Fahiem Bacchus, The twentieth national conference on artificial intelligence -- AAAI-05.
Nogood Processing in CSPs, George Katsirelos, PhD Thesis, University of Toronto, 2008.

George Katsirelos