search

dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

Bug on large domains #67

Closed scungao closed 9 years ago

scungao commented 9 years ago

The new version hangs on the following formula. If given reasonable bounds on x then there's no problems. Something's wrong when handling larger domains.

(set-logic QF_NRA) (declare-fun x () Real) (assert (= x (+ x 10.0))) (check-sat) (exit)

soonhokong commented 9 years ago

I will fix it tonight. I just arrived at Pittsburgh by the way.

On Tuesday, January 20, 2015, Sicun Gao notifications@github.com wrote:

The new version hangs on the following formula. If given reasonable bounds on x then there's no problems. Something's wrong when handling larger domains.

(set-logic QF_NRA) (declare-fun x () Real) (assert (= x (+ x 10.0))) (check-sat) (exit)

— Reply to this email directly or view it on GitHub https://github.com/dreal/dreal/issues/67.

Soonho

scungao commented 9 years ago

Great. If I give big bounds it hangs as well, say

(set-logic QF_NRA) (declare-fun x () Real) (assert (< x 1000000000)) (assert (> x -1000000000)) (assert (= x (+ x 10.0))) (check-sat) (exit)

Now I suspect if this is an inherent problem and the solver really start branching on things, due to no clever preprocessing on the linear equality.

pzuliani commented 9 years ago

If I remember correctly Fedor observed a similar thing on the 'building planning' problems of his MSc project. (All linear stuff ...)

soonhokong commented 9 years ago

@scungao, your guess is right. I've added CtcPolytopeHull ibex contractor which uses a linear solver. It reduces the running time to 1.3 sec and it gives UNSAT for your latter example.

scungao commented 9 years ago

Fantastic!

On Jan 21, 2015, at 04:10, Soonho Kong notifications@github.com wrote:

@scungao, your guess is right. I've added CtcPolytopeHull ibex contractor which uses a linear solver. It reduces the running time to 1.3 sec and it gives UNSAT for your latter example.

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

scungao commented 9 years ago

Is this fixed in the new nra version or the main repo?

On Tue, Jan 27, 2015 at 3:28 AM, Soonho Kong notifications@github.com wrote:

Closed #67 https://github.com/dreal/dreal/issues/67.

— Reply to this email directly or view it on GitHub https://github.com/dreal/dreal/issues/67#event-225190877.

soonhokong commented 9 years ago

Not yet but we have a separate issue there.

On Tuesday, January 27, 2015, Sicun Gao notifications@github.com wrote:

Is this fixed in the new nra version or the main repo?

On Tue, Jan 27, 2015 at 3:28 AM, Soonho Kong <notifications@github.com javascript:_e(%7B%7D,'cvml','notifications@github.com');> wrote:

Closed #67 https://github.com/dreal/dreal/issues/67.

— Reply to this email directly or view it on GitHub https://github.com/dreal/dreal/issues/67#event-225190877.

— Reply to this email directly or view it on GitHub https://github.com/dreal/dreal/issues/67#issuecomment-71653047.

Soonho Kong soonhok@cs.cmu.edu