【发布时间】：2018-03-14 11:10:51
【问题描述】：
我有两个方程，其中一个是线性的，而第二个是非线性的。 我必须最小化第一个，同时最大化第二个。
Z3 可以实现这一点吗？似乎它无法优化非线性方程。它返回带有非线性方程的“未知”。
【问题讨论】：
标签： optimization z3 smt
【发布时间】：2018-03-14 11:10:51
【问题描述】：
Z3 优化主要针对线性片段，见这篇论文：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf（请注意，本文中描述的工具现在是 z3 的一部分，你不需要单独的可执行文件。）
话虽如此，一个常见的技巧是使用优化器来做线性部分；并重复调用以获得非线性部分的“更好”值。例如，请参阅此答案：https://stackoverflow.com/a/49180970/936310
【讨论】：
-
我尝试了这个技巧，但我注意到它首先生成最大值。这是巧合吗？还是 z3 旨在首先尝试更大的价值？