Optimisation functions

[zenna]

@scungao and @soonhokong . I added a function for binary-search based optimisation in dReal(in dReal.jl/src/optimize.jl and there are examples in /test). If you would like any enhancements or changes, we can discuss them here.

[scungao]

Great!

I took a brief look at the code and may have missed something: It seems if
the half interval gives you unsat, you stop? Wouldn't you do binary search
in the other half in that case?

On Sat, May 9, 2015 at 5:23 PM, Zenna Tavares [email protected]
wrote:

@scungao https://github.com/scungao and @soonhokong
https://github.com/soonhokong . I added a function for binary-search
based optimisation in dReal(in dReal.jl/src/optimize.jl and there are
examples in /test). If you would like any enhancements or changes, we can
discuss them here.

—
Reply to this email directly or view it on GitHub
#8.

[zenna]

No if the half interval is unsat I set the other half interval (which I
didn't test but must contain the optimal cost) to be the "current interval"
which will be split in the next iteration.
On 9 May 2015 22:23, "Sicun Gao" [email protected] wrote:

Great!

I took a brief look at the code and may have missed something: It seems if
the half interval gives you unsat, you stop? Wouldn't you do binary search
in the other half in that case?

On Sat, May 9, 2015 at 5:23 PM, Zenna Tavares [email protected]
wrote:

@scungao https://github.com/scungao and @soonhokong
https://github.com/soonhokong . I added a function for binary-search
based optimisation in dReal(in dReal.jl/src/optimize.jl and there are
examples in /test). If you would like any enhancements or changes, we can
discuss them here.

—
Reply to this email directly or view it on GitHub
#8.

—
Reply to this email directly or view it on GitHub
#8 (comment).

[scungao]

Ok right. I guess I was looking at the line outside the loop where it does
something when unsat is returned after the loop. I guess if you set the
exit condition of the loop to be only when the size of the cost interval
gets smaller than some epsilon (right now it's ten iterations?), then you
would mostly get the right answer up to epsilon, and the unsat should just
be exceptions.

On Sun, May 10, 2015 at 2:45 AM, Zenna Tavares [email protected]
wrote:

No if the half interval is unsat I set the other half interval (which I
didn't test but must contain the optimal cost) to be the "current interval"
which will be split in the next iteration.
On 9 May 2015 22:23, "Sicun Gao" [email protected] wrote:

Great!

I took a brief look at the code and may have missed something: It seems
if
the half interval gives you unsat, you stop? Wouldn't you do binary
search
in the other half in that case?

On Sat, May 9, 2015 at 5:23 PM, Zenna Tavares [email protected]
wrote:

@scungao https://github.com/scungao and @soonhokong
https://github.com/soonhokong . I added a function for binary-search
based optimisation in dReal(in dReal.jl/src/optimize.jl and there are
examples in /test). If you would like any enhancements or changes, we
can
discuss them here.

—
Reply to this email directly or view it on GitHub
#8.

—
Reply to this email directly or view it on GitHub
#8 (comment).

—
Reply to this email directly or view it on GitHub
#8 (comment).

[zenna]

By get the right answer you mean get SAT? I don't think so. In either case
you could always get UNSAT or always SAT or both. It just depends on where
the true optimal value is compared to where you started.

For example if the minimum is zero but your original interval is -10 to 0
you will always get UNSAT because every test will examine the lower half of
the interval

Currently the default value is to stop after 10 itrrations but the stop
test is parameterised. Maybe a better default is the based on the size of
the interval as you said.

On 10 May 2015 10:33, "Sicun Gao" [email protected] wrote:

Ok right. I guess I was looking at the line outside the loop where it does
something when unsat is returned after the loop. I guess if you set the
exit condition of the loop to be only when the size of the cost interval
gets smaller than some epsilon (right now it's ten iterations?), then you
would mostly get the right answer up to epsilon, and the unsat should just
be exceptions.

On Sun, May 10, 2015 at 2:45 AM, Zenna Tavares [email protected]
wrote:

No if the half interval is unsat I set the other half interval (which I
didn't test but must contain the optimal cost) to be the "current
interval"
which will be split in the next iteration.
On 9 May 2015 22:23, "Sicun Gao" [email protected] wrote:

Great!

I took a brief look at the code and may have missed something: It
seems
if
the half interval gives you unsat, you stop? Wouldn't you do binary
search
in the other half in that case?

On Sat, May 9, 2015 at 5:23 PM, Zenna Tavares <
[email protected]>
wrote:

@scungao https://github.com/scungao and @soonhokong
https://github.com/soonhokong . I added a function for
binary-search
based optimisation in dReal(in dReal.jl/src/optimize.jl and there
are
examples in /test). If you would like any enhancements or changes,
we
can
discuss them here.

—
Reply to this email directly or view it on GitHub
#8.

—
Reply to this email directly or view it on GitHub
#8 (comment).

—
Reply to this email directly or view it on GitHub
#8 (comment).

—
Reply to this email directly or view it on GitHub.

[scungao]

If you exit only when the interval is smaller than epsilon, you do always get the epsilon-optimal value. If the first check before the loop says there's a solution, then in the last round, you can always return the upper half of the epsilon interval as the answer, regardless of whether you get sat or unsat.

The idea is you'll keep throwing away the lower half, and when it's epsilon small you are epsilon-close to the minimum. Take your -10 to 0 example, you'll end up with [-epsilon, -0.5*epsilon] even though it's unsat you are very close to the right value.

We can talk tmr about this.

On May 10, 2015, at 10:57, Zenna Tavares [email protected] wrote:

By get the right answer you mean get SAT? I don't think so. In either case
you could always get UNSAT or always SAT or both. It just depends on where
the true optimal value is compared to where you started.

For example if the minimum is zero but your original interval is -10 to 0
you will always get UNSAT because every test will examine the lower half of
the interval

Currently the default value is to stop after 10 itrrations but the stop
test is parameterised. Maybe a better default is the based on the size of
the interval as you said.

On 10 May 2015 10:33, "Sicun Gao" [email protected] wrote:

Ok right. I guess I was looking at the line outside the loop where it does
something when unsat is returned after the loop. I guess if you set the
exit condition of the loop to be only when the size of the cost interval
gets smaller than some epsilon (right now it's ten iterations?), then you
would mostly get the right answer up to epsilon, and the unsat should just
be exceptions.

On Sun, May 10, 2015 at 2:45 AM, Zenna Tavares [email protected]
wrote:

No if the half interval is unsat I set the other half interval (which I
didn't test but must contain the optimal cost) to be the "current
interval"
which will be split in the next iteration.
On 9 May 2015 22:23, "Sicun Gao" [email protected] wrote:

Great!

I took a brief look at the code and may have missed something: It
seems
if
the half interval gives you unsat, you stop? Wouldn't you do binary
search
in the other half in that case?

On Sat, May 9, 2015 at 5:23 PM, Zenna Tavares <
[email protected]>
wrote:

@scungao https://github.com/scungao and @soonhokong
https://github.com/soonhokong . I added a function for
binary-search
based optimisation in dReal(in dReal.jl/src/optimize.jl and there
are
examples in /test). If you would like any enhancements or changes,
we
can
discuss them here.

—
Reply to this email directly or view it on GitHub
#8.

—
Reply to this email directly or view it on GitHub
#8 (comment).

—
Reply to this email directly or view it on GitHub
#8 (comment).

—
Reply to this email directly or view it on GitHub.
—
Reply to this email directly or view it on GitHub.