巨蟒--优化的不等式组 [英] Python -- Optimize system of inequalities

问题描述

我正在编写一个用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方法？(虽然我不知道怎么做)

推荐答案

Z3是我为这种灵活的方程组找到的最强大的求解器。Z3是一个很好的选择，因为它是在麻省理工学院的许可下发布的。

有很多不同类型的工具具有重叠的用例。您提到了线性编程--还有定理证明器、SMT求解器和许多其他类型的工具。尽管Z3本身被推销为定理证明者，但它经常被推销为SMT解算器。目前，SMT解算器在灵活、自动化地求解布尔、实数和整数上的耦合代数方程和不等式方面处于领先地位，而在SMT解算器领域，Z3是王者。看看the results of the last SMT comp if you want evidence of this.也就是说，如果您的方程式都是线性的，那么您可能还会发现使用CVC4的性能更好。逛一逛也无伤大雅。

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

这篇关于巨蟒--优化的不等式组的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！