Comparison of the Empirical Performance of Greedy, Hill Climb and Simulated Annealing Algorithms in GSAT Solver on DIMAC and Aloul Benchmarks

Abstract

Boolean satisfiability solvers have made a significant impact in different areas of research such as Mathematics, Computer Science (artificial Intelligence, Automatic Test Pattern Generation, and so on). The problem to determine whether a given Boolean formula has a model was proved to be NP complete by Cook in 1971. This area witness a number of research over the past 5 decades. A number of algorithms were developed for solving SAT problem. These algorithms showed varying performance on different categories of SAT instance (random, industrial and handcrafted). This paper proposed to compare three (3) options of the Stochastic Local Search solver GSAT(Greedy SAT Solver). The options are Greedy, Hill Climb and Simulated Annealing. This work was inspired by the need to provide an insight on their performance on different problem Instances to serve as a guide for researchers who are interested in developing hybrid decision heuristic, initialization of variable weights in a decision heuristic and portfolio SAT solver. We empirically compared the performance on the three options on a Dell latitude E7470 laptop. Our result showed that Hill Climb option outperformed the other options in a number of problem instances solved while Simulated Annealing performed large number of downward and sideways moves. This implies that Hill Climb is the best choice for a hybrid solver while Simulated Annealing is preferable for initialization of variable weights.