中国自主研发的求解器获得首届国际SMT大赛冠军。
近日，形式化验证高层会议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云平台虚拟机预配置与异常检测、美国联邦通信委员会频谱分配等项目。
