冠军！中心团队在MaxSAT国际算法竞赛的多个赛道夺冠

2024年8月28日，国际顶级会议SAT 2024的竞赛组委会宣布，华中科技大学霍普克罗夫特计算科学研究中心团队在中心执行主任何琨教授的带领下，团队所研发的求解器在MaxSAT Evaluation 2024算法竞赛中荣获主赛道非完备组冠军，在非完备组的四个子赛道均获得冠军成绩。参赛团队成员包括中心组合优化方向的博士生金明明、郑迥之和硕士生薛靖晖、陈卓。

此外，团队的长期合作者、法国亚眠大学李初民教授带领法国团队，协同何琨教授，同时包揽MaxSAT主赛道完备组的不带权子赛道冠、亚军。

MaxSAT问题是计算机科学领域的经典问题，具有重要的理论研究价值和广泛的应用价值。MaxSAT Evaluation 2024由美国卡内基梅隆大学、德国弗莱堡大学和芬兰赫尔辛基大学合作举办，该系列赛事至今已举办19届。作为可满足性理论与应用国际会议SAT 2024的组成部分，该赛事旨在MaxSAT问题的研究与发展，促进利用MaxSAT求解方法解决各类NP难优化问题。

在此次MaxSAT竞赛中，团队成员结合了该团队提出的三个局部搜索策略: SPB-MaxSAT[IJCAI 2024]、BandMaxSAT[IJCAI 2022]和FPS[AAAI 2023]，对变元的选择进行了优化，提出了三个变体算法。其中变体SPB-MaxSAT-c-Band获得不带权MaxSAT问题的两个子赛道冠军，变体SPB-MaxSAT-c-FPS获得带权MaxSAT问题的两个子赛道冠军。

本次夺冠是中心团队继2022年取得SAT可满足性问题国际算法竞赛主赛道冠军以及2023年取得MaxSAT最大可满足性问题国际算法竞赛总体第2名以来的又一次突破。相较于2023年MaxSAT竞赛中单纯将BandMaxSAT和FPS引入局部搜索算法框架，今年团队提出了SPB-MaxSAT算法，将软冲突伪布尔（SPB）约束加入到局部搜索方法的子句加权系统中，有效的引导算法找到较优解，提高了求解器效率。

金明明： 这次的MaxSAT比赛能拿到赛道冠军是预料之外的，我要感谢老师的指导、迥之师兄的支持以及团队成员的帮助，这次比赛也让我对SAT和MaxSAT问题产生了兴趣。SAT和MaxSAT问题都是经典的NP难问题，求解十分困难，也非常具有挑战性，通过比赛，我更加深入了解了MaxSAT的启发式算法，对MaxSAT局部搜索算法框架有了更进一步的认识，为我以后对这方面的研究打下了基础。未来，我也会在组合优化领域继续深入研究，学习SAT、MaxSAT算法模块，争取能够有所突破。

郑迥之： 一直以来，SAT和MaxSAT问题都深深地吸引着我。这次比赛，我们带着最新的成果SPB-MaxSAT，并结合我们之前提出的BandMaxSAT以及FPS两个局部搜索算法参加本届MaxSAT比赛，并荣幸取得多赛道冠军的成绩。我要感谢老师的支持与师弟师妹们的帮助，这对于我来说也是一份鼓励，让我能够继续在这条路线上深耕。虽然已经毕业，但我并没有离开科研领域，我也会继续开拓自己的眼界，在做好工作的同时，继续深入探索SAT、MaxSAT算法，争取做出全面的突破。

薛靖晖： 在MAXSAT国际比赛中，我们团队荣幸地赢得了冠军，这不仅是对我们努力的肯定，更是对我们技术水平的极大认可。在整个比赛过程中，我们经历了许多挑战，但正是这些挑战让我们在算法优化和团队协作方面有了显著的提升。MAXSAT问题的复杂性要求我们必须在有限的时间内寻找出最优解或近似最优解。为了应对这一挑战，我们使用了Bandit和FPS等策略，最终找到了有效的解决方案。这次比赛的胜利不仅是我们团队的荣耀，更是对我们坚持不懈努力的最好回报。未来，我们将继续在组合优化领域深耕细作，不断挑战自我，追求卓越。

陈卓： 非常幸运能和实验室团队一起参与MaxSAT比赛并获得冠军。感谢何琨导师的指导和实验室同学们的努力。MaxSAT是非常经典和重要的组合优化问题，求解优化这个问题对学术界和工业界都有重大意义。基于实验室之前对于该问题的研究，比赛中团队成员一起思考讨论，获得了对该问题进一步的理解，这是比荣誉更重要的东西。希望以后能更进一步优化和改进，取得更大的成绩。