Toward Easy Parallel SAT Solving

In spite of its computational complexity, the satisfiability problem is a great and competitive approach to solve a wide range of problems. This leads to have a strong demand for high-performance sat-solving tools in industry. Over the years, many different approaches and optimizations have been developed to tackle the problem more efficiently while being unaware of the actual trend in processor development which is from single-core to multi-core CPUs. This paper presents a shared memory parallel solving framework which is able to statically exploit the existing sequential and parallel solvers or preprocessors. This new framework facilitates the future parallel sat solving implementation approaches. It also briefly describes the associated lemma exchange policy. Some examples and experimentations with and without lemma exchange strategies using march, kcnfs and minisat are presented. Finally it shows the relevance of the scheme providing super linear speedups on some satisfiable and unsatisfiable formulas.