1

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

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

  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.

Theo Deep
  • 666
  • 4
  • 15
  • 2
    https://scungao.github.io/papers/delta_complete_decision_procedures.pdf. Delta-satisfiability has a very precise meaning and is explained in this paper. I recommend at least skimming through it and editing your question to just one topic at a time, which is much more productive on stack-overflow. – alias Dec 04 '22 at 17:10
  • Thanks a lot, I will read these papers and ask (individual questions) in case I still have the same doubts. – Theo Deep Dec 04 '22 at 18:13

1 Answers1

2

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.

Soonho Kong
  • 365
  • 1
  • 9
  • Thanks a lot, I will read the documentation and come back in case I still do not understand some points. But, meanwhile, may I ask two quick questions: (1, theoretical): putting '0.0' is not as saying that there is no over-approximation and, thus, `delta-SAT` would be equal to `SAT`? I mean, it sounds natural to me to think that there is a SAT concept when we e.g., do not include any non-linear math function. (2: practical): is there any way I can receive the answer `delta-SAT` or `UNSAT`, instead of the model? – Theo Deep Dec 04 '22 at 18:19
  • 1
    Putting 0.0 shouldn’t be allowed. If you read the paper, it says that delta in Q^+. You can write a frontend module checking wether an input formula includes non-linear functions or not and sending it to Z3 or CVC5 if the formula can be handled by a standard SMT solver. – Soonho Kong Dec 04 '22 at 19:01
  • 1
    I don’t understand the 2nd question. The tool already gives you delta-sat / unsat answers. If you don’t use a model, you can just throw it away. – Soonho Kong Dec 04 '22 at 19:02
  • As for the first question, then putting `0.0` should be reported as an error, right? I mean, in the tool. As for the second one, I mean that when I do `result = CheckSatisfiability(f_sat, 0.001)` then I directly receive the model. In Z3, instead, given a solver `s`, I can use `s.check()` (which responds `sat/unsat`) or use `s_def.model()` (to get the model). The `CheckSatisfiability` of dReal sounds to me like `s.check()`, but works as `s.model()` (since it returns a model); so the question is, is it a `s.check()` in dReal? – Theo Deep Dec 04 '22 at 20:07
  • 1
    1) Correct, getting `0.0` should be reported as an error. We will update the behavior of the API. 2) We also have the context-level API which you can find some examples at https://github.com/dreal/dreal4/blob/master/dreal/test/python/solver_test.py#L70-L76 . However, it only has `CheckSat` which returns a model in case of delta-sat. – Soonho Kong Dec 05 '22 at 21:57
  • Perfect, so to return 'sat' the trick is to manually state that if result of CheckSat is not 'UNSAT', then print 'delta-SAT'. – Theo Deep Dec 07 '22 at 20:31