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。

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

Answer 1

我猜你说的不同是指不同的模型。如果结果从sat更改为unsat，则这是一个bug。

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

请参阅以下相关问题：

• Z3 timing variation