Equivalence between constraints in ILP

Question

Let's have binary variables $x$ and $y$. I'd like to define a helping binary variable $z$ such that $$ z = 1 \; \;\; \mathrm{iff} \; \; \; x + y = 2.$$ If I wanted to express the equivalence between binary variables $a$ and $b$, I would simply convert them into a conjunctive normal form: $$ a \Leftrightarrow b \equiv (a \Rightarrow b) \land (b \Rightarrow a) \equiv (\lnot a \lor b) \land (\lnot b \lor a)$$ and do a standard SAT $\to$ ILP conversion: $$ (1 -a) + b \geq 1, $$ $$ (1 - b) + a \geq 1. $$ Now let's try to substitute $a \to (z = 1)$ and $b \to (x + y = 2)$ into the CNF: $$ (\lnot (z = 1) \lor (x + y = 2)) \land (\lnot (x + y = 2) \lor (z = 1)). $$ Since we can't use inequalities, we can rewrite the equalities as follows $$ (\lnot (z \geq 1) \lor (x + y \geq 2)) \land (\lnot (x + y \geq 2) \lor (z \geq 1)) $$ and then we can simply negate the inequalities $$ ((z \leq 0) \lor (x + y \geq 2)) \land ((x + y \leq 1) \lor (z \geq 1)). $$ Now, my idea was to use the fact that the logical AND is implicit within the constraints and that we can emulate logical OR between the inequalities using big $M$. Let's define helping variables $a_1$ and $a_2$. $$ z \leq \mathrm{M}a_1, $$ $$ x + y + \mathrm{M}(1 - a_1) \geq 2, $$ $$ x + y \leq 1 + Ma_2, $$ $$ z + M(1 - a_2) \geq 1. $$ Now this won't work since we could just use $a_1 = 1$ and $a_2 = 0$ and there would be no constraint on $z$.

My idea is that we would somehow need to connect the lefthand side of the logical AND with the righthand side.

Was my approach correct up until the point right before the last conversion?

How would one go about expressing the logical rules between entire equalities and inequalities in general?

Answer 1

Not sure if you need all this machinery. I would write:

$$ \begin{aligned} & z=0 \iff 0 \le x+ y \le 1 \\ & z=1 \iff 2 \le x+ y \le 2 \end{aligned} $$

or $$ 2z \le x+y \le 1 + z $$

(Actually Rob's answer is better than this: use $z=xy$ and linearize that using $z\le x$, $z \le y$ and $z\ge x+y-1$. That is tighter. In fact it is so tight that we can relax $z$ to be continuous between 0 and 1).

Answer 2

For binary variables $x$ and $y$, notice that $x+y=2$ is equivalent to $xy=1$, so you want to linearize $z=xy$. I gave a derivation via conjunctive normal form in my answer here: https://or.stackexchange.com/a/473/500

Answer 3

You can't let $a_1=1$ and $a_2=0$, because it will enforce $x+y \geq 2$ and $x+y \leq 1$, which is infeasible. That is the connection between the two new variables. So your model is totally correct but maybe not efficient.