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

Question

所以我有 3 个房子 1、2、3 和 3 种颜色。当我运行这个脚本时，我得到了很好的所有变体（总共 9 个）。 1 间房子的颜色为 1，2 间房子的颜色为 3，依此类推。现在我想添加一条规则，没有房子是相同颜色的。所以除非我知道一些房子颜色组合，否则我仍然有所有 9 种变化。但后来我想说，房子 1 有颜色 3，它应该打印（房子：颜色）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)))

，但有点长

Answer 1

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

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, h2, h3]))

myvars = [h1, h2, 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, (Red, Green,  Blue)  = EnumSort('Color', ('Red', 'Green',  '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, h2c, h3c]))
s.add(Distinct([h1s, h2s, h3s]))

myvars = [h1c, h2c, h3c, h1s, h2s, 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

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

How to figure out z3py conditional blocks for this logic

z3py

添加尺码信息