I was thinking there might be some theoretical barrier to parallelization, e.g., maybe naturally-arising SAT instances have poor empirical scaling constants [1]

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) https://en.wikipedia.org/wiki/NC_(complexity) [2]: https://baldur.iti.kit.edu/hordesat/files/horde.pdf https://baldur.iti.kit.edu/hordesat/files/horde.pdf