Z3 结果的随机性

Question

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

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 求解器并检查同一查询的可满足性。查询是located here。

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

Answer 1

我假设您所说的不同是指不同的模型。 如果结果从 sat 变为 unsat，那么它就是一个 bug。

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

请参阅以下相关问题：

• Z3 timing variation