4

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)
)

明確にするために、JAVA APIを介してZ3を使用しています

4

1 に答える 1

6

はい: アイデアは、見つかったモデルによって割り当てられた値が唯一の可能な割り当てであり、したがって一意であると断言することです。これは、すべての定数が割り当てられたモデル値と等しくないことを示す 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 に変更)、これは再び満足できるものになります。完全な例へのrise@funリンクは次のとおりです：http://rise4fun.com/Z3/nD5n

API を使用してプログラムでこれを行う方法の詳細については、次の質問と回答を参照してください。

Z3: 満足のいくモデルをすべて見つける

(Z3Py) 方程式のすべての解をチェック

2番目のリンクされた回答のコメントによると、SMT-libフロントエンドだけを使用してプログラムでこれを行うことはできません。このプロセスを自動化する場合は、APIを使用して見つかったモデルをトラバースする必要があります。

于 2013-04-14T16:17:26.247 に答える