Z3：檢查模型是否唯一

Question

在Z3中有沒有一種方法可以證明/顯示給定的模型是唯一的，並且沒有其他解決方案存在？

一個小例子來說明

(declare-const a1 Int) 
(declare-const a2 Int) 
(declare-const a3 Int) 
(declare-const b1 Int) 
(declare-const b2 Int) 
(declare-const b3 Int) 
(declare-const c1 Int) 
(declare-const c2 Int) 
(declare-const c3 Int) 
(declare-const ra Int) 
(declare-const rb Int) 
(declare-const rc Int) 
(declare-const r1 Int) 
(declare-const r2 Int) 
(declare-const r3 Int) 
(assert (>= a1 0)) 
(assert (>= a2 0)) 
(assert (>= a3 0)) 
(assert (>= b1 0)) 
(assert (>= b2 0)) 
(assert (>= b3 0)) 
(assert (>= c1 0)) 
(assert (>= c2 0)) 
(assert (>= c3 0)) 
(assert (<= a1 9)) 
(assert (<= a2 9)) 
(assert (<= a3 9)) 
(assert (<= b1 9)) 
(assert (<= b2 9)) 
(assert (<= b3 9)) 
(assert (<= c1 9)) 
(assert (<= c2 9)) 
(assert (<= c3 9)) 
(assert (= ra 38)) 
(assert (= rb 1)) 
(assert (= rc 27)) 
(assert (= r1 55)) 
(assert (= r2 72)) 
(assert (= r3 6)) 
(assert (= ra (- (* a1 a2) a3))) 
(assert (= rb (- (- b1 b2) b3))) 
(assert (= rc (* (* c1 c2) c3))) 
(assert (= r1 (- (* a1 b1) c1))) 
(assert (= r2 (* (+ a2 b2) c2))) 
(assert (= r3 (- (+ a3 b3) c3))) 
(check-sat) 
(get-model) 

我知道一個事實，即下面的模型是獨一無二的，但我可以保證這一點無論是使用一些Z3選項或添加斷言？

(model 
    (define-fun c3() Int 
    3) 
    (define-fun c2() Int 
    9) 
    (define-fun c1() Int 
    1) 
    (define-fun b3() Int 
    5) 
    (define-fun b2() Int 
    2) 
    (define-fun b1() Int 
    8) 
    (define-fun a3() Int 
    4) 
    (define-fun a2() Int 
    6) 
    (define-fun a1() Int 
    7) 
    (define-fun r3() Int 
    6) 
    (define-fun r2() Int 
    72) 
    (define-fun r1() Int 
    55) 
    (define-fun rc() Int 
    27) 
    (define-fun rb() Int 
    1) 
    (define-fun ra() Int 
    38) 
) 

爲了澄清，我使用Z3通過德JAVA API

Answer 1

是：這個想法是斷言，在發現模式分配的值是唯一可能的分配，因此它是獨一無二的。這可以通過添加一個斷言來完成，該斷言聲明所有常量不等於其分配的模型值。

對於你的榜樣，這將是：

(assert (not (and 
    (= c3 3) 
    (= c2 9) 
    (= c1 1) 
    (= b3 5) 
    (= b2 2) 
    (= b1 8) 
    (= a3 4) 
    (= a2 6) 
    (= a1 7) 
    (= r3 6) 
    (= r2 72) 
    (= r1 55) 
    (= rc 27) 
    (= rb 1) 
    (= ra 38)))) 
(check-sat) ; unsat => no other model exists 

如果你嘗試更改任何值（例如，改變C3 = 3〜C3 = 4），這將再次成爲滿足的。這裏有一個上升@有趣鏈接到你的完整的例子：http://rise4fun.com/Z3/nD5n

有關如何做到這一點編程方式使用API​​的更多詳細信息，請參閱這些問題和答案：

Z3: finding all satisfying models

(Z3Py) checking all solutions for equation

注根據第二個鏈接答案中的註釋，不能僅使用SMT-lib前端以編程方式執行此操作，如果要自動執行此過程，則必須使用API​​來遍歷找到的模型。