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.
Index Terms—Satisfiability, optimization, dynamic local search.
The authors are with the Faculty of Information Technology, Petra University, Amman, Jordan, (e-mail: aishtaiwi@uop.edu.jo, gissa@uop.edu.jo, whadi@uop.edu.jo, n.ali@uop.edu.jo).
Cite: Abdelraouf Ishtaiwi, Ghassan Issa, Wael Hadi, and Nawaf Ali, "Weight Resets in Local Search for SAT," International Journal of Machine Learning and Computing vol. 9, no. 6, pp. 874-879, 2019.
Copyright © 2019 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).