華為雲天籌 AI 求解器團隊獲得 SAT 國際算法競賽並行賽道 SAT 組冠軍

近日，約束求解與形式化領域的國際頂級賽事 SAT Competition 2026（可滿足性問題國際算法競賽）落下帷幕。由華為雲天籌 AI 求解器團隊、華中科技大學 John Hopcroft 計算中心及華為諾亞方舟實驗室所組成的聯合團隊，榮獲並行 AI 賽道 SAT 組冠軍。

根據報導，本屆賽事吸引了來自全球頂尖高校和機構的 45 支隊伍參賽，其一大亮點是首次設立 AI 賽道，鼓勵參賽團隊利用 AI 技術對求解器進行智能化調優。按照賽事規則，基於 AI 調優的求解器只有在性能上超過最優的非 AI 求解器才能獲得獎項。這意味著，AI 不能僅作為參數推薦或輔助開發工具，而必須帶來真實、可量化、可驗證的算法性能提升。

AI 賽道的設立標誌著算法設計的創新

AI 賽道的設立標誌著賽事從傳統的純算法設計競賽，邁入了經典算法與 AI 融合創新的新階段。本屆賽事的數據集包含軟硬件驗證、EDA、密碼學分析、組合優化等應用領域的 400 個高難度問題。天籌 AI 求解器團隊研發的求解器 Kissat-MAB-HyPre-Evolve，憑藉在複雜問題求解能力、並行搜索效率和算法魯棒性等方面的綜合優勢，獲得並行 AI 賽道 SAT 組冠軍。

這一結果表明，AI 已經能夠突破傳統輔助調優的界限，深入參與求解器算法和代碼設計，並在全新、未見的數據集上形成穩定、可復現的性能增益。