使用 Z3 优化非线性目标函数

Question

我有两个方程，其中一个是线性的，而第二个是非线性的。我必须最小化第一个，同时最大化第二个。

这可以通过Z3实现吗？ 它似乎无法优化非线性方程。 它返回带有非线性方程的"未知"。

Answer 1

Z3 优化主要针对线性片段，请参阅本文：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf (注意，本文描述的工具现在是 z3 的一部分，你不需要单独的可执行文件。

话虽如此，一个常见的技巧是使用优化器来做线性部分;并重复调用以获得非线性部分的"更好"值。有关示例，请参阅此答案：https://stackoverflow.com/a/49180970/936310