Comment by LegionMammal978

It's occasionally helped me with the NP-hard problem of "finding a regular language consistent with a set of samples that also satisfies some structural constraints". But more often, the minimal DFA (when it exists) has a few dozen too many states, and the solver gets trapped in the exponential pit of despair, which hasn't really endeared me to the approach. I've yet to actually run into a class of problems where things like SAT or ILP are wildly successful while all other approaches fail.