Revisiting Clause Exchange in Parallel SAT Solving
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. of Fifteenth International Conference on Theory and Applications of Satisfiability Testing(SAT'12)
Original Kurzfassung:
Managing learnt clause database is known to be a tricky task in SAT
solvers. In the portfolio framework, the collaboration between threads through
learnt clause exchange makes this problem even more difficult to tackle. Several
techniques have been proposed in the last few years, but practical results are still
in favor of very limited collaboration, or even no collaboration at all. This is
mainly due to the difficulty that each thread has to manage a large amount of
learnt clauses generated by the other workers. In this paper, we propose new
efficient techniques for clause exchanges within a parallel SAT solver. In contrast
to most of the current clause exchange methods, our approach relies on both
export and import policies, and makes use of recent techniques that proves very
effective in the sequential case. Extensive experimentations show the practical
interest of the proposed ideas.
Forschungs-