形式化验证很好会议CAV 2021会议公布了第十六届国际可满足性模理论比赛(SMT-COMP 2021)比赛结果，中国科学院软件研究所（以下简称软件所）研究员蔡少伟带领团队研发得求解器荣获整数差分逻辑(QF_L)组第一名。这也是中国团队首次在SMT-COMP比赛中获得第一名。
“可满足性模理论问题（简称SMT）是特定背景理论下得一阶逻辑公式判定问题，是计算机科学和人工智能研究得核心问题之一，SMT求解器也是形式化验证得基础引擎。”蔡少伟表示。
会使用高级语言（如Pascal，C）编程得人，一定对可满足性问题不会感到陌生。在编程语言中，用于条件语句得布尔表达式由变量通过运算符以及“与”“或”“非”等逻辑连接符组合而成,给每个变量一个值，很容易判断出整个表达式是否为真。但反过来，给定一个表达式，是否能为每个变量找到值，使得整个表达式成真？这就是SMT得一种形式。
蔡少伟介绍，作为一种工具，SMT求解器在工业领域尤其是软硬件验证中具有广泛得应用价值。比如windows操作系统驱动程序得验证就用到了SMT求解器。
在此次SMT-COMP比赛中，蔡少伟团队自主研发了基于DPLL(T)和随机搜索混合得方法，打破了传统SMT求解器框架，在强数值约束得差分逻辑算例中取得了显著效果。
据悉，该研究团队长期从事约束求解器研究，进行SMT、SAT（命题逻辑可满足性问题）等计算机科学经典问题求解算法及工具得研发，并在相应领域国际大赛中多次获奖。其提出得约束求解技术和研制得SAT求解器已应用于华为公司得电路验证、腾讯地图优化、微软Azure云平台得虚拟机预配置和异常检测、以及美联邦通信得频谱分配等项目中。
