Poster Reception-Alef Parallel SAT Solver for HPC Hardware
James R. Ezick, Samuel B. Luckenbill, Donald Nguyen, Peter Szilagyi, John Starks, Richard Lethin
Publication Source: The ACM/IEEE SC Conference on High Performance Networking and Computing, Tampa, FL, USA, 2006
Solvers for the Boolean satisfiability problem (SAT) are an enabling technology for a diverse set of applications, including formal verification of both hardware and software, mathematics, and planning. However, solver performance, measured in terms of speed and maximum problem size, is a limiting factor to the application of SAT to real-world problems. We are developing a parallel SAT solver, Alef, to take advantage of HPC hardware.The Alef parallel SAT solver utilizes algorithms and heuristics that improve its performance over existing approaches. We are developing the solver to run well on commercially available HPC hardware. Our analysis shows that our algorithms combined with the low message latency of supercomputers are likely to produce a significant performance improvement over existing solvers in terms of speed and maximum problem size. Our poster will describe the algorithms we are using, illustrate our approach to problem partitioning, and present our performance analysis to date.