2021年11月30日下午2点，计算机与通信工程学院徐超博士在工科一楼B210室为计算机与通信工程学院与部分外院的本科生做了题为“可满足性问题求解器算法及应用”的本科生通识讲座报告。
     徐博士首先介绍了可满足性问题的定义，接着阐述了可满足性问题求解器近10年的快速发展，同时细致讲述了其分别在电子设计自动化（Electronics Design Automation,EDA）领域的广泛应用，以及其他领域，如机器人路线规划领域、密码学领域、资源分配领域、公式自动证明领域的成就。
EDA（电子设计自动化）技术是指包括电路系统设计、系统仿真、设计综合、PCB版图设计和制版的一整套自动化流程，是电子设计的基石产业，被誉为“芯片之母”。从市场规模看，百亿美金的EDA市场构筑了整个电子产业的根基，支撑起万亿美金的电子产业。“谁掌握了EDA，谁就有了芯片领域的主导权。”EDA作为我国“卡脖子”关键技术之一，难点主要在于算法，其核心问题在算法上通常具有极高的计算复杂度，即为NP难解问题。近几十年来，可满足性问题作为第一个NP完全问题，其研究取得了重大进展，特别是CDCL（Conflict Driven Clause Learning）求解器的提出，使得当前最新求解器可以在几分钟内解决数十万变量和数百万个子句的工业实例。由此，许多工业界的难解问题，并不直接求解，而是转化为可满足性问题实例快速求解，是今后很多重要研究领域的核心问题。