Hacker News Reader

What you describe looks like cube-and-conquer technique [1].

[1] https://www.cs.utexas.edu/~marijn/publications/cube.pdf

The thing is much more deeper than what you described. You need to choose which variables you will assign, that's first. Then you have to assign them, and it is important to do as carefully because assignment may produce inbalanced search space.

Splitting on one variable when there are hundredths of thousands of them is very, very inefficient.

The difficulty is which variables to pick so that all subspaces are of comparable difficulty. Cube and conquer is a nice paper on that problem.

Using a naive splitting strategy is trivial, but ensuring the distribution is well-balanced across the subspaces is not. You need to preprocess the formula by setting the variables, then doing some propagation, then restarting, otherwise one core will get stuck doing a bunch of useless work.