Alef Verification and Planning System

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. 


For more information about Reservoir products or to purchase, please