Concurrent calls to isSatisfiable
It would be great to have Sat4j thread-safe.
The use-case I have is that I share one solver, and ask many questions with different assumptions. Even though my code is sequential, the test framework starts all tests in parallel under the hood, which resulted in very misleading exceptions until I realised that there was a concurrency problem.
An easy solution would be to simply add Synchronized to isSatisfiable() functions. The drawback of this will be that the call to model() after isSatisfiable() might give the model for the assumptions of another thread.
Another solution is to add ConcurrentModificationException if isSatisfiable is called while another call to isSatisfiable is in progress. This will not solve problems with model() after isSatisfiable(), but at least might hint early on that there is a concurrency problem.
A great solution would be to allow multiple calls to isSatisfiable (with different sets of assumptions) to be executed in parallel. I’m not sure that this is achievable by any simple code modification, but my thoughts are as following. Whatever is kept in the solver between consecutive calls can be readily shared between two parallel calls. And whatever is removed between consecutive calls should be private to each call of isSatisfiable. API would change, since models would be different for each call to isSatisfiable, but isSatisfiable itself could return the model if there exist one (using some java variant of Haskell’s Maybe or Scala’s Option class).
Parallel calls would create all sorts of problems, for example, what happens if a clause is added to the solver while a call to isSatisfiable() is in progress in another thread. But maybe such issues can be separated somehow.
I don’t yet know what would be the simplest---yet user-friendly--- solution. All ideas welcome :)