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 до с3 = 4), это снова станет выполнимой. Вот рост @ весело ссылку на ваш полный пример: http://rise4fun.com/Z3/nD5n

Для получения более подробной информации о том, как это сделать программно с помощью API-интерфейсов, чтобы эти вопросы и ответы:

Z3: finding all satisfying models

(Z3Py) checking all solutions for equation

Примечание что согласно комментариям во втором связанном ответе вы не можете делать это программно, используя только интерфейс SMT-lib, вам нужно использовать API для перемещения найденной модели, если вы хотите автоматизировать этот процесс.