HCSP - A CSP solver with non-clausal learning Author: Michael Veksler ( mickey.veksler at gmail dot com ) Institute: Information Systems Engineering, Technion, Haifa, Israel HCSP is a constraint solver written in C++, which is capable of solving both CSP's and Constraint Optimization Problems. Its solving algorithm is based on General Arc Consistency (GAC), with constraint propagation and conflict analysis. HCSP adopts classical ideas from the CSP and SAT literature. It uses interval trees to efficiently represent domains. Variables are ordered dynamically according to a modified VSIDs strategy, which prefers variables that are used in conflict analysis, and have small domains. When making a decision, if a variable had been assigned before, its previous value is preferred ('phase saving'), otherwise minimum or maximum values are used. HCSP employs occasional restarts, and forgets old, rarely used, conflict constraints. Learning: HCSP has a novel learning scheme, which is based on learning (general) constraints rather than the generalized no-goods or signed-clauses that were used in the past. This scheme is integrated in a conflict-analysis algorithm reminiscent of a modern systematic propositional satisfiability (SAT) solver: it traverses the conflict graph backwards and gradually builds an asserting conflict constraint. This construction is based on new inference rules that are tailored for various pairs of constraints types, e.g., (x <= y_1 + k_1) and (x >= y_2+ k_2), or (y_1 <= x) and ([x,y_2]\not\subseteq[a,b]). The learned constraint is stronger than what can be learned via signed resolution, and according to our experiments with previous year's competition benchmarks leads to a reduction of at least an order of magnitude in the number of backtracks comparing to other state-of-the-art solvers. More information can be found in [1,2,3] http://ie.technion.ac.il/~ofers/HCSP/index.html [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 general constraints in CSP. In Laurent Michel, editor, Integration of AI and OR Techniques in Constraint Programming - 12th International Conference, CPAIOR, volume 9075 of Lecture Notes in Computer Science, pages 410–426. Springer, 2015. [3] Michael Veksler and Ofer Strichman. Learning general constraints in CSP. Artificial Intelligence Journal, 238:135–153, 2016.