Samuel Luckenbill, James Ezick, Donald Nguyen, Peter Szilagyi, Richard Lethin
Publication Source: The 48th Annual Cray User Group (CUG) Technical Conference, Lugano, Switzerland, 2006
Recently, solvers for the Satisfiability problem (SAT) have become an enabling technology for diverse areas of military and commercial interest. However, solver performance, in terms of speed, maximum problem size, and efficiency, is a limiting factor to the more extensive application of this technology. This paper discusses Reservoir’s SAT-based planning and verification system, Alef, which includes a compiler, intermediate language, and parallel solver for HPC hardware.