与z3并行求解公式 [英] Solving formulas in parallel with z3
问题描述
假设我有一个z3求解器，其中包含一定数量的可满足的已声明约束.假设S为一组约束，我想为S中的每个约束验证将约束添加到求解器时公式是否仍可满足.以这种方式可以很容易地按顺序完成此操作:
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)
现在，我想对此并行化以加快处理速度，但是我不确定如何在z3上正确地做到这一点.
Now, I would like to parallelize this to speed things up, but I'm not sure how to do it properly with z3.
这里是尝试.考虑下面的简单示例.所有变量都是非负整数，必须求和为1.现在，我想验证每个变量x是否可以独立设为> 0.令x = 1并将0赋给其他变量.这是一个可能的并行实现:
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)
令人惊讶的是，这在我的机器上可以完美地工作:结果是声音，而且速度要快得多.但是，我怀疑它是否安全，因为我正在使用单个全局求解器，并且我可以轻松想象出推送/弹出会同时发生.是否有任何干净/安全的方法可以使用z3py实现此目标?
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?
推荐答案
的确，这可能适用于首次测试，但一般而言并非如此.不支持在单个上下文上并行解决问题，并且以后肯定会有数据争用和段错误.
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.
在Python中，Context对象是隐藏的，因此大多数用户无需处理它，但是要并行运行，我们需要为每个线程设置一个Context，然后将正确的对象传递给所有其他函数(之前隐式使用了隐藏的Context).请注意，所有表达式，求解器，策略等均取决于一个特定的上下文，因此，如果对象需要跨越该边界，则需要对其进行翻译(请参阅AstRef和类似文件中的translate(...)).
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).
