近日，形式化驗證頂級會議CAV 2021會議公布了第十六屆國際可滿足性模理論比賽(SMT-COMP 2021)比賽結果。中國科學院軟件研究所計算機科學國家重點實驗室蔡少偉研究員與其學生李博涵、張昕荻研發的求解器榮獲整數差分邏輯(QF_IDL)組冠軍，這是中國團隊首次在SMT-COMP比賽中獲得冠軍。

　　可滿足性模理論問題（簡稱SMT）是特定背景理論下的一階邏輯判定問題，是形式化驗證的基礎引擎。整數差分邏輯理論的SMT可以自然地描述時序相關的問題，廣泛應用于時序系統驗證，偏序數據結構的硬件模型檢測，穩態模型計算。

　　在SMT-COMP 2021比賽中，QF_IDL組的參賽隊伍包括斯坦福大學，愛荷華大學，弗萊堡大學，微軟研究院，國際斯坦福研究所，法國國家信息與自動化研究所等國際知名高校及科研院所。蔡少偉團隊創新性地設計了結合DPLL(T)和隨機搜索方法的混合方法，打破了傳統SMT求解器框架，在強數值約束算例中取得顯著效果，最終在QF_IDL理論的Single query和Model validation賽道上都取得了第一名的好成績。

　　蔡少偉研究員從事約束求解器、EDA核心算法研究，此前多次獲得SAT比賽和MaxSAT比賽冠軍， 2021年獲SAT大賽Main track SAT、UNSAT組亞軍，MaxSAT比賽完備組、非完備組冠軍，EDA Challenge大賽亞軍。相關方法發表在人工智能頂級期刊Artificial Intelligence 以及計算機理論著名會議SAT會議上，題為《Deep Cooperation of CDCL and Local Search for SAT》的論文獲SAT 2021會議最佳論文獎。

　　論文鏈接：Deep Cooperation of CDCL and Local Search for SAT

    報道鏈接：探索工業軟件之魂，板凳要坐十年冷 丨 中科院軟件所蔡少偉專訪