search

meelgroup / approxmc

Approximate Model Counter
Other
70 stars 26 forks source link

Why doesn't multithreading help? #27

Closed hflsmax closed 2 years ago

hflsmax commented 2 years ago

I want to utilize the multithreading feature of cryptominisat5, so I added data->counter.solver->set_num_threads(3); to AppMC::AppMC(). I can see multiple thread running, but approxmc is even slower. Am I not doing it correctly?

msoos commented 2 years ago

Hi,

This is unfortunately a known issue. The problem is, that that the threads you are running need to synchronize. That means that the threads wait for each other when one of them finds a solution (SAT or UNSAT). This waiting can be quite a lot when one of the threads is in the middle of something and doesn't check the terminate flag. I think if you improve the synchronization, or somehow make them work in a way that's asynchronous and still correct, then it would be faster. But I just haven't done that work. You can try to pick that up and see which threads the others are waiting for, debug, and fix, so the flag is checked more often, leading to less waiting, and overall better performance.

Looking forward to the pull request to fix the threads waiting :) It may not be such a big deal to fix, actually, I just don't have the time right now. You can have a go, though! I hope the above helped, and looking forward to a PR to fix,

Mate