Parallel solving support?

[EmnaBl]

Hello,

I am using the Java API and wondering if z3 has support for parallel solving so that I can use more than one core of my machine. Also are there any documentation about other techniques to enhance performance?

Thanks in advance for your help ! Blouta.

[NikolajBjorner]

There are couple of ways to tease out using threads:

• par_or tactic
• enable parallel solving using parallel.enable=true. Mainly for finite domain (bit-vector) problems.
• also for bit-vector problems, setting parameters of the sat solver to use multiple solvers that exchange lemmas.

Though I would say, these options are really for expert use. I doubt they work uniformly for all kinds of problems. Also, for very small problems, multi-threading is a waste. You can have different threads at your level, using separate contexts, as well. Another github issue documents some of the contention issues, some of which have been addressed at this point.

Some of the above options are mentioned here: https://theory.stanford.edu/~nikolaj/programmingz3.html