SMT 求解器的局限性

Question

传统上，大多数计算逻辑工作要么是命题，在这种情况下您使用 SAT（布尔可满足性）求解器，要么是一阶的，在这种情况下，您使用一阶定理证明器。

近年来，SMT（可满足模理论）求解器取得了很大进展，它基本上用算术等理论来扩充命题逻辑； SRI International 的 John Rushby 甚至称其为颠覆性技术。

有哪些最重要的实际问题示例可以用一阶逻辑处理但仍不能用 SMT 处理？尤其是在软件验证领域出现了哪些SMT无法处理的问题？

Answer 1

SMT 求解器并不比 SAT 求解器强大。对于 SAT 中的相同问题，它们仍将在指数时间内运行或不完整。 SMT 的优势在于，许多在 SMT 中显而易见的东西可能需要很长时间才能让等效的 sat 求解器重新发现。

因此，以软件验证为例，如果您使用 QF BV（位向量的无量词理论）SMT 求解器，SMT 求解器将知道 (a+b = b+a) 在字级别相反，虽然 SAT 求解器可能需要很长时间才能证明使用单独的布尔值。

因此，对于软件验证，您可以轻松地在软件验证中遇到任何 SMT 或 SAT 求解器都难以解决的问题。

首先，必须在 QF BV 中展开循环，这意味着实际上您必须限制求解器检查的内容。如果允许使用量词，它就会变成一个 PSPACE 完全问题，而不仅仅是 NP 完全问题。

其次，一般认为很难的问题在 QF BV 中很容易编码。例如，您可以编写如下程序：

void run(int64_t a,int64_t b)
{
  a * b == <some large semiprime>;

  assert (false);
}

当然，现在 SMT 求解器将很容易证明 assert(false) 会发生，但它必须提供一个反例，它将为您提供输入 a,b。如果您将<some large number> 设置为 RSA 半素数，那么您只需反转乘法……也称为整数分解！因此，这对于任何 SMT 求解器都可能是困难的，并且表明软件验证通常是一个难题（除非 P=NP，或者至少整数分解变得容易）。这样的 SMT 求解器只是 SAT 求解器的一个优势，它用一种更易于编写和更易于推理的语言来修饰事物。

解决更高级理论的 SMT 求解器必然是不完整的，甚至比 SAT 求解器还要慢，因为它们试图解决更难的问题。

另见：

• 有趣的是，Beaver SMT solver 将 QF BV 转换为 CNF，并且可以使用 SAT 求解器作为后端。
• Klee 可以将编译为LLVM IR（中间表示）的程序，并检查错误，并找到断言的反例等。如果发现错误，它可以给出正确性的反例（它将为您提供重现错误的输入）。