Decompositions of All Different, Global Cardinality and Related Constraints

TL;DR

This paper presents decompositions of global constraints like ALL-DIFFERENT and GCC into simple arithmetic constraints, enabling effective propagation and sharing in solvers, demonstrated through experiments with a pseudo-Boolean solver.

Contribution

It introduces novel decompositions of key global constraints into arithmetic constraints, enhancing propagation and solver integration.

Findings

Achieved bound and range consistency with decompositions

Enhanced propagation through variable sharing between constraints

Demonstrated effectiveness in a pseudo-Boolean solver

Abstract

We show that some common and important global constraints like ALL-DIFFERENT and GCC can be decomposed into simple arithmetic constraints on which we achieve bound or range consistency, and in some cases even greater pruning. These decompositions can be easily added to new solvers. They also provide other constraints with access to the state of the propagator by sharing of variables. Such sharing can be used to improve propagation between constraints. We report experiments with our decomposition in a pseudo-Boolean solver.