Local Search Characteristics of Incomplete SAT Procedures

Knowledge Representation and Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Boolean Satisfiability

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.