如何解决如何为此逻辑找出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
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。