Unpredictable results from opensmt_check

[zenna]

@soonhokong Calling opensmt_check switches between true and false without any constraints being added.

using dReal
beale(x::Array) =  (1.5 - x[1] + x[1]x[2])^2 +
                (2.25 - x[1] + x[1]x[2]^2)^2 +
                (2.625 - x[1] + x[1]x[2]^3)^2
x = Var(Float64,"x",-5.12,5.12)
y = Var(Float64,"y",-5.12,5.12)
f = Var(Float64,"f",-10.,10.)
constraint = beale([x,y])
print(constraint)
add!(f == constraint)
@show is_satisfiable()
@show is_satisfiable()

(+ (^ (+ (* (^ y 3) x) (+ 2.625 (* -1 x))) 2) (+ (^ (+ (* (^ y 2) x) (+ 2.25 (* -1 x))) 2) (^ (+ (* y x) (+ 1.5 (* -1 x))) 2)))
is_satisfiable() => true
is_satisfiable() => false

[soonhokong]

I'm checking this one now. At least, A SMT2 file with double (check-sat) does not reproduce this problem.

[soonhokong]

It's related to the termination condition of our fixed-point computation. In theory, we should only stop when new_box == old_box holds by the definition of a fixed point. In practice, we use a heuristics in a terminating condition, to accelerate the fixed point computation and to overcome unstable numerical errors. The current heuristics is to stop a fixed-point computation when all dimensions are less than 1% reduced.

What happens in this example is the first check ends up with a box B_n as a result of fixed-point computation. It stops there because the difference between B_n-1 and B_n is small enough (all dimensions are reduced less than 1%). However, next time we compute B_n+1, the contractors prune out B_n to an empty box (B_n+1 = empty).

We can avoid this by changing the threshold. When I changed the line 229 of nra_solver.cpp file to have a smaller threshold (i.e. 0.01 ==> 0.00001), it goes away. However, this slows down the performance in general.

I think we should have two knobs to control fixed-point computation. For incomplete-checks, it's safe to use a bigger threshold so that we can have a good balance between pruning and branching. However, for complete-checks (esp, the final check for SAT), we should use a small enough threshold to guarantee that a solution is indeed a fixed-point.

I'll implement them and let you know what I did and how it changes the performance.

[soonhokong]

@zenna, please try the new version that I just released.

[zenna]

@soonhokong This seems to fix the problem. Thanks.

However, next time we compute B_n+1, the contractors prune out B_n to an empty box (B_n+1 = empty).

Why?

Do you mean when I call check the second time, the contraction starts with the box B_n (that was contracted before). Then, if this box is less than the precision, it's deemed to be empty, causing UNSAT?

[soonhokong]

Do you mean when I call check the second time, the contraction starts with the box B_n (that was contracted before).

Yes.

Then, if this box is less than the precision, it's deemed to be empty, causing UNSAT?

Not always. I meant that it is possible to happen.