Z3 结果中的随机性 [英] Randomness in Z3 Results

问题描述

我正在使用 Z3 Python 接口作为我正在编写的研究工具的一部分，当我在同一个查询上重复运行 Z3 求解器时，我注意到一些非常奇怪的行为:特别是，我似乎没有得到相同的结果每次都会得到结果，即使我在运行前明确重置了求解器.作为参考，这是我的代码:

I am using the Z3 Python interface as part of a research tool that I am writing, and I noticed some pretty odd behavior when I run the Z3 solver repeatedly on the same query: In particular, I seem to not get the same results each time, even though I explicitly reset the solver before running. For reference, here's my code:

import z3

with open("query.smt", "r") as smt_reader:
    query_lines = "".join(smt_reader.readlines())
    for i in xrange(3):
        solver = z3.Solver()
        solver.reset()

        queryExpr = z3.parse_smt2_string(query_lines)
        equivalences = queryExpr.children()[:-1]
        for equivalence in equivalences:
            solver.add(equivalence)

        # Obtain the Boolean variables associated with the constraints.
        constraintVars = [equivalence.children()[0] for equivalence
                          in equivalences]
        # Check the satisfiability of the query.
        querySatResult = solver.check(*constraintVars)

        print solver.model().sexpr()
        print solver.statistics()
        print ""

上面的代码三次重新创建 Z3 求解器并检查同一查询的可满足性.查询位于位于此处.

The code above re-creates the Z3 solver thrice and checks the satisfiability of the same query. The query is located here.

虽然上面的代码部分并不是我将如何使用 Z3 Python 接口，但问题源于一个认识，即 Z3 求解器在同一查询的不同代码点调用两次时，返回不同的结果.我想知道这是否是故意的，是否有任何方法可以禁用它或确保确定性.

While the above section of code is not exactly how I will be using the Z3 Python interface, the problem stemmed from a realization that the Z3 solver, when called twice at different points of the code on the same query, returned different results. I was wondering if this was intentional, and whether there was any way to disable this or to ensure determinism.

推荐答案

我假设不同的意思是不同的模型.如果结果从sat变成unsat，那就是bug了.

I'm assuming by different you meant a different model. If the result changes from sat to unsat, then it is a bug.

话虽如此，如果我们在同一执行路径中解决同一个问题两次，那么 Z3 可以产生不同的模型.Z3 为表达式分配内部唯一 ID.内部 ID 用于打破 Z3 使用的某些启发式方法中的关系.请注意，程序中的循环正在创建/删除表达式.因此，在每次迭代中，表示约束的表达式可能具有不同的内部 ID，因此求解器可能会生成不同的解决方案.

That being said, if we solve the same problem twice in the same execution path, then Z3 can produce different models. Z3 assigns internal unique IDs to expressions. The internal IDs are used to break ties in some heuristics used by Z3. Note that the loop in your program is creating/deleting expressions. So, in each iteration, the expressions representing your constraints may have different internal IDs, and consequently the solver may produce different solutions.

请参阅以下相关问题:

• Z3 时序变化

这篇关于Z3 结果中的随机性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！