Empirical investigation of stochastic local search for maximum satisfiability

The maximum satisfiability (MAX-SAT)problem is an important NP-hard problem in theory,and has a broad range of applications in practice.Stochastic local search (SLS)is becoming an increasingly popular method for solving MAX-SAT.Recently,a powerful SLS algorithm called CCLS shows efficiency on solving random and crafted MAX-SAT instances.However,the performance of CCLS on solving industrial MAX-SAT instances lags far behind.In this paper,we focus on experimentally analyzing the performance of SLS algorithms for solving industrial MAXSAT instances.First,we conduct experiments to analyze why CCLS performs poor on industrial instances.Then we propose a new strategy called additive BMS (Best from Multiple Selections)to ease the serious issue.By integrating CCLS and additive BMS,we develop a new SLS algorithm for MAXSAT called CCABMS,and related experiments indicate the efficiency of CCABMS.Also,we experimentally analyze the effectiveness of initialization methods on SLS algorithms for MAX-SAT,and combine an effective initialization method with CCABMS,resulting in an enhanced algorithm.Experimental results show that our enhanced algorithm performs better than its state-of-the-art SLS competitors on a large number of industrial MAX-SAT instances.