java - Z3多次运行时产生不同的模型

Question

我使用 Z3 和 JAVA 绑定(bind)已经有 2 年了。由于某种原因，我总是自己生成 SMTLib2 代码作为字符串，然后使用 parseSMTLib2String 构建相应的 Z3 Expr。据我所知，每次我用这种方法两次输入完全相同的输入时，我总是得到相同的模型。

但我最近决定更改并直接使用 JAVA API 并使用 ctx.mk...() 构建表达式。基本上，我不会生成字符串然后解析它，而是让 Z3 完成构建 Z3 Expr 的工作。

现在发生的情况是，当我检查求解器确实存储了完全相同的代码时，我得到了不同的模型。我的 JAVA 代码如下所示:

static final Context context = new Context();
static final Solver solver = context.mkSolver();

public static void someFunction(){
    solver.add(context.mk...()); // Add some bool expr to the solver
    Status status = solver.check();
    if(status == SATISFIABLE){
        System.out.println(solver.getModel()); // Prints different model with same expr
    }
}

我在运行时对“someFunction()”进行了超过 1 次调用，并且检查的表达式 context.mk...() 发生了变化。但是，如果我运行程序两次，则会检查相同的表达式序列，有时会从一次运行到另一次运行给出不同的模型。

我尝试禁用自动配置参数并设置我自己的随机种子，但 Z3 有时仍然会产生不同的模型。我只使用有界整数变量和未解释的函数。我是否以错误的方式使用 API？

如果需要，我可以将整个 SMTLib2 代码添加到这个问题中，但它并不短，并且包含多个求解器调用(我什至不知道其中哪个会从一次执行到另一次执行产生不同的模型，我只是知道有些人这样做)。

我必须明确指出，我已阅读以下主题，但发现答案要么已过时，要么(如果我理解正确)支持“Z3 是确定性的，应该为相同的输入生成相同的模型”:

Z3 timing variation

Randomness in Z3 Results

different run time for the same code in Z3

编辑:令人惊讶的是，通过以下代码，我似乎总是得到相同的模型，而 Z3 现在似乎是确定性的。然而，与我之前的代码相比，内存消耗是巨大的，因为我需要将上下文保留在内存中一段时间​​。知道我可以做什么来以更少的内存使用来实现相同的行为吗？

public static void someFunction(){
    Context context = new Context();
    Solver solver = context.mkSolver();
    solver.add(context.mk...()); // Add some bool expr to the solver
    Status status = solver.check();
    if(status == SATISFIABLE){
        System.out.println(solver.getModel()); // Seem to always print the same model :-)
    }
}

这是我多次调用“someFunction”方法得到的内存消耗:

Answer 1

只要它不在同一问题上在 SAT 和 UNSAT 之间切换，就不是错误。

您链接的答案之一解释了正在发生的事情:

Randomness in Z3 Results

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

也许在解析时它会分配相同的 id，而使用 API 时它可能会有所不同，尽管我发现有点难以相信......

如果您需要此行为，并且确定它是通过 SMT 编码执行此操作，则您始终可以从 API 打印表达式，然后解析它们。