Z3：非增量搜索多个模型有效，增量搜索不起作用

Question

在某个区间内搜索多项式的所有零点时，我遇到了 Z3 的一个有趣行为。 这是我的问题陈述：

(declare-fun perr () Real)
(assert
 (let (($x10 (<= perr 1.0)))
 (and (<= 0.0 perr) $x10)))
(assert
 (let ((?x64 (^ perr 8.0)))
 (let ((?x65 (* (- 9.0) ?x64)))
 (let ((?x59 (^ perr 6.0)))
 (let ((?x60 (* (- 4032.0) ?x59)))
 (let ((?x55 (^ perr 5.0)))
 (let ((?x56 (* 8064.0 ?x55)))
 (let ((?x51 (^ perr 4.0)))
 (let ((?x52 (* (- 10080.0) ?x51)))
 (let ((?x46 (^ perr 3.0)))
 (let ((?x47 (* 8064.0 ?x46)))
 (let ((?x41 (^ perr 2.0)))
 (let ((?x42 (* (- 4032.0) ?x41)))
 (let ((?x69 (* 1152.0 perr)))
 (let ((?x33 (^ perr 7.0)))
 (let ((?x34 (* 1152.0 ?x33)))
 (= (+ ?x34 ?x69 ?x42 ?x47 ?x52 ?x56 ?x60 ?x65) 144.0)))))))))))))))))
(check-sat)
(get-model)

这给了我模型

(
    (define-fun perr () Real
        (root-obj (+ (^ x 8) (* (- 128) (^ x 7)) (* 448 (^ x 6)) (* (- 896) (^ x 5)) (* 1120 (^ x 4)) (* (- 896) (^ x 3)) (* 448 (^ x 2)) (* (- 128) x) 16) 1))
)

我可以向Z3询问其他型号：

(declare-fun perr () Real)
(assert
 (let (($x10 (<= perr 1.0)))
 (and (<= 0.0 perr) $x10)))
(assert
 (let ((?x64 (^ perr 8.0)))
 (let ((?x65 (* (- 9.0) ?x64)))
 (let ((?x59 (^ perr 6.0)))
 (let ((?x60 (* (- 4032.0) ?x59)))
 (let ((?x55 (^ perr 5.0)))
 (let ((?x56 (* 8064.0 ?x55)))
 (let ((?x51 (^ perr 4.0)))
 (let ((?x52 (* (- 10080.0) ?x51)))
 (let ((?x46 (^ perr 3.0)))
 (let ((?x47 (* 8064.0 ?x46)))
 (let ((?x41 (^ perr 2.0)))
 (let ((?x42 (* (- 4032.0) ?x41)))
 (let ((?x69 (* 1152.0 perr)))
 (let ((?x33 (^ perr 7.0)))
 (let ((?x34 (* 1152.0 ?x33)))
 (= (+ ?x34 ?x69 ?x42 ?x47 ?x52 ?x56 ?x60 ?x65) 144.0)))))))))))))))))
(assert
 (not (= perr (root-obj (+ (^ x 8) (* (- 128) (^ x 7)) (* 448 (^ x 6)) (* (- 896) (^ x 5)) (* 1120 (^ x 4)) (* (- 896) (^ x 3)) (* 448 (^ x 2)) (* (- 128) x) 16) 1))))
(check-sat)

这给了我

unsat

但是如果我增量这样做，求解器将无法找到

unsat

并且超时：

(declare-fun perr () Real)
(assert
 (let (($x10 (<= perr 1.0)))
 (and (<= 0.0 perr) $x10)))
(assert
 (let ((?x64 (^ perr 8.0)))
 (let ((?x65 (* (- 9.0) ?x64)))
 (let ((?x59 (^ perr 6.0)))
 (let ((?x60 (* (- 4032.0) ?x59)))
 (let ((?x55 (^ perr 5.0)))
 (let ((?x56 (* 8064.0 ?x55)))
 (let ((?x51 (^ perr 4.0)))
 (let ((?x52 (* (- 10080.0) ?x51)))
 (let ((?x46 (^ perr 3.0)))
 (let ((?x47 (* 8064.0 ?x46)))
 (let ((?x41 (^ perr 2.0)))
 (let ((?x42 (* (- 4032.0) ?x41)))
 (let ((?x69 (* 1152.0 perr)))
 (let ((?x33 (^ perr 7.0)))
 (let ((?x34 (* 1152.0 ?x33)))
 (= (+ ?x34 ?x69 ?x42 ?x47 ?x52 ?x56 ?x60 ?x65) 144.0)))))))))))))))))
(check-sat)
(get-model)
(assert
 (not (= perr (root-obj (+ (^ x 8) (* (- 128) (^ x 7)) (* 448 (^ x 6)) (* (- 896) (^ x 5)) (* 1120 (^ x 4)) (* (- 896) (^ x 3)) (* 448 (^ x 2)) (* (- 128) x) 16) 1))))
(check-sat)

为什么会发生这种情况？我想区别在于 Z3 已经知道一些子句，这使它无法找到

unsat

。 谷歌搜索这个问题，似乎增量解决总是好的，所以它在这里有更糟糕的结果似乎很奇怪。

Answer 1

这是不幸的，但一点也不意外。与一次性求解器相比，增量模式使用不同的启发式方法。通常的技巧是查看详细输出（使用

-v:10

或类似命令运行它），并查看内部策略的作用。当然，详细输出即使不是不可能，也可能很难破译。但它通常表明求解器“卡住”的地方。

这样做，我能够使用以下命令让它在增量情况下终止：

(check-sat-using qfnra-nlsat)

而不是普通的

check-sat

。您是否应该始终使用它是一个有趣的问题。这完全是针对具体问题的。但上面的咒语解决了你当前的问题。

您可以在 https://github.com/Z3Prover/z3/discussions 提出这个问题，开发人员可能会有更好的建议。