HaifaCSP is a Constraints-Satisfaction Problem (CSP) solver.


NEWS: HaifaCSP won two gold medals (free search and parallel search categories), and a silver medal (Open class category) of the 2016 MiniZinc challenge .


HCSP (previously called PCS), solves CSP (Constraint Satisfcation Problems), a subset of pseudo-Boolean optimization problems, and COP (Constraint Optimization Problems).

HCSP supports three constraint languages:

  • XCSP 2.1 a format used at the CSP Solver Competition. (Default format)
  • opb a format used at the pseudo-Boolean solver competition.
    Run with: hcsp.big -F opb my_file.opb
  • FlatZinc a format used by the MiniZinc challenge competition.
    To convert from the MiniZinc format to FlatZinc please put this library under the lib/minizinc/ directory of the MiniZinc distribution. After this you can convert a .mzn file to .fzn simply by running
    mzn2fzn -G my_file.mzn my_data.dzn -o my_file.fzn
    Run with: hcsp.big -F fzn my_file.fzn
  • An internal format resembling a subset of the expression language defined by the C standard. It supports most HCSP constraints and, optionally, objective function optimization.

Since HaifaCSP employs elaborate pre-processing with these formats, it is no longer able to produce machine-checkable proofs and interpolants. HaifaCSP can still produce proofs and interpolants for the problem that results from the pre-processing.