如何为此逻辑找出z3py条件块

问题描述

所以我有3种房屋1,2,3和3种颜色。当我运行此脚本时，我会得到所有的变化（总计9个）。 1间颜色为1的房子，第二间颜色为3的房子，依此类推。现在，我想添加一条规则，即没有房子是相同颜色的。因此，除非我知道某种房屋颜色组合，否则我仍然拥有所有9种变体。但是接下来我要说的是，房子1的颜色为3，它应该打印（house：color）1：3、2：1、2：2、3：1、3：2。但是这种情况看起来如何。也许我需要重新安排完全不同的代码？

    from z3 import *
    
    color = Int('color')
    house = Int('house')
    
    color_variations = Or(color==1,color==2,color==3)
    house_variations = Or(house==1,house==2,house==3)
    
    s = Solver()
    
    s.add(color_variations)
    s.add(house_variations)
    
    myvars = [house,color]
    
    res = s.check()
    n = 1
    
    while (res == sat):
      m = s.model()
      block = []
      for var in myvars:
          v = m.evaluate(var,model_completion=True)
          print("%s = %s " % (var,v)),block.append(var != v)      
      s.add(Or(block))
      print("===========\n")
      res = s.check()
      n = n + 1

编辑：

我可以添加s.add(And(house!=1,color!=3))来排除此组合，但是我并不能将其作为打印输出的变体。

编辑2：

这似乎可以解决问题 s.add(Or(And(house!=1,color!=3),And(house==1,color==3)))

或

s.add(And(If(color==3,house==1,house_variations),If(house==1,color==3,color_variations))) 

或

s.add(And(Implies(color==3,house==1),Implies(house==1,color==3)))

，但有些偏长

解决方法

对于此问题，最好使用枚举。请注意，您只需要将房屋的颜色表示为符号变量即可：您已经知道房屋是什么。诀窍是要求颜色不同。这是我的编码方式：

from z3 import *

Color,(Red,Green,Blue) = EnumSort('Color',('Red','Green','Blue'))

h1,h2,h3 = Consts('h1 h2 h3',Color)

s = Solver()

s.add(Distinct([h1,h3]))

myvars = [h1,h3]

res = s.check()

n = 1
while (res == sat):
  print("%d. " % n),m = s.model()
  block = []
  for var in myvars:
      v = m.evaluate(var,model_completion=True)
      print("%s = %-5s " % (var,v)),block.append(var != v)
  s.add(Or(block))
  print
  n = n + 1
  res = s.check()

运行此命令时，我得到：

1.  h1 = Blue   h2 = Green  h3 = Red
2.  h1 = Green  h2 = Red    h3 = Blue
3.  h1 = Red    h2 = Blue   h3 = Green
4.  h1 = Blue   h2 = Red    h3 = Green
5.  h1 = Red    h2 = Green  h3 = Blue
6.  h1 = Green  h2 = Blue   h3 = Red

也就是说，我们获得了所有6种可能的组合。

如果您知道给定的房子是一种特定的颜色，只需将其添加为额外的约束即可。例如，假设house-2是蓝色的。您可以在上面的程序中添加以下约束：

s.add(h2 == Blue)

加上此内容，输出为：

1.  h1 = Green  h2 = Blue   h3 = Red
2.  h1 = Red    h2 = Blue   h3 = Green

希望这可以帮助您入门。要阅读z3py编程的一个好网站是：https://ericpony.github.io/z3py-tutorial/guide-examples.htm

添加尺寸信息

如果要添加其他属性，只需像对Color那样声明即可：

from z3 import *

Color,Blue)  = EnumSort('Color','Blue'))
Size,(Big,Medium,Small) = EnumSort('Size',('Big','Medium','Small'))

h1c,h2c,h3c = Consts('h1c h2c h3c',Color)
h1s,h2s,h3s = Consts('h1s h2s h3s',Size)

s = Solver()

s.add(Distinct([h1c,h3c]))
s.add(Distinct([h1s,h3s]))

myvars = [h1c,h3c,h1s,h3s]

# Add a constrain saying house 2 is medium,and house 3 is Green
s.add(h2s == Medium)
s.add(h3c == Green)

# Rest of the program same as above,elided here for brevity

运行此命令时，我得到：

1.  h1c = Blue   h2c = Red    h3c = Green  h1s = Big    h2s = Medium  h3s = Small
2.  h1c = Red    h2c = Blue   h3c = Green  h1s = Big    h2s = Medium  h3s = Small
3.  h1c = Red    h2c = Blue   h3c = Green  h1s = Small  h2s = Medium  h3s = Big
4.  h1c = Blue   h2c = Red    h3c = Green  h1s = Small  h2s = Medium  h3s = Big