21

Traditionally most work with computational logic was either propositional, in which case you used a SAT (boolean satisfiability) solver, or first-order, in which case you used a first-order theorem prover.

In recent years, a lot of progress has been made on SMT (satisfiability modulo theory) solvers, which basically augment propositional logic with theories of arithmetic etc.; John Rushby of SRI International goes so far as to call them a disruptive technology.

What are the most important practical examples of problems that can be handled in first-order logic but still can't be handled by SMT? Most particularly, what sort of problems arise that can't be handled by SMT in the domain of software verification?

4

1 回答 1

24

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 求解器将 QF BV 转换为 CNF，并且可以使用 SAT 求解器作为后端。
  • Klee可以将程序编译为LLVM IR（中间表示），并检查错误，并找到断言的反例等。如果发现错误，它可以给出正确性的反例（它会给你输入这将重现错误）。
于 2012-09-16T01:56:03.733 回答