Python——优化不等式系统

Question

我正在用 Python 开发一个程序，其中一小部分涉及优化方程组/不等式。理想情况下，我会想像在 Modelica 中那样做，写出方程并让求解器处理它。

求解器和线性规划的操作有点超出我的舒适范围，但我还是决定尝试一下。问题是程序的一般设计是面向对象的，并且有许多不同的组合可能性来构成方程，以及一些非线性，所以我无法将其转化为线性规划问题(但我可能错了)。

经过一些研究，我发现 Z3求解器似乎做了我想做的事。我想到了这个(这看起来像是我想要优化的典型案例):

from z3 import *

a = Real('a')
b = Real('b')
c = Real('c')
d = Real('d')
e = Real('e')
g = Real('g')
f = Real('f')
cost = Real('cost')

opt = Optimize()
opt.add(a + b - 350 == 0)
opt.add(a - g == 0)
opt.add(c - 400 == 0)
opt.add(b - d * 0.45 == 0)
opt.add(c - f - e - d == 0)
opt.add(d <= 250)
opt.add(e <= 250)

opt.add(cost == If(f > 0, f * 50, f * 0.4) + e * 40 + d * 20 + 
  If(g > 0, g * 50, g * 0.54))

h = opt.minimize(cost)
opt.check()
opt.lower(h)
opt.model()

现在这可行了，并给出了我想要的结果，尽管它不是非常快(我需要解决此类系统数千次)。但我不确定我是否使用了正确的工具来完成这项工作(Z3 是一个“定理证明器”)。

API 基本上正是我所需要的，但我很好奇其他包是否允许类似的语法。或者我应该尝试以不同的方式提出问题以允许标准的 LP 方法吗？ (虽然我不知道怎么做)

Answer 1

Z3 是我为此类灵活的方程组找到的最强大的求解器。 Z3 是一个很好的选择，因为它是在 MIT 许可下发布的。

有许多不同类型的工具具有重叠的用例。您提到了线性规划——还有定理证明器、SMT 求解器和许多其他类型的工具。尽管将自己作为定理证明者进行营销，但 Z3 通常作为 SMT 求解器进行营销。目前，SMT 求解器在 bool 、实数和整数耦合代数方程和不等式的灵活和自动化解决方案方面处于领先地位，在 SMT 求解器的世界中，Z3 是王者。看看the results of the last SMT comp if you want evidence of this.也就是说，如果您的方程都是线性的，那么您可能还会发现 CVC4 具有更好的性能。货比三家也没什么坏处。

如果您的方程式具有非常可控的形式(例如，最小化受某些约束的某些函数)，那么您可以使用 GSL 或 NAG 等数值库获得更好的性能。但是，如果您真的需要灵 active ，那么我怀疑您会找到比 Z3 更好的工具。