python - 与 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)

令人惊讶的是，这在我的机器上运行得很好:结果很好，而且速度更快。但是，我怀疑它是否安全，因为我正在处理一个全局求解器，而且我可以很容易地想象 push/pops 是同时发生的。有什么干净/安全的方法可以用 z3py 实现这一点吗？

Answer 1

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

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

另见 Multi-threaded Z3?和 When will the Z3 parallel version be reactivated?