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