On multi-threaded satisfiability solving with openmp

Abstract

The boolean satisfiability problem sat is a well-known NP-Complete problem, which is widely studied because of its conceptual simplicity. Nowadays the number of existing parallel SAT solvers is quite small. Furthermore, they are generally designed for large clusters using the message passing paradigm. These solvers are coarse grained application since they divide the search-tree among the processors avoiding communication and synchronization. In this paper mtss, for Multi Threaded Sat Solver, is introduced. It is a fine grain parallel sat solver, in shared memory. It defines a rich thread in charge of the search-tree evaluation and a set of poor threads that will help the rich one by simplifying the opened node. mtss is well designed for multi-core CPU since it reduces the memory allocation during the search. © 2008 Springer-Verlag Berlin Heidelberg.