问题描述:

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

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)`

.

- Find an arbitrary solution
`(x0, y0, z0)`

to`C(x,y,z)`

. - Compute
`f0 = f(x0, y0, z0)`

. This will be your first lower bound. - 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). - 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.

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.

您可能感兴趣的文章：

- angularjs - Issues with typeahead in angular
- objective c - Email composure iOS 8:
- groovy - ExpandoMetaClass getMetaMethods() doesn't return added methods
- sql - How to put stories into "length" categories based on wordcount?
- c# - How to handle IOException on FileStream.Close/Dispose
- php - Reading a specific line from a text file
- clr - Any implementation of an Unrolled Linked List in C#?
- Finding Hudson Log Files
- Forward to a payment-gateway together with POST data using cURL (or any other PHP server side solution)
- WCF in Winforms app - is it always single-threaded?

随机阅读：

**推荐内容**-

**热点内容**-
- php - Reading a specific line from a text file
- clr - Any implementation of an Unrolled Linked List in C#?
- Finding Hudson Log Files
- Forward to a payment-gateway together with POST data using cURL (or any other PHP server side solution)
- WCF in Winforms app - is it always single-threaded?
- git svn - git svn fetch does not fetch a Subversion commit message modified after initial clone
- java me - Why I am getting the bad length exception when I am running this application?
- java - How to get string.format to complain at compile time
- ruby on rails - Trigger observer of parent class on change
- python - Issue with URL pattern in Django with webmonkey tutorial