z3Opt優化非線性函數使用qfnra-nlsat

Question

我試圖使用z3Opt優化一個真正的非線性函數，但即使簡單的情況下，像下面的一個

http://rise4fun.com/Z3Opt/JbaU

結果不是它預期的。這就像z3它根本沒有優化....任何人都可以幫助我理解？

Answer 1

此時不支持優化非線性函數，因此不保證結果。如果求解器返回未知的（而不是座標）這個情況可能會更好，這是我應該研究的。