Unsatisfiable Cores and Lower Bounding for Constraint Programming

TL;DR

This paper adapts unsatisfiable core techniques from MAXSAT to constraint programming, improving optimization by efficiently handling soft constraints and providing better bounds.

Contribution

It introduces a novel adaptation of unsatisfiable core methods for CP, with extensions and experimental validation on various benchmarks.

Findings

Improved solving efficiency on soft-constraint CP benchmarks

Effective handling of cardinality and preference constraints

Beneficial performance gains demonstrated

Abstract

Constraint Programming (CP) solvers typically tackle optimization problems by repeatedly finding solutions to a problem while placing tighter and tighter bounds on the solution cost. This approach is somewhat naive, especially for soft-constraint optimization problems in which the soft constraints are mostly satisfied. Unsatisfiable-core approaches to solving soft constraint problems in SAT (e.g. MAXSAT) force all soft constraints to be hard initially. When solving fails they return an unsatisfiable core, as a set of soft constraints that cannot hold simultaneously. These are reverted to soft and solving continues. Since lazy clause generation solvers can also return unsatisfiable cores we can adapt this approach to constraint programming. We adapt the original MAXSAT unsatisfiable core solving approach to be usable for constraint programming and define a number of extensions. Experimental results show that our methods are beneficial on a broad class of CP-optimization benchmarks involving soft constraints, cardinality or preferences.