Some questions about dReal: delta-satisfiability, parameter with 0.0, doing the same in Z3 and obtaining sat/unsat result
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)
- If we execute the code, then we obtain the following:
x : [1.2472345184845743, 1.2475802036740027] y : [8.9290649281238181, 8.9297562985026744] z : [0.068150554073343028, 0.068589052763514458]
I know these
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.23455so this would mean setting a precision of ‘only’
0.001is not capable to find the model, so would return
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)
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
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.
- If this is so, is the problem with
0.0representable 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’
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?
- How can I get the result SAT/UNSAT in dReal, instead of a model?
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.
Solution – 1
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.