[blobcode]

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.

[staunton]

> 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.

[nhatcher]

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

[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.