Of course, dividing search space into K pieces is not guaranteed to give you a speed-up _in the worst case_: you might pick an unlucky division where K-1 pieces are easily UNSAT but the last remaining piece is as hard as the original (so the wall clock time is unchanged). However, in practice variable-fixing can and often does give an _expected time_ speed-up, especially if the SAT instance has some inherent parallel search structure (e.g., key or midstate bits for ciphers) and such heuristic tactics are still useful.