SAT求解器

可满足性问题（SAT）是命题逻辑公式上的可满足性判定问题，在计算机理论、人工智能、密码分析，尤其是电子设计自动化等领域有重要的应用价值，其重要性受到多位图灵奖的主高度评价。

串行求解方面，SAT求解算法可以分为系统搜索算法和局部搜索算法，两者具有互补性。本课题组基于格局检测（CC）等技术研制的局部搜索SAT求解器CCASat，获得了国内首个SAT比赛的冠军。

Bart Selman等人于1997年提出了命题逻辑推理与搜索的十大挑战，其中第七项为聚焦于设计一个有效的混合求解算法。团队率先提出了一套"以系统搜索为主体，随机局部搜索辅助进行空间采样"的深度混合求解算法。相关技术投稿于SAT会议，获得了国内首个最佳论文奖。相关求解器获得了SAT比赛的多个冠军，且目前国际顶尖的串行SAT求解器均采用了相关混合求解技术。

并行求解器方面，本课题组自研了并行SAT求解框架PRS，同时支持存内并行和分布式并行。PRS系列求解器曾以大幅优势取得SAT并行组的国内首个冠军，和云计算赛道的亚军。目前国际主流的SAT并行求解器均基于PRS相关技术研制。

相关SAT求解器技术应用于等价性验证、工程变更指令等问题，成功落地于多家国内头部EDA公司；应用于密码分析，取得中央网信办”强网杯“密码数学挑战赛全国总冠军。