Comment by blobcode
2 days ago
I feel like SAT solvers and the like are getting a lot more attention on HN recently (for example https://news.ycombinator.com/item?id=44259476) - justifiably so! I think that they're a great tool that's often criminally underused in industry for a whole subset of problems.
> a whole subset of problems
Like what?
In my experience, 95% of the times I'm considering applying SAT/SMT to a problem, I should actually think about it for another day (perhaps while throwing a SAT solver at it, if that seems fun) and will invariably find that the problem I'm trying to solve is actually something else... In the remaining 5% of problems, there's usually a solution you can download (which maybe uses SMT under the hood).
Sure enough, SMT is really cool and extremely powerful where it's applicable.
You are not wrong. But I can wear both hats (no pun intended, I think).
On one hand people are not going to be using SAT/SMT to solve problems on a dayly basis.
On the other hand these algorithms are a bit overlooked in CS books (not Knuth, of course). Compare, for instance with a FFT. In the livetime of an average programmer they might actually find it convenient to use SAT solvers here and there on a few occasions. Maybe just as much as a FFT.
Combinatorics is a hard subject and SAT shed light in many situations where better tailored algorithms might exist but might be difficult to come up with.
Maybe I'm biased
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.