与z3并行求解公式

Question

假设我有一个z3求解器，其中包含一定数量的可满足的已声明约束。假设S为一组约束，我想为S中的每个约束验证将约束添加到求解器时公式是否仍可满足要求。可以通过以下方式轻松地按顺序完成此操作：

results = []

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

print all(results)

现在，我想并行化它来加快处理速度，但是我不确定如何使用z3正确地执行此操作。

这是一个尝试。考虑下面的简单示例。所有变量都是非负整数，并且必须求和为1。现在，我想验证每个变量x是否可以独立地设为> 0。令x = 1并将0赋给其他变量。这是一个可能的并行实现：

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)

出乎意料的是，这在我的机器上完美地工作了：结果是声音而且速度更快。但是，我怀疑它是否安全，因为我正在使用单个全局求解器，并且我可以轻松想象出推送/弹出会同时发生。z3py是否有任何干净/安全的方法来实现这一目标？

Answer 1

实际上，这可能适用于第一次测试，但一般情况下不适用。不支持在单个上下文上并行求解，以后肯定会出现数据竞争和段错误。

在 Python 中，Context 对象是隐藏的，因此大多数用户不必处理它，但是要并行运行，我们需要为每个线程设置一个 Context，然后将正确的一个传递给所有其他函数（隐式地）之前使用了隐藏的上下文）。请注意，所有表达式、求解器、策略等都取决于一个特定的上下文，因此如果对象需要跨越该边界，我们需要转换它们（请参阅 AstRef 中的 translate(...) 等）。

另请参阅多线程 Z3？而当将Z3水货版本被重新激活？