软件所提出图神经网络模型实现MaxSAT问题求解优化

       中国科学院软件研究所计算机科学国家重点实验室博士研究生刘明昊针对人工智能和理论计算机科学中的基础问题之一——最大可满足性问题（MaxSAT），提出了一种基于图神经网络的深度学习系统，在求解大规模的困难MaxSAT实例时可以快速获得更高质量的解。

　　最大可满足性问题即给定一个命题逻辑公式，要求找到满足最多数量布尔约束的解。该问题在理论计算机科学、知识推理、电子设计自动化和组合优化等领域有重要应用。传统的MaxSAT求解算法主要基于人工设计的高效启发式搜索策略，难以有效迁移到不同分布的问题实例上。该研究创新性地提出了一种图神经网络模型，能够从小规模的简单实例中学习出有效的解生成策略，并泛化到同分布的较大规模实例上。实验结果表明，该模型在两种不同分布的实例集上均能够学习至收敛，在包含1600个变量的困难测试实例上相较于最先进的传统算法可以产生更优的解，且求解阶段用时显著低于传统算法。该研究揭示了将深度学习与符号推理两类人工智能方法进行更深入结合的价值。 

　　相关研究成果以Can graph neural networks learn to solve the MaxSAT problem?为题，发表在人工智能领域国际顶级会议AAAI 2023的学生摘要轨道，并获大会最佳学生摘要提名奖（Honorable Mention）。

消息来源：中科院官网