Parallelisation support

[ChrisJefferson]

I was wondering if there is any current support for parallelisation (I want to solve multiple SAT problems at the same time).

Is either Python threads (you could release the GIL?), or multiprocessing supported?

[alexeyignatiev]

As far as I understand, nothing should prevent PySAT to be used in parallel using let's say threading. I haven't tried it myself, but I remember implementing signal handling to support multiple threads. So it should work I guess. But it is better to try. :)

[WonJayne]

Let me just add that I've successfully used pysat with multiprocessing in python @alexeyignatiev.

[alexeyignatiev]

That's great to know, @WonJayne! Can you share some concrete recipe with us so that I could probably add it to the documentation? (Because, as I mentioned before, I haven't tried multiprocessing with PySAT myself.)

[WonJayne]

@alexeyignatiev Sure. I'll prepare an example, such that you can integrate it. I'll try to follow the style of the existing examples.

I think having a small example is actually quite valuable, as the wrong usage of subprocesses can cause out of memory errors (when the solver instance is not deleted). I'll let you know, when the example is ready.

Let me use this possibility to thank you for this exceptional package, it enabled me to do a great thesis!

[alexeyignatiev]

@WonJayne great to know that the toolkit was of help, thanks! :) And thank you for preparing the example. I believe it will be useful for a wide audience of users!

[alexeyignatiev]

@WonJayne, by any chance, did you manage to prepare the example? :)

[alexeyignatiev]

@WonJayne, please let me know if your use of PySAT in parallel was done in a similar vein.

[WonJayne]

Hi @alexeyignatiev

Indeed, I used PySat in parallel in a similar vein.

However, in the mean time, I found an alternative way to leverage your awesome work and a parallel solver, CryptoMiniSat. CMS is cool, as it supports both single and multithreaded usage and offers incremental usage.

The integration works as follows: I put together a wrapper (crypto_mini_sat.zip) around the Solver of PyCryptoSat, the Python version of CMS, such that one can swap the solvers freely and installed PyCryptoSat with pypi. However, there's one caveat: Currently, the most recent version of CMS that is available for windows is 5.7.0, which is known to suffer from a memory related bug, causing excessive solving times for some cases.

But there's light at the end of the tunnel: The most up to date version of CMS should no longer suffer from that, as it has been fixed. Furthermore, in this comment, it is stated that PyCryptoSat will soon be available on PyPi.

Hence, I would propose the following to integrate CMS in the near Future:
Add a wrapper for CMS to pySat and get PyCryptoSat via PyPi. What is your opinion on that? I see that this is a deviation from your usual pattern of how you implement solvers, so let me know if you think this is worth a try.

[alexeyignatiev]

Hi @WonJayne,

I do like the idea. In fact, @msoos and I discussed this in July 2020. My concern was the limited incremental functionality offered by CMS at that time. Not sure what the status is now. Having said that, I see no issue in integrating CMS through a high-level dependency on PyPI.

[WonJayne]

Great that you like the Idea of integration via PyPI. Just out of curiosity, what is your concern with limited incremental functionality? The get_conflict method is available since May 2019. Are there more things needed for incremental solving?

[alexeyignatiev]

Well, there were quite a few methods in the list here missing in CMS at that point.

[WonJayne]

I see. Could have figured out that myself, since my wrapper has lot's of NotImplemented exceptions for the missing methods.