Weight resets in local search for SAT

Abstract

In this paper, we investigated the influence of resetting weights in what we refer to as safely satisfied sub areas within the search space. Our work is divided into two main tracks; track one is to search for sub areas within the search space where a group of connected clauses are all satisfied. In track two, a Weight Reset mechanism is designed and implemented within the Multi-Level Weight Distribution (mulLWD) algorithm, which produced a new algorithm known as mulLWD+WR. The impact of our new strategy, the Weight Reset mechanism, is illustrated via an extensive experimental range of evaluation on benchmarks obtained from the DIMACS and the SAT Competition 2017 problem sets. Our investigation and experimental evaluation shows that the Weight Reset mechanism, when compared to the state-of-the-art solving algorithms, can significantly improves the process of searching for solutions when solving hard Boolean satisfiability (SAT), Planning, scheduling, and many other hard combinatorial problems. Furthermore, the weight reset could be generalized to be employed by any Dynamic Local Search approach.