关于dReal的几个问题:delta-可满足性，参数为0.0，在Z3中做同样的操作，获得sat/unsat结果

Question

我从dReal开始，我有一系列关于它的问题。

这些问题是基于我们在https://github.com/dreal/dreal4 "Python“小节中可以找到的教程，其中包含以下代码：

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

x : [1.2472345184845743, 1.2475802036740027]
y : [8.9290649281238181, 8.9297562985026744]
z : [0.068150554073343028, 0.068589052763514458]

我知道这些x，y和z在某种程度上是满足公式的模型，但我没有得到它们的确切含义。我的意思是，我知道它们与增量-可满足性有关，但x:[1.2472345184845743, 1.2475802036740027]是什么意思？我(可能错了)的解释是，在这些界限内的任何x都是一个模型。但是，在这种情况下，为什么工具不直接返回边界内的任何模型呢？

1. CheckSatisfiability(f_sat, 0.001)的第二个参数是什么？再一次，它与增量-可满足性有关，但我不知道它到底是什么。这是否意味着我们想要找到模型的“逗号精度”？也就是说，在某些情况下，模型是，例如，unsat.

，这意味着设置“只有”0.001无法找到模型的精度，因此返回0.001

1. 这么精确地玩，我发现我不能把它设为0.0。例如：

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]

这是否意味着5是x、y和z的(唯一)模型？也就是说，为0.0设置精度是否会产生经典的(而不是delta)满意的问题？这意味着dReal也可以作为一个典型的SMT解决程序。

1. 如果是这样的话，0.0的问题可以用Z3来表示吗？在这种情况下，当我在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)

并得到(唯一的)模型：

x : [1.2473857557646206, 1.2473857557646206]
y : [8.9296050612226239, 8.9296050612226239]
z : [0.068270483891846451, 0.068270483891846451]

这是否意味着Z3也可以给我这些模型？但是，在这种情况下，我如何在sin()中实现这些“正确”的cos()和Z3方法？

顺便说一句，它给模型一个巨大的逗号精度的原因(设置参数0.0)对我在第二个问题中所做的解释没有反应。那么，再说一遍，CheckSatisfiability(f_sat, 0.001)的第二个参数是什么意思？

1. 如何在dReal而不是模型中获得SAT/UNSAT的结果？

PS:我在哪里可以找到更多的信息，例如关于该工具的教程？我们知道其他处理非线性函数的类似工具吗？我只听说过MetiTarski。

Answer 1

我是dReal的作者之一。

正如评论中所建议的那样，我建议阅读dReal工具文件和“基于Reals的可满足性的完全决策过程”文件。你可以在https://scungao.github.io找到他们。

当包含非线性数学函数(例如三角函数)时，Reals上的SMT问题是不可判定的。这意味着我们不能有一个通用的SMT求解者为这一理论。delta-可满足性是通过引入过逼近来解决这一问题的一种方法.因此，增量-可满足性求解器可能返回两种类型的答案: delta-SAT和UNSAT。UNSAT的解释是标准的，输入公式是无法满足的。三角卫星的解释是过逼近问题是可满足的.过逼近度由用户提供的输入参数(-precision)决定.准确地说，当一个求解者返回一个盒子时，这个盒子中采样的任何点都满足过近似公式。