提问人：tomp 提问时间：9/16/2022 更新时间：9/16/2022 访问量：84
帕累托优先级和目标为“错误”的一个循环，这意味着什么？（Z3）
one loop for pareto priority and objectives are 'False', what does this mean? (Z3)
问：
我试图为我自己的优化问题复制以下代码。
但是，我只得到一个循环。
在不调用方法 value（） 的情况下打印以下目标时，每个目标都是 True。对我来说，它们是错误的。
我该如何解释这些结果？
非常感谢。
x, y = Ints('x y')
opt = Optimize()
opt.set(priority='pareto')
opt.add(x + y == 10, x >= 0, y >= 0)
mx = opt.maximize(x)
my = opt.maximize(y)
while opt.check() == sat:
print (mx.value(), my.value())
答：
1赞
alias
9/16/2022
#1
很难理解你的意思。通过“我只得到一个循环”，我假设你的意思是你只打印一次值，仅此而已。这完全没问题，它只是意味着帕累托前沿只有一个元素。
为了获得更好的分析，您必须发布实际代码（尽可能简化）。如果不确切地看到你在做什么，就不可能进一步发表意见。
评论
0赞
tomp
9/16/2022
谢谢。不幸的是，我无法发布我的代码，但目标的设置和优化器的运行与发布的示例完全相同。我仍然有一个问题是，如果（OptimizeObjective 对象）是 True 或 False，这意味着什么？作为对其他评论的回应，check does return sat。
1赞
alias
9/16/2022
如果求解器处于 sat 状态，则所有目标都必须为 True。否则，这是一个错误。
1赞
alias
9/16/2022
我应该说“所有约束”必须是 True。当然，目标就是你要优化的。我希望这是清楚的。
0赞
tomp
9/16/2022
满足所有约束，check 返回 sat，但目标返回为 False。我不确定为什么它们被返回为 False。如果你能帮我理解，我很想知道。非常感谢。
1赞
alias
9/16/2022
我不会给这个结果赋予任何意义。可能是 Python 绑定松散类型性质的产物。
评论