python - Solución de fórmulas en paralelo con z3

parallel-processing smt

Question

Digamos que tengo un solucionador z3 con un cierto número de restricciones afirmadas que son satisfactorias. Deje que S sea un conjunto de restricciones, me gustaría verificar para cada restricción en S si la fórmula es aún satisfactoria al agregar la restricción al solucionador. Esto se puede hacer fácilmente de forma secuencial de tal manera:

results = []

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

print all(results)

Ahora, me gustaría paralelizar esto para acelerar las cosas, pero no estoy seguro de cómo hacerlo correctamente con z3.

Aquí hay un intento. Considere el siguiente ejemplo sencillo. Todas las variables son enteros no negativos y tienen que sumar 1. Ahora me gustaría verificar si cada variable x puede hacerse independientemente> 0. Obviamente es el caso; deje x = 1 y asigne 0 a las otras variables. Aquí hay una posible implementación paralela:

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)

Sorprendentemente, esto funciona perfectamente en mi máquina: los resultados son sólidos y es mucho más rápido. Sin embargo, dudo que sea seguro, ya que estoy trabajando en un único solucionador global y puedo imaginar fácilmente que los push / pop ocurran al mismo tiempo. ¿Hay alguna manera limpia / segura de lograr esto con z3py?

Answer 1

De hecho, esto podría funcionar para una primera prueba, pero no en general. No se admite la resolución paralela en un contexto único y definitivamente habrá carreras de datos y segmentaciones posteriores.

En Python, el objeto Context está oculto, por lo que la mayoría de los usuarios no tendrán que lidiar con él, pero para ejecutar cosas en paralelo, necesitamos configurar un Contexto por hilo y luego pasar el correcto a todas las demás funciones (lo que implícitamente utilizó el contexto oculto antes). Tenga en cuenta que todas las expresiones, los solucionadores, las tácticas, etc., dependen de un Contexto particular, de modo que si los objetos necesitan cruzar ese límite, necesitamos traducirlos (vea translate (...) en AstRef y similares).

Ver también Z3 con múltiples hilos? y ¿ Cuándo se reactivará la versión paralela Z3?