可滿足性問題求解器算法及應用--徐超博士作通識教育講座
發布時間: 2021-12-05 19:46:41 瀏覽量:
2021年11月30日下午2點，計算機與通信工程學院徐超博士在工科一樓B210室為計算機與通信工程學院與部分外院的本科生做了題為“可滿足性問題求解器算法及應用”的本科生通識講座報告。
徐博士首先介紹了可滿足性問題的定義，接著闡述了可滿足性問題求解器近10年的快速發展，同時細致講述了其分別在電子設計自動化（Electronics Design Automation,EDA）領域的廣泛應用，以及其他領域，如機器人路線規劃領域、密碼學領域、資源分配領域、公式自動證明領域的成就。
EDA（電子設計自動化）技術是指包括電路系統設計、系統仿真、設計綜合、PCB版圖設計和制版的一整套自動化流程，是電子設計的基石產業，被譽為“芯片之母”。從市場規模看，百億美金的EDA市場構筑了整個電子產業的根基，支撐起萬億美金的電子產業。“誰掌握了EDA，誰就有了芯片領域的主導權。”EDA作為我國“卡脖子”關鍵技術之一，難點主要在于算法，其核心問題在算法上通常具有極高的計算復雜度，即為NP難解問題。近幾十年來，可滿足性問題作為第一個NP完全問題，其研究取得了重大進展，特別是CDCL（Conflict Driven Clause Learning）求解器的提出，使得當前最新求解器可以在幾分鐘內解決數十萬變量和數百萬個子句的工業實例。由此，許多工業界的難解問題，并不直接求解，而是轉化為可滿足性問題實例快速求解，是今后很多重要研究領域的核心問題。