报告时间：2022.10.25周二 10.00
腾讯会议号：606-831-515
题目：EDA与约束求解
摘要：EDA（电子设计自动化）软件被成为芯片之母，其中，约束求解器是EDA软件的底层引擎。本报告介绍EDA中常见的约束问题包括布尔可满足性问题（SAT），可满足性模理论（SMT）问题，以及调度问题在EDA中的应用，并介绍主要的求解方法。
个人简介: 蔡少伟，中科院软件所研究员，博导，中科院优秀导师，获得国家优青项目资助。主要研究方向为约束求解、组合优化、EDA（电子设计自动化）算法。在CCF-A类国际顶级期刊和会议上共发表论文50余篇，首次解决布尔可满足性问题十大挑战的第7个挑战，获得SAT会议最佳论文奖，AIJ期刊5年最受欢迎论文，曾受邀在组合搜索领域国际著名会议SOCS 2021上做主旨报告。多次获得国际SAT比赛和SMT比赛的冠军，以及EDA比赛亚军。提出了格局检测策略，有效解决局部搜索的重要缺陷—循环现象，被广泛用于NP难组合优化问题。设计了搜索+推理的新型方法求解大规模组合优化问题，在多个著名组合优化问题如最大团，图着色，顶点覆盖，集合覆盖等NP难优化问题保持着前沿水平。他也致力于研究成果产业化，在EDA、软件验证、云计算、排班、智慧园区等领域展开了系列项目，担任EDA2开放合作机制的团队合作标准牵头人和形式化方向主编，发起了IJCAI workshop： Heuristic Search in Industries，并担任程序主席。
