报告题目：SAT求解及其在EDA的应用

报告时间：2021年10月29日下午14:30-16:00

会议形式：线上会议

会议平台：腾讯会议

会议ID：231 272 198

报告人：蔡少伟 研究员

报告人简介：

蔡少伟，中科院软件所研究员, 博导，国家优青，智源青年科学家，中科院优秀导师，任中科院青促会信息与管理分会会长。2012年和2014年分别从北京大学获计算机博士学位，从Griffith大学与NICTA联合培养获应用数学博士学位，获优秀博士论文奖。主要研究约束求解，组合优化，自动算法工程。曾获得人工智能顶级期刊AIJ “近五年最受欢迎”论文，SAT 会议最佳论文奖，多次获得国际SAT比赛、MaxSAT比赛和SMT比赛的冠军，获国际EDA比赛亚军，联合逻辑奥林匹克金牌。发表CCF A类论文40余篇。研究成果被应用于芯片验证，云计算，电子地图导航，频谱分配等多个实际场景。

报告简介：命题逻辑可满足性问题（SAT）是计算机科学的一个核心问题，也是数理逻辑的基础问题，SAT求解器在工业中有重要应用，尤其是EDA领域的基础引擎，是芯片设计多个环节不可或缺的底层工具。本报告介绍SAT问题及其在EDA中的典型应用，并介绍常见的SAT算法以及近期在此方向的进展。