近日，形式化验证顶级会议CAV 2021会议公布了第十六届国际可满足性模理论比赛(SMT-COMP 2021)比赛结果。中国科学院软件研究所计算机科学国家重点实验室蔡少伟研究员与其学生李博涵、张昕荻研发的求解器荣获整数差分逻辑(QF_IDL)组冠军，这是中国团队首次在SMT-COMP比赛中获得冠军。

　　可满足性模理论问题（简称SMT）是特定背景理论下的一阶逻辑判定问题，是形式化验证的基础引擎。整数差分逻辑理论的SMT可以自然地描述时序相关的问题，广泛应用于时序系统验证，偏序数据结构的硬件模型检测，稳态模型计算。

　　在SMT-COMP 2021比赛中，QF_IDL组的参赛队伍包括斯坦福大学，爱荷华大学，弗莱堡大学，微软研究院，国际斯坦福研究所，法国国家信息与自动化研究所等国际知名高校及科研院所。蔡少伟团队创新性地设计了结合DPLL(T)和随机搜索方法的混合方法，打破了传统SMT求解器框架，在强数值约束算例中取得显著效果，最终在QF_IDL理论的Single query和Model validation赛道上都取得了第一名的好成绩。

　　蔡少伟研究员从事约束求解器、EDA核心算法研究，此前多次获得SAT比赛和MaxSAT比赛冠军， 2021年获SAT大赛Main track SAT、UNSAT组亚军，MaxSAT比赛完备组、非完备组冠军，EDA Challenge大赛亚军。相关方法发表在人工智能顶级期刊Artificial Intelligence 以及计算机理论著名会议SAT会议上，题为《Deep Cooperation of CDCL and Local Search for SAT》的论文获SAT 2021会议最佳论文奖。

　　论文链接：Deep Cooperation of CDCL and Local Search for SAT

    报道链接：探索工业软件之魂，板凳要坐十年冷 丨 中科院软件所蔡少伟专访