Alef® - Parallel SAT Solver
Alef is a parallel SAT solver that delivers substantial improvement over existing SAT solvers in terms of speed and maximum problem size. Alef's key applications are software verification and complex problem solving such as mission / work planning.
As software grows in complexity and criticality, software correctness is emerging as the key challenge for successful system deployment. Traditional testing-based verification approaches are no longer adequate to the task. Formal verification is the only approach that ensures complete bug detection for today's complex systems and architectures.
Satisfiability (SAT) solvers have proven to be an enabling technology for software and hardware verification. Formal verification of complex designs can be reduced to a SAT problem (see Salt & Shaker). However, solver performance, in terms of speed, maximum problem size, and efficiency, has to date been a limiting factor
Alef parallel SAT solver delivers substantial improvement over existing SAT solvers in terms of speed and maximum problem size. The solver does this by exploiting data parallelism present in BCP, algorithmic parallelism of running several searches at the same time, and by distributing the problem instance over HPCS hardware. Included is a compiler that transforms problems from the planning and verification domains to the input representation of our parallel solver.
Alef® Key Benefits
- Performance improvement over existing SAT solvers in terms of speed and maximum problem size
- Parallelizing the SAT problem enables the use of supercomputer hardware
Request a White Paper
For more information about Alef, including performance results and licensing terms, please contact us.
|
