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

可滿足性測試?yán)碚撆c應(yīng)用國際會(huì)議(SAT)是專注于命題可滿足性問題的理論與應(yīng)用的研究人員的頂級(jí)年度會(huì)議, 每一到兩年舉辦一次，至今已經(jīng)舉辦了二十六屆。SAT（可滿足性，SATisfiability）是當(dāng)今數(shù)學(xué)、計(jì)算機(jī)科學(xué)和人工智能等領(lǐng)域研究的前沿核心問題之一。許多重要領(lǐng)域中的大量問題，如大規(guī)模集成電路的自動(dòng)布線及其正確性驗(yàn)證、軟件自動(dòng)開發(fā)及其正確性驗(yàn)證、機(jī)器人動(dòng)作規(guī)劃、大型數(shù)據(jù)庫的維護(hù)以及包括財(cái)政、金融領(lǐng)域在內(nèi)的許多優(yōu)化問題等，都可轉(zhuǎn)化為SAT問題求解。在過去的二十年里，SAT研究的理論和實(shí)踐的進(jìn)步已經(jīng)使SAT技術(shù)成為許多領(lǐng)域（包括在形式驗(yàn)證、人工智能、運(yùn)籌學(xué)、計(jì)算生物學(xué)、密碼學(xué)、數(shù)據(jù)挖掘、機(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三個(gè)賽道。共有來自于26個(gè)國家的81個(gè)求解器參賽。參賽單位中國科學(xué)院軟件研究所計(jì)算機(jī)科學(xué)國家重點(diǎn)實(shí)驗(yàn)室、中國科學(xué)院大學(xué)、華中科技大學(xué)、上海交通大學(xué)、美國卡耐基梅隆大學(xué)、奧地利林茨大學(xué)、德國德累斯頓大學(xué)、弗萊堡大學(xué)、卡爾斯魯厄理工學(xué)院、加拿大滑鐵盧大學(xué)、荷蘭埃因霍溫理工大學(xué)、法國皮卡第儒勒·凡爾納大學(xué)、索邦大學(xué)、丹麥哥本哈根大學(xué)、瑞典隆德大學(xué)、印度理工學(xué)院、喀麥隆德尚大學(xué)、華為技術(shù)有限公司2012實(shí)驗(yàn)室、日本國家信息學(xué)研究所、德國理論信息學(xué)研究所等世界各地的大學(xué)、研究機(jī)構(gòu)及企業(yè)。

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

相關(guān)鏈接：

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

競賽成績公布文檔：

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