All-different constraint

An all-different constraint requires its variables to take pairwise distinct values. For domains $D(X)=D(Y)=\{1,2\}$ and $D(Z)=\{1,2,3\}$, the first two variables consume values one and two in every solution, forcing $Z=3$. Pairwise inequality propagation may miss this deduction, while a global propagator can use a matching in a bipartite graph between variables and values. Hall's marriage theorem supplies the feasibility condition: every subset of variables needs at least as many available values as variables. This constraint appears in schedules, assignments and numerical puzzles.