0

I have two equations, one of them is linear while the second one is non-linear. I have to minimize the first one while maximizing the second one at the same time.

Is this achievable with Z3? it seems that it can't optimize non-linear equations. it returns "Unknown" with non-linear equations.

Rehab11
  • 483
  • 2
  • 7
  • 16

1 Answers1

2

Z3 optimization is mostly for the linear fragment, see this paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf (Note that the tool described in this paper is now part of z3, yo do not need a separate executable.)

Having said that, a common trick is to use the optimizer to do the linear part; and do repeated calls to get "better" values for the non-linear parts. See this answer for an example: https://stackoverflow.com/a/49180970/936310

alias
  • 28,120
  • 2
  • 23
  • 40
  • I tried the trick but i noticed that it generates the maximum value first. Is that a coincidence? Or is z3 designed to try greater values first? – Rehab11 May 09 '18 at 13:53