How should I interpret this output?

LeventErkok commented 4 years ago

This is a question on how to interpret this output. For this benchmark:

(set-option :smtlib2_compliant true)
(set-option :produce-models true)
(set-logic ALL)
(declare-fun s1 () Real) (assert (= s1 0.0))
(declare-fun s3 () Real) (assert (= s3 (/ 1.0 1.0)))
(declare-fun s0 () Real)
(declare-fun s2 () Bool) (assert (= s2 (> s0 s1)))
(declare-fun s4 () Bool) (assert (= s4 (< s0 s3)))
(declare-fun s5 () Bool) (assert (= s5 (and s2 s4)))
(declare-fun s6 () Real) (assert (= s6 (sin s0)))
(declare-fun s7 () Real) (assert (= s7 (* s6 s6)))
(declare-fun s8 () Real) (assert (= s8 (cos s0)))
(declare-fun s9 () Real) (assert (= s9 (* s8 s8)))
(declare-fun s10 () Real) (assert (= s10 (+ s7 s9)))
(declare-fun s11 () Bool) (assert (= s11 (= s3 s10)))
(declare-fun s12 () Bool) (assert (= s12 (and s5 s11)))
(declare-fun s13 () Bool) (assert (= s13 (not s12)))
(assert s13)
(check-sat)
(get-option :precision)
(get-value (s0))

dReal produces:

delta-sat
0.001
(
    (s0 (interval (closed (/ 6005532640758553 9007199254740992)) (closed (/ 683 1024))))
)

The benchmark is asking dreal to find a value between 0 and 1 such that sin^2 x + cos^2 x is not equal to 1. Since this is a trigonometric identity, I'd have expected dReal to say unsat, but perhaps I'm misinterpreting the output here.

If I do a simple calculation on the lower-bound with an IEEE-754 double, I get:

Prelude> let x = (6005532640758553 / 9007199254740992) :: Double
Prelude> sin x * sin x + cos x * cos x
1.0

that is, I do not get a numeric error. My understanding is that the proof is over arbitrary reals backed by IEEE-doubles in models.

So, how should I interpret this output?

soonho-tri commented 4 years ago

Let me first rewrite the original formula:

  sin²x + cos²x ≠ 1
= ¬(sin²x + cos²x = 1)
= ¬[(sin²x + cos²x ≥ 1) ∧ (sin²x + cos²x ≤ 1)]
= (sin²x + cos²x < 1) ∨ (sin²x + cos²x > 1)

The meaning of delta-sat with a model is that any point in the model satisfies the delta-perturbation of the original formula:

(sin²x + cos²x ≤ 1 + δ) ∨ (sin²x + cos²x ≥ 1 - δ)

Since this is a trigonometric identity, LHS is always 1. So the formula reduces to:

  (1 ≤ 1 + δ) ∨ (1 ≥ 1 - δ)]
= (0 ≤ δ) ∨ (0 ≥ -δ)
= (0 ≤ δ)

Since δ is a positive rational, this formula always holds regardless of the choice of δ.

Reference:

LeventErkok commented 4 years ago

Thanks for the explanation. I need to read up on delta-perturbation more. Much appreciated.

dreal / dreal4

How should I interpret this output? #222