Python - Ottimizza il sistema di disuguaglianza

Question

Sto lavorando ad un programma in Python in cui una piccola parte comporta l'ottimizzazione di un sistema di equazioni/disuguaglianze. Idealmente, avrei voluto fare come si può fare in Modelica, scrivere le equazioni e lasciare che il risolutore si prenda cura di esso.

L'operazione di risolutori e programmazione lineare è un po 'fuori dalla mia zona di comfort, ma ho deciso di provare comunque. Il problema è che il design generale del programma è orientato agli oggetti, e ci sono molte diverse possibilità di combinazioni per formare le equazioni, così come alcune non-linearità, quindi non sono stato in grado di tradurre questo in una programmazione lineare problema (ma potrei sbagliarmi).

Dopo alcune ricerche ho scoperto che il risolutore Z3 sembrava fare ciò che volevo. Sono venuto con questo (questo appare come un tipico caso di quello che vorrei per ottimizzare):

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

Ora questo funziona, e mi dà il risultato che voglio, nonostante non sia estremamente veloce (ho bisogno di risolvere tali sistemi diverse migliaia di volte). Ma non sono sicuro di utilizzare lo strumento giusto per il lavoro (Z3 è un "dimostratore di teoremi").

L'API è fondamentalmente esattamente ciò di cui ho bisogno, ma sarei curioso se altri pacchetti consentano una sintassi simile. O dovrei provare a formulare il problema in un modo diverso per consentire un approccio LP standard? (anche se non ho idea di come)

Answer 1

Z3 è il risolutore più potente che ho trovato per tali sistemi flessibili di equazioni. Z3 è una scelta eccellente ora che è rilasciata con la licenza MIT.

Esistono molti tipi diversi di strumenti con casi d'uso sovrapposti. Lei ha menzionato la programmazione lineare - ci sono anche teoremi dimostrativi, risolutori SMT e molti altri tipi di strumenti. Nonostante la commercializzazione stessa come dimostratore di teoremi, Z3 è spesso commercializzato come un solutore SMT. Al momento, i solutori SMT stanno guidando il pacchetto per la soluzione flessibile e automatizzata di equazioni algebriche accoppiate e disuguaglianze su valori booleani, reali e interi, e nel mondo dei risolutori SMT, Z3 è il re. Dai un'occhiata a the results of the last SMT comp if you want evidence of this. Detto questo, se le tue equazioni sono tutte lineari, potresti anche trovare prestazioni migliori con CVC4. Non fa male a guardarsi intorno.

Se le equazioni hanno una forma molto controllata (ad esempio, ridurre alcune funzioni soggette ad alcuni vincoli), è possibile ottenere prestazioni migliori utilizzando una libreria numerica come GSL o NAG. Tuttavia, se hai davvero bisogno della flessibilità, dubito che troverai uno strumento migliore di Z3.

Answer 2

La soluzione migliore sarà probabilmente quella di utilizzare un risolutore ILP. Il tuo problema può essere formulato come un'istanza di programmazione lineare (ILP) intera. Ci sono molti solutori di ILP, e alcuni potrebbero ottenere risultati migliori di Z3. Per solo 7 variabili, qualsiasi risolutore di ILP decente dovrebbe trovare una soluzione molto rapidamente.

L'unico bit difficile sono le espressioni condizionali (If(...)). Tuttavia, come @Erwin Kalvelagen suggests, i condizionali possono essere gestiti utilizzando la divisione variabile. Ad esempio, introdurre le variabili fplus e fminus, con i vincoli f = fplus - fminus e fplus >= 0 e fminus >= 0. Ora è possibile sostituire If(f > 0, f * 50, f * 0.4) con 50 * fplus - 0.4 * fminus. In questo caso, sarà equivalente.

La divisione variabile non funziona sempre. Devi pensare se potrebbe introdurre soluzioni spurie (dove sia fplus > 0 e fminus > 0). In questo caso, tuttavia, le soluzioni spurie non saranno mai ottimali - si può dimostrare che la soluzione ottimale non sarà mai ottimale.Di conseguenza, la divisione variabile funziona bene qui.

Se si dispone di una condizione in cui sono presenti istruzioni condizionali ma la divisione variabile non funziona, è possibile utilizzare spesso le tecniche a https://cs.stackexchange.com/q/12102/755 per formulare il problema come istanza di ILP.