Local Search Characteristics of Incomplete SAT Procedures

Dale Schuurmans and Finnegan Southey, University of Waterloo

Effective local search methods for finding satisfying assignments of CNF formulae exhibit several systematic characteristics in their local search. We identify a series of measurable characteristics of local search behavior that are predictive of problem solving efficiency. These measures are shown to be useful for diagnosing inefficiencies 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 flood''), that builds upon the intuitions gained by our study. SDF works by greedily descending in an informative objective (that considers how strongly clauses are satisfied, in addition to counting the number of unsatisfied clauses) and, once trapped in a local minima, ``floods'' this minima by re-weighting unsatisfied clauses to create a new descent direction. The resulting procedure exhibits effective local search characteristics under our measures. We then show that our method is competitive with the state of the art techniques, and typically reduces the number of search steps by a significant factor.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.