Thank you for the detailed reply, this is the first cogent answer I have read that explains why GPU solvers are not as widely used in SAT. The argument that we should focus on getting sequential solvers to run fast, then parallelizing that in hopes that it can be reused on each core does make sense, although I can't help but wonder if there isn't a smarter way to leverage parallelism than simply running CDCL in parallel on n-independent cores.

I guess if I were to summarize your argument, (current) solvers do not use GPUs because there are not many algorithms that can leverage the additional compute (and maybe there is some theoretical barrier?). On the other hand, the continuous optimization folks had neural networks for more than half a century before they figured out how to make them run fast, and were also ridiculed for pursing what was widely believed to be a dead-end. So I would be careful about falling for the "smart people tried really hard for a while" argument.