近期，中国科学院软件研究所研究员蔡少伟团队在逻辑约束求解器研究中取得多项进展，并在命题逻辑可满足性问题（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每四年举办一次，在数理逻辑和计算机科学领域有着重要影响。