如何用z3py解决这个排斥/包含问题？

Question

感谢社区的帮助，我想出了下面的代码：

    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()
    
    myvars = [h1c, h2c, h3c, h1s, h2s, h3s]
    
    s.add(Distinct([h1c, h2c, h3c]))
    s.add(Distinct([h1s, h2s, h3s]))
    
    s.add(h3s == Medium)
    s.add(h3c == Red)
    
    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))
      n = n + 1
      res = s.check()

这解决了问题，只有一个房子可以，例如，中等大小和红色。而其他组合则以变异的形式存在。

然而，我也想要的是一个条件，那就是众议院为什么是，例如，绿色是小的。一开始没有指向特定的房子。这将排除所有的变化，绿色或小不是组合(绿色不能是中，小不能是红色，等等)。但也要保持鲜明，例如，只有一个房子可以是绿色的和小的。所以以后如果我说房子1是绿色的还是小的，那么对于房子1来说，这是一个变化，没有其他的房子(变化)可以是绿色的或小的。

Example after 1st condition (Green is Small):

h1 = Green + Small
h2 = Green + Small
h3 = Green + Small
h1 = Red + Medium
h1 = Red + Big
h2 = Red + Medium
h2 = Red + Big
h3 = Red + Medium
h3 = Red + Big
h1 = Blue + Medium
h1 = Blue + Big
h2 = Blue + Medium
h2 = Blue + Big
h3 = Blue + Medium
h3 = Blue + Big ( I might missed something)

Example after 2nd condition (House 1 is Small/Green):

h1 = Green + Small
h2 = Red + Medium
h2 = Red + Big
h3 = Red + Medium
h3 = Red + Big
h2 = Blue + Medium
h2 = Blue + Big
h3 = Blue + Medium
h3 = Blue + Big ( I might missed something)

我一直在研究Functions和children变量，但是看不出如何比较堆栈中的任何变量。我认为代码需要完全重组？

Answer 1

@JohanC的回答很好，但我同意这一观点，即如果不系统地处理这些约束，这种约束可能会失控，也不可能得到管理。我发现创建字典和你自己的摘要确实有帮助。请注意，这实际上并不是z3/z3py特定的，而是一般用于编程的。例如，我将如何编码您的问题：

from z3 import *

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

# Create a house and store properties in a dictionary
def mkHouse(name):
    return { 'name' : name
           , 'color': Const(name + "_color", Color)
           , 'size' : Const(name + "_size",  Size)
           }

allHouses = [mkHouse(n) for n in ["house1", "house2", "house3"]]

s = Solver ()

# Assert sizes and colors are different
s.add(Distinct([h['color'] for h in allHouses]))
s.add(Distinct([h['size']  for h in allHouses]))

def forallHouses(pred):
    cond = True
    for house in allHouses:
        cond = And(cond, pred(house))
    s.add(cond)

# Assert that Green house is small. Note the implication.
forallHouses(lambda h: Implies(h['color'] == Green, h['size'] == Small))

# Assert that If a house is Red, then it cannot be Medium
forallHouses(lambda h: Implies(h['color'] == Red, h['size'] != Medium))

# Collect the solutions:
res = s.check()

n = 1
while (res == sat):
  print("Solution %d: " % n)
  m = s.model()
  block = []
  for house in allHouses:
      hcolor = m.evaluate(house['color'], model_completion=True)
      hsize  = m.evaluate(house['size'],  model_completion=True)
      print("  %-5s = %-5s %-5s" % (house['name'], hcolor, hsize))
      block.append(Or(house['color'] != hcolor, house['size'] != hsize))
  s.add(Or(block))
  n = n + 1
  res = s.check()

注意使用字典记录房子的名称、大小和颜色。您可以根据自己的意愿添加新的属性，一切都保持在本地，以便稍后进行轻松的操作和提取。特别是，函数forallHouses捕捉到了你想要说的东西的本质:你想对每个单独的房子说些什么，它通过一个lambda函数来捕捉这一点。

在上面的例子中，我断言Green house是Small，Red house不是Medium。(这意味着Red的房子一定很大，这是z3为我们发现的。)当我运行它时，我得到：

Solution 1:
  house1 = Blue  Medium
  house2 = Green Small
  house3 = Red   Big
Solution 2:
  house1 = Green Small
  house2 = Red   Big
  house3 = Blue  Medium
Solution 3:
  house1 = Green Small
  house2 = Blue  Medium
  house3 = Red   Big
Solution 4:
  house1 = Red   Big
  house2 = Blue  Medium
  house3 = Green Small
Solution 5:
  house1 = Red   Big
  house2 = Green Small
  house3 = Blue  Medium
Solution 6:
  house1 = Blue  Medium
  house2 = Red   Big
  house3 = Green Small

我相信这和你想要达到的目标是一致的。希望您可以从这个框架开始，并将其转化为您在建模更复杂的约束时可以使用的东西。

Answer 2

无论如何，您都需要添加一个条件：

