Neighbourhood Clause Weight Redistribution in Local Search for SAT

Abstract. In recent years, dynamic local search (DLS) clause weighting algorithms have emerged as the local search state-of-the-art for solving propositional satisfiability problems. This paper introduces a new approach to clause weighting, known as Divide and Distribute Fixed Weights (DDFW), that transfers weights from neighbouring satisfied clauses to unsatisfied clauses in order to break out from local minima. Unlike earlier approaches, DDFW continuously redistributes a fixed quantity of weight between clauses, and so does not require a weight smoothing heuristic to control weight growth. It also exploits inherent problem structure by redistributing weights between neighbouring clauses. To evaluate our ideas, we compared DDFW with two of the best reactive local search algorithms, AdaptNovelty+ and RSAPS. In both these algorithms, a problem sensitive parameter is automatically adjusted during the search, whereas DDFW uses a fixed default parameter. Our empirical results show tha...

• Type: Conference
• Year: 2005
• Where: CP
• Authors: Abdelraouf Ishtaiwi, John Thornton, Abdul Sattar, Duc Nghia Pham
• Keywords: Clause Weighting, Clause Weighting Algorithms, CP 2005, Local Search, Programming Languages