# How to model a set of integer variables getting assigned different values than another set of integer variables

Assume we have variables $$x_1, x_2, x_3, x_4$$ that each can belong to $$\{1,2,...,10\}$$. How can we model a constraint that variables $$x_1, x_2$$ get assigned different values than $$x_3, x_4$$?

Because of scaling issue, it is not efficient to enumerate all assignment combinations as $$\\x_1 \neq x_3, \quad x_1 \neq x_4, \quad x_2 \neq x_3, \quad x_2 \neq x_4$$.

I am using OR-Tools CP-SAT.

• Is (1, 3) and (1, 4) OK ? – Laurent Perron Oct 10 at 21:34
• Since $x_1=x_3$ it is not allowed, @LaurentPerron. $(x_1=1, x_2=1) and (x_3=3, x_4=4)$ is allowed though. – Mahmoud Oct 11 at 1:24

If you mean $$(x_1,x_2)\not=(x_3,x_4)$$, you can enforce this with: $$10(x_1-1) + (x_2-1) \not= 10(x_3-1)+(x_4-1)$$ Equivalently: $$10x_1 + x_2 \not= 10x_3+x_4 \tag1$$

If instead you meant the four disequalities you listed, you can impose $$(x_1 - x_3)(x_1 - x_4)(x_2 - x_3)(x_2 - x_4)\not=0$$ Alternatively, you might consider generating your four disequalities dynamically only if they are violated. In this case, $$(1)$$ is still valid but is only a relaxation.

Here's a MILP formulation. Let binary variable $$y_{i,j}$$ indicate whether $$x_i=j$$, and let binary variable $$z_{g,j}$$ indicate whether any variable in group $$g$$ is assigned value $$j$$. Then your constraints are \begin{align} \sum_j y_{i,j} &= 1 &&\text{for i\in\{1,\dots,1000\}} \\ \sum_j j y_{i,j} &= x_i &&\text{for i\in\{1,\dots,1000\}} \\ y_{i,j} &\le z_{g,j} &&\text{for g\in\{1,2\}, i in group g, and j\in\{1,\dots,10\}} \\ \sum_g z_{g,j} &\le 1 &&\text{for j\in\{1,\dots,10\}} \end{align}

• The product is catastrophically slow. – Laurent Perron Oct 10 at 21:30
• If you want the product to be != 0, just add that all 4 differences are != 0. – Laurent Perron Oct 10 at 21:35
• Indeed, reformulating as one big product constraint does not help much in the context of a CP (or CP-SAT) solver. Moreover, this reformulation also leads to a quadratic number of terms to create. – LocalSolver Oct 10 at 22:01
• Correct, I was hoping it can be modeled using what's available in constraint programming. – Mahmoud Oct 11 at 1:28
• I do not understand the scalability problem. Is it in the number of variables, or the number of values, or both ? I recommend reading github.com/google/or-tools/blob/stable/ortools/sat/doc/… and going back to Boolean logic as soon as possible. – Laurent Perron Oct 11 at 9:09