基于动态子句加权策略的MaxSAT问题局部搜索算法研究

Research on Local Search Algorithm for MaxSAT Problem Based on Dynamic Clause-Weighting Strategy

摘要: 最大可满足性问题(Maximum Satisfiability Problem, MaxSAT)是布尔可满足性问题(Satisfiability Problem, SAT)的优化延伸，是NP难组合优化问题。在理论研究以及工程应用中的诸多优化问题都可以转化并编码为MaxSAT问题，从而借助其策略开展相关的研究与求解，是一种具有极其强大表达能力的逻辑约束优化模型。MaxSAT问题主要研究的是，给定一个命题逻辑合取范式公式(Conjunctive Normal Form, CNF)，通过局部搜索算法寻找是否存在使其被满足的可行赋值。本研究主要聚焦于非完备算法中的随机局部搜索算法，并用其对最大可满足性问题进行求解。首先，详细介绍了SATLike3.0的子句加权方案，分析SATLike3.0子句加权策略中的硬惩罚增量和软惩罚增量，该加权策略均为设定的定值较为固化。其次，基于SATLike3.0子句加权阶段的加权部分，提出了动态惩罚增量调整的子句加权策略SR-Weighting()。最后，将硬子句满足率以及本组满足加权条件的软子句原始权重占比，融合到硬惩罚增量和软惩罚增量中，使其呈现灵活动态的调整，形成了高效的随机局部搜索求解器WrSATLike3.0。实验结果表明，在国际MaxSAT竞赛(MaxSAT Evaluation, MSE)2023和2024年的实例中。求解器WrSATLike3.0在成功求解实例个数以及求解质量上显著优于原始求解器SATLike3.0。在WPMS问题中进行对比时，成功求解实例个数上对比NuWLS以及BandMaxSAT也取得了一定的优势。

Abstract: The Maximum Satisfiability Problem (MaxSAT) is an optimized extension of the Boolean Satisfiability Problem (SAT). It is an NP-hard combinatorial optimization problem. Many optimization problems in theoretical research and engineering applications can be transformed and encoded into MaxSAT problems. Relevant research and solving can be carried out using its strategies. It is a logical-constraint optimization model with extremely strong expressive power. For the MaxSAT problem, we are given a propositional logic formula in Conjunctive Normal Form (CNF). Local search algorithms are used to find feasible assignments to satisfy this formula. This study mainly focuses on stochastic local search algorithms among incomplete algorithms. It employs such algorithms to solve the Maximum Satisfiability Problem. First, this paper describes the clause-weighting scheme of SATLike3.0 in detail. It analyzes the hard penalty increment and soft penalty increment in the clause-weighting strategy of SATLike3.0. These values are preset fixed numbers. The weighting strategy is rather rigid. Second, based on the weighting component in the clause-weighting stage of SATLike3.0, this paper proposes a clause-weighting strategy with dynamic penalty increment adjustment. Finally, this work integrates the satisfaction rate of hard clauses and the proportion of original weights of soft clauses that satisfy the weighting conditions in the current group into the hard penalty increment and soft penalty increment. These two increments can realize flexible and dynamic adjustment. An efficient stochastic local search solver called WrSATLike3.0 is developed. The experimental results show that the test instances come from MaxSAT Evaluation (MSE) 2023 and 2024. The solver WrSATLike3.0 significantly outperforms the original solver SATLike3.0 in the number of successfully solved instances and solution quality. For WPMS problem benchmarks, WrSATLike3.0 also achieves certain advantages in the number of solved instances. The comparison targets include NuWLS and BandMaxSAT.