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 求解器在灵活、自动地求解耦合代数方程以及布尔值、实数和整数上的不等式方面处于领先地位，在 SMT 求解器的世界中，Z3 是王者。如果您需要证据，请查看上一次 SMT 比较的结果。 话虽这么说，如果您的方程都是线性的，那么您可能还会发现 CVC4 具有更好的性能。货比三家也没什么坏处。

如果您的方程具有非常受控的形式（例如，最小化某些受某些约束影响的函数），那么您可能能够使用 GSL 或 NAG 等数值库获得更好的性能。然而，如果您确实需要灵活性，那么我怀疑您是否会找到比 Z3 更好的工具。