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