How to linearize $z \iff x = y$?

Question

I have a constraint that reads $z \iff x = y$ where $z$ is a $0$-$1$ variable and $x$,$y$ are non-zero, positive integer variables. I'm managed to formulate equivalence going in the right direction, but not in the left. Does anyone have any idea here?

Answer 1

Here's a straightforward big-M approach. Introduce binary variables $u$ and $v$, and impose linear constraints \begin{align} -M(1-z) \le x - y &\le M(1-z) \tag1 \\ x - y + 1 &\le M (1-u) \tag2 \\ y - x + 1 &\le M (1-v) \tag3 \\ 1 - z &\le u + v \tag4 \end{align} Constraint $(1)$ enforces $z \implies x=y$. Constraint $(2)$ enforces $u \implies x<y$. Constraint $(3)$ enforces $v \implies x>y$. Constraint $(4)$ enforces $\lnot z \implies (u \lor v)$.

---

A stronger formulation is: \begin{align} -Mu + 0z + 1v \le x - y &\le -1u + 0z + Mv \tag5 \\ u + z + v &= 1 \tag6 \end{align} The three cases are:

• $u \implies -M \le x - y \le -1$, that is $x < y$.
• $z \implies 0 \le x - y \le 0$, that is $x = y$.
• $v \implies 1 \le x - y \le M$, that is $x > y$.