Greedy or not? Best improving versus first improving stochastic local search for MAXSAT

Abstract

Stochastic local search (SLS) is the dominant paradigm for incomplete SAT and MAXSAT solvers. Early studies on small 3SAT instances found that the use of "best improving" moves did not improve search compared to using an arbitrary "first improving" move. Yet SLS algorithms continue to use best improving moves. We revisit this issue by studying very large random and industrial MAXSAT problems. Because locating best improving moves is more expensive than first improving moves, we designed an "approximate best" improving move algorithm and prove that it is as efficient as first improving move SLS. For industrial problems the first local optima found using best improving moves are statistically significantly better than local optima found using first improving moves. However, this advantage reverses as search continues and algorithms must explore equal moves on plateaus. This reversal appears to be associated with critical variables that are in many clauses and that also yield large improving moves. Copyright © 2013, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.