爲什麼這個非線性實例不能被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)。