SMT/SAT从0到0.1

最近在学习一些关于SMT/SAT solver的东西，在这里简单总结一下。

概念

• SMT: satisfiability modulo theories；wiki
• SAT: (boolean) satisfiability wiki

SMT可以认为是SAT的泛化。SAT基本只限制在求解boolean的一个表达式的satifiability上，即（是否有）赋值使得一个表达式为真(SAT)。 如若不存在这样的一组赋值，则这个表达式无法被满足(UNSAT)。

Software Verification

本章主要可以参考《Handbook of Satisfiability》中同名章节。

一般而言程序可以抽象为State + State Transition。前者是一些mappings(e.g., registers and memories)，后者则是在两个state上的relationship。

当知道程序目前的状态$s$和期望的属性$p$时，$s$ 和$\neg p$输入到SMT solver中。如果结果是UNSAT，则说明这个属性$p$被某一个状态$s$满足。 反之如果结果是SAT，则说明存在某一情况使得属性$p$被违背了。通常solver可以给出具体的一个例子。

在SMT solver的背后其实是SAT。在计算机中，整数被表示成bit vector的形式(e.g., 32位整数是32个bit组成的)，其计算也可以被“表示”成bit-wise logic arithmatics。 “这里”的表示实际上和数字电路里面用与或非门实现二进制运算的原理是一样的。而当把这些state转换成boolean value之后，SMT把这些东西随后丢进SAT solver中求解。

Soundness

然而SMT有时会给出错误的答案，这也催生了不少SMT fuzzing的工作。也有工作使用多个SMT solver来求解同一个问题，观察他们结果的不一致。

更加具体的文献可以参考我的note。

针对这个问题，人们也给出了很多解决方案。一方面是设计formally verified SAT/SMT solver，另一方面则是使得proof能够被验证。 此外，前者和后者也是可以相结合的。相关的工具和paper也可以在刚刚的note中找到。