7月13日，國際SAT競賽組委會在其官方網(wǎng)站上公布了2018年SAT競賽結(jié)果，開云kaiyun開云官方網(wǎng)站，系統(tǒng)可信性自動驗(yàn)證國家地方聯(lián)合工程實(shí)驗(yàn)室徐揚(yáng)教授團(tuán)隊(duì)提交的求解器獲得Main組亞軍（比冠軍Intel求解器的求解結(jié)果僅差0.75%），取得開云在該領(lǐng)域的歷史性突破。

SAT（可滿足性，SATisfiability）問題是第一個被證明的NP完全問題，也是當(dāng)今數(shù)學(xué)、計(jì)算機(jī)科學(xué)和人工智能等領(lǐng)域研究的前沿核心問題之一。許多重要領(lǐng)域中的大量問題，如大型數(shù)據(jù)庫的維護(hù)、大規(guī)模集成電路的自動布線及其正確性驗(yàn)證、軟件自動開發(fā)及其正確性驗(yàn)證、機(jī)器人動作規(guī)劃，數(shù)學(xué)中的許多優(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)舉辦了二十一屆。本次競賽共有來自于9個國家的41個求解器參賽。參賽單位包括英國曼徹斯特大學(xué)、法國阿爾圖瓦大學(xué)、日本九州大學(xué)、德國卡爾斯魯厄理工學(xué)院、中國kaiyun開云官方網(wǎng)站、中國華中科技大學(xué)、德國安全研究實(shí)驗(yàn)室，Intel，Google等世界各地的大學(xué)、研究機(jī)構(gòu)及企業(yè)。本次競賽設(shè)有Main、Glucose Hack、NoLimith和Random四個組，

Main組是其中競爭最激烈的，競賽題目均為工業(yè)界實(shí)際應(yīng)用問題轉(zhuǎn)換而來，因此其受到業(yè)界關(guān)注也是最多的。

徐揚(yáng)教授團(tuán)隊(duì)在基于邏輯的自動推理相關(guān)研究領(lǐng)域工作多年，開云此次參賽的這類求解器已求解SAT問題24億1700多萬個，其中規(guī)模最大的有3.13萬億個文字（相當(dāng)于有3.13萬個邏輯電路器件），并基于這類求解器研發(fā)了Scavel系列的C程序、PLC程序自動驗(yàn)證工具，已廣泛應(yīng)用于航空航天、軌道交通、武器裝備、信息安全、家用電子等領(lǐng)域。開云參加今年SAT競賽團(tuán)隊(duì)主要成員包括徐揚(yáng)教授、陳青山博士、吳貫鋒博士等系統(tǒng)可信性自動驗(yàn)證國家地方聯(lián)合工程實(shí)驗(yàn)室的多名教師和研究生。

相關(guān)鏈接：http://sat2018.forsyte.tuwien.ac.at/