Local Search Characteristics of Incomplete SAT Procedures
Effective local search methods for finding 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 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 superior local search characteristics under our measures. We show that this method can compete with the state of the art techniques, and significantly reduces the number of search steps relative to many recent methods. Copyright 2001 Elsevier Science B.V.Citation
D. Schuurmans, F. Southey. "Local Search Characteristics of Incomplete SAT Procedures". National Conference on Artificial Intelligence (AAAI), June 2000.| Keywords: | constraint satisfication, experimental analysis, local search, satisfiability |
| Category: | In Conference |
BibTeX
@incollection{Schuurmans+Southey:AAAI00,
author = {Dale Schuurmans and Finnegan Southey},
title = {Local Search Characteristics of Incomplete SAT Procedures},
booktitle = {National Conference on Artificial Intelligence (AAAI)},
year = 2000,
}Last Updated: June 01, 2007Submitted by Staurt H. Johnson
