報告題目：SAT求解及其在EDA的應用

報告時間：2021年10月29日下午14:30-16:00

會議形式：線上會議

會議平臺：騰訊會議

會議ID：231 272 198

報告人：蔡少偉 研究員

報告人簡介：

蔡少偉，中科院軟件所研究員, 博導，國家優(yōu)青，智源青年科學家，中科院優(yōu)秀導師，任中科院青促會信息與管理分會會長。2012年和2014年分別從北京大學獲計算機博士學位，從Griffith大學與NICTA聯(lián)合培養(yǎng)獲應用數學博士學位，獲優(yōu)秀博士論文獎。主要研究約束求解，組合優(yōu)化，自動算法工程。曾獲得人工智能頂級期刊AIJ “近五年最受歡迎”論文，SAT 會議最佳論文獎，多次獲得國際SAT比賽、MaxSAT比賽和SMT比賽的冠軍，獲國際EDA比賽亞軍，聯(lián)合邏輯奧林匹克金牌。發(fā)表CCF A類論文40余篇。研究成果被應用于芯片驗證，云計算，電子地圖導航，頻譜分配等多個實際場景。

報告簡介：命題邏輯可滿足性問題（SAT）是計算機科學的一個核心問題，也是數理邏輯的基礎問題，SAT求解器在工業(yè)中有重要應用，尤其是EDA領域的基礎引擎，是芯片設計多個環(huán)節(jié)不可或缺的底層工具。本報告介紹SAT問題及其在EDA中的典型應用，并介紹常見的SAT算法以及近期在此方向的進展。