I was thinking there might be some theoretical barrier to parallelization, e.g., maybe naturally-arising SAT instances have poor empirical scaling constants [1], so sequential solvers with good branch heuristics are pretty close to optimal. There are some portfolio solvers (e.g., [2]) that have shown modest, but not dramatic speedups. Or maybe we just haven't tried hard enough.

[1]: https://en.wikipedia.org/wiki/NC_(complexity)

[2]: https://baldur.iti.kit.edu/hordesat/files/horde.pdf