8月

华中科技大学计算机学院

何琨教授与博士生郑迥之等研发的求解器在

SAT Competition 2022算法竞赛中

荣获Main Track冠军！

参赛团队成员还包括何琨教授的硕士生陈卓、博士生周建荣，以及该团队长期的合作者、华中科技大学客座教授、法国亚眠大学李初民教授。

从左至右：陈卓、郑迥之、何琨、周建荣

SAT Competition 2022比赛由第25届可满足性测试理论与应用国际会议SAT 2022组织举办，该系列赛事至今已举办了15届，比赛的目标在于推动布尔可满足性问题（SAT）求解的发展。

SAT问题是计算机科学领域的经典问题，也是第一个被证明为NP完全的问题，不仅具有重要的理论研究价值，而且在工业领域尤其是软硬件验证中具有广泛的应用。本次SAT Competition共有来自卡内基梅隆大学、埃因霍温理工大学、上海交通大学、德累斯顿工业大学、萨班齐大学、约翰开普勒大学、俄罗斯ITMO大学、华为公司等国际知名高校及科研院所的50多个求解器参加比赛。何琨教授团队提出将随机游走策略与决策树模型相结合的创新方法，使求解器在面对具有不同特征的算例时采用不同的随机游走策略辅助搜索，很好地提升了SAT求解器的鲁棒性，最终取得了Main Track第一名的好成绩。

与此同时，何琨教授团队在由SAT 2022国际会议举办的MaxSAT Evaluation 2022算法竞赛的非完备组四个赛道中荣获三个亚军和一个季军的好成绩。参赛的MaxSAT求解器采用决策树模型结合了包括该团队提出的BandMaxSAT、Farsighted Probability Sampling (FPS)等局部搜索算法。其中BandMaxSAT已发表在国际人工智能顶会IJCAI 2022上。

何琨教授为ACM高级会员，IEEE高级会员，CCF杰出会员，为NeurIPS、ICML、ICLR等十余个顶会的程序委员会（高级）委员。她的团队长期从事组合优化、深度学习的安全性和可解释性，以及社交网络挖掘的研究，在NeurIPS、ICLR、CVPR、ICCV、ECCV、ACL、EMNLP、AAAI、IJCAI等权威会议期刊发表了百余篇论文。她多次指导本科生获得ACM-ICPC区域赛金奖、美国大学生数学建模竞赛F奖和发表NIPS、ICDM等顶会论文，她参与的合作论文Combining Clause Learning and Branch-and-Bound for MaxSAT获得CP 2021最佳论文奖。她的硕士研究生曾获2020年ImageNet图像分类对抗攻击比赛第一名、IJCAI2019人工智能对抗算法竞赛防御赛道第三名等对抗学习竞赛的佳绩。

斩获国际冠军的小伙伴们

都有什么心得想要分享？

一起来看看

郑迥之：一直以来，SAT和MaxSAT问题都深深地吸引着我。这一次，我们带着最近做BandMaxSAT和Farsighted Probability Sampling (FPS)这两个MaxSAT局部搜索算法的些许经验参加了今年的SAT和MaxSAT比赛。在何老师的指导下创新性地提出了用决策树模型辅助求解器选择局部搜索策略的这一方法，最终获得了SAT比赛主赛道串行组冠军，MaxSAT比赛非完备组四个赛道中三个亚军、一个季军的好成绩。

在看到组委会宣布比赛结果时，我非常高兴，这对于我来说是一份鼓励与肯定，激励我继续努力学习和探索。目前我们的方法与策略几乎都围绕着求解器中的局部搜索模块，往后我会继续深入学习SAT、MaxSAT求解器中的其他模块，争取能够做出更全面的突破。

陈卓：在这次的SAT比赛中，何老师和两位学长都给予了我许多的指导与帮助。由于我的本科毕业设计内容是与SAT问题相关的组合优化问题，所以在打比赛的过程中也有一些新的想法和启发。根据我本科毕设的研究问题，通过一些转换方法得到SAT问题的算例。在这次的比赛中我只贡献了一点绵薄之力，但是这个过程提升了我对SAT问题的兴趣，也学到了许多新的思想。今后的科研生活我也会继续跟随着导师和学长的步伐，继续探索。

周建荣：非常开心和实验室团队一起参与SAT/MaxSAT竞赛获奖。SAT和MaxSAT问题是组合优化领域中非常经典的NPC/NP-Hard问题，这两个问题的求解是十分困难、十分有挑战的。此次有幸和何琨老师、郑迥之和陈卓一起思考、理解和设计相关算法，使我对SAT问题以及相关组合优化问题有了更进一步的理解。此次参赛队伍都是来自世界各个知名大学的非常有竞争力的团队，能在比赛中获奖都是十分不易的。参与此次竞赛我收获良多，同时也十分感谢导师的指导和两位同学的努力付出。

恭喜

HUSTer

请再接再厉！

来源：华中科技大学官方微信公众号

编辑：高翔、李芊芊