Systems & HPC

Parallel & Distributed SAT Solver

Serial, multithreaded, and MPI Boolean SAT solvers on a DPLL search with unit propagation — a work-stealing scheduler delivers near-linear scaling, then scales out to distributed memory over MPI.

C++17MultithreadingMPIAlgorithms

View the code

8.1× speedup on 10 threads

Flight recording

See it run

SAT_Project — serial vs. threads vs. MPI

Built from the original sources and run on a 10-core MacBook against the repo’s 1,000-variable, 8,000-clause problem. Long silent stretches are fast-forwarded; the timings printed are the solvers’ own.