search

sat-group / open-wbo

Open-WBO: state-of-the-art MaxSAT and Pseudo-Boolean solver
Other
69 stars 12 forks source link

Run open-wbo with multiple threads #1

Closed haghshenas closed 6 years ago

haghshenas commented 6 years ago

Hi there,

Thanks for providing this great tool. Considering that Glucose 4.1 supports multiple threads, is it possible to tweak open-wbo to run on multiple cores? This would help a lot. Thanks.

rubengmartins commented 6 years ago

Thanks for your interest in Open-WBO.

We currently call the SAT solver as black-box. I believe it should be possible to use the parallel version of Glucose instead of the sequential solver. The parallel version would need to support incremental SAT solving and computing an unsat core via assumptions. If this is the case, then the integration should be straightforward.

I will do some testing next week on using a parallel SAT solver as the back-end and will let you know if this is easily supported by Open-WBO.

haghshenas commented 6 years ago

Hi again,

Are there any updates with regards to this issue? Did you have a chance to do testings?

Cheers!

nlw0 commented 6 years ago

I would be very interested in a parallel version! I am willing to contribute, but I have little knowledge of the inner workings of all the tools. Have we at least determined whether it is feasible?

conp-solutions commented 6 years ago

From looking at the glucose 4.* code, it looks like the parallel solver implementations do not support assumptions in their implementation, hence the unsatisfiable core computation would also fail.

rubengmartins commented 6 years ago

At this time, we do not plan to support parallel solving.

If the parallel SAT solver supports assumptions then it should be easy to integrate with Open-WBO. However, if this is not the case (like Glucose 4.*) then unsatisfiable-based algorithms will not work properly and you can only use the linear search sat-unsat algorithm (option -algorithm=1).

If you want to try parallel MaxSAT solving then I would recommend checking PWBO (even though it is an older solver it does support parallelism): http://sat.inesc-id.pt/pwbo/

I am closing this issue for now but if there are volunteers to either look for parallel SAT solvers that support assumptions or are interested in modifying a parallel SAT solver to be integrated in Open-WBO, then I would be happy to create a branch for that version and give some pointers.