Salt & Alef: Unlocking the Power of Boolean Satisfiability
James Ezick, Samuel Luckenbill, Donald Nguyen, Peter Szilagyi, Richard Lethin
Publication Source: The 10th Annual High Performance Embedded Computing Workshop (HPEC), Lexington, MA, USA, 2006
Solvers for the Boolean satisfiability problem (SAT) are an enabling technology for a diverse set of applications relevant to the HPEC community. These applications include formal verification, analysis of numerical precision for embedded pipelines, and cognitive reasoning. 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 constraint language, translation tool, and parallel SAT solver to significantly mitigate the impact of these limitations.