Huawei, in collaboration with the team from Huazhong University of Science and Technology, won the championship in the Parallel AI Track SAT Group at the newly established AI track of the 2026 SAT Competition. As a top international event in the field of constraint solving and formal methods, the SAT Competition, for the first time in this edition, required that the performance of AI-tuned solvers must surpass that of the best non-AI solvers to win an award. This marks the event's entry into a new era of integrated innovation between classical algorithms and AI. Huawei's victory this time was attributed to its use of the Huawei Cloud Tianchou Decision Intelligence Engine and AI algorithm automatic design technology to build a dedicated self-tuning pipeline for SAT solvers. This innovation enabled AI to deeply participate in the entire process of the solver, achieving stable and reproducible improvements in solving performance for various new datasets. Additionally, the relevant capabilities rely on the open-source algorithm design platform LLM4AD_Next, jointly developed by Huawei and the team led by Professor Qingfu Zhang from City University of Hong Kong. The platform features four core functions: automatic algorithm construction, independent memory management, lightweight Skill deployment, and an automatic research platform. It is open to algorithm practitioners, helping them efficiently transform their ideas into verifiable outcomes.
