Watches play a central role in the speed of HaifaCSP. Watches minimize the number of redundant attempts to propagate a constraint. Watches are based on the work done on the Minion constraint solver, which in turn were based on work done by zChaff and Grasp before it.

Only watches may invoke a constraint during constraint propagation. When a watched event occurs then the watch invokes all constraints registered on the event. This scheme reduces the number of propagated constraints.

Currently HaifaCSP support the following types of watches:

  • Value watch: The watched value has been removed from variable’s domain.
    Two watch literals of Signed Clauses are implemented using Value Watches.
  • Modification watch: Any value has been removed from variable’s domain
  • Assignment watch: The variable has been assigned, the domain contains only one element
  • Upper (or lower) bound watch: The maximal (minimal) value of a domain has been deleted.

Conflict analysis

Conflict analysis also plays a critical role in the speed of HaifaCSP. Conflict analysis lets the solver avoid repeating many types of bad decisions by figuring out what is the cause of a conflict. This process generates a conflict constraint, which can be any constraint. Many times HCSP will generate a signed CNF clause such as (x1 ∈ {1,2} ∨ x2 ∈ {3,4}). The EFC constraint solver also generates conflict clauses and refers to them as generalized-nogoods (g-nogoods). HCSP is unique in generating global constraints such as (2*x+3*y-2*z >= 5).


HaifaCSP has an inefficient handling of sets. Set handling takes a considerable amount of time, which can and will be improved by rewriting this part. A big part of the inefficiency comes from the use of std::map, which is neither memory nor cache friendly. The two possible solutions I am contemplating with are:

  1. Immutable sets represented by sorted vectors. This should work since most of the times the sets are only traversed or queried.
  2. B-trees. This might work since it will optimize CPU cache lines, and minimize pointers to children.