4 ms·
If I had to write a SAT solver to use lots of cores on an arbitrary boolean formula, I would farm out the work like this: This walk the tree to find the variab
by alan-crowe 8y ago
If I had to write a SAT solver to use lots of cores on an arbitrary boolean formula, I would farm out the work like this:
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.
- sevensor 8y agoThis 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.
- Const-me 8y agoI 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 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/threadpoolapiset/nf-threadpoolapiset-submitthreadpoolwork https://docs.microsoft.com/en-us/windows/desktop/api/threadp...