Solving formulas in parallel with z3

Question

Let's say I have a z3 solver with a certain number of asserted constraints that are satisfiable. Let S be a set of constraints, I would like to verify for every constraint in S whether the formula is still satisfiable when adding the constraint to the solver. This can be easily done sequentially in such a fashion:

results = []

for constraint in S:
  solver.push()
  solver.add(constraint)
  results.append(solver.check() == z3.sat)
  solver.pop()

print all(results)

Now, I would like to parallelize this to speed things up, but I'm not sure how to do it properly with z3.

Here is an attempt. Consider the following simple example. All variables are non negative integers and have to sum to 1. Now I would like to verify whether every variable x can independently be made > 0. Obviously it is the case; let x = 1 and assign 0 to the other variables. Here is a possible parallel implementation:

from multiprocessing import Pool
from functools import partial
import z3

def parallel_function(f):
    def easy_parallize(f, sequence):
        pool   = Pool(processes=4)
        result = pool.map(f, sequence)

        pool.close()
        pool.join()

        return result

    return partial(easy_parallize, f)

def check(v):
    global solver
    global variables

    solver.push()
    solver.add(variables[v] > 0)
    result = solver.check() == z3.sat
    solver.pop()

    return result

RANGE = range(1000)
solver = z3.Solver()
variables = [z3.Int('x_{}'.format(i)) for i in RANGE]

solver.add([var >= 0 for var in variables])
solver.add(z3.Sum(variables) == 1)

check.parallel = parallel_function(check)
results = check.parallel(RANGE)
print all(results)

Surprisingly this works perfectly on my machine: the results are sound and it is much faster. However, I doubt that it is safe since I'm working on a single global solver and I can easily imagine the push/pops to happen concurrently. Is there any clean/safe way to achieve this with z3py?

score 5 · Accepted Answer · edited May 23 '17 at 11:54

5

Indeed, this might work for a first test, but not in general. Parallel solving on a single Context is not supported and there will definitely be data races and segfaults later.

In Python, the Context object is hidden, so most users won't have to deal with it, but to run things in parallel, we need to set up one Context per thread and then pass the right one to all other functions (which implicitly used the hidden Context before). Note that all expressions, solvers, tactics, etc, all depend on one particular Context, so if objects need to cross that boundary we need to translate them (see translate(...) in AstRef and similar).

See also Multi-threaded Z3? and When will the Z3 parallel version be reactivated?

edited May 23 '17 at 11:54

Community

1
1

answered Jun 14 '15 at 16:40

Christoph Wintersteiger

8,234
1
16
30

So if I understand correctly, I can (1) initialize one solver s (2) for each thread i, create one solver s_i within a context c_i (3) copy s into each s_i with s_i.add(s.assertions().translate(c_i)) (4) perform the tests in parallel by first making sure to translate the additional constraint to the appropriate context. Is that right? – Michael Blondin Jun 14 '15 at 22:04
1

You need one context, that is a Z3 Context object, for each thread. Only once we have a Context, we can construct a solver (making sure that the right Context object is used for each of them). Then all constraints can be translated into each of those contexts. – Christoph Wintersteiger Jun 16 '15 at 05:50

Solving formulas in parallel with z3

1 Answers1

Linked