Python - Inequality System Optimization

Question

I am working on a Python program in which a small part includes optimizing the system of equations / inequalities. Ideally, I would like to do the same as in Modelica, write out the equations and let the solver take care of this.

Solvers and linear programming went a little out of my comfort zone, but I decided to try it anyway. The problem is that the overall design of the program is object-oriented, and there are many different combinations for generating equations, as well as some non-linearities, so I could not translate this into linear programming problem (but I can be wrong).

After some research, I found that the Z3 solver did what I wanted. I came up with this (this seems like a typical case of what I would like to optimize):

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

Now it works and gives me the result that I want, despite the fact that it is not very fast (I need to solve such systems several thousand times). But I'm not sure I'm using the right tool for the job (Z3 is a “theoretical breakthrough”).

The API is basically what I need, but I would be curious if other packages allow similar syntax. Or should I try to formulate the problem differently to allow a standard LP approach? (although I have no idea how)

Answer 1

Z3 is the most powerful solver I have found for such flexible systems of equations. The Z3 is a great choice now that it is released under the MIT license.

There are many different types of tools with overlapping use cases. You mentioned linear programming — there are also theoretical predictors, SMT solvers, and many other types of tools. Although it sells itself as a theoretical breakthrough, the Z3 is often marketed as an SMT solver. At the moment, SMT solvers are leading the package for flexible and automated solutions to related algebraic equations and inequalities over Boolean, real and integer numbers, and in the world of solvers SMT Z3 is king. Take a look at the results of the latest SMT comp if you want to prove it . Saying, if your equations are all linear, then you can also find better performance with CVC4. Doesn't bother to go shopping.

If your equations have a very controlled form (for example, to minimize some functions associated with some restrictions), then you can get better performance using a numerical library such as GSL or NAG. However, if you really need flexibility, I doubt that you will find a better tool than the Z3.

Answer 2

The best solution is probably to use an ILP solution. Your problem can be formulated as an instance of integer linear programming (ILP). There are many ILP solvers, and some may work better than Z3. For only 7 variables, any decent ILP solver must find a solution very quickly.

The only hard bit is conditional expressions ( If(...) ). However, as @Erwin Kalvelagen suggests , conditional expressions can be processed using difference splitting. For example, enter the variables fplus and fminus with the constraints f = fplus - fminus and fplus >= 0 and fminus >= 0 . Now you can replace If(f > 0, f * 50, f * 0.4) with 50 * fplus - 0.4 * fminus . In this case, it will be equivalent.

Variable splitting does not always work. You should think about whether they can introduce false solutions (where both fplus > 0 and fminus > 0 ). In this case, however, false decisions will never be optimal — it can be shown that the optimal solution will never be optimal. Therefore, variable splitting works fine here.

If you have a situation where you have conditional statements, but separation of variables does not work, you can often use https://cs.stackexchange.com/q/12102/755 methods to formulate the problem as an example of ILP.