SAT solvers and the algorithms surrounding them are so much fun. I agree they are very unappreciated.

Shameless plug: I wrote a (admittedly very deriative) introduction with some examples I thought at the time were cool.

https://www.nhatcher.com/post/on-hats-and-sats/