选择一个选项并赋值

Question

我有一个项目列表，我希望求解器从给定列表中选择一个项目。我读到我们不能在 SOLVER 上赋值。

例如： 如果我有字符串列表 A = {"opt1","opt2","opt3"} 求解器条件“opt1”或“opt2”或“opt3” 求解器将 SAT 并选择一个。

有什么方法可以分配字符串值来做到这一点？！

Answer 1

很难准确解读您的要求；但这当然是完全可能的。如果您分享您的代码和您尝试过的内容，它会有所帮助。下面是一个可以帮助您入门的示例：

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, 1, 0) + If(opt3, 1, 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 版本等，您可以通过这种方式获得与您的问题一致的任意设置。