Comparison of the Empirical Performance of Greedy, Hill Climb and SimulatedAnnealing Algorithms in GSATSolver on DIMAC andAloul 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.