Accelerating SAT solving with best-first-search

Bartók, Dávid and Mann, Zoltán Ádám (2014) Accelerating SAT solving with best-first-search. In: 15th IEEE International Symposium on Computational Intelligence and Informatics.

Text bfs_sat.pdf Restricted to Registered users only Download (737kB)

Abstract

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.

Actions (login required)

Edit Item