icp_solver ignoring negated equality constraints

[danbryce]

In constructing the rp_constraints, the icp solver prints the literals to strings and compares them to "0 = 0". Looking at Enode.C, the print_infix method specifically looks for negated equality constraints and prints them as "0 = 0". This is causing me to get some wrong solutions. Am I missing something?

[soonhokong]

Looking at Enode.C, the print_infix method specifically looks for negated equality constraints and prints them as "0 = 0".

Yes, this is the case. Here is the related code: https://github.com/dreal/dreal/blob/master/src/opensmt/egraph/Enode.C#L356-L359

It's because under delta-perturbation, an expression of the form "X != Y" always evaluates to true. We don't really have "true" in realpaver, so it outputs "0 = 0" instead.

I believe this is meant to remove literals like the integral literals.

No. Removing integral literals and forall_t literals is done in different part of the code: https://github.com/dreal/dreal/blob/master/src/dsolvers/icp_solver.cpp#L299

This is causing me to get some wrong solutions. Am I missing something?

Well.. I don't really see a problem yet. Could you elaborate your problem more specifically?

[scungao]

This actually follows from the theory of delta-decision. The idea is any measure zero set would be ignored by the solver. The negation of an equality is consequently always delta sat -- it's only false at exactly 0, which means it's true almost everywhere. This is equivalent to treating strict and nonstrict inequalities as the same.

On Mar 12, 2015, at 09:36, Daniel Bryce notifications@github.com wrote:

In constructing the rp_constraints, the icp solver prints the literals to strings and compares them to "0 = 0". I believe this is meant to remove literals like the integral literals. Looking at Enode.C, the print_infix method specifically looks for negated equality constraints and prints them as "0 = 0". This is causing me to get some wrong solutions. Am I missing something?

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

[danbryce]

I don't have a small smt2 example just yet that illustrates the issue, but its something like this:

(= x_0_0 0)
(flow (d/dt[x] = 0))
(not (= x_0_t 0))

This should be unsat b/c we will infer that x_0_t is zero and it cannot be zero.

[soonhokong]

This is the corner case which Sean mentioned. You have two point values x = 0 and y = 0 and evaluate !(= x y) which should be false but we return true.

In dReal3, I've added an eval contractor which literally evaluates a constraint with a given box and rejects it if the evaluated result violates the constraint. https://github.com/dreal/dreal3/blob/master/src/util/constraint.cpp#L137-L168 Using this, for example, we can reject abs(x) < 0 with an assignment x = 0. So far, it supports >, <, >=, <=, == but not != simply because IBEX doesn't even have != in its data structure. But it's not so difficult to add support for != there using some hack.

In dReal2, if you really need this, you can implement one using realpaver and add the checking routine at the end of check as a final sweeper.

[soonhokong]

FYI, the following is UNSAT in dReal3 now:

(set-logic QF_NRA_ODE)
(declare-fun x_0 () Real)
(declare-fun x_t () Real)
(declare-fun time_0 () Real)
(define-ode flow_0 ((= d/dt[x] 0)))
(assert (>= time_0 0))
(assert (<= time_0 0.01))
(assert (= x_0 0))
(assert (not (= x_t 0)))
(assert (= [x_t]
           (integral 0. time_0 [x_0] flow_0)))
(check-sat)
(exit)

[danbryce]

Great. I’m going to wait for dreal3 instead of fixing dreal2. I was able to use an inequality for the same effect because the variable in question is an integer. I.e., x >= 1 has the same effect as x =/= 0.

On Mar 13, 2015, at 3:26 AM, Soonho Kong notifications@github.com wrote:

FYI, the following is UNSAT in dReal3 now:

(set-logic QF_NRA_ODE)
(declare-fun x_0 () Real)
(declare-fun x_t () Real)
(declare-fun time_0 () Real)
(define-ode flow_0 ((= d/dt[x]
0
)))
(assert (>= time_0
0
))
(assert (<= time_0
0.01
))
(assert (= x_0
0
))
(assert (not (= x_t
0
)))
(assert (= [x_t](integral
0
. time_0 [x_0] flow_0)))
(check-sat)
(exit)

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

[soonhokong]

OK. I'll let you know when ODE part of dReal3 is as good as the one in dReal2.