Z3 中的回溯增加了求解器找到答案的时间

Question

我有一个用 Java 实现的工具。 我们使用Java JNI 连接了 Z3 Sat Solver C-API。 我正在使用 Z3 4.1 版

鉴于这种情况，我做了以下实验-

实验 1 -

1. 我在 Solver 中声明了一些约束。
2. 我检查结果是饱和还是不饱和。

实验 2 -

1. 我在 Solver 中声明了相同约束的子集。
2. 我使用 Z3_solver_push() API 推送求解器的上下文。
3. 我断言剩余的约束。
4. 我检查结果是饱和还是不饱和。

我做实验 2 的原因是需要回溯。

现在在实验 1 中，我得到查询所需的时间始终小于 5 秒。到目前为止，我已经检查了大约 20-30 次。有时甚至不到 2 秒。

现在进行实验 2，注意约束完全相同的事实，我得到的查询时间有时是 5 秒，有时是 10 秒，有时是 50 秒。我还看到查询是“超时”，超时为 60 秒。

为了消除一些疑虑，我从命令行执行了相同的实验。 通过实验一，我发现查询时间总是在 2.3 - 2.7 秒之间。 然而，对于实验 2，（我手动放置了 push 语句），时间变得如前所述的可变。它在 10-60 秒之间变化。

我想知道pushing的上下文是否会导致查询的这种变化？ 理想情况下不应该。但是有机会吗？

我们如何避免这种随机性并获得类似于没有push 语句的稳定行为？

更新

我已经添加了示例约束，我想找出使用​​哪种策略。 请注意，它无法重现实验中提到的问题。但是，我们使用了多个这样的约束，如下所示，这可以重现问题 -

(set-option :produce-models true) ; enable model generation
(set-option :print-success false)
(declare-const goal1 Int)
(declare-const goal2 Int)
(declare-const goal3 Int)
(declare-const kmax Int)
(declare-const ordA0_A0 Bool)
(declare-const ordA0_B0 Bool)
(declare-const ordB0_B0 Bool)
(declare-const ordB0_A0 Bool)
(declare-const stA0 Int)
(declare-const stB0 Int)
(declare-const stPA_0 Int)
(declare-const enPA_0 Int)
(declare-const stPB_0 Int)
(declare-const enPB_0 Int)
(declare-const kstA0 Int)
(declare-const kyA_0 Int)
(declare-const kstB0 Int)
(declare-const kyB_0 Int)
(declare-const resA_0 Int)
(declare-const resB_0 Int)

(assert (if (>= stPA_0 enPA_0) (= ordA0_A0 true) (= ordA0_A0 false)))
(assert (if (>= stPB_0 enPB_0) (= ordB0_B0 true) (= ordB0_B0 false)))
(assert (if (>= stPA_0 enPB_0) (= ordB0_A0 true) (= ordB0_A0 false)))
(assert (if (>= stPB_0 enPA_0) (= ordA0_B0 true) (= ordA0_B0 false)))

(assert (and (>= stA0 0) (<= stA0 goal2)))
(assert (and (>= stB0 0) (<= stB0 goal2)))
(assert (or (= stA0 0) (= stB0 0)))
(assert (>= stB0 (+ stA0 1)))
(assert (=> (and (= resA_0 resB_0) (= ordA0_A0 false) (= ordB0_B0 false)) (or (= ordA0_B0 true) (= ordB0_A0 true))))
(assert (=> (and (= resA_0 resB_0) (or (= ordA0_A0 true) (= ordB0_B0 true))) (and (= ordA0_B0 true) (= ordB0_A0 true))))

(assert (and (>= resA_0 0) (< resA_0 goal3)))
(assert (and (>= resB_0 0) (< resB_0 goal3)))

(assert (=> (= resA_0 resB_0) (or (= ordA0_A0 false) (= ordB0_B0 false))))

(assert (= stPA_0 (- stA0 (* goal1 kstA0))))
(assert (= enPA_0 (- (+ stA0 1) (* goal1 kyA_0))))
(assert (= stPB_0 (- stB0 (* goal1 kstB0))))
(assert (= enPB_0 (- (+ stB0 2) (* goal1 kyB_0))))
(assert (= kstA0 (div stA0 goal1)))
(assert (= kyA_0 (div (+ stA0 1) goal1)))
(assert (= kstB0 (div stB0 goal1)))
(assert (= kyB_0 (div (+ stB0 2) goal1)))
(assert (= goal2 (+ stB0 1)))
(assert (>= goal1 1))
(assert (<= goal2 6))
(assert (= kmax (div 6 goal1)))
(assert (<= goal2 6))
(assert (<= goal3 5))
(assert (= goal1 3))

(check-sat)
(get-model)

Answer 1

Z3 是求解器的集合。默认求解器对象是求解器组合。并非投资组合中的每个求解器都是增量的。只要我们使用Z3_solver_push()，它将使用通用增量求解器。这种通用求解器可能比非增量求解器效率低得多。即使使用Z3_solver_push()，您也可以强制 Z3 使用非增量求解器。但是，对于每个 check，Z3 将从头开始，并且不会重用以前的 check 查询中的任何工作。

用于创建非增量求解器的主要 API 是 Z3_mk_solver_from_tactic。