Not SAT but this a recent example of using Mixed Integer Programming in real life: https://medium.com/netflix-techblog/predictive-cpu-isolation... (I'm one of the author of the article)