近日，中國科學院軟件研究所蔡少偉團隊在邏輯約束求解器研究中獲得新突破，SAT求解器和SMT求解器研究上的成果被重要期刊和會議錄用，并在SAT、MaxSAT和SMT競賽中斬獲佳績。 

　　求解器被譽為“工業軟件之魂”，是繼芯片與操作系統之后的國之重器。命題邏輯可滿足性問題（SAT）和可滿足性模理論問題（SMT）是兩個最重要的邏輯約束問題，SAT是命題邏輯上的約束求解問題， SMT是一階謂詞邏輯上的約束求解問題。它們不但在自動定理證明、軟件工程等學術研究中有廣泛應用，更是信息安全、集成電路設計自動化和軟件驗證等領域的底層計算引擎。 

　　2022年8月5日，SAT會議正式公布了SAT和MaxSAT的比賽結果。在SAT比賽中，蔡少偉團隊以明顯優勢獲得了SAT比賽主賽道并行組冠軍和NoLimits 賽道冠軍（主要參與者包括蔡少偉研究員及其博士生張昕荻和碩士生陳志翰）。在MaxSAT比賽中，該團隊贏得了幾乎大滿貫的好成績：在總共6個賽道中獲得5個冠軍和1個亞軍（主要參與者包括蔡少偉研究員及其博士后初一，其中1個冠軍是與華為理論實驗室的雷震東、東北師范大學的王藝源等人合作獲得）。 

　　值得一提的是，蔡少偉團隊與國際上SAT研究的另一個主要團隊（包括Armin Biere等人）合作的一篇SAT混合求解方法的論文以“Better Decision Heuristics in CDCL through Local Search and Target Phases.”為題，發表在人工智能著名期刊Journal Of Artificial Intelligence Research上。這篇文章為SAT混合求解方向提供了系統性的理論參考。 

　　近兩年，該團隊開始轉向更具挑戰的SMT求解方向。SMT求解器的軟件架構復雜，開發和維護工程難度大；而且SMT求解器體量龐大，目前的主流求解器，如Z3，CVC5，Yices2等都具有幾十萬甚至上百萬行的代碼量；此外，還需要開發者擁有扎實深厚的數學和邏輯學基礎。因此SMT求解器的開發技術門檻比較高。 

　　2022年8月11日，在FLoC (Federated Logic Conference，國際聯合邏輯大會 )的IJCAR（國際聯合自動推理會議）會議上宣布了SMT 2022比賽結果。蔡少偉團隊研發的SMT求解器Z3++在比賽中獲得線性算術理論和非線性算術理論的多項第一，并在Model Validation的所有賽道綜合評分中求解能力領先。其總分獲得FLoC奧林匹克競賽頒發的2塊金牌（大賽共設6枚金牌2枚銀牌）。這是國內團隊首次在FLoC奧林匹克競賽的SMT比賽中取得金牌。FLoC每四年舉辦一次，對數理邏輯和計算機科學社區產生重要影響。 

　　Z3++求解器是基于國際主流求解器Z3的衍生求解器，由蔡少偉研究員發起和領導，主要參與者包括他的博士生李博涵、張昕荻、趙夢宇和來自晞德軟件公司的林錦坤博士，以及詹博華副研究員和他的碩士生王忠漢。Z3++針對其參與的各個理論都進行了深入的優化。對于位向量理論，Z3++采用了詞級別和位級別的重寫規則來化簡約束；對于整數算術理論，該團隊創新性地開發了首個針對整數算術理論的局部搜索求解器；對于非線性實數算術理論，該團隊實現了可行域一致性檢測并在NLSAT框架下實現了胞腔采樣投影。Z3++顯著地改進了著名的Z3求解器，其相關創新技術以“Local Search for SMT on Linear Integer Arithmetic”為題發表在理論計算機頂級會議CAV 2022上。 

　　本次奪冠是蔡少偉團隊繼去年在SMT比賽中首次取得整數差分邏輯冠軍后的又一次重大突破。相較于去年因單一理論取得第一，本次奪冠覆蓋的理論更為廣泛，也更為重要。團隊現已將Z3++開源（https://z3-plus-plus.github.io）用于幫助更多研究人員及時學習Z3++相關技術，同時推動更多國內相關方向的研究人員對SMT求解器進行更深入地研究。 

　　蔡少偉團隊重視學術研究和工程實踐的結合，提出的創新想法最終都能實現為求解器。研究成果多次在國際比賽獲獎，并且應用于多個重要的工業場景。該團隊還通過舉辦閉門論壇、專題訓練營及新媒體科普等形式，為推動約束求解領域產業生態建設作出積極貢獻。 

（在SAT比賽中以明顯優勢獲得主賽道并行組冠軍）

（在國際聯合邏輯大會(FLoC)奧林匹克競賽SMT比賽中獲得2枚金牌）