近日,軟件所計算機科學國家重點實驗室蔡少偉研究員與其博士生張昕荻研發的求解器在SAT Competition 2020比賽中榮獲Main Track SAT冠軍。SAT Competition 2020比賽由第23屆可滿足性測試理論與應用國際會議SAT 2020（https://sat2020.idea-researchlab.org）組織舉辦。  

　　布爾可滿性問題（SAT）是計算機科學的經典問題，也是歷史上第一個被證明為NP完全的問題，不僅具有重要的理論研究價值，而且在工業領域尤其是軟硬件驗證中具有廣泛的應用。例如，Intel芯片和Windows操作系統驗證中都用到了SAT求解器。為促進SAT問題求解算法及工具的研發和應用，國際SAT學會自2002年以來每年（或每兩年）組織SAT Competition國際比賽，至今已經舉辦了13屆。 

　　在SAT Competition 2020比賽中，共有來自康奈爾大學、多倫多大學、曼徹斯特大學、俄羅斯科學院、柏林祖思研究所、法國國家信息與自動化研究所和Google等國際知名高校及科研院所的68個求解器參加比賽。蔡少偉研究員團隊創新性的提出了松弛子句沖突學習方法，并采取變元重分配策略，很好的提高了主流SAT方法的尋解能力，最終取得了Main Track SAT第一名的好成績。蔡少偉研究員團隊曾在SAT Competition中多次獲獎，包括SAT Competition 2014、2016亞軍和2018冠軍，并獲得2018年聯合邏輯奧林匹克金牌。 

　　蔡少偉研究員提出的啟發式搜索技術和研制的SAT求解器被分別應用于微軟Azure云平臺的虛擬機預配置和異常檢測、騰訊地圖優化以及美聯邦通信委員會的頻譜分配等項目中，最近研究成果Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability發表在國際人工智能學報Artificial Intelligence (2020) 。 

    論文鏈接

　　SAT Competition 2020 Main Track SAT前三名