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?
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
(x0, y0, z0)to
f0 = f(x0, y0, z0). This will be your first lower bound.
C(x,y,z) ∧ f(x,y,z) > 2 * L, where
Lis your best lower bound (initially,
f0, then whatever you found that was better).
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) / 2is 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
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.
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:
Exact nonlinear optimization on demand
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
The library for computing with infinitesimals has already been implemented, and is available in the
unstable (work-in-progress) branch, and online at rise4fun.