7月8日，在意大利阿爾蓋羅結(jié)束的第26屆可滿足性測試?yán)碚撆c應(yīng)用國際會議(The 26th International Conference on Theory and Applications of Satisfiability Testing)中，開云kaiyun開云官方網(wǎng)站系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室徐揚教授團隊取得優(yōu)異成績，李志輝副教授小組研發(fā)的求解器“CaDiCaL-Scave”獲得Main組第二名。

可滿足性測試?yán)碚撆c應(yīng)用國際會議(SAT)是專注于命題可滿足性問題的理論與應(yīng)用的研究人員的頂級年度會議, 每一到兩年舉辦一次，至今已經(jīng)舉辦了二十六屆。SAT（可滿足性，SATisfiability）是當(dāng)今數(shù)學(xué)、計算機科學(xué)和人工智能等領(lǐng)域研究的前沿核心問題之一。許多重要領(lǐng)域中的大量問題，如大規(guī)模集成電路的自動布線及其正確性驗證、軟件自動開發(fā)及其正確性驗證、機器人動作規(guī)劃、大型數(shù)據(jù)庫的維護以及包括財政、金融領(lǐng)域在內(nèi)的許多優(yōu)化問題等，都可轉(zhuǎn)化為SAT問題求解。在過去的二十年里，SAT研究的理論和實踐的進步已經(jīng)使SAT技術(shù)成為許多領(lǐng)域（包括在形式驗證、人工智能、運籌學(xué)、計算生物學(xué)、密碼學(xué)、數(shù)據(jù)挖掘、機器學(xué)習(xí)、數(shù)學(xué)等領(lǐng)域出現(xiàn)的問題）不可或缺的工具。因此，致力于構(gòu)建求解SAT問題的快速有效系統(tǒng)——SAT求解器這一基礎(chǔ)性工具，不僅在理論研究上而且在應(yīng)用領(lǐng)域都具有極其重要的意義。

本年度SAT求解器國際競賽共分為Main Track、Parallel Track、Cloud Track三個賽道。共有來自于26個國家的81個求解器參賽。參賽單位中國科學(xué)院軟件研究所計算機科學(xué)國家重點實驗室、中國科學(xué)院大學(xué)、華中科技大學(xué)、上海交通大學(xué)、美國卡耐基梅隆大學(xué)、奧地利林茨大學(xué)、德國德累斯頓大學(xué)、弗萊堡大學(xué)、卡爾斯魯厄理工學(xué)院、加拿大滑鐵盧大學(xué)、荷蘭埃因霍溫理工大學(xué)、法國皮卡第儒勒·凡爾納大學(xué)、索邦大學(xué)、丹麥哥本哈根大學(xué)、瑞典隆德大學(xué)、印度理工學(xué)院、喀麥隆德尚大學(xué)、華為技術(shù)有限公司2012實驗室、日本國家信息學(xué)研究所、德國理論信息學(xué)研究所等世界各地的大學(xué)、研究機構(gòu)及企業(yè)。

開云系統(tǒng)可信性自動驗證國地實驗室徐揚教授團隊長期致力于基于邏輯的自動演繹推理相關(guān)領(lǐng)域研究，原創(chuàng)地提出了基于矛盾體分離的多元、協(xié)同、動態(tài)自動演繹推理理論與方法。此次實驗室組織了包括數(shù)學(xué)、計算機、電氣在內(nèi)的跨學(xué)科團隊，結(jié)合多領(lǐng)域研究問題的形式化樣例特征，進行多輪研討推出了最新的求解器參賽。

相關(guān)鏈接：

第26屆國際SAT競賽主頁：https://satcompetition.github.io/2023/index.html

競賽成績公布文檔：

https://satcompetition.github.io/2023/downloads/satcomp23slides.pdf