That's not really a proof that we can't get a nice thing, though. SAT is NP-complete, but here we are talking about it. There may be ways to use parallelism at a higher level. And even if there isn't an alternative to unit propagation, a purely constant factor speedup with parallel processors isn't out of bounds and would still be fantastic.

>a purely constant factor speedup with parallel processors isn't out of bounds and would still be fantastic.

The state of the art with this is about 2x the speedup with an unbounded number of threads.

That's not bad, but is not very useful because in most use cases of SAT you have multiple distinct problems solvable in parallel anyway.

Isn’t UP complete with respect to CNF satisfiability though? How does P completeness relate to parallelizability of SAT?

It's related in the sense that we can guarantee that all threads have to communicate at every step of the algorithm.

It's not a deal breaker, but we really need some unprecedented advance in mathematics to negate this or to solve SAT without this communication.

I remain skeptical. NC=P? is still an open conjecture, so there could be problems which are decidable in P, but only when using a polynomial number of processors or superpolynomial on a single processor, but polynomial on a polynomial number of processors. Furthermore, the amortized complexity of common instances could turn out to be tractable on average (e.g., random 3-SAT instances are tractable unless they fall in a very narrow region where the ratio of clauses to variables is ~4.25, but NP-complete in the worst case).

You're not wrong, but people have been trying to do this for a while now without much success.

So much that you can probably get a turing award by making a SAT solver that can be 100-1000x faster on a GPU than on a CPU.

Also that would lead to solving a bunch of NP complete problems 1000x faster, so you can see why that would be a big deal.