Propagation redundancy in redundant modelling

Combining mutually redundant models with channelling constraints increases constraint propagation. However, the extra computation efforts of the additional variables and constraints may outweigh the gain of reduction in search space. In fact, many of the constraints in redundant modelling are not only logically redundant but also propagation redundant and hence cannot further reduce search space. We give general theorems for proving propagation redundancy of one constraint with respect to channelling constraints and constraints in the other model. We define a broad form of channelling constraints that are covered by our approach. We illustrate, using problems from CSPLib (http://www.csplib.org/), how detecting and removing propagation redundant constraints can significantly speed up solving behaviour.