8月5日,国际顶级会议SAT 2022的竞赛组委会宣布,华中科技大学计算机学院何琨教授与其博士生郑迥之等研发的求解器在SAT Competition 2022算法竞赛中荣获Main Track冠军。参赛团队成员还包括硕士生陈卓、博士生周建荣,以及该团队长期的合作者、我校客座教授、法国亚眠大学李初民教授。
SAT问题是计算机科学领域的经典问题,也是第一个被证明为NP完全的问题,不仅具有重要的理论研究价值,而且在工业领域尤其是软硬件验证中具有广泛的应用。SAT Competition 2022比赛由第25届可满足性测试理论与应用国际会议SAT 2022组织举办,该系列赛事至今已举办了15届,比赛的目标在于推动布尔可满足性问题(SAT)求解的发展。
此次SAT Competition共有来自卡内基梅隆大学、埃因霍温理工大学、上海交通大学、德累斯顿工业大学、萨班齐大学、约翰开普勒大学、俄罗斯ITMO大学、华为公司等国际知名高校及科研院所的50多个求解器参加比赛。何琨教授团队提出将随机游走策略与决策树模型相结合的创新方法,使求解器在面对具有不同特征的算例时采用不同的随机游走策略辅助搜索,很好地提升了SAT求解器的鲁棒性,最终取得了Main Track第一名的好成绩。
与此同时,何琨教授团队在由SAT 2022国际会议举办的MaxSAT Evaluation 2022算法竞赛的非完备组四个赛道中荣获三个亚军、一个季军的好成绩。参赛的MaxSAT求解器采用决策树模型结合了包括该团队提出的BandMaxSAT、Farsighted Probability Sampling (FPS)等局部搜索算法,其中BandMaxSAT已发表在国际人工智能顶会IJCAI 2022上。