Assuming $y$ is a boolean variable in an ILP program (that is $y \in Z$, s.t. $0 <= y <= 1$) and $x_1$, $x_2$ are bounded integer variables between $0$ and $M$. I want to encode the following high level constraint:$$y = 1 \iff x_1 \le x_2$$So far I've got this:$$x_1 \le x_2 + (M+1)y$$This enforces that whenever $x_1 > x_2$ is true, $y$ must be $1$ or the equation won't hold. However, if $x_1 \le x_2$, nothing is restricting $y$ and thus could either be $0$ or $1$. What other equation could I add in order to encode the constraint?
Boolean variable true iff equation is satisfied in ILP
integer programming
You can do this by introducing the two inequalities$$x_1 \le x_2 + M (1-y)$$and$$x_1 > x_2 - M y.$$The former encodes the requirement $y=1 \implies x_1 \le x_2$ (you can see that if $y=1$, then the $M(1-y)$ term disappears; if $y=0$, then $M(1-y)$ becomes something huge and the inequality is automatically satisfied).  The latter encodes the requirement $y=0 \implies x_1 > x_2$ (for similar reasons).  Hopefully this gives you an idea how to handle other kinds of implications as well, should they arise.  Basically, multiply by something big, and add it/subtract it somewhere.