Author: HaifaCSP, or HCSP for short, has been written by Michael Veksler
        as part of a PhD research.
        
Affiliation: Technion - Israel Institute of Technology,
             Industrial Engineering and Management.

Solver description:

HCSP (previously named PCS) has a clean, from-scratch, C++ implementation.

The solving algorithm is derived from well known SAT solving algorithms, which
were extended to CSP. Like in most SAT solvers, variable ordering, value
ordering and backtracking are affected by conflict analysis. In HCSP, conflict
analysis is performed directly on non-clausal constraints.

Consider for example the following unsolvable problem:
  c1:   a XOR b XOR c XOR d == false;
  c2:   a XOR b == true;
  c3:   c == d;

Assume that after several decisions a conflict is encountered, and is analyzed.
The conflict analysis algorithm The Combine rule, analogous to clause-Resolve,
on pairs of constraints as follows:

Constraints: 
     c1:      a XOR b XOR c XOR d == false;
     c3:      c == d;
Combine consequent:
     temp1:   a XOR b == false;

Constraints of the second application of Combine:
     temp1:   a XOR b == false;
     c2:      a XOR b == true
Second Combine consequent:
     false == true;

More rules can be found at [2]

The fact that the problem is unsolvable has been detected before the first
backtrack was applied, in contrast to clause-based learning which requires an
exponential number of Resolution operations (exponential in the number of
variables). 

HCSP supports combination rules for many pairs of constraints types, derived
from a generic Combine, but all. It is practically impossible to implement
combination rules for all possible pairs of constraints, since every pair
requires to derive a specific rule from Combine and to implement it. When an
unsupported pair is encountered, HCSP falls-back to signed-clause explanation
resolution [1].


The variable ordering of HCSP.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Similar to VSIDS, for each variable HCSP maintains a weight which is incremented
every time it participates in conflict-analysis. After every backtrack all
weights are effectively lowered by a constant factor. A variable with the
smallest evaluation of dom/weight*extra is selected, where 'extra' is 1.0
for variables that participated in the latest conflict analysis and 8.0
otherwise. In effect, the ordering algorithm prefers to use variables which have
a higher probability to cause a conflict in the current solver state.

The value ordering of HCSP.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Values are selected using a variant of SAT phase-saving technique.

If the variable was fully assigned before then if possible assign the previous
value. If the variable was fully assigned before but the past value is not in
the domain, then consider the pair {min(dom),max(dom)} and select whichever is
closest to the past value or select one at random in case of a tie. If the
variable was not fully assigned before, then select the smallest value.

The deletion of constraints.
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Learned constraints are deleted from time to time. A constraint which has
not been in use for many conflicts is erased. A constraint which caused a domain
reduction due to propagation, or used during conflict analysis is considered
"used". If a constraint may still be used in future conflict analysis it will
not be erased, even if it has not been used for many backtracks, 


-----

[1] Michael Veksler and Ofer Strichman. A proof-producing csp solver.
    In Proceedings of the Twenty-Fourth AAAI Conference on Artificial
    Intelligence, 2010.

[2] Michael Veksler and Ofer Strichman. Learning non-clausal constraints
    in csp (long version). Technical report, Technion, 2014
    http://ie.technion.ac.il/tech_reports/1397342213_resolution-paper.pdf