Z3:检查型号是否唯一 [英] Z3: Check if model is unique

问题描述

Z3中是否有办法证明/显示给定模型是唯一的，并且不存在其他解决方案?

Is there a way in Z3 to prove/show that a given model is unique and that no other solution exists?

一个小例子来演示

(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选项或添加断言来确保这一点吗?

I know for a fact that the following model is unique, but can I ensure this using either some Z3 option or adding assertions?

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

为澄清起见，我正在通过de JAVA API使用Z3

For clarification, I'm using Z3 through de JAVA API

推荐答案

是的:我们的想法是断言由找到的模型分配的值是唯一可能的分配，因此它是唯一的.可以通过添加一个声明来声明所有常数不等于为其分配的模型值.

Yes: the idea is to assert that the values assigned by the found model are the only possible assignments, and hence it is unique. This can be done by adding one assertion that states that all the constants are NOT equal to their assigned model values.

以您的示例为例，

(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

If you try changing any of the values (e.g., change c3 = 3 to c3 = 4) this will again become satisfiable. Here's a rise@fun link to your complete example: http://rise4fun.com/Z3/nD5n

有关如何使用API​​以编程方式执行此操作的更多详细信息，请参阅以下问题和答案:

For more details on how to do this programmatically using the APIs, see these questions and answers:

Z3:找到所有令人满意的模型

(Z3Py)检查方程的所有解

请注意，根据第二个链接的答案中的注释，您不能仅使用SMT-lib前端以编程方式执行此操作，如果要自动执行此过程，则必须使用API​​遍历找到的模型.

Note that as per comments in the second linked answer, you cannot do this programmatically using just the SMT-lib frontend, you have to use an API to traverse the found model if you want to automate this process.

这篇关于Z3:检查型号是否唯一的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！