## 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 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 `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.

- 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)
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?

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