Software and benchmarks

  • Please visit the Haifa solvers’ suite for updated information on our solvers HaifaSAT, HaifaCSP, HMUC, HHLMUC, HSMTMUC and the benchmarking platform HBench.
  • EduSAT: a SAT solver for educational purposes.
  • The Regression Verification Tool (RVT) – proving the equivalence of programs.
  • pv – program visualizer. Builds an automata that represents a program’s behavior, or traces that lead to an error.
  • TVS: A translation validation tool from Simulink to C.

Benchmarks: difficult benchmarks in CNF, OPB, SMT2, WCNF, MOD (cplex) and MZN (miniZinc) formats, resulting from university scheduling (time-tabling) problems, are available here.