Finding Maximum Value Given a Set of Constraints

[MuhammadAbuBakar95]

Hi,

I know this question has been asked in the past but I was wondering what the most efficient solution will be.

I want to find the maximum value for a variable given a set of constraints. For example, I have the following set of constraints over variables x, y and z.

25 <= x <= 50
10 <= y <= 100
z == x * y

Now the maximum value of z is 5000. Is there a way to obtain this result by passing the above constraints to Z3? What will be the most efficient way to do it?

[NikolajBjorner]

Optimizaiton for non-linear constraints is not well supported. You can use optimization otherwise by specifying maximization and/or minimization objectives together with constraints. See the rise4fun tutorial.