Local Search Characteristics of Incomplete SAT Procedures

Abstract

Eective local search methods for nding satisfying assignments of CNF formulae exhibit several systematic characteristics in their search. We identify a series of measurable characteristics of local search behavior that are predictive of problem solving eciency. These measures are shown to be useful for diagnosing ineciencies in given search procedures, tuning parameters, and predicting the value of innovations to existing strategies. We then introduce a new local search method, SDF (\\smoothed descent and ood"), that builds upon the intuitions gained by our study. SDF works by greedily descending in an informative objective (that considers how strongly clauses are satised, in addition to counting the number of unsatised clauses) and, once trapped in a local minima, \\oods" this minima by reweighting unsatised clauses to create a new descent direction. The resulting procedure exhibits superior local search characteristics under our measures. We show that this method c...