In recent years, dynamic clause weighting stochastic local search algorithms have emerged as thestate-of-the-art for solving satisfiability problems.In our study we experimentally investigated the weights behaviors and movements during searching for satisfiability.Firstly, We show that, second level neighboring clauses could be the culprit of causing the delay during the search.Secondly, we developed and experimentally investigated a new heuristic for enhancing Dynamic Local Search known as Multi Level Weight distribution (mulLWD).Our new heuristic is divided into two main phases.Phase one is to distribute weights within the same neighboring area.When phase one is no longer effective, phase two take place in which the second level neighboring area is exploited and its weights are used within the weight distribution process.To test our new heuristic, we conducted a detailed experimental study, comparing mulLWD with one of the leading clause weighting algorithm: Divide and Distribute Fixed Weight (DDFW).Experimental results showed that mulLWD heuristic has significantly better performance than DDFW (of up to an order of magnitude).This enhancement indicates that the multi level weight distribution is the key to further exploitation of local search SAT structures.Moreover, mulLWD could be easily generalized to be used with any dynamic local search weighting heuristic with some minor modifications
Tópico:
Constraint Satisfaction and Optimization
Citaciones:
1
Citaciones por año:
Altmétricas:
0
Información de la Fuente:
FuenteInternational journal of computing, communication and instrumentation engineering