Python - Optimiere das System der Ungleichungen

Question

Ich arbeite an einem Programm in Python, in dem ein kleiner Teil die Optimierung eines Systems von Gleichungen/Ungleichungen beinhaltet. Im Idealfall hätte ich das tun wollen, was in Modelica gemacht werden kann, schreibe die Gleichungen aus und lasse den Solver sich darum kümmern.

Der Betrieb von Solvern und lineare Programmierung ist ein wenig außerhalb meiner Komfortzone, aber ich habe mich trotzdem entschieden. Das Problem ist, dass der allgemeine Entwurf des Programms objektorientiert ist, und es gibt viele verschiedene Kombinationsmöglichkeiten, um die Gleichungen zu bilden, sowie einige Nichtlinearitäten, so dass ich nicht in der Lage war, dies in eine lineare Programmierung zu übersetzen Problem (aber ich könnte falsch liegen).

Nach einigen Recherchen fand ich, dass der Z3 Löser schien zu tun, was ich wollte. Ich kam mit diesem (das sieht aus wie ein typischer Fall von dem, was Ich mag würde optimieren):

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() 

Jetzt das funktioniert, und gibt mir das Ergebnis, das ich will, obwohl es nicht extrem schnell zu sein (ich muß solche Systeme mehrere tausend Mal lösen). Aber ich bin mir nicht sicher, ob ich das richtige Werkzeug für den Job verwende (Z3 ist ein "Theorembeweiser").

Die API ist im Grunde genau das, was ich brauche, aber ich wäre neugierig, wenn andere Pakete eine ähnliche Syntax erlauben. Oder sollte ich versuchen, das Problem anders zu formulieren, um einen Standard-LP-Ansatz zu ermöglichen? (obwohl ich keine Ahnung habe, wie)

Answer 1

Z3 ist der mächtigste Löser, den ich für solche flexible Systeme von Gleichungen gefunden habe. Z3 ist jetzt eine ausgezeichnete Wahl, da es unter der MIT Lizenz veröffentlicht wurde.

Es gibt viele verschiedene Arten von Werkzeugen mit überlappenden Anwendungsfällen. Sie haben die lineare Programmierung erwähnt - es gibt auch Theorembeweiser, SMT-Löser und viele andere Arten von Werkzeugen. Trotz der Vermarktung als Theorembeweiser wird Z3 oft als SMT-Solver vermarktet. Momentan sind SMT-Löser führend in der flexiblen und automatisierten Lösung von gekoppelten algebraischen Gleichungen und Ungleichungen über die Booleschen, reellen und ganzen Zahlen. In der Welt der SMT-Löser ist Z3 der König. Werfen Sie einen Blick auf the results of the last SMT comp if you want evidence of this.. Wenn Ihre Gleichungen alle linear sind, können Sie auch eine bessere Leistung mit CVC4 finden. Es tut nicht weh, herum zu shoppen.

Wenn Ihre Gleichungen eine sehr kontrollierte Form haben (z. B. eine Funktion mit einigen Einschränkungen minimieren), können Sie möglicherweise eine bessere Leistung mit einer numerischen Bibliothek wie GSL oder NAG erzielen. Wenn Sie jedoch wirklich die Flexibilität benötigen, dann bezweifle ich, dass Sie ein besseres Werkzeug als Z3 finden werden.

Answer 2

Die beste Lösung wird wahrscheinlich die Verwendung eines ILP-Solvers sein. Ihr Problem kann als Integer Linear Programming (ILP) -Instanz formuliert werden. Es gibt viele ILP-Löser, und einige sind möglicherweise besser als Z3. Für nur 7 Variablen sollte jeder vernünftige ILP-Solver eine Lösung sehr schnell finden. Das einzige knifflige Bit sind die bedingten Ausdrücke (If(...)). Als @Erwin Kalvelagen suggests können die Bedingungen jedoch unter Verwendung der Variablenaufteilung gehandhabt werden. Stellen Sie zum Beispiel die Variablen fplus und fminus mit den Einschränkungen f = fplus - fminus und fplus >= 0 und fminus >= 0 ein. Jetzt können Sie If(f > 0, f * 50, f * 0.4) durch 50 * fplus - 0.4 * fminus ersetzen. In diesem Fall wird das gleichwertig sein.

Variables Teilen funktioniert nicht immer. Sie müssen darüber nachdenken, ob es zu falschen Lösungen kommen könnte (sowohl fplus > 0 als auch fminus > 0). In diesem Fall werden falsche Lösungen niemals optimal sein - man kann zeigen, dass die optimale Lösung niemals optimal sein wird.Folglich funktioniert die variable Aufteilung hier gut.

Wenn Sie eine Situation haben, in der Sie bedingte Anweisungen haben, die variable Aufteilung jedoch nicht funktioniert, können Sie häufig die Techniken unter https://cs.stackexchange.com/q/12102/755 verwenden, um das Problem als ILP-Instanz zu formulieren.