Unsatisfiable Cores and Lower Bounding for Constraint Programming
This work addresses a specific inefficiency in CP solvers for optimization problems with soft constraints, offering incremental improvements over existing approaches.
The paper tackles the inefficiency of naive bound-tightening in Constraint Programming (CP) solvers for soft-constraint optimization problems by adapting unsatisfiable-core methods from SAT (e.g., MAXSAT) to CP, with extensions. Experimental results show the methods are beneficial on a broad class of CP-optimization benchmarks involving soft constraints, cardinality, or preferences.
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.