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