Il Tue, 15 Jun 2021 01:53:09 +0000, Martin Di Paola ha scritto: > From what I'm understanding it is an "optimization problem" like the > ones that you find in "linear programming". > > But in your case the variables are not Real (they are Integers) and the > function to minimize g() is not linear. > > You could try/explore CVXPY (https://www.cvxpy.org/) which it's a solver > for different kinds of "convex programming". I don't have experience > with it however. > > The other weapon in my arsenal would be Z3 > (https://theory.stanford.edu/~nikolaj/programmingz3.html) which it's a > SMT/SAT solver with a built-in extension for optimization problems. > > I've more experience with this so here is a "draft" of what you may be > looking for. > > > from z3 import Integers, Optimize, And, If > > # create a Python array X with 3 Z3 Integer variables named x0, x1, x2 X > = Integers('x0 x1 x2') > Y = Integers('y0 y1') > > # create the solver solver = Optimize() > > # add some restrictions like lower and upper bounds for x in X: > solver.add(And(0 <= x, x <= 2)) # each x is between 0 and 2 > for y in Y: > solver.add(And(0 <= y, y <= 2)) > > def f(X): > # Conditional expression can be modeled too with "If" > # These are *not* evaluated like a normal Python "if" but # modeled > as a whole. It'll be the solver which will "run it" > return If( > And(x[0] == 0, x[1] == 0), # the condition Y[0] == 0, # Y[0] will > *must* be 0 *if* the condition holds Y[0] == 2 # Y[0] will *must* > be 2 *if* the condition doesn't hold ) > > solver.add(f(X)) > > # let's define the function to optimize g = Y[0]**2 solver.maximize(g) > > # check if we have a solution solver.check() # this should return 'sat' > > # get one of the many optimum solutions solver.model() > > > I would recommend you to write a very tiny problem with 2 or 3 variables > and a very simple f() and g() functions, make it work (manually and with > Z3) and only then build a more complex program. > > You may find useful (or not) these two posts that I wrote a month ago > about Z3. These are not tutorials, just personal experience with a > concrete example. > > Combine Real, Integer and Bool variables: > https://book-of-gehn.github.io/articles/2021/05/02/Planning-Space- Missions.html > > Lookup Tables (this may be useful for programming a f() "variable" > function where the code of f() (the decision tree) is set by Z3 and not > by you such f() leads to the optimum of g()) > https://book-of-gehn.github.io/articles/2021/05/26/Casting-Broadcasting- LUT-and-Bitwise-Ops.html > > > Happy hacking. > Martin. > >
Interesting, I completely didn't know about this Z3 tool, I'll try to go into that. Thank you for hint. BTW the first two links I think are broken. Ele -- https://mail.python.org/mailman/listinfo/python-list
