Think of it in terms of weird graph problems and algorithms. It is now easier and faster to encode most graph problems and have a SAT solver go at it, compared

Think of it in terms of weird graph problems and algorithms. It is now easier and faster to encode most graph problems and have a SAT solver go at it, compared to carefully designing and tuning your custom graph algorithm for performance in the kinds of graphs you care about. As for examples, there isn't much retail software that really needs SAT. But you might have indirectly used firewall/configuration management, home automation, flight/factory scheduling, route planning, etc.