Warped Landscapes and Random Acts of SAT Solving

10 years 1 months ago
Warped Landscapes and Random Acts of SAT Solving
Recent dynamic local search (DLS) algorithms such as SAPS are amongst the state-of-the-art methods for solving the propositional satisfiability problem (SAT). DLS algorithms modify the search landscape during the search process by means of dynamically changing clause penalties. In this work, we study whether the resulting, ‘warped’ landscapes are easier to search than the landscapes that correspond to the original problem instances. We present empirical evidence indicating that (somewhat contrary to common belief) this is not the case, and that the main benefit of the dynamic penalty update mechanism in SAPS is an effective diversification of the search process. In most other high-performance stochastic local search algorithms, the same effect is achieved by the strong use of randomised decisions throughout the search. We demonstrate that in SAPS, random decisions are only required in the (standard) search initialisation procedure, and can be completely eliminated from the rema...
Dave A. D. Tompkins, Holger H. Hoos
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where AMAI
Authors Dave A. D. Tompkins, Holger H. Hoos
Comments (0)