Learning general constraints in CSP

We present a new learning scheme for solvers of the Constraint Satisfaction Problem (CSP), which is based on learning (general) constraints rather than the generalized no-goods or signed-clauses that were used in the past. The new 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 ] ⊈ [ a, b ]. The learned constraint is stronger than what can be learned via signed resolution. Our experiments show that our solver HCSP backtracks orders of magnitude less than other state-of-the-art solvers, and is overall on par with the winner of this year's MiniZinc challenge.

Authors

• Michael Veksler Technion
• Ofer Strichman

Keywords

• Constraints solving
• Inference rules