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

作者：于瀚一; 陈寅^*

来源：计算机系统应用, 2023, 32(05): 300-307.

DOI：10.15888/j.cnki.csa.009074

• SATLike3.0
• 动态局部搜索算法
• 反馈机制
• 初始解生成
• 初始权重配置

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

• 单位
  华南师范大学