ySAT

Parallel Multithreaded Satisfiability Solver:

Design and Implementation

Abstract

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

Documentation

• Yulik Feldman under supervision of Nachum Dershowitz. "Parallel Multithreaded Satisfiability Solver: Design and Implementation". A thesis submitted in partial fulfillment of the requirements for the degree of Master of Science. The School of Computer Science, Raymond and Beverly Sackler Faculty of Exact Sciences, Tel-Aviv University, Israel. January 2005. Download (383K).
• Yulik Feldman, Nachum Dershowitz and Ziyad Hanna. "Parallel Multithreaded Satisfiability Solver: Design and Implementation". Proceedings of the 3rd International Workshop on Parallel and Distributed Methods in Verification (PDMC 2004). Electronic Notes in Theoretical Computer Science (ENTCS), Volume 128, Issue 3 (2005), pages 75–90. Download (265K).

C++ sources

• C++ sources of the initial single-threaded version of ySAT. This version was used as a basis for implementation of the multithreaded version. Since it was not designed as the final product, the implementation and documentation of this version are not as complete as those of the multithreaded version. Download (43K).

• C++ sources of the multithreaded version of ySAT. This is the final version implementing the parallel multithreaded algorithm described in the documents above. To compile this version, there is a need to install Boost.Threads library (http://www.boost.org). For more information, refer to the documents above. Download (62K).