7月13日，國際SAT競賽組委會在其官方網(wǎng)站上公布了2018年SAT競賽結(jié)果，開云kaiyun開云官方網(wǎng)站，系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室徐揚教授團隊提交的求解器獲得Main組亞軍（比冠軍Intel求解器的求解結(jié)果僅差0.75%），取得開云在該領(lǐng)域的歷史性突破。
SAT（可滿足性，SATisfiability）問題是第一個被證明的NP完全問題，也是當今數(shù)學、計算機科學和人工智能等領(lǐng)域研究的前沿核心問題之一。許多重要領(lǐng)域中的大量問題，如大型數(shù)據(jù)庫的維護、大規(guī)模集成電路的自動布線及其正確性驗證、軟件自動開發(fā)及其正確性驗證、機器人動作規(guī)劃，數(shù)學中的許多優(yōu)化問題等，都可轉(zhuǎn)化為SAT問題求解。因此，致力于構(gòu)建求解SAT問題的快速有效系統(tǒng)——SAT求解器這一基礎(chǔ)性工具，不僅在理論研究上而且在許多應(yīng)用領(lǐng)域都具有極其重要的意義。
國際SAT競賽是學術(shù)界和工業(yè)界在SAT問題研究領(lǐng)域的最頂級賽事，每一到兩年舉辦一次，至今已經(jīng)舉辦了二十一屆。本次競賽共有來自于9個國家的41個求解器參賽。參賽單位包括英國曼徹斯特大學、法國阿爾圖瓦大學、日本九州大學、德國卡爾斯魯厄理工學院、中國kaiyun開云官方網(wǎng)站、中國華中科技大學、德國安全研究實驗室，Intel，Google等世界各地的大學、研究機構(gòu)及企業(yè)。本次競賽設(shè)有Main、Glucose Hack、NoLimith和Random四個組，
Main組是其中競爭最激烈的，競賽題目均為工業(yè)界實際應(yīng)用問題轉(zhuǎn)換而來，因此其受到業(yè)界關(guān)注也是最多的。
徐揚教授團隊在基于邏輯的自動推理相關(guān)研究領(lǐng)域工作多年，開云此次參賽的這類求解器已求解SAT問題24億1700多萬個，其中規(guī)模最大的有3.13萬億個文字（相當于有3.13萬個邏輯電路器件），并基于這類求解器研發(fā)了Scavel系列的C程序、PLC程序自動驗證工具，已廣泛應(yīng)用于航空航天、軌道交通、武器裝備、信息安全、家用電子等領(lǐng)域。開云參加今年SAT競賽團隊主要成員包括徐揚教授、陳青山博士、吳貫鋒博士等系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室的多名教師和研究生。
相關(guān)鏈接：http://sat2018.forsyte.tuwien.ac.at/
