Z3最大化API：切换目标

关于Z3中最大化API的另一个问题。我得到错误的答案，如果我通过切换最大化目标的中途：Z3最大化API：切换目标

from z3 import Real, Optimize 

x = Real('x') 
y = Real('y') 
opt = Optimize() 

opt.add(x >= 0) 
opt.add(y >= 0)  
opt.add(x + y <= 15) 

print "Optimizing", x 
h = opt.maximize(x) 
print opt.check() 
print opt.upper(h) 
print opt.model() 

print "Optimizing", y 
h = opt.maximize(y) 
print opt.check() 
print opt.upper(h) 
print opt.model()

后者呼吁opt.model()回报y = 0，而明确的答案应该是15。它是一个错误还是根本不支持的功能？（我应该手动重新添加约束每次我想切换目标？）

此外，有一个单独的错误，当我删除非负性约束，但这是一个单独的问题出现（坏为处理无界的目标，我相信？）

from z3 import Real, Optimize 

x = Real('x') 
y = Real('y') 
opt = Optimize() 

opt.add(x + y <= 15) 

print "Optimizing", x 
h = opt.maximize(x) 
print opt.check() 
print opt.upper(h) 
print opt.model()

与

Optimizing x 
terminate called after throwing an instance of 'std::bad_typeid' 
    what(): std::bad_typeid 
fish: Job 1, 'python opt.py' terminated by signal SIGABRT (Abort)

来源

2014-10-06 George Karpenkov

你可以检查，如果你告诉opt.add（x <= 14）会发生什么？现在回答1？我的意思是它是单独应用这两种对比还是相互应用。 – mico 2014-10-14 20:16:43

@mico感谢您的评论！除了应用这两种优化之外，这意味着什么？优化“x”，然后优化“y”而不使“x”变小？ – 2014-10-15 08:48:16

如果存在x，y，z，那么可能会优化两者。不过，这是疯狂的猜测，我只想指出如何获得更多信息。 – mico 2014-10-15 11:50:33

感谢在崩溃的bug报告死亡。这不应该发生。

对于您报告的第一个问题。添加目标的语义是相加的。也就是说，您指示引擎优化x和y（在第二个调用中）。它默认选择x，y的词典组合。在词典排序中，价值（15,0）主导其他价值。

来源

2014-11-05 09:26:47

Z3最大化API：切换目标

回答

相关问题