preprocessing loses precision

[scungao]

dReal returns unsat on the following formula

(set-logic QF_NRA) (declare-fun omega0 () Real) (assert (>= omega0 0.49999952316284185)) (assert (<= omega0 0.4999997615814209)) (assert (not (>= omega0 0.5))) (check-sat) (exit)

and it's clearly wrong.

What happens is when passing constants like 0.49999952316284185 from preprocessing to solving, it blurs it with 0.5, which is horrible. What's funny is the 2.14.5 version handles this formula right -- I found that out because the webpage is still using that version. So this is a second problem: we are not updating the version used on the webpage.

[soonhokong]

Yes, this is the item 7 that I mentioned in the chat. It also affects the proof checking as a side effect.

I will work on this today.

[nikosarechiga]

I can't believe you are working on Christmas.

[soonhokong]

Christmas holidays is known to be the most productive time for the geeks (i.e. Guido van Rossum created Python) :-)

[scungao]

Free parking!

[scungao]

Apart from precise representation, the deeper problem is when there isn't enough precision (which can always happen), the solver should have used the right rounding mode to ensure overapproximation, not rounding to the nearest.

[nikosarechiga]

I can't believe your wife lets you. On Dec 25, 2014 9:59 AM, "Sicun Gao" notifications@github.com wrote:

Free parking!

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

[soonhokong]

@scungao, can you check the version that you're using?

$ ./dReal --version
dReal version 2.14.12 (commit f0f27053ee5a)

In the latest version, I have SAT for the example with the following log:

$ ./dReal --verbose omega.smt2
nra_solver::check(incomplete)
icp_solver::create_rp_problem: variables
    omega0 : Real = [0.4999995231628419, 0.4999997615814209]
icp_solver::create_rp_problem: constraints
icp_solver::create_rp_problem: constraint: Not (<= 0.5 omega0)
icp_solver::create_rp_problem: constraint:  (<= omega0 0.5)
icp_solver::create_rp_problem: constraint:  (<= 0.5 omega0)
nra_solver::check(incomplete) result = true
============================
nra_solver::check(complete)
icp_solver::create_rp_problem: variables
    omega0 : Real = [0.4999995231628419, 0.4999997615814209]
icp_solver::create_rp_problem: constraints
icp_solver::create_rp_problem: constraint: Not (<= 0.5 omega0)
icp_solver::create_rp_problem: constraint:  (<= omega0 0.5)
icp_solver::create_rp_problem: constraint:  (<= 0.5 omega0)
icp_solver::prop_with_ODE()
Split Var: 0
icp_solver::solve: SAT with the following box:
         omega0 : [0.4999995231628419, 0.4999997615814209]
nra_solver::check(complete) result = true
============================
sat

[scungao]

The latest released version is still 2.14.8, which is what people are still using and told me about this bug. Do make a formal release of 2.14.12. However, the problem of failing to ensure overapproximation is not solved. I simply added a couple of 9 to make the following formula and it's unsat in the newest version.

(set-logic QF_NRA)
(declare-fun omega0 () Real)
(assert (>= omega0 0.4999999999999999999999952316284185))
(assert (<= omega0 0.499999999999999999999997615814209))
(assert (not (>= omega0 0.5)))
(check-sat)
(exit)

In fact, even with the original formula which seems to have the correct answer, something wrong is still going on. I changed 0.5 to 0.6 to make sure we don't confuse between the constants, i.e.:

(set-logic QF_NRA)
(declare-fun omega0 () Real)
(assert (>= omega0 0.499999952316284185))
(assert (<= omega0 0.49999997615814209))
(assert (not (>= omega0 0.6)))
(check-sat)
(exit)

and the trace becomes:

nra_solver::check(incomplete)
icp_solver::create_rp_problem: variables
    omega0 : Real = [0.4999999523162842, 0.4999999761581421]
icp_solver::create_rp_problem: constraints
icp_solver::create_rp_problem: constraint: Not (<= 0.6 omega0)
icp_solver::create_rp_problem: constraint:  (<= omega0 0.5)
icp_solver::create_rp_problem: constraint:  (<= 0.5 omega0)
nra_solver::check(incomplete) result = true
============================
nra_solver::check(complete)
icp_solver::create_rp_problem: variables
    omega0 : Real = [0.4999999523162842, 0.4999999761581421]
icp_solver::create_rp_problem: constraints
icp_solver::create_rp_problem: constraint: Not (<= 0.6 omega0)
icp_solver::create_rp_problem: constraint:  (<= omega0 0.5)
icp_solver::create_rp_problem: constraint:  (<= 0.5 omega0)
icp_solver::prop_with_ODE()
Split Var: 0
icp_solver::solve: SAT with the following box:
         omega0 : [0.4999999523162842, 0.4999999761581421]
nra_solver::check(complete) result = true
============================
sat

You see how the constants with multiple digits are simply treated as 0.5, which violates overapproximation.

[soonhokong]

1. 2.14.12 released.
2. There was a problem in printing Enode which caused icp_solver::create_rp_problem: constraint: (<= 0.5 omega0). I fixed it in the release.
3. The problem of failing to ensure over-approximation is not solved yet.

[soonhokong]

The problem of failing to ensure over-approximation is not solved yet.

1. For a domain definition such as:

   (assert (>= x c_1))
   (assert (<= x c_2))

where c_1 and c_2 are numeric constants, we can handle them specially so that in effect we have

   (assert (>= x ROUND_DOWNWARD(c_1)))
   (assert (<= x ROUND_UPWARD(c_2)))

2. In general, we have a constraint

   (>= f(..., c, ...))

   and it's not straightforward whether we need to use ROUND_DOWNWARD or ROUND_UPWARD to get the floating-point value of the string literal c.

I think there can be two approaches to solve the problem.

• (Plan A) Introduce a temporary variable for each numerical literal c.

  (declare-fun __tmp_c () Real)
  (assert (>= __tmp_c ROUND_DOWNWARD(c)))
  (assert (<= __tmp_c ROUND_UPWARD(c)))
  ...
  (>= f(..., __tmp_c, ...))

  We need to filter those temporary variables when we output a model, or visualize the ODEs.

• (Plan B) Another approach is to keep the string literal of c instead of converting it to its floating-point value. Then pass these string literals to constraint solvers (i.e. IBEX, CAPD, Realpaver). For this approach to work, we need to make sure that all the participating constraint solvers are handling the arbitrary-length string constants in a rigorous manner.

To me, (plan A) is the way to go.. What do you think?

[scungao]

Yes A is the way to go. We only need to do this when, at parsing time, we realize that it's possible to lose digits from a particular constant.