如何用 z3py 解决这个 exclusion/inclusion 问题？
How to solve this exclusion/inclusion problem with z3py?
感谢社区的帮助，我想出了这个代码：
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()
这解决了只有一个房子可以是中等大小和红色的问题。其他组合保持变化。
但是我还想要一个条件，即House why is，例如Green is Small。最初不指向特定的房子。这将排除所有未组合绿色或小型的变体（绿色不能是中型，小型不能是红色等）......但也要保持不同，例如，只有一个房子可以是绿色和小型.所以稍后如果我说 house 1 是 Green 或 Small，那么 house 1 就是这个变体，没有其他房子（变体）可以是 Green 或 Small。
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 变量，但看不出如何比较堆栈中的任何变量。我认为代码需要完全重组？
您需要以某种方式添加条件：
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 求解器的格式总是有点棘手。
@JohanC 的回答很好，但我同意 OP 的观点，即如果您不以系统的方式处理这些限制，这些限制可能会真正失控并且无法管理。我发现创建字典和自己的抽象真的很有帮助。请注意，这并不是 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-function.
捕捉到这一点
在上面的例子中，我断言 Green 房子是 Small 而 Red 房子是 而不是 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
我认为这符合您要实现的目标。希望您可以从这个骨架开始，将它变成可以在建模更复杂的约束时使用的东西。
感谢社区的帮助，我想出了这个代码：
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()
这解决了只有一个房子可以是中等大小和红色的问题。其他组合保持变化。
但是我还想要一个条件，即House why is，例如Green is Small。最初不指向特定的房子。这将排除所有未组合绿色或小型的变体（绿色不能是中型，小型不能是红色等）......但也要保持不同，例如，只有一个房子可以是绿色和小型.所以稍后如果我说 house 1 是 Green 或 Small，那么 house 1 就是这个变体，没有其他房子（变体）可以是 Green 或 Small。
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 变量，但看不出如何比较堆栈中的任何变量。我认为代码需要完全重组？
您需要以某种方式添加条件：
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 求解器的格式总是有点棘手。
@JohanC 的回答很好，但我同意 OP 的观点，即如果您不以系统的方式处理这些限制，这些限制可能会真正失控并且无法管理。我发现创建字典和自己的抽象真的很有帮助。请注意，这并不是 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-function.
在上面的例子中，我断言 Green 房子是 Small 而 Red 房子是 而不是 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
我认为这符合您要实现的目标。希望您可以从这个骨架开始，将它变成可以在建模更复杂的约束时使用的东西。