基于SATLike3.0局部搜索求解器的算法改进

Algorithm Improvement Based on Local Search Solver SATLike3.0

部分最大可满足性问题是可满足性问题的重要变体,它可以同时处理硬约束和软约束,因此可以对广泛的现实问题进行建模.局部搜索求解器是为该问题寻找高质量解的主流方法,它依赖于问题实例的初始数据状态.本文针对局部搜索求解器SATLike3.0的初始解生成过程,提出了优先满足硬约束的改进策略,最终得到的算法名为HFCRP-F.该算法作用于构造初始解和初始权重配置阶段,主要包括优先传播尚未满足的硬约束中的未赋值变量,以及根据已找到的解为约束增加初始权重,由此指导后续的局部搜索过程.本文采用MaxSAT Evaluation 2018–2021中的数据集对HFCRP-F和SATLike3.0进行测试,结果表明HFCRP-F处理加权实例的性能明显优于SATLike3.0,同时处理非加权实例的性能与SATLike3.0基本持平.

The partial maximum satisfiability problem is an important variant of the satisfiability problem.It can handle both hard and soft constraints simultaneously and thus can model a wide range of realistic problems.Local search solvers are the mainstream method to find high-quality solutions to the partial maximum satisfiability problem,and they rely on initial data states of problem instances.Aiming at the initial solution generation process of a local search solver,namely,SATLike3.0,this study proposes an improvement strategy that gives priority to satisfy the hard constraints,and the obtained algorithm is dubbed HFCRP-F.The algorithm works on the stages of initial solution construction and initial weight configuration,including propagating unassigned variables in unsatisfied hard constraints and adding initial weights to constraints based on found solutions,so as to guide the subsequent local search process.HFCRP-F and SATLike3.0 are tested by using data sets from MaxSAT Evaluation 2018–2021.The results reveal that HFCRP-F performs much better than SATLike3.0 in processing weighted instances and shows nearly the same performance as SATLike3.0 in processing non-weighted instances.