Dreal4 Forall() SMT

Question

我想使用 Dreal4 SMT 求解器来检查控制 lyapunov 函数的以下条件：

对于V(x,u)为负的集合X中包含的所有x，存在一个包含在集合U中的u。（对于熟悉 CLF 的人，我将 V(x,u) 称为 V(x) 的导数。

我相信我应该能够使用 forall() 函数调用解决这个问题（尽管我似乎无法在文档中找到 exists()），但我不理解 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 boundrys（即使我设置的值会导致函数不能在任何地方都变成负数）我只得到一个 None return.

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

Answer 1

dReal 使用了delta-satisfiability 的概念；这不是你想要的。此外，它通过机器浮点数对实际值进行建模；这对于许多实际应用来说已经足够了，但是当你想证明这样的定理时，它在数学上并不可靠。

我不确定如何在 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 询问他们可能对您有更好建议的地方。请post回到这里你发现了什么！

获取模型

请注意，z3（和一般的 SMT 求解器）不显示模型中量化变量的值。要获取该值，您需要将其设为 top-level 声明的变量。为此，我们声明一个求解器并断言我们想要“证明”的内容是否定的。因此，您可以按如下方式对其进行编码：

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]

Dreal4 Forall() SMT

Dreal4 Forall() SMT

smt

z3

z3py

dreal

获取模型