A fun exercise is to write a series of sat solvers: brute force, DPLL and CDCL you really get an immediate feel for the strength of the algorithms and none of these implementations need to go much beyond 50-100 lines in a modern language.

You can then of course spend months tuning and optimizing the hell out of your code to squeeze a further 10x performance.

If you're really crazy like Sarek, you can also formally verify these implementations: https://sarsko.github.io/_pages/SarekSkot%C3%A5m_thesis.pdf

You may want to read "A Time Leap Challenge for SAT Solving". It's just a really fun paper: https://arxiv.org/abs/2008.02215

And yet, despite tremendous progress accelerating continuous optimization workloads, there are still no competitive GPU-based SAT solvers. I wonder why?

Parallelizing SAT solvers seems like a strikingly important avenue for future research.