Does PySAT support parallel solving?

Question

I'm using PySAT. Is there a threads number parameter somewhere? Or a packaged solver that can be parallelized in this way?

(Currently, I'm using the Glucose4 solver.)

Answer 1

I dug into the source code, and the answer seems to be no.

The only reference to threading in the PySAT codebase is some code that checks whether the current thread is the ‘main’ one and adjusts signal handling logic based on that. Nothing in the library allows the user to control the level of parallelism used by the actual solver.

The best workaround was mentioned by the asker in the comments: manually split the problem space into sub-cases that can be independently solved in parallel. Fortunately enough, SAT lends itself to that approach particularly easily.

Reposting comment:

The trick is to case-split on n variables, in that way you can utilize 2^n cores. You solve the same formula in each thread, but with True/False substituted for those variables, and hopefully it's faster