如何解决选择一个选项并赋值
我有一个项目列表,我希望求解器从给定的列表中选择一个项目。我读到我们不能在 SOLVER 上赋值。
例如: 如果我有字符串列表 A = {"opt1","opt2","opt3"} 求解器条件“opt1”或“opt2”或“opt3” 求解器将 SAT 并选择一个。
有没有办法分配字符串值来做到这一点?!
解决方法
很难准确地解读您的要求;但这当然是完全可能的。如果你分享你的代码和你尝试过的东西,它会有所帮助。下面是一个可以帮助您入门的示例:
from z3 import *
opt1 = Bool("opt1")
opt2 = Bool("opt2")
opt3 = Bool("opt3")
s = Solver()
# Add some constraints on the options
s.add(Or(opt1,opt2))
s.add(Or(opt2,opt3))
# make sure only one is picked
s.add(If(opt1,1,0) + If(opt2,0) + If(opt3,0) == 1)
if s.check() == sat:
m = s.model()
if m.evaluate(opt1): print("picked: opt1")
if m.evaluate(opt2): print("picked: opt2")
if m.evaluate(opt3): print("picked: opt3")
运行时,打印:
picked: opt2
根据您的其他限制条件、z3 版本等,您可以通过这种方式获得与您的问题一致的任意设置。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。