SMT 求解器的局限性

Posted 2023-02-19

【中文标题】SMT 求解器的局限性

【英文标题】：Limits of SMT solvers

【发布时间】：2012-07-20 12:06:55

【问题描述】：

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

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

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

【问题讨论】：

另见Computer Science甚至Theoretical Computer Science

【参考方案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（中间表示）的程序，并检查错误，并找到断言的反例等。如果发现错误，它可以给出正确性的反例（它将为您提供重现错误的输入）。

【讨论】：

您能否详细说明为什么给定的 QF BV 示例对于 SMT 求解器来说会很困难？如果可能的话，您是否也能对此类问题表现出一般的直觉。对此事的任何参考也受到高度赞赏。谢谢。

@is7s 我们可以在chat讨论这个问题。

在run() 中，我想您的意思可能是assert(a*b != <some large number>); 或if (a*b == <some large number>) assert(false);。 a*b 不是左值；不能分配给它。如果这就是您的意思，SMT 求解器无法轻易证明assert(false); 会发生：它首先必须证明大数是复合数。无论如何，您可能需要编辑答案以修复 run() 的定义。

嗨@D.W.，很久了。是的，它是伪代码，但假设是类似 c 的语言，你是对的。在 SMT 语言中，您只需进行逻辑陈述，因此当时我编写它的方式更有意义。