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