verification - SMT求解器的局限性

Question

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

近年来，在SMT(可满足性模理论)求解器方面取得了许多进展，它们基本上用算术理论等扩充了命题逻辑。 SRI International的John Rushby甚至称其为破坏性技术。

可以用一阶逻辑处理但仍不能由SMT处理的最重要的实际问题示例是什么？最特别的是，在软件验证 Realm ，SMT无法解决哪些问题？

Answer 1

SMT求解器没有比SAT求解器强大的功能。对于SAT中的相同问题，它们仍将以指数时间运行或不完整。 SMT的优势在于，对于等效的饱和求解器来说，在SMT中显而易见的许多事情可能需要很长时间才能重新发现。

因此，以软件验证为例，如果您使用QF BV(无量化 vector 理论的位 vector )SMT求解器，则SMT求解器将意识到在单词级别上(a + b = b + a)，而SAT解算器可能需要很长时间才能证明使用各个 bool(boolean) 值。

因此，对于软件验证，您可以轻松地在软件验证中造成任何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求解器不完整，甚至比SAT求解器慢，因为它们正在尝试解决更难的问题。

也可以看看:

有趣的是，Beaver SMT solver将QF BV转换为CNF，并且可以使用SAT求解器作为后端。

Klee，它可以将程序编译为LLVM IR(中间表示)，并检查错误，并找到断言的反例。如果发现错误，则可以提供正确性的反例(它将为您提供)输入会重现该错误)。