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：切換目標

回答

相關問題