基于差异化子句加权技术的MaxSAT问题局部搜索算法研究

Research on Local Search Algorithms for MaxSAT Problems Based on Differentiated Clause Weighting Techniques

摘要: 最大可满足性问题(Maximum Satisflability Problem,MaxSAT)是一类经典的组合优化问题，在理论计算机科学及人工智能领域中有着广泛应用。局部搜索作为求解MaxSAT的主流方法之一，已被广泛应用于各类MaxSAT问题的求解中。深入研究局部搜索的内部机制对推动MaxSAT求解具有重要作用。本研究首先详细介绍了求解MaxSAT问题局部搜索算法的研究进展、发展历程及主要框架。然后针对子句加权技术提出基于子句重要性差异化的加权思想， 即Diff-Weighting策略。在增加子句惩罚权重阶段，我们仅对拥有两个变元且不被满足的硬子句， 赋予2倍的硬惩罚权重增量，以及根据原始权重的大小动态调整不被满足软子句的软惩罚权重增量。 我们把Diff-Weighting思想融合到SATLike3.0和ImSATLike求解器中,得出DiSATLike3.0以 及DiImSATLike求解器。在近两届MaxSAT国际算法竞赛MaxSAT Evaluation 非完备组的所有（W)PMS实例上取得的实验结果表明，应用Diff-Weighting技术获得的改进算法，相对于原算法在成功求解实例的个数上，能够提升约10%至60%的性能，体现了基于子句重要性差异化的加权技术在求解（W)PMS问题时的有效性。

Abstract: The Maximum Satisfiability Problem (MaxSAT) is a classical combinatorial optimiza- tion problem with extensive applications in theoretical computer science and artificial intelligence. Local search is one of the mainstream approaches for solving MaxSAT and has been widely applied to various MaxSAT instances. A deep investigation into the internal mechanisms of local search is essential for advancing MaxSAT solving. This study first provides a comprehensive overview of the research progress, development history, and main algorithmic frameworks of local search algorithms for MaxSAT. Then, focusing on clause weighting techniques, we propose a novel weighting strategy based on the differentiation of clause importance, referred to as the Diff-Weighting strategy. Specifically, during the clause weight increment phase, we assign a doubled hard penalty weight increment only to unsatisfied hard clauses containing exactly two literals, and dynamically adjust the soft penalty weight increment for unsatisfied soft clauses based on their original weights. By integrating the Diff-Weighting strategy in- to the SATLike3.0 and ImSATLike solvers, we develop the new solvers DiSATLike3.0 and DiImSATLike. Experimental results on all (W)PMS instances from the incom- plete track of the last two MaxSAT Evaluations show that the improved algorithms incorporating Diff-Weighting achieve a performance improvement of approximately 10% to 60% in the number of successfully solved instances compared to the original algorithms, demonstrating the effectiveness of the clause importance-differentiated weighting technique in solving (W)PMS problems.