4 ms·
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
by andrewprock 3y ago
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.
- bmc7505 3y agoUsing 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.
- c-cube 3y agoThe difficulty is which variables to pick so that all subspaces are of comparable difficulty. Cube and conquer is a nice paper on that problem.
- thesz 3y agoWhat you describe looks like cube-and-conquer technique [1]. [1] https://www.cs.utexas.edu/~marijn/publications/cube.pdf 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.