MaxSAT is an optimization version of the famous NP-complete Satisfiability problem (SAT). Algorithms for MaxSAT mainly include complete solvers and local search incomplete solvers. In many complete solvers, once a better solution is found, a Soft conflict Pseudo Boolean (SPB) constraint will be generated to enforce the algorithm to find better solutions. In many local search algorithms, clause weighting is a key technique for effectively guiding the search directions. In this paper, we propose to transfer the SPB constraint into the clause weighting system of the local search method, leading the algorithm to better solutions. We further propose an adaptive clause weighting strategy that breaks the tradition of using constant values to adjust clause weights. Based on the above methods, we propose a new local search algorithm called SPB-MaxSAT that provides new perspectives for clause weighting on MaxSAT local search solvers. Extensive experiments demonstrate the excellent performance of the proposed methods.

翻译：MaxSAT是著名的NP完全可满足性问题（SAT）的优化版本。MaxSAT算法主要包括完备求解器和局部搜索不完备求解器。在许多完备求解器中，一旦找到更优解，就会生成一个软冲突伪布尔（SPB）约束，以强制算法寻找更优解。而在许多局部搜索算法中，子句加权是有效引导搜索方向的关键技术。本文提出将SPB约束迁移到局部搜索方法的子句加权系统中，从而引导算法找到更优解。我们进一步提出一种自适应子句加权策略，打破了使用恒定值调整子句权重的传统方法。基于上述方法，我们提出一种新的局部搜索算法SPB-MaxSAT，为MaxSAT局部搜索求解器中的子句加权提供了新视角。大量实验证明了所提方法的优异性能。