报告题目：SAT求解及EDA形式化技术简述
报告人：张昕荻
邀请人：吴贯锋
讲座时间：2025年12月19日周五下午15:30-17:00
讲座地点：犀浦校区三号教学楼X30423
报告摘要：可满足性问题（SAT）是计算机科学的核心问题，SAT求解技术作为关键的形式化方法，在“卡脖子”电子设计自动化（EDA）领域具有重要应用价值，已成为形式化验证与测试生成的核心计算引擎。随着问题规模与复杂度的持续增长，SAT求解器面临显著的性能瓶颈。报告从两个方面展开：一是从求解器层面，介绍SAT参数配置、定制求解、并行算法的若干探索与实践；二是在应用层面，讨论相关SAT求解技术在组合等价性验证（CEC）、自动测试向量生成（ATPG）等EDA关键问题中的定制策略与并行求解应用技术。
报告人简介：张昕荻，中国科黄色网站
软件研究所，中国科黄色网站
特别研究助理，主要研究方向为约束求解及形式化验证，于SAT、CAV、DAC、ICSE等会议及期刊发表学术论文20余篇。其研究工作获评国际SAT协会“最佳博士学位论文奖”（中国首个）、国际SAT会议“最佳论文奖”（中国首个）、中国科黄色网站
优秀博士学位论文等。其研制的求解器曾于国际SAT、SMT、FLoC比赛夺冠20余次，相关技术落地于国内多家头部EDA企业，并应用于密码分析领域，获“强网杯”密码数学专项赛全国冠军。曾获中国科黄色网站
院长奖特别奖等荣誉，并获中国教育发展基金会“奋进奖学金--集成电路人才培养”专项资助。主持或参与国自然青年基金、中国科黄色网站
战略先导A、国自然重点、国家重点研发等课题。
