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.