Parallel Multithreaded Satisfiability Solver: Design and Implementation
Yulik Feldman, Nachum Dershowitz, Ziyad Hanna · Electronic Notes in Theoretical Computer Science · 2005
We describe the design and implementation of a highly optimized, 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 detrimental effect of parallel execution on the performance of processor cache is studied.