Some questions about dReal: delta-satisfiability, parameter with 0.0, doing the same in Z3 and obtaining sat/unsat result

Some questions about dReal: delta-satisfiability, parameter with 0.0, doing the same in Z3 and obtaining sat/unsat result

Problem Description:

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, 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)
  1. 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 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?

  1. 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.

  2. 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)

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.

  1. If this is so, is the problem with 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)

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?

  1. 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 .

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.

Rate this post
We use cookies in order to give you the best possible experience on our website. By continuing to use this site, you agree to our use of cookies.