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.

  • $\begingroup$ Is (1, 3) and (1, 4) OK ? $\endgroup$ – Laurent Perron Oct 10 at 21:34
  • $\begingroup$ 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. $\endgroup$ – 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}

| improve this answer | |
  • 1
    $\begingroup$ The product is catastrophically slow. $\endgroup$ – Laurent Perron Oct 10 at 21:30
  • $\begingroup$ If you want the product to be != 0, just add that all 4 differences are != 0. $\endgroup$ – Laurent Perron Oct 10 at 21:35
  • 1
    $\begingroup$ 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. $\endgroup$ – LocalSolver Oct 10 at 22:01
  • $\begingroup$ Correct, I was hoping it can be modeled using what's available in constraint programming. $\endgroup$ – Mahmoud Oct 11 at 1:28
  • $\begingroup$ 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. $\endgroup$ – Laurent Perron Oct 11 at 9:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.