Constraint solving is a declarative approach for solving combinatorial satisfaction and optimization problems. The user specifies their problem through constraints and decision variables, and a generic solver is used to find a solution. Several constraint-solving technologies exist, and certain solvers perform well on certain problems. Therefore, it is useful to try different solvers given a particular application. However, each solving paradigm supports different types of constraints and decision variables. Our goal is to translate high-level constraint satisfaction and optimization problems into any lower-level formalism, including CP, SMT QF-LIA, ILP, PB and (Max)SAT. This allows for comparing different solving technologies for a particular problem, without requiring a user to manually remodel it for each solving paradigm. We define a high-level language of logical and arithmetic operations, and useful additional functions and constraints, which are known as global constraints in the CP community. We then present a modular framework for transforming our high-level modeling language to CP/SMT/ILP/PB and (Max)SAT solvers. While many transformations are partly described in the literature, we observe that they can be implemented through a modular waterfall of smaller components, where lower-level paradigms reuse the transformations of higher-level paradigms. Two recurring challenges are handling the negation of arbitrary subexpressions and avoiding the introduction of auxiliary variables. Additionally, we take special care linearizing non-linear operators for ILP, PB and SAT-solvers. The transformation waterfall is implemented and evaluated in the open-source CPMpy library. Our results show that constraint models significantly change throughout the transformations, and that optimizations to the linearization of constraints are essential for ILP and PB solvers.
Tias Guns, Ignace Bleukx, H. Bierlee et al.· 0 citations
Background: In declarative constraint solving, a user formulates a constraint model in terms of variables and constraints, and uses a generic, off-the-shelf solver to solve the problem. Constraint Programming (CP) is one such constraint-solving paradigm, which has a wide support for many types of constraints, including global constraints. Global constraints capture complex relations between several decision variables, and CP solvers have specialized propagators to solve them efficiently.
Objectives: While CP solvers support a wide range of global constraints, few solvers support them in a reified or even halfreified context. Hence, for most CP solvers, reified global constraints must be decomposed into non-global constraints. This bypasses the global constraint propagator, which can considerably slow the solving process, suppressing one of the key benefits of modeling with global constraints: a faster solve-time. This is a problem for generic CP-modeling, as reified constraints are often introduced by the modeling system during translation and flattening of compound constraints. Additionally, half-reified global constraints are also used extensively in eXplainable Constraint Programming techniques (XCP). Therefore, XCP techniques suffer from scalability issues when global constraints occur in the model. In this paper, we aim to alleviate this bottleneck, allowing the use of the propagators of global constraints when modeling their half-reification, for all CP-solvers.
Methods: We propose a set of reformulation rules that allow the use of half-reification of a global constraint with any CP solver that supports the “normal” global constraint propagator. This is achieved by introducing auxiliary variables for the decision variables in the global constraint and the use of a reified channeling constraint, which most CP solvers support. Additionally, we show how to reduce the overhead of these auxiliary variables, by limiting the number of variables introduced, and by fixing their value when unconstrained. Finally, we prove the propagation strength of our reformulation for a variety of global constraint families.
Results: We experimentally evaluate the reformulations on a variety of global constraints and applications where reified constraints can occur. Our results show that this reformulation is much faster compared to decomposing the global constraint, and in some cases, even outperforms solver-level propagation routines for reified global constraints.
Conclusions: Using the reformulations proposed in this paper, we make the use of reified global constraints easily available for any CP solver. Hence, we expand the range of available solvers and constraint models that can be used in XCP techniques or for solving CSPs with compound constraints.
Ignace Bleukx, Hélène Verhaeghe, Dimos Tsouros et al.· Journal of Artificial Intell...· 1 citation