[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