What would be a concrete problem you could solve with SAT solvers, besides the obvious "satisfy this boolean expression" (which doesn't exactly come up every day)? Is it a useful tool for other NP-complete problems?
I mean, certainly you COULD reduce the Traveling Salesman Problem to SAT (it's NP-complete, after all), but I would assume that it would be a totally impractical way of doing it compared to more specialized algorithms.
I'm asking since the title contains the word "underused", but doesn't elaborate on practical use-cases. What would you use it for?
https://en.wikipedia.org/wiki/Concolic_testing
Basically, the problem "find an input that causes the program to execute this sequence of statements".
---
Identification of missing optimizations in the LLVM backend.