Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers

TL;DR

The paper addresses improving MaxSAT local search by integrating Soft conflict Pseudo Boolean constraints into the clause weighting framework and introducing an adaptive weighting scheme. The proposed SPB-MaxSAT maintains an SPB constraint with a dynamic weight and defines a scoring function that combines hard-clause impact with SPB influence, plus an adaptive SPB weighting mechanism to sustain progress. Empirical results show SPB-MaxSAT and its SAT-based variant SPB-MaxSAT-c outperform state-of-the-art local-search solvers (NuWLS, BandMaxSAT) and robustly beat baselines across PMS/WPMS benchmarks, highlighting improved guidance away from local optima and better feasible solutions. The work demonstrates the practical potential of importing complete-solver ideas into local-search MaxSAT, with implications for more effective incomplete solvers in industrial and academic applications.

Abstract

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.

Figures (1)

• Figure 1: How $R_{inc}$ and $I_{inc}$ change with the increment of the number of times $w(SPB)$ increases.