摘要：

约束求解根植于数理逻辑和数学优化等基础理论。其中，布尔可满足性 (Boolean Satisfiability，简称 SAT)问题是命题逻辑判定问题，可满足性模理论（Satisfiability Modula Theories，简称SMT）问题则对应带背景理论的逻辑判定问题。SAT求解器是芯片设计与验证的计算引擎，SMT求解器是软件测试与验证的计算引擎，它们也在数学定理自动证明和密码学等多个领域有重要应用。本报告介绍EDA问题和软件验证问题到SAT和SMT的建模，以及SAT和SMT的主要算法，包括基于CDCL框架的方法和局部搜索算法，最后介绍基于大模型的研发方法。

报告人简介：

蔡少伟， 北京航空航天大学教授，主要研究约束求解和硬件形式化验证，获得领域顶级会议CAV/CP/SAT的最佳论文奖/杰出论文奖，多次获得SAT比赛和SMT比赛冠军，在我国密码学顶级赛事，华为鸿蒙创新大赛，EDA精英挑战赛等多次获得冠军和特别奖。带领研发的求解器被集成到英伟达、微软、英特尔、华大九天等公司的软件中，应用于芯片设计和验证、操作系统验证、云平台故障检测、以及工业调度。担任SAT 2027会议程序委员会主席，EDA^2形式化验证标准组组长，《EDA技术白皮书》形式化验证方向主编，曾在FMCAD、CP和SOCS等著名国际会议做特邀报告。