2196
2
0
2021-10-27 16:01:34
2021-10-27
報(bào)告題目：SAT求解及其在EDA的應(yīng)用
報(bào)告時(shí)間：2021年10月29日下午14:30-16:00
會(huì)議形式：線上會(huì)議
會(huì)議平臺(tái)：騰訊會(huì)議
會(huì)議ID：231 272 198
報(bào)告人：蔡少偉 研究員
報(bào)告人簡(jiǎn)介：
蔡少偉，中科院軟件所研究員, 博導(dǎo)，國(guó)家優(yōu)青，智源青年科學(xué)家，中科院優(yōu)秀導(dǎo)師，任中科院青促會(huì)信息與管理分會(huì)會(huì)長(zhǎng)。2012年和2014年分別從北京大學(xué)獲計(jì)算機(jī)博士學(xué)位，從Griffith大學(xué)與NICTA聯(lián)合培養(yǎng)獲應(yīng)用數(shù)學(xué)博士學(xué)位，獲優(yōu)秀博士論文獎(jiǎng)。主要研究約束求解，組合優(yōu)化，自動(dòng)算法工程。曾獲得人工智能頂級(jí)期刊AIJ “近五年最受歡迎”論文，SAT 會(huì)議最佳論文獎(jiǎng)，多次獲得國(guó)際SAT比賽、MaxSAT比賽和SMT比賽的冠軍，獲國(guó)際EDA比賽亞軍，聯(lián)合邏輯奧林匹克金牌。發(fā)表CCF A類論文40余篇。研究成果被應(yīng)用于芯片驗(yàn)證，云計(jì)算，電子地圖導(dǎo)航，頻譜分配等多個(gè)實(shí)際場(chǎng)景。
報(bào)告簡(jiǎn)介：命題邏輯可滿足性問(wèn)題（SAT）是計(jì)算機(jī)科學(xué)的一個(gè)核心問(wèn)題，也是數(shù)理邏輯的基礎(chǔ)問(wèn)題，SAT求解器在工業(yè)中有重要應(yīng)用，尤其是EDA領(lǐng)域的基礎(chǔ)引擎，是芯片設(shè)計(jì)多個(gè)環(huán)節(jié)不可或缺的底層工具。本報(bào)告介紹SAT問(wèn)題及其在EDA中的典型應(yīng)用，并介紹常見(jiàn)的SAT算法以及近期在此方向的進(jìn)展。
