Simulated annealing for hard satisfiability problems
William Spears · DIMACS series in discrete mathematics and theoretical computer science · 1996
Satisfiability (SAT) refers to the task of finding a truth assignment that makes an arbitrary boolean expression true. This paper compares a simulated annealing algorithm (SASAT) with GSAT (Selman et al., 1992), a greedy algorithm for solving satisfiability problems. GSAT can solve problem instances that are extremely difficult for traditional satisfiability algorithms. Results suggest that SASAT scales up better as the number of variables increases, solving at least as many hard SAT problems with less effort. The paper then presents an ablation study that helps to explain the relative advantage of SASAT over GSAT. Finally, an improvement to the basic SASAT algorithm is examined, based on a random walk suggested by Selman et al. (1993). 1 Introduction Satisfiability (SAT) refers to the task of finding a truth assignment that makes an arbitrary boolean expression true. For example, the boolean expression a & b is true iff the boolean variables a and b are true. Satisfiability is of int...