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 Satisfaction 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.