Python -- Optimize system of inequalities
Question: I am working on a program in Python in which a small part involves optimizing
a system of equations / inequalities. Ideally, I would have wanted to do as
can be done in Modelica, write out the equations and let the solver take care
of it.

The operation of solvers and linear programming is a bit out of my comfort
zone, but I decided to try anyway. The problem is that the general design of
the program is object-oriented, and there are many different possibilities of
combinations to form up the equations, as well as some non-linearities, so I
have not been able to translate this into a linear programming problem (but I
might be wrong) .

After some research I found that the [Z3](https://github.com/Z3Prover/z3)
solver seemed to do what I wanted. I came up with this (this looks 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 this works, and gives me the result I want, despite it not being extremely
fast (I need to solve such systems several thousands of times). But I am not
sure I am using the right tool for the job (Z3 is a "theorem prover").

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


Answer: Z3 is the most powerful solver I have found for such flexible systems of
equations. Z3 is an excellent choice now that it is released under the MIT
license.

There are a lot of different types of tools with overlapping use cases. You
mentioned linear programming -- there are also theorem provers, SMT solvers,
and many other types of tools. Despite marketing itself as a theorem prover,
Z3 is often marketed as an SMT solver. At the moment, SMT solvers are leading
the pack for the flexible and automated solution of coupled algebraic
equations and inequalities over the booleans, reals, and integers, and in the
world of SMT solvers, Z3 is king. Take a look at [the results of the last SMT
comp if you want evidence of
this.](http://smtcomp.sourceforge.net/2015/results-summary.shtml?v=1446209369)
That being said, if your equations are all linear, then you might also find
better performance with CVC4. It doesn't hurt to shop around.

If your equations have a very controlled form (for example, minimize some
function subject to some constraints) then you might be able to get better
performance using a numerical library such as GSL or NAG. However, if you
really need the flexibility, then I doubt you are going to find a better tool
than Z3.

