近期，中國科學院軟件研究所研究員蔡少偉團隊在邏輯約束求解器研究中取得多項進展，并在命題邏輯可滿足性問題（SAT）、可滿足性模理論問題（SMT）等多項競賽中斬獲佳績。

　　在邏輯約束求解器領域，SAT和SMT是兩個最重要的邏輯約束問題。SAT是命題邏輯上的約束求解問題，SMT是一階謂詞邏輯上的約束求解問題。它們不僅在自動定理證明、軟件工程等學術研究中有廣泛應用，還是信息安全、集成電路設計自動化和軟件驗證等領域的底層計算引擎。

　　近日，SAT會議公布SAT和MaxSAT比賽結果，F(xiàn)LoC（Federated Logic Conference，國際聯(lián)合邏輯大會）的IJCAR（國際聯(lián)合自動推理會議）會議宣布SMT 2022比賽結果。 

　　在SAT比賽中，蔡少偉團隊以明顯優(yōu)勢獲得主賽道并行組冠軍和NoLimits賽道冠軍；在MaxSAT比賽中，團隊贏得幾乎大滿貫的成績，在總共6個賽道中獲得5個冠軍和1個亞軍（其中1個冠軍與華為理論實驗室、東北師范大學等團隊合作獲得）。

　　在SMT 2022比賽中，蔡少偉團隊研發(fā)的SMT求解器Z3++（基于國際主流求解器Z3的衍生求解器）在比賽中獲得線性算術理論和非線性算術理論的多項第一，并在Model Validation的所有賽道綜合評分中求解能力領先。其總分獲得FLoC奧林匹克競賽頒發(fā)的2塊金牌（大賽共設6枚金牌2枚銀牌）。這是國內團隊首次在FLoC奧林匹克競賽的SMT比賽中取得金牌。FLoC每四年舉辦一次，在數(shù)理邏輯和計算機科學領域有著重要影響。