本报讯（记者胡珉琦） 近日，形式化验证顶级会议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云平台的虚拟机预配置和异常检测，以及美联邦通信委员会的频谱分配等项目中。