Parallel Multithreaded Satisfiability Solver: Design and Implementation

Yulik Feldman, Nachum Dershowitz, Ziyad Hanna


Abstract

We describe the design and implementation of a highly optimized, parallel multithreaded algorithm for the propositional satisfiability problem. The algorithm is based on the Davis-Putnam- Logemann-Loveland sequential algorithm, but includes many of the optimization techniques introduced in recent years. We provide experimental results for the execution of the parallel algorithm on a variety of multiprocessor machines with shared memory architecture. In particular, the effect of parallel execution on the performance of processor cache is studied.