Fun fact. Most power grids in the developed world are run off of some of the largest MILP and LP problems. We're talking about millions of constraints to commit units and hundreds of thousands to dispatch them. These run around the clock 24/7.

I've only recently learned about SAT type solvers as MILP/LP problems are very fast and globally optimal, unlike things like A* or Genetic Algorithms. I think GA's are cool because you can write one in less than 1/2 page of Python, where MIP solvers are usually large black-box C codesets (Ex: GLPK, CPLEX, GUROBI, XPRESS, Open-Solver).