作者：胡珉琦 来源：中国科学报

近日，形式化验证顶级会议CAV 2021会议公布了第十六届国际可满足性模理论比赛(SMT-COMP 2021)比赛结果，中国科学院软件研究所（以下简称软件所）研究员蔡少伟带领团队研发的求解器荣获整数差分逻辑(QF_IDL)组冠军。这也是中国团队首次在SMT-COMP比赛中获得冠军。

“可满足性模理论问题（简称SMT）是特定背景理论下的一阶逻辑公式判定问题，是计算机科学和人工智能研究的核心问题之一，SMT求解器也是形式化验证的基础引擎。”蔡少伟表示。

会使用高级语言（如Pascal，C）编程的人，一定对可满足性问题不会感到陌生。在编程语言中，用于条件语句的布尔表达式由变量通过运算符以及“与”“或”“非”等逻辑连接符组合而成,给每个变量一个值，很容易判断出整个表达式是否为真。但反过来，给定一个表达式，是否能为每个变量找到值，使得整个表达式成真？这就是SMT的一种形式。

蔡少伟介绍，作为一种工具，SMT求解器在工业领域尤其是软硬件验证中具有广泛的应用价值。比如windows操作系统驱动程序的验证就用到了SMT求解器。

在此次SMT-COMP比赛中，蔡少伟团队自主研发了基于DPLL(T)和随机搜索混合的方法，打破了传统SMT求解器框架，在强数值约束的差分逻辑算例中取得了显著效果。

据悉，该研究团队长期从事约束求解器研究，进行SMT、SAT（命题逻辑可满足性问题）等计算机科学经典问题求解算法及工具的研发，并在相应领域国际大赛中多次获奖。其提出的约束求解技术和研制的SAT求解器已应用于华为公司的电路验证、腾讯地图优化、微软Azure云平台的虚拟机预配置和异常检测、以及美联邦通信委员会的频谱分配等项目中。