在 Z3py 中重复匹配的模型答案

【问题标题】：Repeating the matched models in Z3py在 Z3py 中重复匹配的模型
【发布时间】：2013-02-25 17:47:42
【问题描述】：

在下面的工作示例中，我试图检索匹配的模型，在这种情况下有两个令人满意的模型：

 t1= cl7          t2= cl4      t3= cl5

和

 t1= cl4          t2= cl3      t3= cl9

问题是重复匹配的模型，直到正在运行的求解器超时。如何在不重复的情况下检索满意的模型。

非常感谢，

        S, (cl1, cl2, cl3, cl4, cl5, cl6, cl7,cl8,cl9) = EnumSort('S', ['cl1', 'cl2', 'cl3', 'cl4', 'cl5','cl6' ,'cl7', 'cl8', 'cl9'])



       s = Solver()

       x = Const('x', S)
      def fun1(x):
        return Or(x == cl1, x == cl2, x == cl3, x == cl4, x == cl5, x == cl6, x == cl7, x == cl8, x == cl9)


       y1, y2 = Consts('y1 y2', S)
      def fun2(y1, y2):
          return Or(And(y1 == cl7, y2 == cl4), And(y1 == cl4, y2 == cl3), And(y1 == cl3, y2 == cl2),And(y1 == cl8, y2 == cl9))


      q1,q2 = Consts('q1 q2', S)
      def fun3(q1,q2):
        return Or(And(q1 == cl7, q2 == cl5), And(q1 == cl4, q2 == cl9))



 t1, t2 ,t3 = Consts('t1 t2 t3', S)

 s.add(fun1(t1))
 s.add(fun2(t1,t2))
 s.add(fun3(t1,t3))


while s.check() == sat:
s.add(Or(t1 != s.model()[t1], t2 != s.model()[t2],t3 != s.model()[t2]))
print s.model()

【问题讨论】：

标签： z3 smt constraint-programming

【解决方案1】：

您的部分似乎有一个小错字，阻止了相同的模型在新的可满足性检查中再次使用，特别是倒数第二行应该是 t3 != s.model()[t3] 而不是 t3 != s.model()[t2]。

这是生成您在开头放置的两个模型的更新示例（z3py 链接：http://rise4fun.com/Z3Py/AxJv）：

S, (cl1, cl2, cl3, cl4, cl5, cl6, cl7,cl8,cl9) = EnumSort('S', ['cl1', 'cl2', 'cl3', 'cl4', 'cl5','cl6' ,'cl7', 'cl8', 'cl9'])

s = Solver()

x = Const('x', S)
def fun1(x):
  return Or(x == cl1, x == cl2, x == cl3, x == cl4, x == cl5, x == cl6, x == cl7, x == cl8, x == cl9)

y1, y2 = Consts('y1 y2', S)
def fun2(y1, y2):
  return Or(And(y1 == cl7, y2 == cl4), And(y1 == cl4, y2 == cl3), And(y1 == cl3, y2 == cl2),And(y1 == cl8, y2 == cl9))

q1,q2 = Consts('q1 q2', S)
def fun3(q1,q2):
  return Or(And(q1 == cl7, q2 == cl5), And(q1 == cl4, q2 == cl9))

t1, t2 ,t3 = Consts('t1 t2 t3', S)

s.add(fun1(t1))
s.add(fun2(t1,t2))
s.add(fun3(t1,t3))

while s.check() == sat:
  s.add(Or(t1 != s.model()[t1], t2 != s.model()[t2], t3 != s.model()[t3]))
  print s.model()

【讨论】：