I am starting with dReal and I have a set of questions about it.
These questions are based on the tutorial we can find in https://github.com/dreal/dreal4, section "Python bindings", with the following code:
from dreal import *
x = Variable("x")
y = Variable("y")
z = Variable("z")
f_sat = And(0 <= x, x <= 10,
0 <= y, y <= 10,
0 <= z, z <= 10,
sin(x) + cos(y) == z)
result = CheckSatisfiability(f_sat, 0.001)
print(result)
x : [1.2472345184845743, 1.2475802036740027]
y : [8.9290649281238181, 8.9297562985026744]
z : [0.068150554073343028, 0.068589052763514458]
I know these x,y and z are somehow the model that satisfies the formula, but I do not get their exact meanings. I mean, I know they have to do with delta-satisfiability, but what does x:[1.2472345184845743, 1.2475802036740027] mean? My (possibly wrong) interpretation is that any x within those bounds is a model. But, in that case, why does not the tool simply return any model within the bounds?
What is the second parameter of CheckSatisfiability(f_sat, 0.001)? Once again, it has to do with delta-satisfiability, but I do not know what it is exactly. Does it mean the 'comma precision' for which we want to find a model? That is, there could be cases in which a model is, say, 1.23455 so this would mean setting a precision of 'only' 0.001 is not capable to find the model, so would return unsat.
Playing with this precision, I find that I cant set it to be 0.0. For instance:
f_sat2 = And(0 <= x, x <= 10,
0 <= y, y <= 10,
0 <= z, z <= 10)
result2 = CheckSatisfiability(f_sat2, 0.0)
print(result2)
This outputs:
x : [5, 5]
y : [5, 5]
z : [5, 5]
Does this (a bound with a single number) mean that 5 is the (unique) model of x,y and z? That is, does setting precision to 0.0 yield the classic (not a delta-sat) satisfiabiliy problem? This would mean that dReal can be used also as a classic SMT solver.
0.0 representable with Z3? In that case, when I do the following in dReal:f_sat3 = And(0 <= x, x <= 10,
0 <= y, y <= 10,
0 <= z, z <= 10,
sin(x) + cos(y) == z)
result3 = CheckSatisfiability(f_sat3, 0.0)
print(result3)
And get the (unique) model:
x : [1.2473857557646206, 1.2473857557646206]
y : [8.9296050612226239, 8.9296050612226239]
z : [0.068270483891846451, 0.068270483891846451]
Does this mean that Z3 would also be able to give me these models? But, in that case, how could I implement these 'correct' sin() and cos() methods in Z3?
By the way, the reason that it is giving models with a huge comma precision (having set parameter 0.0) responds NO to the interpretation I made in the second question. So, again, what does the second parameter of CheckSatisfiability(f_sat, 0.001) mean?
PS: Where can I find more info, such as tutorials about the tool? Do we know any other similar tools that deal with nonlinear functions? I only have heard about MetiTarski.
I am one of the authors of dReal.
As suggested in the comment, I recommend to read dReal tool paper and “Delta-Complete Decision Procedures for Satisfiability over the Reals” paper. You can find them in https://scungao.github.io .
SMT problems over Reals are undecidable when they include non-linear math functions (e.g. trigonometric functions). This means that we cannot have a generic SMT solver for this theory. delta-satisfiability is a way to tackle this problem by introducing over-approximation. Consequently, a delta-satisfiability solver may return two types of answers; delta-SAT and UNSAT. The interpretation of UNSAT is standard, the input formula is unsatisfiable. The interpretation of delta-sat is that the over-approximated problem is satisfiable. The degree of over-approximation is determined by the user-provided input parameter (—precision). To be precise, when a solver returns a box, any point sampled in this box satisfies the over-approximated formula.