为什么这个非线性实例不能用 QF_NRA 求解器求解，但可以用默认求解器求解？

Question

下面的SMT2实例可以求解（是UNSAT），但是如果我用qfnra求解器，结果未知

(declare-fun NONDET_INT_32_1 () Int)
(declare-fun lv_n_1_1 () Int)
(declare-fun lv_n_8_1 () Bool)
(declare-fun lv_n_9_1 () Int)
(declare-fun lv_n_10_1 () Bool)
(declare-fun lv_n_18_1 () Bool)
(declare-fun lv_n_19_1 () Int)
(declare-fun lv_n_15_1 () Real)
(declare-fun lv_n_14_1 () Int)
(assert (and true
     (not (distinct lv_n_19_1 0))
     (= lv_n_14_1 (* lv_n_1_1 lv_n_1_1))
     (= lv_n_15_1 (to_real lv_n_14_1))
     (= lv_n_18_1 (distinct (- lv_n_15_1 2.0) 0.0))
     (= lv_n_19_1 (ite lv_n_18_1 1 0))
     lv_n_10_1
     (= lv_n_9_1 (ite lv_n_8_1 1 0))
     (= lv_n_10_1 (distinct lv_n_9_1 0))
     (= lv_n_8_1 (<= lv_n_1_1 10))
     (>= lv_n_1_1 (- 10))
     (= lv_n_1_1 NONDET_INT_32_1)
     ))
;(check-sat-using (then simplify sat qfnra))
(check-sat)

为什么会这样？

Answer 1

你的问题不在QF_NRA逻辑上，因为你的问题是整数。 (check-sat-using (then simplify sat qfnra)) 行将强制 Z3 仅使用 simplify、sat 和 qfnra 策略。如果你只写 (check-sat)，Z3 将使用其内置的 default 策略，应用多个预处理步骤，然后使用最强大的适用求解器。

某些涉及整数的问题确实可以被 qfnra 求解器证明不满足，因为如果没有满足给定公式的实数，那么也没有满足该公式的整数，给定整数是实数的子集。但是，这是一种特殊情况，显然你的公式不属于这一类。

通常情况下，你会在Z3中使用默认策略得到最好的结果，所以你的结果对我来说并不奇怪。您可以使用默认策略 (check-sat)，或者如果您想将其与其他专门策略结合使用 (check-sat-using default)。

为什么这个非线性实例不能用 QF_NRA 求解器求解，但可以用默认求解器求解？

Why can this nonlinear instance not be solved by the QF_NRA solver, but can be solved by the default solver?

z3