BandMaxSAT: A Local Search MaxSAT Solver with Multi-armed Bandit
This work addresses optimization challenges in constraint satisfaction for researchers and practitioners in AI and operations research, representing an incremental improvement over existing local search methods.
The paper tackles the Partial MaxSAT and Weighted MaxSAT problems by proposing BandMaxSAT, a local search solver that uses a multi-armed bandit model to guide search direction, and it significantly outperforms the state-of-the-art SATLike3.0, with BandMaxSAT achieving better results on about twice as many instances.
We address Partial MaxSAT (PMS) and Weighted PMS (WPMS), two practical generalizations of the MaxSAT problem, and propose a local search algorithm for these problems, called BandMaxSAT, that applies a multi-armed bandit model to guide the search direction. The bandit in our method is associated with all the soft clauses in the input (W)PMS instance. Each arm corresponds to a soft clause. The bandit model can help BandMaxSAT to select a good direction to escape from local optima by selecting a soft clause to be satisfied in the current step, that is, selecting an arm to be pulled. We further propose an initialization method for (W)PMS that prioritizes both unit and binary clauses when producing the initial solutions. Extensive experiments demonstrate that BandMaxSAT significantly outperforms the state-of-the-art (W)PMS local search algorithm SATLike3.0. Specifically, the number of instances in which BandMaxSAT obtains better results is about twice that obtained by SATLike3.0. Moreover, we combine BandMaxSAT with the complete solver TT-Open-WBO-Inc. The resulting solver BandMaxSAT-c also outperforms some of the best state-of-the-art complete (W)PMS solvers, including SATLike-c, Loandra and TT-Open-WBO-Inc.