java – Z3：检查模型是否唯一

内容导读

互联网集市收集整理的这篇技术教程文章主要介绍了java – Z3：检查模型是否唯一，小编现在分享给大家，供广大互联网技能从业者学习和参考。文章包含2341字，纯文字阅读大概需要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)
)

为了澄清,我正在使用Z3到de JAVA API

解决方法:

是的：我们的想法是断言找到的模型分配的值是唯一可能的分配,因此它是唯一的.这可以通过添加一个声明所有常量不等于其指定模型值的断言来完成.

对于您的示例,这将是：

(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),这将再次变得令人满意.这是一个上升的@ fun链接到您的完整示例：http://rise4fun.com/Z3/nD5n

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

Z3: finding all satisfying models

(Z3Py) checking all solutions for equation

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

内容总结

以上是互联网集市为您收集整理的java – Z3：检查模型是否唯一全部内容，希望文章能够帮你解决java – Z3：检查模型是否唯一所遇到的程序开发问题。 如果觉得互联网集市技术教程内容还不错，欢迎将互联网集市网站推荐给程序员好友。

内容备注

版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 gblab@vip.qq.com 举报，一经查实，本站将立刻删除。

内容手机端