s.add(Or(And(h1c == Green, h1s == Small),
         And(h2c == Green, h2s == Small),
         And(h3c == Green, h3s == Small)))

所有东西都可以用数组编写得更灵活一点：

from z3 import EnumSort, Consts, Solver, Distinct, Or, And, sat

Color, (Red, Green, Blue) = EnumSort('Color', ('Red', 'Green', 'Blue'))
Size, (Big, Medium, Small) = EnumSort('Size', ('Big', 'Medium', 'Small'))
hc = Consts('h1c h2c h3c', Color)
hs = Consts('h1s h2s h3s', Size)

s = Solver()
s.add(Distinct(hc))
s.add(Distinct(hs))

s.add(Or([And(hci == Green, hsi == Small) for hci, hsi in zip(hc, hs)]))

res = s.check()
n = 1
while (res == sat):
    print(f"{n:-2d}.", end=" ")
    m = s.model()
    block = []
    for i, (hci, hsi) in enumerate (zip(hc, hs), start=1):
        hci_v = m.evaluate(hci, model_completion=True)
        hsi_v = m.evaluate(hsi, model_completion=True)
        print(f'{f"h{i}:{hci_v}+{hsi_v}":<15}', end="")
        block.append(hci != hci_v)
        block.append(hsi != hsi_v)
    print()
    s.add(Or(block))
    n += 1
    res = s.check()

结果：

 1. h1:Blue+Big    h2:Green+Small h3:Red+Medium  
 2. h1:Green+Small h2:Red+Medium  h3:Blue+Big    
 3. h1:Red+Medium  h2:Blue+Big    h3:Green+Small 
 4. h1:Red+Big     h2:Blue+Medium h3:Green+Small 
 5. h1:Blue+Big    h2:Red+Medium  h3:Green+Small 
 6. h1:Blue+Medium h2:Red+Big     h3:Green+Small 
 7. h1:Blue+Medium h2:Green+Small h3:Red+Big     
 8. h1:Red+Big     h2:Green+Small h3:Blue+Medium 
 9. h1:Red+Medium  h2:Green+Small h3:Blue+Big    
10. h1:Green+Small h2:Blue+Medium h3:Red+Big     
11. h1:Green+Small h2:Blue+Big    h3:Red+Medium  
12. h1:Green+Small h2:Red+Big     h3:Blue+Medium 

PS:简化了小房子是绿色的条件的一种方法，就是改变表示。与其代表每个房屋的颜色和大小，还可以表示每种颜色和每个大小的房屋编号。这需要额外的条件，即每种颜色都应该是1、2或3种颜色。同样的条件适用于大小：

from z3 import Ints, Solver, Distinct, Or, And, sat

Red, Green, Blue = Ints('Red Green Blue')
Big, Medium, Small = Ints('Big Medium Small')
colors = [Red, Green, Blue]
sizes = [Big, Medium, Small]

s = Solver()
s.add(Distinct(colors))
s.add(Distinct(sizes))
s.add(And([Or([color == i for i in (1, 2, 3)]) for color in colors]))
s.add(And([Or([size == i for i in (1, 2, 3)]) for size in sizes]))

s.add(Green == Small)

res = s.check()
n = 1
while (res == sat):
    print(f"{n:-2d}.", end=" ")
    m = s.model()
    block = []
    for x in colors + sizes:
        x_v = m.evaluate(x, model_completion=True).as_long()
        print(f"{x}:h{x_v}", end=" ")
        block.append(x != x_v)
    print()
    s.add(Or(block))
    n += 1
    res = s.check()

结果：

 1. Red:h3 Green:h2 Blue:h1 Big:h3 Medium:h1 Small:h2 
 2. Red:h2 Green:h3 Blue:h1 Big:h2 Medium:h1 Small:h3 
 3. Red:h2 Green:h3 Blue:h1 Big:h1 Medium:h2 Small:h3 
 4. Red:h1 Green:h2 Blue:h3 Big:h1 Medium:h3 Small:h2 
 5. Red:h3 Green:h2 Blue:h1 Big:h1 Medium:h3 Small:h2 
 6. Red:h1 Green:h3 Blue:h2 Big:h1 Medium:h2 Small:h3 
 7. Red:h3 Green:h1 Blue:h2 Big:h3 Medium:h2 Small:h1 
 8. Red:h3 Green:h1 Blue:h2 Big:h2 Medium:h3 Small:h1 
 9. Red:h1 Green:h3 Blue:h2 Big:h2 Medium:h1 Small:h3 
10. Red:h1 Green:h2 Blue:h3 Big:h3 Medium:h1 Small:h2 
11. Red:h2 Green:h1 Blue:h3 Big:h2 Medium:h3 Small:h1 
12. Red:h2 Green:h1 Blue:h3 Big:h3 Medium:h2 Small:h1 

如果有必要，可以将输出重新格式化为与第一个解决方案相同的格式。一个解决方案是“不那么变通”，还是“更清晰”，还是“更容易维护”，似乎是一个非常主观的问题。将问题转换为SAT/SMT解决程序的格式总是有点棘手。