I am attempting to move from a commercial solver to Z3 for large integer satisfiability problem. By "large" I mean that the model I am trying to solve has on the order of 300,000 integers and 300,000 (assert (=... statements, each with a combination of perhaps 8-16 variables.
Our commercial solver took 1353 seconds to solve the big problem. Our commercial solver is actually an optimizer and this was solved as a mixed integer optimization problem. The problem transformed into an integer problem with 5,093,121 variables, 9901 constraints, 63,450,472 zeros, 5,093,120 integers, and it was solved in 4690 iterations. However, it was a simple SAT problem, so I'm hoping to move this to Z3 and ditch the commercial optimizer.
As I indicated, the commercial optimizer took 1353 seconds, but it was also allowed to use 32 cores and indications are that I used many of them (I didn't track how many cores it ended up using).
I would like Z3 to be able to use multiple cores. At the present time it doesn't seem that it does. Is there any way to make it do so? Failing that, is there another SMT solver that will?
Z3 does support parallel processing, see: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-parallel-z3
Parameters can be set on the command line. So to make z3 use 4 threads and process file solve.z3, use:
z3 parallel.enable=true parallel.threads.max=4 solve.z3
Note that if parallel.enable is set to true, Z3 will default to the number of processors.
Unfortunately this feature is rather poorly documented. Please do report your findings if you try it out!