Antti Hyvärinen: Incorporating Clause Learning in Grid-Based Randomized SAT Solving

HIIT seminar Otaniemi, Monday September 20, 13:15
Location: Computer Science building, hall T2

Antti Hyvärinen
Helsinki Institute for Information Technology HIIT
Department of Information and Computer Science
Aalto University School of Science and Technology

Title:
Incorporating Clause Learning in Grid-Based Randomized SAT Solving

Abstract:
Computational Grids provide a widely distributed computing environment suitable for randomized SAT solving. This paper develops techniques for incorporating clause learning, known to yield significant speed-ups in the sequential case, in such a distributed framework.

The approach exploits existing state-of-the-art clause learning SAT solvers by embedding them with virtually no modifications. The paper presents an algorithmic framework for learning-enhanced randomized SAT solving in Grid environments. With a substantial amount of controlled experiments it is demonstrated that this approach enables a form of clause learning which is not directly available in the underlying sequential SAT solver. Finally, an implementation of the algorithm is run in a production level Grid where it solves several problems not solved in the SAT 2007 solver competition.

Joint work with Tommi Junttila and Ilkka Niemelä