3 ms·

I've used satisfiability solvers, but I don't know enough about their internals to evaluate ESR's claim that satisfiability is intrinsically serial. ESR's argu

I've used satisfiability solvers, but I don't know enough about their internals to evaluate ESR's claim that satisfiability is intrinsically serial. ESR's argument seems to hinge on this idea, that regardless of how well you handle parallelism, it's not going to help with certain tasks.

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 ago
  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.
  - Const-me 8y ago
    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 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...

3 ms·

I've used satisfiability solvers, but I don't know enough about their internals to evaluate ESR's claim that satisfiability is intrinsically serial. ESR's argu

by sevensor 8y ago

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 ago
  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.
  - Const-me 8y ago
    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 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...