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

Posted 2023-03-28

【中文标题】Dafny 作为 SAT-QBF 求解器没有给出正确的结果

【英文标题】：Dafny as a SAT-QBF solver is not giving right results

【发布时间】：2021-05-24 09:37:43

【问题描述】：

我正在努力养成使用 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（以及典型的 triggerswarnings），我也将其解释为 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

【参考方案1】：

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

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

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

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

【讨论】：

您好，感谢您的回答！！在我的编辑中，我使用未解释的函数解决了触发警告，但仍然无法正常工作。似乎我误解了断言违规的含义（我认为在某些情况下这是一个强有力的句子：assert(5