Accelerating SAT solving with best-first-search
David Bartok, Zoltán Ádám Mann · 2014
Solvers for Boolean satisfiability (SAT), like other algorithms for NP-complete problems, tend to have a heavy-tailed runtime distribution. Successful SAT solvers make use of frequent restarts to mitigate this problem by abandoning unfruitful parts of the search space after some time. Although frequent restarting works fairly well, it is a quite simplistic technique that does not do anything explicitly to make the next try better than the previous one. In this paper, we suggest a more sophisticated method: using a best-fIrst-search approach to quickly move between different parts of the search space. This way, the search can always focus on the most promising region. We investigate empirically how the performance of frequent restarts, best-fIrst-search, and a combination of the two compare to each other. Our findings indicate that the combined method works best, improving 36–43 % on the performance of frequent restarts on the used set of benchmark problems.