Local Search Characteristics of Incomplete SAT Procedures
Full Text: schuurmans00local.pdf
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. 2001 Elsevier Science B.V. All rights reserved.
Citation
D. Schuurmans, F. Southey. "Local Search Characteristics of Incomplete SAT Procedures". Value of Information in Inference, Learning and Decision-Making, July 2002.| Keywords: | local search, constraint satisfaction |
| Category: | In Workshop |
BibTeX
@misc{Schuurmans+Southey:VOI-NIPS02,
author = {Dale Schuurmans and Finnegan Southey},
title = {Local Search Characteristics of Incomplete SAT Procedures},
booktitle = {Value of Information in Inference, Learning and Decision-Making},
year = 2002,
}Last Updated: August 16, 2007Submitted by Russ Greiner
