Scaling and probabilistic smoothing: Efficient dynamic local search for SAT

Abstract

In this paper, we study the approach of dynamic local search for the SAT problem. We focus on the recent andpro mising Exponentiated Sub-Gradient (ESG) algorithm, and examine the factors determining the time complexity of its search steps. Based on the insights gained from our analysis, we developed Scaling and Probabilistic Smoothing (SAPS), an efficient SAT algorithm that is conceptually closely related to ESG. We also introduce a reactive version of SAPS (RSAPS) that adaptively tunes one of the algorithm’s important parameters. We show that for a broadra nge of standard benchmark problems for SAT, SAPS and RSAPS achieve significantly better performance than both ESG andthe state-of-the-art WalkSAT variant, Novelty+.