形式化11：SMT概念

概念"/>

形式化11：SMT概念

SMT

SMT (satisfiability modulo theories)：可满足性模理论

课件描述

从形式上讲，SMT实例是一阶逻辑中的一个公式，其中一些函数和谓词符号具有额外的解释，SMT是确定此类公式是否可满足的问题。

对于常规的谓词逻辑来说，SAT是不可解的，但计算机科学往往采取一些折中的方案，将问题限制在一个特定子集中，这个子集被称为理论。

例如：EUF理论将问题限定在等式及未解释函数，LA理论将问题限定在线性算术及等式/不等式，BitVector将问题限制在位向量，可以说：

知乎回答

我理解的SMT就是在SAT的基础上，增加了一些一阶理论的内容。
首先明确SMT和SAT的概念，SAT是指命题逻辑公式可满足性判定问题，而SMT是指另外一类公式的可满足性判定问题。这一类公式具有两个特点：

• 在命题逻辑公式里面混入了一些一阶逻辑表达式；
• 具有任意的布尔结构。

命题逻辑公式大家都知道，比如：

P ∧ Q ∧ ( R → S ∨ ¬ T ) P\land Q \land (R \to S \lor \neg T) P∧Q∧(R→S∨¬T)

也就是只允许出现变量、变量的否定和逻辑连接词。

而SMT的公式可以是这样：

g ( a ) = c ∧ ( f ( g ( a ) ) ≠ f ( c ) ∨ g ( a ) = d ) ∧ c ≠ d g(a)=c\land (f(g(a))\ne f(c) \lor g(a)=d)\land c \ne d g(a)=c∧(f(g(a))=f(c)∨g(a)=d)∧c=d

• 这里面相对于命题逻辑公式，多了一些东西，也就是一开始所说的两个特点：首先多了一些非逻辑符号，比如函数 g ( a ) , f ( g ( a ) ) g(a),f(g(a)) g(a),f(g(a))，比如常量 c , d c,d c,d。命题逻辑里只有$P,Q,R,\to, \lor ,\land $这些逻辑符号，而非逻辑符号是一阶逻辑才有的内容；
• 其次，布尔结构被拓展了，这里可以理解为“变成了宏观的布尔结构”。比如 f ( g ( a ) ) ≠ f ( c ) , g ( a ) = d f(g(a))\ne f(c), g(a)=d f(g(a))=f(c),g(a)=d这种表达式，替代了原来布尔表达式所规定的“原子(atom)”的定义。

对于上面的第二点“拓展的布尔结构”，可以用这个例子加以理解。同样是借用上面的公式，进行以下转换：

g ( a ) = c ↦ P 1 f ( g ( a ) ) = f ( c ) ↦ P 2 g ( a ) = d ↦ P 3 c = d ↦ P 4 \begin{align} g(a)=c &\mapsto P1\\ f(g(a))= f(c) &\mapsto P2\\ g(a)=d &\mapsto P3\\ c = d &\mapsto P4 \end{align} g(a)=cf(g(a))=f(c)g(a)=dc=d​↦P1↦P2↦P3↦P4​​

于是原式变为了：

P 1 ∧ ( ¬ P 2 ∨ P 3 ) ∧ ¬ P 4 P1 \land (\neg P2 \lor P3)\land \neg P4 P1∧(¬P2∨P3)∧¬P4

这就变成了最普通的布尔表达式。所以可以说SMT的公式具有任意的抽象布尔结构，不关心atom的语义由什么构成（在命题逻辑中由变量构成，在一阶逻辑中由变量函数谓词构成），只关心逻辑连接词是什么。
因为SMT是由SAT+一阶理论构成，所以SMT的求解办法就是综合了SAT solver和Theory solver（默认它们俩都有自动求解工具），二者互相配合，共同求解。