基于搜索信息反馈策略的MaxSAT非完备求解算法  

Incomplete Solver based on Search Information Feedback for MaxSAT

作　　者：徐振兴 何琨[1] 李初民[1,2] 刘燕丽 郑迥之[1] XU Zhen-Xing;HE Kun;LI Chu-Min;LIU Yan-Li;ZHENG Jiong-Zhi(Department of Computer Science,Huazhong University of Science and Technology,Wuhan 430074;Department of Computer Science,University of Picardie Jules Verne,Amiens,France 80039;Department of Science,Wuhan University of Science and Technology,Wuhan 430074)

机构地区：[1]华中科技大学计算机科学与技术学院,武汉430074 [2]亚眠大学计算机科学系,亚眠法国800393 [3]武汉科技大学理学院,武汉430081

出　　处：《计算机学报》2023年第4期711-726,共16页Chinese Journal of Computers

基　　金：科技部高端外国专家引进计划项目智能学习与优化核心算法研究(No.G2022154012L);微软亚洲研究院联合研究基金基于学习的组合优化问题求解(No.100338928)资助.

摘　　要：MaxSAT问题是SAT可满足性问题的优化形式,具有NP难度.本文分析了传统的MaxSAT局部搜索求解器对工业算例求解存在的局限性,并基于此分析提出了新的初始解构造算法ASIF.ASIF是一个基于树形赋值的初始解构造算法,其中包含了一个全局信息反馈策略.该算法选取并定义了构造过程中有意义的统计量,使用这些量设计了一个全局搜索信息更新反馈机制,对初始解构造过程中的经验进行积累并为后续解的构造提供指导信息,再根据后续解的构造情况对全局经验进行反馈和更新,从而有效利用了解构造过程中的经验和信息.进一步地,将ASIF作为初始解构造算法,结合IPBMR算法中的路径截断(PB)策略,提出了新的算法PB-ASIF.实验设计与比较共分为三个阶段.第一阶段,将ASIF在300秒内首次找到的可行解与IPBMR求解300秒的结果进行对比.ASIF初始可行解更优的数量是IPBMR在300秒内求解的可行解更优数量的两倍多,其中非加权偏类算例更优解数量上前者更是后者的3.68倍.该阶段的实验结果表明,ASIF算法能快速构造优质的初始可行解.第二阶段,将PB-ASIF与IPBMR进行对比实验,在300秒求解时间内,PB-ASIF求得更优解的数量总体上是IPBMR的2.38倍,在非加权偏类算例更优解数量上前者更是后者的3.85倍.该阶段的实验结果表明,PB-ASIF算法求解工业算例的能力明显超过了IPBMR算法,有效改进了使用PB策略求解工业算例的效果.第三阶段,将PB-ASIF与其它优秀求解器进行联合求解,包括CCEHC求解器和SATLike3.0求解器.该阶段的实验结果表明,PB-ASIF算法与其它局部搜索类算法有很强的互补性,有提升其它求解器求解效果的能力.MaxSAT problem is the optimization version of the SAT problem,and it is NP hard.There are two classes of algorithms for solving the MaxSAT problem,the complete algorithms and incomplete algorithms.A complete algorithm requires to return a feasible solution that is optimal.An incomplete algorithm requires to return the best-quality feasible solution within the specified time or steps.The two classes of algorithms have made great progress in recent decades.The local search algorithm is a typical and effective kind of incomplete algorithm.The structure of different types of MaxSAT instances varies greatly,making it hard for a method to have good performance on all types of instances.This paper analyzes the limitations of traditional local search MaxSAT solvers in solving industrial instances,and proposes a new algorithm for the initial solution construction based on the analysis,termed ASIF(Assignment approach by Search Information Feedback).ASIF is an initial solution construction algorithm based on tree assignment,which includes a global information feedback strategy.This algorithm selects and defines meaningful quantities in the construction process,uses these quantities to design a global search information update feedback mechanism,accumulates the experience in the construction process of the initial solution and provides guidance information for the construction of subsequent solutions,and then feeds back and updates the global experience according to the construction of subsequent solutions.The goal is to effectively use the experience and information in the construction process.Taking ASIF for the initial solution construction,we combine it with the Path-Breaking(PB)strategy in IPBMR algorithm,and propose a new algorithm called PB-ASIF(Path-Breaking approach with ASIF strategies).There are three stages in our experiments.In the first stage,the first feasible solution found by ASIF in 300 seconds was compared with the best solution found by IPBMR in the same time limit.The number of better feasible solutions

关 键 词：组合优化 最大可满足性问题 非完备算法 搜索信息反馈 赋值算法 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]