unsat result when a TaylorHOE Exception occurs

[ghost]

dReal is giving an unsat result for a satisfiable set of constraints.

Consider the van der pol oscillator system with dynamics x'=y, y'=(1-xx) \ y - x, with reach time 10, from the initial state x=1, y=0.5, and goal state x=0. The goal state is reachable, as can be seen from the following matlab plot:

This system corresponds to the following drh file:

//Vars
[0, 10.0] time;
[-1000,1000] x;
[-1000,1000] y;

// start modes
// running
{
  mode 1;
  invt:
  flow:
    d/dt[x] = y;
    d/dt[y] = (1.0 - x * x) * y - x;

  jump:

  // end running
}
// end modes

init:
@1 (and (x = 1.0) (y = 0.5));

goal:
@1 (x = 0);

which produces the following .smt2 file:

(set-logic QF_NRA_ODE)
(declare-fun y () Real)
(declare-fun x () Real)
(declare-fun y_0_0 () Real)
(declare-fun y_0_t () Real)
(declare-fun x_0_0 () Real)
(declare-fun x_0_t () Real)
(declare-fun time_0 () Real)
(declare-fun mode_0 () Real)
(define-ode flow_1 ((= d/dt[x] y) (= d/dt[y] (- (* (- 1 (* x x)) y) x))))
(assert (<= -1000 y_0_0))
(assert (<= y_0_0 1000))
(assert (<= -1000 y_0_t))
(assert (<= y_0_t 1000))
(assert (<= -1000 x_0_0))
(assert (<= x_0_0 1000))
(assert (<= -1000 x_0_t))
(assert (<= x_0_t 1000))
(assert (<= 0 time_0 [0.000000]))
(assert (<= time_0 10 [0.000000]))
(assert (<= 1 mode_0))
(assert (<= mode_0 1))
(assert (and (and (= y_0_0 0.5) (= x_0_0 1)) (= mode_0 1) (= [y_0_t x_0_t] (integral 0. time_0 [y_0_0 x_0_0] flow_1)) (= mode_0 1) (= mode_0 1) (= x_0_t 0)))
(check-sat)
(exit)

When running this in dReal, the result unsat is produced, which is incorrect.

When running with the -debug flag, I notice the computation is proceeding in inner_loop_forward, until a TaylorHOE Error occurs, as shown in this log snippet:

...
ode_solver::inner_loop_forward:[1.87826,1.87826]    {[0.000117051,0.000120758],[-1.72771,-1.7277]}
ode_solver::inner_loop_forward:[1.87826,1.87826]    {[0.000113344,0.000117051],[-1.72771,-1.72771]}
ode_solver::inner_loop_forward:[1.87826,1.87826]    {[0.000109637,0.000113344],[-1.72772,-1.72771]}
ode_solver::compute_forward: exception: TaylorHOE Error: minimal time step reached. Cannot integrate.
the set: {[0.000109637,0.000109637],[-1.72772,-1.72772]}
time step: [6.29425e-05,6.29425e-05]
ode_solver::compute_forward result = EXCEPTION
callODESolver: solve_forward result = UNSAT
***************** Not branched on Found UNSAT box ***********
icp_solver::solve: UNSAT
...

I believe this corresponds to around time ~= 1.878 and state x ~= 0.0001, y ~= -1.72, which is consistent with the matlab simulation. After the TaylorHOE Error occurs, the result of EXCEPTION becomes UNSAT, which propagates to be the final result the tool outputs.

Looking at the code, in src/dsolvers/ode_solver.cpp, in function ode_solver::solve_forward around line 557, we have this code, which we can relate to the log:

else {
        ret = compute_forward(bucket);
        DREAL_LOG_DEBUG << "ode_solver::compute_forward result = " << ret;
    }
    if (!m_trivial && (ret == ODE_result::SAT  || (ret == ODE_result::EXCEPTION && bucket.size() > 0))) {
        return prune_forward(bucket);
    } else {
        return ret;
    }

In this case, the second condition of the if statement is true, and prune_bucket is called. In turn, prune_bucket can only return SAT or UNSAT, which is where the result gets changed to UNSAT.

[soonhokong]

Dear @bak2, thank you for the report. I believe that the e8a9564 fixed the problem.

To test it, I had to modify your drh file as follows.

//Vars
[0, 10.0] time;
[0, 10.0] tau;
[-15,15] x;
[-15,15] y;

// start modes
// running
{
  mode 1;
  invt:
  flow:
    d/dt[x] = y;
    d/dt[y] = (1.0 - x * x) * y - x;
    d/dt[tau] = 1.0;

  jump:

  // end running
}
// end modes

init:
@1 (and (x = 1.0) (y = 0.5) (tau = 0.0));

goal:
@1 (and (x = 0) (tau > 5));

The changes are:

• introduce an explicit time variable tau to give constraint on it.
• reduce the range of x and y to [-15, 15]

It gives SAT result with the following visualization:

To test it, please delete build/external directory if you have any, then rebuild dReal.

[ghost]

Hello @soonhokong, thanks for the change; it seems to work.

A few questions:

• The variable tau and constraint tau > 5 was introduced just to show find the counter-example later time, right? Is there another reason for this?
• Limiting the ranges of the variables is just to improve performance, correct? It wouldn't be wrong to use [-1000,1000], just slow?
• The visualization you gave a is a .png image. Is there a way to generate these directly in the tool (as an alternative to the JSON output)?

Thanks!!

[soonhokong]

Dear @bak2,

The variable tau and constraint tau > 5 was introduced just to show find the counter-example later time, right? Is there another reason for this?

That is correct. It's just to generate a similar counterexample that you shared with us.

Limiting the ranges of the variables is just to improve performance, correct? It wouldn't be wrong to use [-1000,1000], just slow?

Yes, just for the performance issues.

The visualization you gave a is a .png image. Is there a way to generate these directly in the tool (as an alternative to the JSON output)?

For now, dReal only generates a .json file which is used to visualize a counterexample (details are explained in this link).