Building Structure into Local Search for SAT

Local search procedures for solving satisfiability problems have attracted considerable attention since the development of GSAT in 1992. However, recent work indicates that for many real-world problems, complete search methods have the advantage, because modern heuristics are able to effectively exploit problem structure. Indeed, to develop a local search technique that can effectively deal with variable dependencies has been an open challenge since 1997. In this paper we show that local search techniques can effectively exploit information about problem structure producing significant improvements in performance on structured problem instances. Building on the earlier work of Ostrowski et al. we describe how information about variable dependencies can be built into a local search, so that only independent variables are considered for flipping. The cost effect of a flip is then dynamically calculated using a dependency lattice that models dependent variables using gates (specific...

• Type: Conference
• Year: 2007
• Where: IJCAI
• Authors: Duc Nghia Pham, John Thornton, Abdul Sattar
• Keywords: Artificial Intelligence, IJCAI 2007, Local Search, Local Search Techniques, Variable Dependencies