SMT求解器的限制

Question

传统上，计算逻辑的大部分工作要么是命题逻辑，此时使用 SAT（布尔可满足性）求解器；要么是一阶逻辑，此时使用一阶定理证明器。

近年来，SMT（可满足性模理论）求解器取得了很多进展，基本上将命题逻辑与算术等理论结合起来；SRI国际公司的约翰•拉什比甚至称它们是一种颠覆性技术。

在一阶逻辑中可以处理的最重要的实际问题中，哪些问题仍无法通过 SMT 处理？尤其在软件验证领域中，会出现哪些不能由 SMT 处理的问题？

- rwallace

---

请参阅[cs.se]或[cstheory.se]。 - vzn

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。如果你将某个大数设置为RSA半素数，那么你刚刚颠倒了乘法……也就是整数分解！因此，这对于任何SMT求解器来说可能都很困难，并且表明软件验证通常是一个困难的问题（除非P=NP，或者至少整数分解变得容易）。这样的SMT求解器只是通过用更容易编写和更容易理解的语言来装扮事物，使SAT求解器更容易使用。

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

另请参见：

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

- Realz Slaw

---

请您能否详细说明为什么给出的QF BV示例对于SMT求解器来说会很困难？如果可能的话，您是否也可以一般性地展示这类问题的直觉。关于此事的任何参考资料也将不胜感激。谢谢。 - is7s

@is7s 我们可以在 聊天室 中讨论这个问题。 - Realz Slaw

在 run() 函数中，我认为你可能是想要 assert(a*b != <some large number>); 或者 if (a*b == <some large number>) assert(false);。a*b 不是一个左值，不能被赋值。如果这就是你的意思，那么 SMT 求解器不能轻易地证明 assert(false); 会发生：它首先必须证明这个大数是合数。无论如何，你可能需要编辑答案来修正 run() 的定义。 - D.W.

嗨@D.W.，好久不见了。是的，这是伪代码，但假设是类C语言，你是正确的。在SMT语言中，你只需制作逻辑语句，所以当时我写的方式更有意义。 - Realz Slaw

我对这个说法并不信服：“SMT求解器并不比SAT求解器更强大。”- 我猜你的意思是任何可以通过SMT求解器解决的问题都可以编码为SAT问题。对于固定BV问题来说，这显然是正确的，但对于参数化BV、非线性算术、字符串和量词等类型的问题呢？ - selig

请编辑并提供更准确的答案。 - Realz Slaw