近日,软件所计算机科学国家重点实验室蔡少伟研究员与其博士生张昕荻研发的求解器在SAT Competition 2020比赛中荣获Main Track SAT冠军。SAT Competition 2020比赛由第23届可满足性测试理论与应用国际会议SAT 2020（https://sat2020.idea-researchlab.org）组织举办。  

　　布尔可满性问题（SAT）是计算机科学的经典问题，也是历史上第一个被证明为NP完全的问题，不仅具有重要的理论研究价值，而且在工业领域尤其是软硬件验证中具有广泛的应用。例如，Intel芯片和Windows操作系统验证中都用到了SAT求解器。为促进SAT问题求解算法及工具的研发和应用，国际SAT学会自2002年以来每年（或每两年）组织SAT Competition国际比赛，至今已经举办了13届。 

　　在SAT Competition 2020比赛中，共有来自康奈尔大学、多伦多大学、曼彻斯特大学、俄罗斯科学院、柏林祖思研究所、法国国家信息与自动化研究所和Google等国际知名高校及科研院所的68个求解器参加比赛。蔡少伟研究员团队创新性的提出了松弛子句冲突学习方法，并采取变元重分配策略，很好的提高了主流SAT方法的寻解能力，最终取得了Main Track SAT第一名的好成绩。蔡少伟研究员团队曾在SAT Competition中多次获奖，包括SAT Competition 2014、2016亚军和2018冠军，并获得2018年联合逻辑奥林匹克金牌。 

　　蔡少伟研究员提出的启发式搜索技术和研制的SAT求解器被分别应用于微软Azure云平台的虚拟机预配置和异常检测、腾讯地图优化以及美联邦通信委员会的频谱分配等项目中，最近研究成果Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability发表在国际人工智能学报Artificial Intelligence (2020) 。 

    论文链接

　　SAT Competition 2020 Main Track SAT前三名