CODEWITHSUNDEEP
z3
omerkatz
omerkatz

Reputation: 71

Does Z3 have support for optimization problems

I saw in a previous post from last August that Z3 did not support optimizations. However it also stated that the developers are planning to add such support.

I could not find anything in the source to suggest this has happened.

Can anyone tell me if my assumption that there is no support is correct or was it added but I somehow missed it?

Thanks, Omer

Upvotes: 4

Views: 2090

Answers (2)

Philippe
Philippe

Reputation: 9742

If your optimization has an integer valued objective function, one approach that works reasonably well is to run a binary search for the optimal value. Suppose you're solving the set of constraints C(x,y,z), maximizing the objective function f(x,y,z).

  1. Find an arbitrary solution (x0, y0, z0) to C(x,y,z).
  2. Compute f0 = f(x0, y0, z0). This will be your first lower bound.
  3. As long as you don't know any upper-bound on the objective value, try to solve the constraints C(x,y,z) ∧ f(x,y,z) > 2 * L, where L is your best lower bound (initially, f0, then whatever you found that was better).
  4. Once you have both an upper and a lower bound, apply binary search: solve C(x,y,z) ∧ 2 * f(x,y,z) > (U - L). If the formula is satisfiable, you can compute a new lower bound using the model. If it is unsatisfiable, (U - L) / 2 is a new upper-bound.

Step 3. will not terminate if your problem does not admit a maximum, so you may want to bound it if you are not sure it does.

You should of course use push and pop to solve the succession of problems incrementally. You'll additionally need the ability to extract models for intermediate steps and to evaluate f on them.

We have used this approach in our work on Kaplan with reasonable success.

Upvotes: 3

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Z3 currently does not support optimization. This is on the TODO list, but it has not been implemented yet. The following slide decks describe the approach that will be used in Z3:

The library for computing with infinitesimals has already been implemented, and is available in the unstable (work-in-progress) branch, and online at rise4fun.

Upvotes: 2

Related Questions