为啥 CVC4 SMT 求解器返回未知（不完整）？

Posted 2023-02-25

【中文标题】为啥 CVC4 SMT 求解器返回未知（不完整）？

【英文标题】：Why does CVC4 SMT solver return unknown (incomplete)?为什么 CVC4 SMT 求解器返回未知（不完整）？

【发布时间】：2022-01-12 20:30:52

【问题描述】：

我正在摆弄CVC4 SMT solver online version（使用 lang = cvc4）。

我没有使用标准的SMT-LIB format，而是the native language implemented by CVC4，因为它要简单得多。但是，我无法证明非常直接和明显的陈述。例如，第一个 CHECKSAT 给我 sat（可满足），这是正确的，但第二个 CHECKSAT 给我 unknow。

OPTION "incremental";

ASSERT FORALL (k : INT): ((k > 5 AND k < 7) => (k = 6));

CHECKSAT; % this returns sat, okay!

arr: ARRAY INT OF REAL;
ASSERT arr[6] = 123;

ASSERT FORALL (k : INT): ((k > 5 AND k < 7) => (arr[k] = 123));

CHECKSAT; % this returns unknown, why?

为什么 CVC4 不能证明这么简单的谓词逻辑表达式？据我了解，SMT 检查是不可判定的，因此，没有程序可以证明所有正确的陈述。但是，这似乎是一个非常简单的案例，所以我认为我误解了一些东西。

【参考方案1】：

正如您所指出的，量词使逻辑具有半可判定性，而 SMT 求解器通常不能很好地处理此类问题。然而，在这种特殊情况下，--fmf-bound 选项似乎是有效的。 （运行cvc4 --fmf-bound，你会看到它回复sat）。此参数启用基于有限整数边界的有限实例化，这恰好解决了这种情况。请注意，它可能适用于其他问题，也可能不适用于其他问题。

您可以通过在脚本中添加以下行来达到同样的目的：

OPTION "fmf-bound";

详情见本文：https://cvc4.cs.stanford.edu/papers/CADE24-2013/qi_for_fmf_reynolds_cade24.pdf

【讨论】：

成功了，谢谢！但是，如果我想使用更复杂的表达式，例如嵌套量词，您推荐哪些工具而不是 SMT 求解器？ Isabelle、HOL、Coq 等自动定理证明器？谢谢！

是的。如果您对使用量词进行推理感兴趣，Isabelle、HOL、Coq、Lean 等都是可以使用的工具。