前言
创作开始时间：2022年11月16日16:18:59
如题，学习一下可满足性模理论 Satisfiability Modulo Theories的相关知识。参考：熊英飞老师2018《软件分析》课件。
正文
从SAT到SMT
理论（Theory）：
- 理论用于对这类符号（如大于，小于）赋予含义
- 理论包含一组公理和这组公理能推导出的结论
SMT可满足性模理论：
- 给定一组理论，根据给定背景逻辑，求在该组理论解释下公式的可满足性。
SMT历史
- Eager方法：将SMT编码成SAT问题
- Lazy方法：黑盒混合SAT求解器和各种理论求解器
z3求解器
参考：z3求解器(SMT)解各类方程各种逻辑题非常简单直观 https://blog.csdn.net/as604049322/article/details/120279521
z3-solver是由Microsoft Research(微软)开发的SMT求解器，它用于检查逻辑表达式的可满足性，可以找到一组约束中的其中一个可行解，缺点是无法找出所有的可行解
这个网页给了很多求解实例（含Python源码）。
SMT求解
参考：
- 金继伟，马菲菲，张 健.SMT求解技术简述[J].计算机科学与探索，2015，9（7）：769-780
SAT（satisfiability）问题指的是命题逻辑公式的
可满足性问题。随着研究的深入，人们发现SAT在 表达能力上有很大的局限性，许多应用用SAT进行 编码并不是很明智的选择，它们需要比SAT更强的 表达方式。
SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。SMT的全称是Satisfiability Modulo Theories，可被翻译为“可满足性模理论”、“多理论下的可满足性 问题”或者“特定（背景）理论下的可满足性问题”，其 判定算法被称为SMT求解器。
简单地说，一个SMT 公式是结合了理论背景的逻辑公式，其中的命题变 量可以代表理论公式。
命题逻辑、一阶逻辑和二阶逻辑
命题是具有真假值的陈述句。
一阶逻辑不同于单纯的“命题逻辑”，因为，一阶逻辑里面使用了任意和存在。举一个一阶逻辑表达式的例子：
谓词：一个含有变量的命题，例如上述math(x)。
二阶逻辑的量词符号竟然作用在谓词符号上∀ P \forall P∀P,之前我们在一阶谓词中只允许量词作用在个体上，例如∀ x P ( x ) \forall x P(x)∀xP(x)。这就是一阶逻辑和二阶逻辑的区别。
参考：
- 数理逻辑初步：命题逻辑、一阶逻辑和二阶逻辑 https://blog.csdn.net/qq_43391414/article/details/117397388
小结
后续再补充完善。
创作结束时间：2022年11月16日16:55:49