Hard Neighboring Variables Based Configuration Checking in Stochastic Local Search for Weighted Partial Maximum Satisfiability

Weighted partial maximum satisfiability (WPMS) is a significant generalization of maximum satisfiability (MAXSAT), weighted maximum satisfiability (weighted MAX-SAT) and unweighted partial maximum satisfiability (PMS), and WPMS can be widely used in real-world application domains. Recently, great breakthroughs have been made on stochastic local search (SLS) for solving MAX-SAT, weighted MAX-SAT, PMS and WPMS, resulting in several state-of-the-art SLS algorithms, such as CCLS, Dist and CCEHC. Indeed, boosting the practical performance on solving WPMS is of great interest, and the performance of SLS algorithms on solving WPMS could be further improved. In this paper, we follow this research direction, and propose a new SLS algorithm named CCHNV for solving WPMS. CCHNV adopts the framework of CCEHC, and employs a new forbidding strategy of configuration checking, named hard neighboring variables based configuration checking (HNVCC). Extensive experiments on a broad range of WPMS instances present that CCHNV pushes forward the state-of-the-art performance of SLS algorithms on solving WPMS, and is complementary to a state-of-the-art complete algorithm for solving WPMS.