总站|20700app大阳城

面向世界科技前沿、面向经济主战场、面向国家重大需求、面向人民生命健康,率先实现科学技术跨越发展,率先建成国家创新人才高地,率先建成国家高水平科技智库,率先建设国际一流科研机构。

——总站|20700app大阳城办院方针

首页 > 一线动态

软件所在逻辑约束求解领域多项比赛中取得佳绩

2022-09-02 软件研究所
【字体:

语音播报

  近期,总站|20700app大阳城软件研究所研究员蔡少伟团队在逻辑约束求解器研究中取得多项进展,并在命题逻辑可满足性问题(SAT)、可满足性模理论问题(SMT)等多项竞赛中斩获佳绩。

  在逻辑约束求解器领域,SAT和SMT是两个最重要的逻辑约束问题。SAT是命题逻辑上的约束求解问题,SMT是一阶谓词逻辑上的约束求解问题。它们不仅在自动定理证明、软件工程等学术研究中有广泛应用,还是信息安全、集成电路设计自动化和软件验证等领域的底层计算引擎。

  近日,SAT会议公布SAT和MaxSAT比赛结果,FLoC(Federated Logic Conference,国际联合逻辑大会)的IJCAR(国际联合自动推理会议)会议宣布SMT 2022比赛结果。 

  在SAT比赛中,蔡少伟团队以明显优势获得主赛道并行组冠军和NoLimits赛道冠军;在MaxSAT比赛中,团队赢得几乎大满贯的成绩,在总共6个赛道中获得5个冠军和1个亚军(其中1个冠军与华为理论实验室、东北师范大学等团队合作获得)。

  在SMT 2022比赛中,蔡少伟团队研发的SMT求解器Z3++(基于国际主流求解器Z3的衍生求解器)在比赛中获得线性算术理论和非线性算术理论的多项第一,并在Model Validation的所有赛道综合评分中求解能力领先。其总分获得FLoC奥林匹克竞赛颁发的2块金牌(大赛共设6枚金牌2枚银牌)。这是国内团队首次在FLoC奥林匹克竞赛的SMT比赛中取得金牌。FLoC每四年举办一次,在数理逻辑和计算机科学领域有着重要影响。  

打印 责任编辑:程博

扫一扫在手机打开当前页

© 1996 - 总站|20700app大阳城 版权所有 京ICP备05002857号-1 京公网安备110402500047号 网站标识码bm48000002

地址:北京市西城区三里河路52号 邮编:100864

电话: 86 10 68597114(总机) 86 10 68597289(总值班室)

编辑部邮箱:casweb@cashq.ac.cn

  • © 1996 - 总站|20700app大阳城 版权所有 京ICP备05002857号-1 京公网安备110402500047号 网站标识码bm48000002

    地址:北京市西城区三里河路52号 邮编:100864

    电话: 86 10 68597114(总机) 86 10 68597289(总值班室)

    编辑部邮箱:casweb@cashq.ac.cn

  • © 1996 - 总站|20700app大阳城 版权所有
    京ICP备05002857号-1
    京公网安备110402500047号
    网站标识码bm48000002

    地址:北京市西城区三里河路52号 邮编:100864
    电话:86 10 68597114(总机)
       86 10 68597289(总值班室)
    编辑部邮箱:casweb@cashq.ac.cn

  • Baidu
    sogou