An Empirical Study of Optimal Noise and Runtime Distributions in Local Search

This paper presents a detailed empirical study of local search for Boolean satisfiability (SAT), highlighting several interesting properties, some of which were previously unknown or had only anecdotal evidence. Specifically, we study hard random 3-CNF formulas and provide surprisingly simple analytical fits for the optimal (static) noise level and the runtime at optimal noise, as a function of the clause-to-variable ratio. We also demonstrate, for the first time for local search, a power-law decay in the tail of the runtime distribution in the low noise regime. Finally, we discuss a Markov Chain model capturing this intriguing feature. Designing, understanding, and improving, local search methods for constraint reasoning, and in particular for Boolean satisfiability (SAT), has been the focus of hundreds of research papers since the 1990’s and even earlier. For SAT, techniques such as greedy local search, tabu search, solution guided search, focused random walk, and reactive or ...

• Type: Journal
• Year: 2010
• Where: SAT
• Authors: Lukas Kroc, Ashish Sabharwal, Bart Selman
• Keywords: Anecdotal Evidence, Hardware, Local Search, Local Search Methods, SAT 2010