关于SMT问题的讨论

Posted 2023-01-21 3A是个坏同志

SAT问题作为世界上第一个被证明的NP完全问题，在先前的博文中已经介绍过。虽然许多形式验证问题都可以归结为SAT问题，但由于SAT问题只以命题逻辑公式为处理对象而没有量词，制约了其描述能力和抽象层次，同时也限制了SAT问题的应用。例如在RTL电路中，由于SAT求解器的抽象层次较低，用位级信息描述问题将丢失大量的逻辑，同时增加问题的规模和复杂性，导致结果不准确并且增加求解的空间与时间开销。而SMT问题作为以引入了量词、谓词和个体词的一阶逻辑公式为处理对象的可满足性理论更加适用于求解这类复杂问题，因为它的描述能力更强，可以对于描述问题提供一个更灵活的框架。目前，SMT问题已经广泛应用于软件和硬件验证、类型推断、扩展静态检查、测试用例生成、调度、规划等问题中。

SMT问题的一种泛化问题是计数SMT问题，该问题不只需要找到一组解满足给定的一阶逻辑公式，还需要计算满足给定的一阶逻辑公式所有解的个数。因此计数SMT问题的难度也难于SMT问题。高效地解决计数SMT问题对人工智能、软件工程等很多领域都有着深远的影响。例如：在软件测试中，计算数据满足路径的个数问题可以转换成计数SMT问题进行求解；在电路设计上，可以利用计数SMT求解出使用较为频繁的电路，针对这些电路进行冗余设计。

近年来，计数SMT问题的研究已经开始得到重视。不过因为一阶逻辑系统虽然完备但并不可判定（不可判断任意公式的真假），所以目前的SMT求解器一般只针对一部分一阶逻辑的一个真子集求解，如比较简单的差分逻辑和线性实数运算，稍微复杂的线性整数运算，而更复杂的命题就进入了不可判定的领域。目前马菲菲等人给出了一种精确求解计数SMT问题的方法，但该求解器只能求解小规模的线性问题。求解大规模计数SMT问题的方法目前还处于研究当中，目前周俊萍等人使用差分进化算法优化了先前的精确SMT方法，可以求解大规模SMT问题的近似解。