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

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

Jiongzhi Zheng, Zhuo Chen, Chu-Min Li, Kun He

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence
Main Track. Pages 1989-1997. https://doi.org/10.24963/ijcai.2024/220

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.
Keywords:
Constraint Satisfaction and Optimization: CSO: Satisfiabilty
Constraint Satisfaction and Optimization: CSO: Solvers and tools
Search: S: Local search