This is appealing, but I think you're only going to have full utilization for a short time? Many of your partitions of the problem are going to come back unsatisfiable, and then those cores go idle.
I have recently parallelized 3D flood fill algorithm, it’s essentially a graph search on a 3D grid of nodes. More precisely, the problem is known as connected-component labeling: https://en.wikipedia.org/wiki/Connected-component_labeling
The solution is to keep partitioning until you saturate all cores. As soon as all saturated, stop partitioning and compute. As soon as any task finished, resume partitioning.
On the lower level, I used a thread pool. BTW, the infrastructure for that is built-in in Windows, see SubmitThreadpoolWork API: https://docs.microsoft.com/en-us/windows/desktop/api/threadp...
This walk the tree to find the variable, X, that occurs most often. There is a weighting issue. Occurrences higher up the tree count more.
Then I would create two expressions by substituting X = true and X = false.
Now two cores can race to see which can find a satisfying assignment first. Clearly this division can be applied recursively until all the cores are busy.