2021年7月10日，正在巴塞羅那舉辦的國際SAT競賽組委會學(xué)術(shù)年會公布了2021年度第24屆國際SAT競賽結(jié)果，開云kaiyun開云官方網(wǎng)站系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室徐揚教授團隊取得優(yōu)異成績，李志輝副教授小組研發(fā)的求解器“Relaxed LCMDCBDL SCAVEL01”獲得Crypto組第二名、吳貫鋒老師小組研發(fā)的求解器“P-MCOMSPS-STR-32-SC”獲得Parallel Track UNSAT組第三名。
SAT（可滿足性，SATisfiability）問題是第一個被證明的NP完全問題，也是當今數(shù)學(xué)、計算機科學(xué)和人工智能等領(lǐng)域研究的前沿核心問題之一。許多重要領(lǐng)域中的大量問題，如大規(guī)模集成電路的自動布線及其正確性驗證、軟件自動開發(fā)及其正確性驗證、機器人動作規(guī)劃、大型數(shù)據(jù)庫的維護以及包括財政、金融領(lǐng)域在內(nèi)的許多優(yōu)化問題等，都可轉(zhuǎn)化為SAT問題求解。因此，致力于構(gòu)建求解SAT問題的快速有效系統(tǒng)——SAT求解器這一基礎(chǔ)性工具，不僅在理論研究上而且在應(yīng)用領(lǐng)域都具有極其重要的意義。
國際SAT競賽是學(xué)術(shù)界和工業(yè)界在SAT問題研究領(lǐng)域的最頂級賽事，每一到兩年舉辦一次，至今已經(jīng)舉辦了二十四屆。本次競賽設(shè)有Main、Crypto Track、Parallel Track、No-Limit Track、Cloud Track和CaDiCaL Hack Track共六個組，共有來自于16個國家的七十多個求解器參賽。參賽單位包括奧地利約翰尼斯開普勒大學(xué)、英國曼徹斯特大學(xué)、法國阿爾圖瓦大學(xué)、中國中科院、中國西安電子科技大學(xué)、德國安全研究實驗室，Intel，Google等世界各地的大學(xué)、研究機構(gòu)及企業(yè)。競賽題目均為業(yè)界實際應(yīng)用問題轉(zhuǎn)換而來，其中Crypto Track組競賽題目200個基準測試樣例，全部來自于密碼破解問題。
相關(guān)鏈接：
第24屆國際SAT競賽主頁：https://satcompetition.github.io/2021/
競賽成績公布文檔：https://satcompetition.github.io/2021/slides/ISC2021.pdf
