SMT求解器的限制

Question

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

近年来,SMT(可满足模理论)求解器取得了很大进展,基本上用算术等理论来增强命题逻辑.SRI International的John Rushby甚至称他们为颠覆性技术.

在一阶逻辑中可以处理但仍然无法由SMT处理的问题最重要的实际例子是什么？最特别的是,SMT在软件验证领域无法解决哪些问题？

Answer 1

SMT求解器不比SAT求解器强大.对于SAT中的相同问题,它们仍将在指数时间内运行或不完整.SMT的优势在于许多SMT中显而易见的事情可能需要很长时间才能重新发现等效的坐标求解器.

因此,以软件验证为例,如果使用QF BV(无量词理论的位向量)SMT求解器,SMT求解器将意识到(a + b = b + a)在字级上,而它可能需要一个SAT求解器很长时间来证明使用单独的布尔值.

因此,对于软件验证,您可以轻松地在任何SMT或SAT求解器难以进行的软件验证中出现问题.

首先,循环必须在QF BV中展开,这意味着实际上你必须限制求解器检查的内容.如果允许量词,它就会成为PSPACE完全问题,而不仅仅是NP-complete.

其次,一般认为很难的问题很容易在QF BV中编码.例如,您可以编写如下程序:

void run(int64_t a,int64_t b)
{
  a * b == <some large semiprime>;

  assert (false);
}

当然,SMT求解器很容易证明断言(假)会发生,但它必须提供一个计数器示例,它将为您提供输入a,b.如果你设置 <some large number>为RSA semiprime,那么你只需要反转乘法...否则称为整数分解!因此,对于任何SMT求解器来说这可能都很难,并且证明软件验证通常是一个难题(除非P = NP,或者至少整数因子分解变得容易).这样的SMT求解器只是SAT求解器的一部分,它通过一种易于编写且易于理解的语言来装饰.

解决更高级理论的SMT求解器必然不完整或甚至比SAT求解器更慢,因为它们试图解决更难的问题.

也可以看看:

• 有趣的是,Beaver SMT求解器将QF BV转换为CNF,并且可以使用SAT求解器作为后端.
• Klee可以将程序编译为LLVM IR(中间表示),并检查错误,并查找断言的反例等.如果发现错误,它可以给出正确性的反例(它会给你输入这将重现这个bug).