欧冠滚球app

从SAT到SMT——逻辑约束求解研究获新突破

文章来源:  |  发布时间:2022-08-31  |  【打印】 【关闭

  

  近日,欧冠滚球app蔡少伟团队在逻辑约束求解器研究中获得新突破,SAT求解器和SMT求解器研究上的成果被重要期刊和会议录用,并在SAT、MaxSATSMT竞赛中斩获佳绩。 

  求解器被誉为工业软件之魂,是继芯片与操作系统之后的国之重器。命题逻辑可满足性问题(SAT)和可满足性模理论问题(SMT)是两个最重要的逻辑约束问题,SAT是命题逻辑上的约束求解问题, SMT是一阶谓词逻辑上的约束求解问题。它们不但在自动定理证明、软件工程等学术研究中有广泛应用,更是信息安全、集成电路设计自动化和软件验证等领域的底层计算引擎。 

  202285日,SAT会议正式公布了SATMaxSAT的比赛结果。在SAT比赛中,蔡少伟团队以明显优势获得了SAT比赛主赛道并行组冠军和NoLimits 赛道冠军(主要参与者包括蔡少伟研究员及其博士生张昕荻和硕士生陈志翰)。在MaxSAT比赛中,该团队赢得了几乎大满贯的好成绩:在总共6个赛道中获得5个冠军和1个亚军(主要参与者包括蔡少伟研究员及其博士后初一,其中1个冠军是与华为理论实验室的雷震东、东北师范大学的王艺源等人合作获得)。 

  值得一提的是,蔡少伟团队与国际上SAT研究的另一个主要团队(包括Armin Biere等人)合作的一篇SAT混合求解方法的论文以“Better Decision Heuristics in CDCL through Local Search and Target Phases.”为题,发表在人工智能著名期刊Journal Of Artificial Intelligence Research上。这篇文章为SAT混合求解方向提供了系统性的理论参考。 

  近两年,该团队开始转向更具挑战的SMT求解方向。SMT求解器的软件架构复杂,开发和维护工程难度大;而且SMT求解器体量庞大,目前的主流求解器,如Z3,CVC5,Yices2等都具有几十万甚至上百万行的代码量;此外,还需要开发者拥有扎实深厚的数学和逻辑学基础。因此SMT求解器的开发技术门槛比较高。 

  2022811日,在FLoC (Federated Logic Conference,国际联合逻辑大会 )IJCAR(国际联合自动推理会议)会议上宣布了SMT 2022比赛结果。蔡少伟团队研发的SMT求解器Z3++在比赛中获得线性算术理论和非线性算术理论的多项第一,并在Model Validation的所有赛道综合评分中求解能力领先。其总分获得FLoC奥林匹克竞赛颁发的2块金牌(大赛共设6枚金牌2枚银牌)。这是国内团队首次在FLoC奥林匹克竞赛的SMT比赛中取得金牌。FLoC每四年举办一次,对数理逻辑和计算机科学社区产生重要影响。 

  Z3++求解器是基于国际主流求解器Z3的衍生求解器,由蔡少伟研究员发起和领导,主要参与者包括他的博士生李博涵、张昕荻、赵梦宇和来自晞德软件公司的林锦坤博士,以及詹博华副研究员和他的硕士生王忠汉。Z3++针对其参与的各个理论都进行了深入的优化。对于位向量理论,Z3++采用了词级别和位级别的重写规则来化简约束;对于整数算术理论,该团队创新性地开发了首个针对整数算术理论的局部搜索求解器;对于非线性实数算术理论,该团队实现了可行域一致性检测并在NLSAT框架下实现了胞腔采样投影。Z3++显著地改进了著名的Z3求解器,其相关创新技术以“Local Search for SMT on Linear Integer Arithmetic”为题发表在理论计算机顶级会议CAV 2022上。 

  本次夺冠是蔡少伟团队继去年在SMT比赛中首次取得整数差分逻辑冠军后的又一次重大突破。相较于去年因单一理论取得第一,本次夺冠覆盖的理论更为广泛,也更为重要。团队现已将Z3++开源(https://z3-plus-plus.github.io)用于帮助更多研究人员及时学习Z3++相关技术,同时推动更多国内相关方向的研究人员对SMT求解器进行更深入地研究。 

  蔡少伟团队重视学术研究和工程实践的结合,提出的创新想法最终都能实现为求解器。研究成果多次在国际比赛获奖,并且应用于多个重要的工业场景。该团队还通过举办闭门论坛、专题训练营及新媒体科普等形式,为推动约束求解领域产业生态建设作出积极贡献。 

SAT比赛中以明显优势获得主赛道并行组冠军

在国际联合逻辑大会(FLoC)奥林匹克竞赛SMT比赛中获得2枚金牌

 

欧冠滚球app(发展)有限公司