dReal gives unexpected result

[nikosarechiga]

Hello,

On the newest version of dReal (the one currently on the website), dReal claims that the following input is unsat, even though it is sat, when x1=0 and x2 = -1.

Interestingly, an older version of dReal (no idea from when) gives the correct answer.

(set-logic QF_NRA) (declare-fun x1 () Real) (declare-fun x2 () Real)

(assert (< x1 2)) (assert (< x2 2)) (assert (> x1 -2)) (assert (> x2 -2))

(assert (< (+ (^ x1 2) (^ x2 3)) 0))

(check-sat) (exit)

[scungao]

I fear that it’s related to the bug in floating point library again? Here’s some additional test cases:

1. Changing from < to <= makes it sat. But apparently the search is localized around zero.

   (set-logic QF_NRA) (declare-fun x1 () Real) (declare-fun x2 () Real)

   (assert (< x1 2)) (assert (< x2 2)) (assert (> x1 -2)) (assert (> x2 -2))

   (assert (<= (+ (^ x1 2) (^ x2 3)) 0))

   (check-sat) (exit)

2. Replacing x2^3 with x2 or sin(x2) will give sat

   (set-logic QF_NRA) (declare-fun x1 () Real) (declare-fun x2 () Real)

   (assert (< x1 2)) (assert (< x2 2)) (assert (> x1 -2)) (assert (> x2 -2))

   (assert (< (+ (^ x1 2) (sin x2)) 0))

   (check-sat) (exit)

but any other odd-power terms give unsat as well, for instance x2^5

(set-logic QF_NRA) (declare-fun x1 () Real) (declare-fun x2 () Real)

(assert (< x1 2)) (assert (< x2 2)) (assert (> x1 -2)) (assert (> x2 -2))

(assert (< (+ (^ x1 2) (^ x2 5)) 0))

(check-sat) (exit)

So I think something’s wrong about the interval evaluation of the power function..

On Jul 31, 2014, at 4:29 AM, Nikos Aréchiga notifications@github.com wrote:

Hello,

On the newest version of dReal (the one currently on the website), dReal claims that the following input is unsat, even though it is sat, when x1=0 and x2 = -1.

Interestingly, an older version of dReal (no idea from when) gives the correct answer.

(set-logic QF_NRA) (declare-fun x1 () Real) (declare-fun x2 () Real)

(assert (< x1 2)) (assert (< x2 2)) (assert (> x1 -2)) (assert (> x2 -2))

(assert (< (+ (^ x1 2) (^ x2 3)) 0))

(check-sat) (exit)

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

[scungao]

Apparently the power function is broken.

(set-logic QF_NRA) (declare-fun x () Real) (assert (< x 2)) (assert (> x -2)) (assert (< (^ x 3) 0)) (check-sat) (exit)

returns unsat.

[scungao]

The problem comes from bugs in the implementation of the interval power function in FILIB++. For the time being I reverted it to realpaver implementation of it and the answers are correct now. But I wouldn't be surprised if some other bugs can appear.

@narechiga Please try to build the new version and try. If you see other bugs just let us know.

Meanwhile @soonhokong and I are looking into more reliable interval computation libraries. The fundamental problem to solve is still the correctness of floating point implementations for basic functions.