Adaptive memory-based local search for MAX-SAT

Many real world problems, such as circuit designing and planning, can be encoded into the maximum satisfiability problem (MAX-SAT). To solve MAX-SAT, many effective local search heuristic algorithms have been reported in the literature. This paper aims to study how useful information could be gathered during the search history and used to enhance local search heuristic algorithms. For this purpose, we present an adaptive memory-based local search heuristic (denoted by AMLS) for solving MAX-SAT. The AMLS algorithm uses several memory structures to define new rules for selecting the next variable to flip at each step and additional adaptive mechanisms and diversification strategies. The effectiveness and efficiency of our AMLS algorithm is evaluated on a large range of random and structured MAX-SAT and SAT instances, many of which are derived from real world applications. The computational results show that AMLS competes favorably, in terms of several criteria, with four state-of-the-art SAT and MAX-SAT solvers AdaptNovelty+, AdaptG2WSATp, IRoTS and RoTS.

Figure optionsDownload as PowerPoint slideHighlights
► This paper studies how useful information gathered during the search history could be used to enhance local search heuristic algorithms.
► We present a new adaptive memory-based local search heuristic for solving MAX-SAT, which integrates several memory structures.
► The proposed algorithm defines new heuristic rules for selecting the next variable to flip at each step.
► The algorithm introduces additional adaptive mechanisms and diversification strategies.