Dreal4 Forall() SMT

Question

我想使用Dreal4 SMT解算器来检查控制李亚普诺夫函数的下列条件：

集合U中包含一个u，对于集合X中包含的所有x，其中V(x，u)是负的。(我称V(x，u)为那些熟悉CLFs的人的V(x)的李导数)。

我相信我应该能够使用forall()函数调用来解决这个问题(虽然我在文档中似乎找不到一个存在())，但是我不理解forall函数的语法。

简单的例子：

我们会说x是有界的区间：-5，5和u -25,25。

def V(x,u):
    return (x**2) - 1 + u
problem = forall([x], And(V(x,u) < 0, x < 5, x > -5, u > -25, u < 25)
result = CheckSatisfiablitity(problem,0.01)

根据上述条件，这应该是正确的，因为对于每一个x，您都可以选择一个使函数为负值的u。不管我设置的u边界(即使我设置的值会导致函数在任何地方都不能变成负值)，我也只能得到一个无返回。

似乎我不理解forall()函数的语法，我应该如何使用forall()函数来验证这个条件？

Answer 1

dReal使用了增量可满足性的概念，这不是您想要的。另外，它还通过机器浮动来建模真值；对于许多实际应用来说，这是足够的，但是当你想要证明这样的定理时，它在数学上是不可靠的。

我不确定如何在dReal中证明这一点，但在z3中，您可以按照以下方式编写代码：

from z3 import *

def V(x, u):
    return (x**2) - 1 + u

x = Real('x')
u = Real('u')

prove(ForAll([x], Implies(And(x < 5, x > -5),
                          Exists([u], And(u > -25, u < 25, V(x, u) < 0)))))

注意嵌套量词的使用，它与您的问题定义相匹配。这些指纹：

proved

如果您出于其他原因不得不使用dReal，我建议您在https://github.com/dreal/dreal4/issues上询问他们可能有哪些更好的建议。请把你发现的东西寄回这里！

得到一个模型

请注意，z3 (和SMT求解器在一般情况下)不显示模型中量化变量的值。要获得该值，需要将其改为顶级声明变量。为了做到这一点，我们宣布一个解决者，并断言否定我们想要“证明”的东西。因此，您可以将其编码如下：

from z3 import *

def V(x, u):
    return (x**2) - 1 + u

x = Real('x')
u = Real('u')

s = Solver()
s.add(x < 5)
s.add(x > -5)

# Add the negation of what we want to prove
s.add(Not(Exists([u], And(u > -20, u < 25, V(x, u) < 0))))

r = s.check()
if r == sat:
    print("Counter-example:")
    print(s.model())
else:
    print("Solver said: ", r)

这些指纹：

Counter-example:
[x = 19/4]