search

dreal / DReal.jl

Nonlinear Constraint Solving and Optimization
https://dreal.github.io/
Other
7 stars 4 forks source link

Boolean SAT is wrong #4

Closed zenna closed 9 years ago

zenna commented 9 years ago

@scungao was correctly surprised the Boolean types work because actually they don't seem to be. The C-API gives back a=1,b=1 for a formula not a or not b. Any thoughts @soonhokong?

using dReal
using Base.Test
a = Var(Bool,"a")
b = Var(Bool,"b")
add!(!a | !b)
model_a,model_b =  model(a,b)
@test !model_a | !model_b
soonhokong commented 9 years ago

Let me check this in an hour.

soonhokong commented 9 years ago

Good news is that our SMT solver is correct in a sense that the following example gives us UNSAT:

(set-logic QF_NRA)
(declare-fun x () Bool)
(declare-fun y () Bool)
(assert (= x true))
(assert (= y true))
(assert (or
         (not x)
         (not y)))
(check-sat)
(exit)

I think the problem is in the way dReal assigns Boolean model. I guess nothing really happens for Boolean cases for now and it gets True(1) which is a default value. Let me take a closer look at this one.

soonhokong commented 9 years ago

@zenna, I think the problem is at https://github.com/dreal/dReal.jl/blob/master/src/construct.jl#L179. Note that the return type of opensmt_get_bool is not Bool but opensmt_result which is a three-valued entity (-1 : false, 0 : undef, +1 : true).

I think what happens is that OpenSMT returns x : False (-1) and y : True (+1), but dReal.jl interprets both of them as True (non-zero values).

Can you check whether this is the case?

zenna commented 9 years ago

Yes. You were right.

Fixed in d9d39077eadc8f24a37f9aec7a8c7f549247ba43

soonhokong commented 9 years ago

Nice. Thanks!!

soonhokong commented 9 years ago

I agree that @scungao is great! No doubt he foresaw all these details :-)