SMT求解器的限制

Question

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

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

在一阶逻辑中可以处理但SMT仍然不能处理的问题的最重要的实际示例是什么？最特别的是，在软件验证领域出现了哪些SMT无法处理的问题？

Answer 1

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

因此，以软件验证为例，如果您使用QF BV (无量词理论的位向量) SMT求解器，则SMT求解器将意识到字级别上的(a+b = b+a)，而使用单个布尔值可能需要很长时间才能证明这一点。

因此，对于软件验证，您可以很容易地在软件验证中产生任何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解算器更慢，因为它们试图解决更难的问题。

另请参阅：

• Interestingly，Beaver SMT solver将QF BV转换为CNF，并可以使用SAT求解器作为back-end.
• Klee，该求解器可以接受编译为LLVM IR (中间表示)的程序，检查错误，并找到断言等的反例。如果发现错误，它可以给出正确的反例(它将给您提供将重现错误的输入)。