Integrating Systematic and Local Search Paradigms: A New Strategy for MaxSAT

Systematic search and local search paradigms forcombinatorial problems are generally believed tohave complementary strengths. Nevertheless, attemptsto combine the power of the two paradigmshave had limited success, due in part to the expensiveinformation communication overhead involved.We propose a hybrid strategy based onshared memory, ideally suited for multi-core processorarchitectures. This method enables continuousinformation exchange between two solverswithout slowing down either of the two. Such a hybridsearch strategy is surprisingly effective, leadingto substantially better quality solutions to manychallenging Maximum Satisfiability (MaxSAT) instancesthan what the current best exact or heuristicmethods yield, and it often achieves this within seconds.This hybrid approach is naturally best suitedto MaxSAT instances for which proving unsatisfiabilityis already hard; otherwise the method fallsback to pure local search.

Lukas Kroc, Ashish Sabharwal, Carla P. Gomes, Bart Selman