The AllDifferent Constraint

The AllDifferent constraint forces a list of integer variables to take pairwise distinct values. In CP-SAT, we add it to a model with

$$\texttt{model.AddAllDifferent([}x_1, x_2, \ldots, x_n\texttt{])}.$$

This single call enforces $x_i \neq x_j$ for every pair of indices $i \neq j$.

For example, suppose we declare three integer variables $a, b, c$ each with domain $\{0, 1, 2\}$ and add $\texttt{AddAllDifferent([}a, b, c\texttt{])}$. Then $(a, b, c)$ must be a permutation of $(0, 1, 2)$, giving $3! = 6$ feasible assignments:

$$(0,1,2),\ (0,2,1),\ (1,0,2),\ (1,2,0),\ (2,0,1),\ (2,1,0).$$

Note: If the number of variables exceeds the size of the common domain, the constraint is infeasible. Four variables, all with domain $\{0, 1, 2\}$, cannot all be distinct — by pigeonhole, at least two must coincide.