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