無法解釋如何進行簡單的調整導致「未知」Z3結果

Question

我正在學習Z3。我正在使用一些簡單的「isPrime」函數，並偶然發現了一些難以理解的行爲。看似「更簡單」的內聯公式(> q 1)導致「未知」，而更復雜的定義樂趣（宏）(isPrime q)導致快速解決方案，即使(isPrime q)包含(> q 1)。 http://rise4fun.com/Z3/slg2D。

(define-fun isPrime ((x Int)) Bool 
    (and (> x 1) (not (exists ((z Int) (y Int)) (and (not (= y x)) (and (not (= z x)) (and (> y 1) (> z 1) (= x (* y z))))))))) 
(declare-const q Int) 
(declare-const r Int) 
(assert (and 
    ;with this the '+ 2' variation is sat: 5, 3 
    ;(isPrime q) 
    (> q 1) 
    (> r 1) 
    ;always answers sat: 2, 2 
    ;(isPrime (+ (* q r) 1)) 
    ;unknown 
    (isPrime (+ (* q r) 2)) 
)) 
(check-sat) 
(get-model) 

Answer 1

量化邏輯是一種先進的功能，你應該閱讀有關Z3如何解決這些公式，這將使你的角度上，你可以從Z3的期望。用量詞來解決公式是一種微妙的藝術，以我卑微的經驗。對你來說很明顯的事情，對Z3來說可能並不明顯。

你有一個forall量詞（你把它寫成not exists），Z3會試圖滿足。我猜Z3正在挑選一些q和r，然後檢查isPrime是否成立，否則它會嘗試使用新的對，依此類推。如果Z3沒有做出正確的選擇，它可能需要一段時間，直到找到這樣的q和r，所以也許你應該給它更多的時間（解決rise4fun問題有超時）。

另一種進行的方式可能是幫助 Z3多一點。例如，讓它知道z和y小於x。這樣你可以爲這些變量提供一個下限和一個上限。

(define-fun isPrime ((x Int)) Bool 
    (and (> x 1) (not (exists ((z Int) (y Int)) (and (< y x) (and (< z x) (and (> y 1) (> z 1) (= x (* y z))))))))) 

This適合我。

更新

參考文獻：

1. 萊昂納多·德莫拉的上SAT/SMT暑期學校2012（https://es-static.fbk.eu/events/satsmtschool12/）
2. Z3教程，量詞（http://rise4fun.com/Z3/tutorial/guide）
3. 通用Z3教程談話（http://research.microsoft.com/en-us/um/redmond/projects/z3/mbqi-tutorial/main.html）