keyboard_arrow_up
Weights Stagnation in Dynamic Local Search for SAT

Authors

Abdelraouf Ishtaiwi, University of Petra, Jordan

Abstract

Since 1991, tries were made to enhance the stochastic local search techniques (SLS). Some researchers turned their focus on studying the structure of the propositional satisfiability problems (SAT) to better understand their complexity in order to come up with better algorithms. Other researchers focused in investigating new ways to develop heuristics that alter the search space based on some information gathered prior to or during the search process. Thus, many heuristics, enhancements and developments were introduced to improve SLS techniques performance during the last three decades. As a result a group of heuristics were introduced namely Dynamic Local Search (DLS) that could outperform the systematic search techniques. Interestingly, a common characteristic of DLS heuristics is that they all depend on the use of weights during searching for satisfiable formulas. In our study we experimentally investigated the weights behaviors and movements during searching for satisfiability using DLS techniques, for simplicity, DDFW DLS heuristic is chosen. As a results of our studies we discovered that while solving hard SAT problems such as blocks world and graph coloring problems, weights stagnation occur in many areas within the search space. We conclude that weights stagnation occurrence is highly related to the level of the problem density, complexity and connectivity.

Keywords

Full Text  Volume 6, Number 6