How to transform a logical constraint with integer variables?

Question

Consider the binary variables $x_1, x_2 \in \{0,1\}$ and the integer variable $y \in \mathbb{Z}$ with $0 \leq y \leq 3$.

I'd like to formulate the following logical constraint:

$$ x_1 = 1 \wedge y \geq 2 \implies x_2 = 1 $$

and I don't have access to commercial solvers or modelling frameworks. Any ideas?

Answer 1

You can derive the desired linear constraint by rewriting in conjunctive normal form and rearranging to an equivalent implication: $$ (x_1 \land (y\ge 2)) \implies x_2 \\ \lnot (x_1 \land (y\ge 2)) \lor x_2 \\ \lnot x_1 \lor (y\le 1) \lor x_2 \\ \lnot x_1 \lor x_2 \lor (y\le 1) \\ \lnot (x_1 \land \lnot x_2) \lor (y\le 1) \\ (x_1 \land \lnot x_2) \implies (y\le 1) \\ (x_1 \land \lnot x_2) \implies (2\le 3-y) \\ 2(x_1 + (1 - x_2) - 1) \le 3-y \\ 2(x_1 - x_2) + y \le 3 $$ You can alternatively view this as a big-M constraint arising from the implication $x_1-x_2=1 \implies y \le 1$.

Answer 2

The range of values of the variable $y$ is quite small, so you could use the binary representation $y = b_0 + 2b_1$ with two binary variables $b_0$ and $b_1$ instead of the integer variable $y$.

Then your logical constraint is equivalent to

$$ x_1 = 1 \wedge b_1 = 1 \implies x_2 = 1, $$

which can be modelled by

$$ x_1 + b_1 \leq 1 + x_2. $$

Answer 3

Another approach I was trying to do, also based on @RobPratt hints, would be by substituting $y \geq 2$ as an indicator constraint and changing the original logical expression into:

$$ \{x_1 = 1 \wedge y \geq 2 \implies x_2 = 1\} \rightarrow \{x_1 = 1 \land \lnot z\implies x_2 = 1\}$$ $$\lnot x_1 \lor z \lor x_2$$ $$(1-x_1) + z + x_2 \geq 1$$ $$-x_1 + x_2 + z \geq 0$$

For the second part we need to add: $$y + Mz \leq 3$$ with $M=2$ to enforce $y\ge 2\implies \lnot z$.