Re:The Silent (R)evolution of SAT
by andrewprock on Friday May 26, 2023 @10:19AM
(#36084513)
Unless I'm missing something, space splitting should be trivial. If you have two cores and three propositional variables x1, x2, x3, you could simply set x1 to tier on one core and false on the other, and then perform two parallel SAT searches on a space with one less variable.
[ Parent
| on HN ]
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.
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.
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.