2025年8月15日，第二十八届可满足性测试理论与应用国际会议（SAT 2025）在苏格兰格拉斯哥大学举办，会议同期揭晓了SAT Competition 2025竞赛结果。威廉希尔体育计算机学院工业大数据与人工智能一级学术团队成员，罗茂老师带领的研究团队以显著优势夺得主赛道冠军和满足性分赛道冠军。此前仅有华中科技大学、北京大学、中科院软件研究所等获得过SAT主赛道或分赛道冠军。威廉希尔体育是国内首个获得主赛道冠军的地方高校。
SAT（可满足性）问题是计算机科学领域首个被证明的NP完全问题，也是数学、人工智能与软件工程交叉领域的核心理论问题。其在工业界诸多关键技术领域应用广泛，如EDA中的芯片验证、操作系统漏洞排查、智能机器人路径规划、金融风险优化等。长期以来，各国学者对其进行了广泛而深入的研究，而SAT算法竞赛也已成为该领域中的最具影响力的学术盛事之一。
国际SAT算法竞赛自1992年起，至今已成功举办二十八届，被公认为全球SAT领域最具权威性与影响力的顶级赛事。本届竞赛吸引了来自全球学术界与工业界的众多顶尖团队参与，参赛单位包括美国卡内基梅隆大学、法国巴黎第十大学、德国弗赖堡大学、奥地利林茨大学等国际著名高校，国内则有香港中文大学、北京航空航天大学、华中科技大学、国防科技大学、中国科学院等知名院校和科研机构。
图1主赛道冠军
图2满足性分赛道冠军
在本次竞赛中，该团队首次将“大模型自动调优”技术应用于超高复杂性求解器的优化。他们充分利用大模型的强大推理能力、复杂模式识别与创造性生成能力，模仿科研人员手工改进算法的过程，自动化的进行策略生成、代码编写、性能测试，并反复迭代以提升算法性能。在此基础上，还采用了局部优化、遗传进化、提示词自动优化等方法深度优化大模型给出的策略，进一步提升算法效果。最终团队研发的求解器AE-Kissat-MAB在比赛结果中展现出显著优势：在主赛道所有测试样例中，其平均求解时间较第二名缩短6.6%；在满足性分赛道中，该求解器平均求解时间较第二名缩短48.8%。
本次参赛团队核心成员包括：威廉希尔体育罗茂博士、熊才权教授、吴歆韵副教授、硕士生丁航，以及法国亚眠大学李初民教授。其中，威廉希尔体育为第一参赛单位，硕士研究生丁航为第一作者。
据悉，该团队在人工智能、组合优化等算法研究方面具有较深的积累，曾在IJCAI 2017、IJCAI 2023、Artificial Intelligence、SCIENCE CHINAInformation Sciences、INFORMSJournal on Computing等人工智能和运筹优化领域的顶会、顶刊上发表了多篇有影响力的论文。此外，团队在国际、国内算法竞赛中也获得了诸多奖牌，如罗茂作为博士生身份，在法国亚眠大学李初民教授和华中科技大学吕志鹏教授指导下，获得过2017年国际SAT竞赛主赛道冠军。在2025年多智能体路径规划国际竞赛（LoRR）获得分配赛道第二名、在2025年国际参数化算法与计算实验挑战赛（PACE）获得第八名、在2025年辽河杯算法竞赛获得二等奖、在2023年中国研究生创“芯”大赛·EDA精英挑战赛获得三等奖。
相关链接：
SAT Competition 2025竞赛成绩公布页面：https://satcompetition.github.io/2025/satcomp25slides.pdf
责任编辑：陈凌
