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.

Add the inequalities

$$\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.

StackExchange Computer Science Q#104990, answer score: 4