# Boolean variable that captures whether an inequality holds

I have an integer linear program with variables $$x_1,\dots,x_n$$. I have an inequality $$a_1 x_1 + \dots + a_n x_n \ge b$$ that I care about; it may or may or not hold.

I want to introduce a boolean variable $$y$$, with the intent that $$y=1$$ if this inequality holds or $$y=0$$ if it doesn't. How can I write linear inequalities to constrain $$y$$ to take this value?

All of $$a_1,\dots,a_n,b$$ are constants. I know upper and lower bounds for all of the $$x_i$$'s.

\begin{align*} a_1 x_1 + \dots + a_n x_n &\ge b - M (1-y)\\ a_1 x_1 + \dots + a_n x_n &< b + M y, \end{align*}
where $$M$$ is chosen sufficiently large.
Why does this work? If $$y=1$$, then the first inequality forces $$a_1 x_1 + \dots + a_n x_n \ge b$$ to hold. If $$y=0$$, then the second inequality forces $$a_1 x_1 + \dots + a_n x_n < b$$ to hold, i.e., $$a_1 x_1 + \dots + a_n x_n \ge b$$ to be false.
How large does $$M$$ need to be? If the $$x_i$$'s are zero-or-one variables, then it suffices to take $$M$$ to be at least $$\max(b,a_1+\dots+a_n-b+1)$$. In general, if you have upper and lower bounds for each $$x_i$$, you can derive how large $$M$$ needs to be.