REAL

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.

[img] 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.

Item Type: Conference or Workshop Item (Lecture)
Subjects: Q Science / természettudomány > QA Mathematics / matematika > QA75 Electronic computers. Computer science / számítástechnika, számítógéptudomány
Depositing User: Dr. Zoltán Ádám Mann
Date Deposited: 22 Sep 2014 21:23
Last Modified: 29 May 2016 20:22
URI: http://real.mtak.hu/id/eprint/16021

Actions (login required)

Edit Item Edit Item