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

Question

我使用 Z3 和 JAVA 绑定已有 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 打印表达式然后解析它们。

Answer 2

我想我发现了产生这些奇怪相反行为的代码的特定部分。 如果我完全错了，也许周围的 Z3 专家可以告诉我。

首先，如果我在程序的一次运行中尝试两次相同的代码（无论是手动生成的代码还是使用 API 生成的代码），有时我会得到不同的模型。这是我以前没有注意到的，这对我来说实际上不是一个真正的问题。

然而，我主要担心的是如果我运行我的程序两次，在两次运行期间检查完全相同的代码会发生什么。

当我手动生成代码时，我最终会得到这样的函数定义：

(declare-fun var!0 () Int)
(declare-fun var!2 () Int)
(declare-fun var!42 () Int)

(assert (and
    (or (= var!0 0) (= var!0 1))
    (or (= var!2 0) (= var!2 1))
    (or (= var!42 0) (= var!42 1))
))

(define-fun fun ((i! Int)) Int
    (ite (= i! 0) var!0
        (ite (= i! 1) var!2
            (ite (= i! 2) var!42 -1)
        )
    )            
)

据我所知（以及我所读到的有关它的内容（参见here）），API 无法处理我定义“有趣”函数的方式。 所以我用 API 定义它是这样的：

(declare-fun var!0 () Int)
(declare-fun var!2 () Int)
(declare-fun var!42 () Int)

(assert (and
    (or (= var!0 0) (= var!0 1))
    (or (= var!2 0) (= var!2 1))
    (or (= var!42 0) (= var!42 1))
))

(declare-fun fun (Int) Int)
(assert (forall
    ((i! Int))
    (ite (= i! 0) (= (fun i!) var!0)
        (ite (= i! 1) (= (fun i!) var!2)
            (ite (= i! 2) (= (fun i!) var!42) (= (fun i!) -1))
        )
    )
))

似乎对于第一种方法，总是（或至少经常检查不同运行的相同代码，这对我来说不是一个真正的问题）给出了相同的模型。 p>

使用第二种方法，经常检查不同运行的相同代码会产生不同模型。

谁能告诉我我所揭露的关于 Z3 实际工作原理的背后是否确实存在一些逻辑？

因为我需要我的结果尽可能可重现，所以我回到了手动代码生成，它似乎工作得非常好。我希望在 API 中看到一个函数，允许我们直接定义函数，而不必使用“forall”方法，看看我刚才描述的是否正确。