optimization of rule-based model on discrete variables

[Elena]

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