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...

• Type: Conference
• Year: 2004
• Where: AMAI
• Authors: Dave A. D. Tompkins, Holger H. Hoos
• Keywords: AMAI 2004, Artificial Intelligence, Local Search, SAPS, Search Process