Home Conference Schedule
	SCHEDULE: NOV 11-17, 2006 Alef Parallel SAT Solver for HPC Hardware Session: Poster Reception Event Type: Poster Time: 5:15pm - 7:15pm Author(s): James R Ezick, Samuel B Luckenbill, Donald Nguyen, Peter Szilagyi, John Starks, Richard A Lethin Location: Ballroom Corridor Abstract: 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. Chair/Author Details: James R Ezick Reservoir Labs Samuel B Luckenbill Reservoir Labs Donald Nguyen Reservoir Labs Peter Szilagyi Reservoir Labs John Starks Reservoir Labs Richard A Lethin Reservoir Labs
	Home | About | Contact Us | Registration | Sitemap