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.