Dafny 作为 SAT-QBF 求解器没有给出正确的结果

问题描述

我试图养成使用 Dafny 作为一些简单公式的友好 SAT-QBF 求解器的习惯，因为在例如 Z3 中这样做太不舒服了。

这里的上下文是我已经实现了 Cooper 的量词消除算法，并且当所有变量都有界时，它可以用作决策过程：因此，我想知道我应该得到哪个结果之前执行它。

但是，我在 Dafny 中遇到了一个问题。

例如，让我们提出这个公式（用 Dafny 编写）：

  assert forall x_1: int :: exists y_1: int :: forall x_2: int :: exists y_2 : int
    :: (y_2<y_1) && (x_2<y_2) && (x_1<x_2);

在我的 Cooper 中，它返回 False，而 Dafny 返回 assertion violation（以及典型的 triggers 警告），我也将其解释为 False。好的，所以没问题。

但如果我加注：

  assert exists x_1: int :: exists y_1: int :: exists x_2: int :: exists y_2 : int
    :: (y_2<y_1) && (x_2<y_2) && (x_1<x_2);

在我的 Cooper 中，它返回 True，而 Dafny 也返回 assertion violation。我已经完成了手动 Cooper 执行（铅笔和纸），我认为 True 是正确的。

知道发生了什么吗？

PS：我还没有在 Z3 中尝试过，因为我正在尝试其他理论。

编辑

使用一个简单的技巧来实例化量化变量可以避免触发警告：创建一个未解释的函数。


method Main() {
 assert exists x_1 : int {:trigger P(x_1)} :: exists y_1: int {:trigger P(y_1)} 
    :: exists x_2: int {:trigger P(x_2)} :: exists y_2 : int {:trigger P(y_2)}
        :: (y_2<y_1) && (x_2<y_2) && (x_1<x_2);
}


predicate P(a: int)
{
   true
}

解决方法

你不能用 Dafny 做到这一点。虽然 Dafny 支持量词、布尔值、算术和许多其他东西（递归函数、集合、序列、对象和引用、多维数组、归纳、归纳和共归纳数据类型、位向量、单调函数的最大和最小固定点等），不适用于SAT-QBF（或QBF + artihmetic）基准测试。

Dafny 的错误，包括 assertion violation，告诉您验证者无法进行证明。可能该财产仍然有效，但您需要自己提供更多证据。换句话说，您应该将 assertion violation 解释为“不知道”的答案。换句话说，你不能用 Dafny 决定（只能半决定）公式。

Dafny 通过匹配模式（即触发器）在 SMT 求解器中使用量词。当一个量词没有好的触发器时，这就是 Dafny 的“无触发器”警告告诉你的，你可能会看到糟糕的性能、不稳定的验证和所谓的蝴蝶效应（程序中一个看似无关的小部分导致更改在其他证明的自动构造中）。触发器由未解释的函数符号驱动，您的示例根本没有。

如果你想要一个可读的语法，你可以通过 Boogie 来做你正在尝试的事情。我还没有尝试过，但是您可以尝试将 Boogie 置于其单态模式，然后提供证明者选项来要求 SAT-QBF 或类似的东西（请参阅 Boogie 的 /help）。否则，如果您对决定这些问题感兴趣，那么直接使用 SMT 求解器是最佳选择。

bounded-quantification dafny quantifiers z3